Символдық верификация

Символдық верификация

Аджан С. Мейран А. Ертаева Н. Кенкоз Д.

Model checking әдісімен символдық верификация жиі model checking+екілік шешуші диаграммалар (model checking+BDDs) ретінде анықталады.

• Model checking әдісімен символдық верификация жиі model checking+екілік шешуші диаграммалар (model checking+BDDs) ретінде анықталады.
• Алдынғы-тарауларда қарастырылған реактивті жүйелерді верификациялаудың классикалық алгоритмдері Крипке құрылымының жай-күйін анық көрсететін Алгоритмдер болып табылады. Қазіргі компьютерлерде олар миллиондаған күйден тұратын жүйелерді верификациялау үшін пайдаланылуы мүмкін. Әрбір жағдайды ұсыну әдетте бірнеше жүз байтты талап етеді, мұндай құрылымдарды өңдеу жылдамдығы-секундына жүздеген күйлер. Бұл жүйені верификациялау үшін жеткілікті. Алайда, нақты жүйелер үлкен күй санымен модельдермен сипатталады. Кез келген нақты жүйені есептеу өз өмірінің процесінде мүмкін болатын жай-күйлердің аз ғана үлесінен өтуі мүмкін болса да, әдетте қандай жай-күйлер мен ауысуларды тексеру қажет екендігі алдын ала белгісіз. Ол жүйенің барлық ықтимал траекториясын толық тексеруге мүмкіндік береді.

Қарапайым жүйенің үлгісін қарастырайық (сурет. 10.1). Жүйе екіден тұрады

әрбір төрт басқарушы күйі бар болсын процестер

(мысалы, командалардың есептеуішінің мәндері) және тек бір бүтін айнымалы short (1 байт) типті әрекет етеді. Сонымен қатар, бұл ақпаратты буферде сақтауға болады (яғни бірден көп жібермеуге).

BDD арқылы көрінбейтін көрініс(неявное)

1020 = ~270 күй саны бар жүйе үшін Крипке құрылымы:

□ бір бульдік функциясы ~70 екілік айнымалы

бастауыш күйлер жиыны;

□ бір булеву функциясы ~140 екілік айнымалы

көптеген өткелдер;

□ әрбір атомдық предикат және тексерілетін әрбір ішкі пішім үшін

темпоральной .формулалар ~70 екілік айнымалы функцияның бір булевасы, бұл формула шынайы болатын көптеген жағдайларды білдіретін.

Проблемы взрыва числа состояний (state explosion problem).

верификация оны тексеру үшін пайдаланыла алмайды: оның жай-күйінің саны model checking классикалық айқын алгоритмін пайдалана алатыннан бірнеше рет асып түседі.