Disjunctive Modal Transition Systems - Beneš, Nikola (2012)
Otázka korektnosti je bezpochyby zásadním faktorem při návrhu počítačových systémů, což dělá z oblasti specifikace a verifikace důležitou součást informatiky. K tomu, abychom mohli v této oblasti použít formálních metod, potřebujeme dobrý specifikační formalismum. Jednou možností je popsat požadované vlastnosti systému pomocí formulí vhodné logiky. Jinou možností je přístup založený na chování, při němž se jak specifikace, tak implementace systému popisují za použití stejného formalismu a správnost systému se pak ověřuje za použití jistého druhu ekvivalence či jiné relace. V této práci se zaměřujeme hlavně na tento přístup, ačkoli i ten dáváme do souvislosti s přístupem logickým. Modální přechodové systémy jsou formalismem, který je schopen popisovat specifikace i implementace. Jeho hlavním přínosem je to, že umožnuje jistou volnost ve specifikacích, možnost nechat části systému nedospecifikovány. Toho je dosaženo rozšířením standardních přechodových systémů o dva druhy přechodů - tzv.