Model checking of control-user systems - Moravcová Vařeková, Pavlína (2009)
Řada reálných softwarových systémů (tzv. kontroler-uživatel systémů) je složena ze stabilní části (kontroler) a libovolného počtu dynamických komponent stejného typu (uživatel). Modely těchto systémů jsou parametrizovány počtem komponent uživatelů a tudíž stavové prostory těchto modelů mají potenciálně nekonečně mnoho stavů. Tradiční techniky na ověřování modelu (model checking) proto mohou být použity pouze na verifikaci konkrétních instancí těchto systémů, ale ne na systém jako celek. Tato práce prezentuje tři plně automatické techniky na verifikaci vlastností systémů typu kontroler-uživatel. První technika umožňuje verifikovat vlastnosti dosažitelnosti. Popisovaný algoritmus je úplný, je typu on-the-fly a umožňuje také souběžnou verifikaci více vlastností. Druhý algoritmus, využívající první přístup, odpovídá na otázky typu "Kolik nejvíce uživatelů může být v dané specifické situaci?". Třetí algoritmus ověřuje s využitím dvou dříve popsaných technik vlastnosti logiky SE-LTL na syst.