Airson a bhith air a ghabhail a-steach don kernel Linux 5.20 (is dòcha gum bi am meur air a h-àireamhachadh 6.0), thathas a’ moladh seata de phìosan le buileachadh an uidheamachd RV (Runtime Verification), a bheir seachad innealan airson a bhith a’ sgrùdadh obrachadh ceart air siostaman fìor earbsach a tha a’ gealltainn an neo-làthaireachd fàilligeadh. Bithear a’ dearbhadh aig àm ruith le bhith a’ ceangal luchd-làimhseachaidh ri puingean lorg a bhios a’ cumail sùil air an fhìor adhartas a thaobh coileanadh an aghaidh modal dearbhte ro-shuidhichte den automaton a mhìnicheas an giùlan ris a bheil dùil san t-siostam.
Bidh fiosrachadh bho phuingean lorg a ’gluasad a’ mhodail bho aon stàit gu stàite eile, agus mura h-eil an stàit ùr a rèir crìochan a ’mhodail, thèid rabhadh a chruthachadh no thèid an kernel a chuir ann an staid“ clisgeadh ”(tha dùil gum faigh siostaman earbsachd àrd lorg. agus a’ freagairt nan suidheachaidhean sin). Tha am modal automaton, a tha a’ mìneachadh eadar-ghluasadan bho aon stàit gu stàite eile, air a chuir a-mach gu cruth “dot” (graphviz), às deidh sin tha e air eadar-theangachadh a ’cleachdadh goireas dot2c gu riochdachadh C, a tha air a luchdachadh ann an cruth modal kernel a tha a’ cumail sùil air claonaidhean ann an adhartas cur gu bàs bhon mhodail ro-mhìnichte.
Tha sgrùdadh modail ùine-ruith air a shuidheachadh mar dhòigh nas aotroime agus nas fhasa a chuir an gnìomh airson a bhith a’ dearbhadh coileanadh ceart air siostaman a tha deatamach do mhisean, a’ cur ri modhan dearbhaidh earbsachd clasaigeach leithid sgrùdadh mhodail agus dearbhaidhean matamataigeach de ghèilleadh còd a rèir nan sònrachaidhean a chaidh a thoirt seachad ann am foirm fhoirmeil. cànain. Am measg nam buannachdan a tha an lùib RV tha an comas dearbhadh teann a thoirt seachad gun a bhith a’ buileachadh an t-siostam gu lèir ann an cànan modaladh, a bharrachd air freagairt sùbailte do thachartasan ris nach robh dùil, mar eisimpleir, gus casg a chuir air iomadachadh fàilligeadh ann an siostaman èiginneach.
Source: fosgailtenet.ru