ലിനക്സിനായി, കേർണലിന്റെ ശരിയായ പ്രവർത്തനം പരിശോധിക്കുന്നതിനുള്ള ഒരു സംവിധാനം നിർദ്ദേശിച്ചിട്ടുണ്ട്

ലിനക്സ് കേർണൽ 5.20-ൽ ഉൾപ്പെടുത്തുന്നതിന് (ഒരുപക്ഷേ ബ്രാഞ്ച് 6.0 എന്നതായിരിക്കും), RV (റൺടൈം വെരിഫിക്കേഷൻ) സംവിധാനം നടപ്പിലാക്കുന്നതിനൊപ്പം ഒരു കൂട്ടം പാച്ചുകൾ നിർദ്ദേശിക്കപ്പെടുന്നു, ഇത് വളരെ വിശ്വസനീയമായ സിസ്റ്റങ്ങളിൽ ശരിയായ പ്രവർത്തനം പരിശോധിക്കുന്നതിനുള്ള ഉപകരണങ്ങൾ നൽകുന്നു. പരാജയങ്ങളുടെ അഭാവം. സിസ്റ്റത്തിന്റെ പ്രതീക്ഷിക്കുന്ന സ്വഭാവം നിർവചിക്കുന്ന ഓട്ടോമാറ്റണിന്റെ മുൻകൂട്ടി നിശ്ചയിച്ച റഫറൻസ് ഡിറ്റർമിനിസ്റ്റിക് മോഡലിനെതിരെ എക്സിക്യൂഷന്റെ യഥാർത്ഥ പുരോഗതി പരിശോധിക്കുന്ന ട്രെയ്‌സ് പോയിന്റുകളിലേക്ക് ഹാൻഡ്‌ലറുകൾ ഘടിപ്പിച്ച് റൺടൈമിൽ പരിശോധന നടത്തുന്നു.

ട്രെയ്‌സ് പോയിന്റുകളിൽ നിന്നുള്ള വിവരങ്ങൾ മോഡലിനെ ഒരു സ്റ്റേറ്റിൽ നിന്ന് മറ്റൊന്നിലേക്ക് മാറ്റുന്നു, കൂടാതെ പുതിയ അവസ്ഥ മോഡലിന്റെ പാരാമീറ്ററുകളുമായി പൊരുത്തപ്പെടുന്നില്ലെങ്കിൽ, ഒരു മുന്നറിയിപ്പ് ജനറേറ്റുചെയ്യുന്നു അല്ലെങ്കിൽ കേർണൽ ഒരു "പാനിക്" അവസ്ഥയിൽ സ്ഥാപിക്കുന്നു (ഉയർന്ന വിശ്വാസ്യതയുള്ള സംവിധാനങ്ങൾ കണ്ടെത്തുമെന്ന് പ്രതീക്ഷിക്കുന്നു. അത്തരം സാഹചര്യങ്ങളോട് പ്രതികരിക്കുകയും ചെയ്യുക). ഒരു സ്റ്റേറ്റിൽ നിന്ന് മറ്റൊന്നിലേക്കുള്ള പരിവർത്തനങ്ങളെ നിർവചിക്കുന്ന ഓട്ടോമാറ്റൺ മോഡൽ, "ഡോട്ട്" ഫോർമാറ്റിലേക്ക് (ഗ്രാഫ്വിസ്) എക്‌സ്‌പോർട്ടുചെയ്യുന്നു, അതിനുശേഷം അത് dot2c യൂട്ടിലിറ്റി ഉപയോഗിച്ച് ഒരു സി പ്രാതിനിധ്യത്തിലേക്ക് വിവർത്തനം ചെയ്യുന്നു, അത് ഒരു കേർണൽ മൊഡ്യൂളിന്റെ രൂപത്തിൽ ലോഡ് ചെയ്യുന്നു. മുൻകൂട്ടി നിശ്ചയിച്ച മോഡലിൽ നിന്ന് നിർവ്വഹണ പുരോഗതിയുടെ വ്യതിയാനങ്ങൾ ട്രാക്ക് ചെയ്യുന്നു.

മിഷൻ-ക്രിട്ടിക്കൽ സിസ്റ്റങ്ങളിൽ ശരിയായ നിർവ്വഹണം പരിശോധിക്കുന്നതിനുള്ള ഭാരം കുറഞ്ഞതും നടപ്പിലാക്കാൻ എളുപ്പമുള്ളതുമായ രീതിയാണ് റൺ-ടൈം മോഡൽ പരിശോധന, മോഡൽ ചെക്കിംഗ്, ഔപചാരികമായി നൽകിയിരിക്കുന്ന സ്പെസിഫിക്കേഷനുകളുമായി കോഡ് പാലിക്കുന്നതിന്റെ ഗണിതശാസ്ത്ര തെളിവുകൾ തുടങ്ങിയ ക്ലാസിക്കൽ വിശ്വാസ്യത സ്ഥിരീകരണ രീതികൾ പൂർത്തീകരിക്കുന്നു. ഭാഷ. ഒരു മോഡലിംഗ് ഭാഷയിൽ മുഴുവൻ സിസ്റ്റവും പ്രത്യേകമായി നടപ്പിലാക്കാതെ തന്നെ കർശനമായ സ്ഥിരീകരണം നൽകാനുള്ള കഴിവ്, അതുപോലെ തന്നെ അപ്രതീക്ഷിത സംഭവങ്ങളോടുള്ള വഴക്കമുള്ള പ്രതികരണം, ഉദാഹരണത്തിന്, ഗുരുതരമായ സിസ്റ്റങ്ങളിലെ പരാജയത്തിന്റെ കൂടുതൽ പ്രചരണം തടയുക എന്നതാണ് ആർവിയുടെ ഗുണങ്ങളിൽ ഒന്ന്.

അവലംബം: opennet.ru