För att inkludera i kÀrnan av Linux 5.20 (det Àr möjligt att grenen fÄr nummer 6.0) föreslÄs en uppsÀttning patchar med en implementation av RV (Runtime Verification) mekanismen, som representerar medel för att kontrollera korrektheten i driften av högpÄlitliga system som garanterar avbrottsfrihet. Kontroll utförs under körning genom att fÀsta hanterare vid spÄrningspunkter som verifierar den faktiska exekveringen med en fördefinierad referensmodell av en automat som definierar det förvÀntade beteendet i systemet.
Information frÄn spÄrpunkterna omvandlar modellen frÄn ett tillstÄnd till ett annat, och om det nya tillstÄndet inte överensstÀmmer med modellens parametrar genereras en varning eller kÀrnan gÄr in i "panic"-lÀget (det antas att hög- pÄlitliga system kommer att identifiera sÄdana situationer och reagera pÄ dem). Automatan som definierar övergÄngarna mellan tillstÄnd exporteras i "dot"-format (graphviz), och översÀtts sedan med hjÀlp av verktyget dot2c till en representation pÄ C-sprÄket, som laddas som en kÀrnmodul som övervakar avvikelser frÄn den fördefinierade modellen.
Verifiering mot modellen under körning positioneras som en mer lÀttviktig och praktiskt genomförbar metod för att bekrÀfta korrektheten i driften av kritiska system, som komplementerar klassiska metoder för att bekrÀfta tillförlitlighet, sÄsom modellkontroll och matematiska bevis för att koden överensstÀmmer med specifikationerna som definieras i ett formellt sprÄk. Bland fördelarna med RV nÀmns möjligheten att sÀkerstÀlla strikt verifiering utan att hela systemet implementeras pÄ modelleringssprÄket, samt flexibel reaktion pÄ oförutsedda hÀndelser, exempelvis för att blockera ytterligare spridning av fel i kritiska system.
KĂ€lla: opennet.ru
