Para sa pagsasama sa Linux kernel 5.20 (marahil ang sangay ay mabibilang na 6.0), ang isang hanay ng mga patch ay iminungkahi sa pagpapatupad ng RV (Runtime Verification) na mekanismo, na nagbibigay ng mga tool para sa pagsuri sa tamang operasyon sa lubos na maaasahang mga sistema na ginagarantiyahan ang kawalan ng mga kabiguan. Isinasagawa ang pag-verify sa runtime sa pamamagitan ng pag-attach ng mga humahawak sa mga trace point na sumusuri sa aktwal na pag-usad ng pagpapatupad laban sa isang paunang natukoy na reference deterministic na modelo ng automat na tumutukoy sa inaasahang pag-uugali ng system.
Ang impormasyon mula sa mga trace point ay naglilipat ng modelo mula sa isang estado patungo sa isa pa, at kung ang bagong estado ay hindi tumutugma sa mga parameter ng modelo, isang babala ang bubuo o ang kernel ay inilalagay sa isang "panic" na estado (ang mga mataas na reliability system ay inaasahang makakakita ng at tumugon sa mga ganitong sitwasyon). Ang modelo ng automat, na tumutukoy sa mga paglipat mula sa isang estado patungo sa isa pa, ay na-export sa "tuldok" na format (graphviz), pagkatapos nito ay isinalin gamit ang dot2c utility sa isang representasyong C, na na-load sa anyo ng isang kernel module na sinusubaybayan ang mga paglihis ng progreso ng pagpapatupad mula sa paunang natukoy na modelo.
Ang run-time model checking ay nakaposisyon bilang isang mas magaan at mas madaling ipatupad na paraan ng pag-verify ng tamang pagpapatupad sa mga mission-critical system, na umaakma sa mga klasikal na paraan ng pag-verify ng pagiging maaasahan gaya ng pagsuri ng modelo at mga mathematical na patunay ng pagsunod sa code sa mga detalye na ibinigay sa isang pormal na paraan. wika. Kabilang sa mga pakinabang ng RV ay ang kakayahang magbigay ng mahigpit na pag-verify nang walang hiwalay na pagpapatupad ng buong sistema sa isang wika ng pagmomodelo, pati na rin ang kakayahang umangkop na tugon sa mga hindi inaasahang kaganapan, halimbawa, upang harangan ang karagdagang pagpapalaganap ng isang pagkabigo sa mga kritikal na sistema.
Pinagmulan: opennet.ru