ProbDiVinE: A Parallel Qualitative LTL Model Checker

• Název česky: ProbDiVinE: Paralelní qualitativní model checker
• Autoři: BARNAT Jiří; BRIM Luboš; ČERNÁ Ivana; ČEŠKA Milan; TŮMOVÁ Jana
• Rok publikování: 2007
• Druh: Článek ve sborníku
• Konference: Fourth International Conference on the Quantitative Evaluation of Systems (QEST'07)
• Fakulta / Pracoviště MU: Fakulta informatiky
• Obor: Informatika
• Klíčová slova: ProbDiVinE; Qualitative LTL; Probabilistic; Model Checking
• Popis: Prezentujeme paralelní model checker pro ověřování Markovových rozhodovacích procesů (MDP) na vlastnosti formulované v lineární temporální logice. Nástroj rozšiřuje paralelní model checker DiVinE a podporuje verifikaci qualitativních vlastností.

Související projekty

• Techniky automatické verifikace a validace softwarových a hardwarových systémů
• Institut Teoretické Informatiky
• Vysoce paralelní a distribuované výpočetní systémy