Distributed breadth-first search LTL model checking

• Název česky: Distribuované ověřování modelu LTL s využitím prohledávání grafu do šířky
• Autoři: BARNAT Jiří; ČERNÁ Ivana
• Rok publikování: 2006
• Druh: Článek v odborném periodiku
• Časopis / Zdroj: Formal Methods in System Design
• Fakulta / Pracoviště MU: Fakulta informatiky
• www: http://www.springerlink.com/content/94376q360325p688/?p=1a1a7d483531453686a95f499872d47e&pi=1
• Obor: Informatika
• Klíčová slova: LTL model checking; Distributed memory; Breadth-first Search
• Popis: Je zde navrhnut a experimentalně vyhodnocen algoritmus pro detekci akceptujicích cyklů v grafu, založený na tzv. back-level hranách. Algoritmus je dále rozšířen o několik nezbytných módů, které jsou nezbytné pro vytvoření skutečného verifikačního nástroje pro LTL ověřování modelů. Tento nástroj byl implementován a experimentálně vyhodnocen na několika směrodatných vstupech.

Související projekty

• Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
• Techniky automatické verifikace a validace softwarových a hardwarových systémů
• Institut Teoretické Informatiky
• Vysoce paralelní a distribuované výpočetní systémy
• Automatizovaná verifikace softwaru