Local Quantitative LTL Model Checking

• Název česky: Lokální kvantitafivní ověřování modelů LTL
• Autoři: BARNAT Jiří; BRIM Luboš; ČERNÁ Ivana; ČEŠKA Milan; TŮMOVÁ Jana
• Rok publikování: 2008
• Druh: Článek ve sborníku
• Konference: 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008)
• Fakulta / Pracoviště MU: Fakulta informatiky
• Obor: Informatika
• Klíčová slova: LTL Model Checking; Probabilistic; Parallel
• Popis: Kvantitativní analýza pravděpodobnostních systémů byla dosud studována zejména v kontextu globálních algoritmů pro model-checking. V tomto článku je popsán postup, jakým lze proceduru kvantitativní analýzy pravděpodobnostních systémů zdokonalit v případě, že se zajímáme o výsledek analýzy pouze pro iniciální stav systému. Experimentálně bylo ukázáno, že použitím nových metod dochází k redukci časové náročnosti procedury verifikace z řádu dnů na řády minut.

Související projekty

• Techniky automatické verifikace a validace softwarových a hardwarových systémů
• Institut Teoretické Informatiky
• Automatizovaná verifikace softwaru