Fun ifisi ninu ekuro Linux 5.20 (boya ẹka naa yoo jẹ nọmba 6.0), ṣeto awọn abulẹ kan ti dabaa pẹlu imuse ti ẹrọ RV (Imudaniloju akoko), eyiti o pese awọn irinṣẹ lati ṣayẹwo iṣẹ ṣiṣe ti o pe lori awọn eto igbẹkẹle giga ti o ṣe iṣeduro isansa ti awọn ikuna. Ijẹrisi ni a ṣe ni akoko asiko nipasẹ sisọ awọn olutọju si awọn aaye itọpa ti o ṣayẹwo ilọsiwaju gangan ti ipaniyan lodi si awoṣe ipinnu ipinnu ti a ti pinnu tẹlẹ ti automaton ti o ṣalaye ihuwasi ireti ti eto naa.
Alaye lati awọn aaye itọpa gbe awoṣe lati ilu kan si ekeji, ati pe ti ipo tuntun ko ba awọn aye ti awoṣe naa, ikilọ kan ti ipilẹṣẹ tabi ekuro ti gbe sinu ipo “ijaaya” (awọn eto igbẹkẹle giga ni a nireti lati rii daju). ati dahun si iru awọn ipo). Awoṣe adaṣe, eyiti o ṣalaye awọn iyipada lati ipinlẹ kan si ekeji, ti wa ni okeere si ọna kika “dot” (graphviz), lẹhin eyi ti o tumọ si nipa lilo ohun elo dot2c sinu aṣoju C, eyiti o jẹ ti kojọpọ ni irisi module ekuro ti tọpasẹ awọn iyapa ti ilọsiwaju ipaniyan lati awoṣe asọye.
Ṣiṣayẹwo awoṣe akoko-ṣiṣe wa ni ipo bi iwuwo-fẹẹrẹfẹ ati ọna ti o rọrun lati ṣe ti ijẹrisi ipaniyan ti o pe lori awọn ọna ṣiṣe-pataki, ni ibamu pẹlu awọn ọna ijẹrisi igbẹkẹle kilasika gẹgẹbi iṣayẹwo awoṣe ati awọn ẹri mathematiki ti ibamu koodu pẹlu awọn pato ti a fun ni aṣẹ ede. Lara awọn anfani ti RV ni agbara lati pese iṣeduro ti o muna laisi imuse lọtọ ti gbogbo eto ni ede awoṣe, bakanna bi idahun rọ si awọn iṣẹlẹ airotẹlẹ, fun apẹẹrẹ, lati ṣe idiwọ itankale siwaju ti ikuna ni awọn eto to ṣe pataki.
orisun: opennet.ru