Distributed breadth-first search LTL model checking

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

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
Citace
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