Az 5.20-as Linux kernelbe (talán az ág számozása 6.0 lesz) a javítások készletét javasoljuk az RV (Runtime Verification) mechanizmus megvalósításával, amely eszközöket biztosít a nagyon megbízható rendszerek helyes működésének ellenőrzéséhez, amelyek garantálják a kudarcok hiánya. Az ellenőrzés futás közben történik úgy, hogy kezelőket csatolnak a nyomkövetési pontokhoz, amelyek ellenőrzik a végrehajtás tényleges előrehaladását az automata előre meghatározott referencia-determinisztikus modelljéhez képest, amely meghatározza a rendszer várható viselkedését.
A nyomkövetési pontokból származó információk áthelyezik a modellt egyik állapotból a másikba, és ha az új állapot nem egyezik a modell paramétereivel, akkor figyelmeztetés generálódik, vagy a kernel "pánik" állapotba kerül (nagy megbízhatóságú rendszerektől elvárható és reagálni az ilyen helyzetekre). Az egyik állapotból a másikba való átmeneteket meghatározó automata modellt a „pont” formátumba (graphviz) exportálják, majd a dot2c segédprogrammal lefordítják C-reprezentációra, amelyet egy kernelmodul formájában töltenek be, nyomon követi a végrehajtás előrehaladásának eltéréseit az előre meghatározott modelltől.
A futásidejű modellellenőrzés egy könnyebb és könnyebben megvalósítható módszer a küldetéskritikus rendszerek helyes végrehajtásának ellenőrzésére, kiegészítve a klasszikus megbízhatóság-ellenőrzési módszereket, például a modellellenőrzést és a kódnak a formális specifikációkkal való megfelelésének matematikai bizonyítását. nyelv. Az RV előnyei közé tartozik, hogy szigorú ellenőrzést biztosít anélkül, hogy a teljes rendszert külön implementálnák egy modellező nyelven, valamint rugalmasan reagálhat előre nem látható eseményekre, például megakadályozhatja a kritikus rendszerek meghibásodásának továbbterjedését.
Forrás: opennet.ru