2003
Parallel Breadth-First Search LTL Model-Checking
BARNAT, Jiří, Luboš BRIM a Jakub CHALOUPKAZákladní údaje
Originální název
Parallel Breadth-First Search LTL Model-Checking
Autoři
BARNAT, Jiří (203 Česká republika, garant), Luboš BRIM (203 Česká republika) a Jakub CHALOUPKA (203 Česká republika)
Vydání
Montreal, 18th IEEE International Conference on Automated Software Engineering (ASE'03), od s. 106-115, 10 s. 2003
Nakladatel
IEEE Computer Society
Další údaje
Jazyk
angličtina
Typ výsledku
Stať ve sborníku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Kanada
Utajení
není předmětem státního či obchodního tajemství
Kód RIV
RIV/00216224:14330/03:00008593
Organizační jednotka
Fakulta informatiky
ISBN
0-7695-2035-9
UT WoS
000186519300011
Klíčová slova anglicky
model checking; parallel algorithm; breadth first search
Příznaky
Mezinárodní význam, Recenzováno
Změněno: 1. 6. 2009 21:17, prof. RNDr. Jiří Barnat, Ph.D.
Anotace
V originále
We propose a practical parallel on-the-fly algorithm for enumerative LTL model-checking. The algorithm is designed for a cluster of workstations communicating via MPI. The detection of cycles (faulty runs) effectively employs the so called back-level edges. In particular, a parallel level-synchronized breadth-first search of the graph is performed to discover back-level edges. For each level the back-level edges are checked in parallel by a nested depth-first search to confirm or refute the presence of a cycle. Several optimizations of the basic algorithm are presented and advantages and drawbacks of their application to distributed LTL model checking are discussed. Experimental implementation of the algorithm shows promising results.
Návaznosti
| GA201/03/0509, projekt VaV |
| ||
| MSM 143300001, záměr |
|