Publikace na Matematicko-fyzikální fakulta |
2007
Abstrakt
Při formální verifikaci systémů se setkáváme s problémem přibližně exponenciálního růstu počtu stavů s velikostí popisu modelu. To ve svém důsledku vede k neakceptovatelným prostorovým a časovým nárokům.
V tomto článku, zaměřeném na obecné komunikující automaty (Interfering Automata), prezentujeme metodu nahrazování běhěm ověřování skupiny stavů za stav jediný (zástupce). Jelikož počet zástupců je výrazně nižší než počet stavů, tato metoda dále posouvá hranice praktické možnosti formálního ověřováni.
Náš přístup zohledňuje paralelní s distribuované prostředí.