A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties

• Název česky: Časově optimální on-the-fly paralelní algoritmus pro ověřování modelu slabých LTL vlastností
• Autoři: BARNAT Jiří; BRIM Luboš; ROČKAI Petr
• Rok publikování: 2009
• Druh: Článek ve sborníku
• Konference: Formal Methods and Software Engineering
• Fakulta / Pracoviště MU: Fakulta informatiky
• Doi: http://dx.doi.org/10.1007/978-3-642-10373-5_21
• Obor: Informatika
• Klíčová slova: on-the-fly; parallel; LTL Model Checking
• Popis: Jeden z nejdůležitějších otevřených problému v paralelním ověřování modelu LTL je existence on-the-fly škálovatelného paralelního algoritmu s lineární časovou složitostí. V tomto článku dáváme částečnou odpověď na tento problém, jmenovitě řešíme tento problém pro poměrně bohatou podtřídu LTL vlastností, a to konkrétně slabých LTL vlastností.

Související projekty

• Techniky automatické verifikace a validace softwarových a hardwarových systémů
• Realistická aplikace formálních metod v komponentových systémech
• Vysoce paralelní a distribuované výpočetní systémy
• Verifikace a analýza velmi velkých počítačových systémů
• Automatizovaná formální verifikace s využitím soudobého hardware