loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
18th IEEE International Conference on Automated Software Engineering (ASE'03)
Parallel Breadth-First Search LTL Model-Checking
Montreal, Quebec, Canada
October 06-October 10
ISBN: 0-7695-2035-9
Jir? Barnat, Masaryk University Brno
Lubos Brim, Masaryk University Brno
Jakub Chaloupka, Masaryk University Brno
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.
Citation:
Jir? Barnat, Lubos Brim, Jakub Chaloupka, "Parallel Breadth-First Search LTL Model-Checking," ase, pp.106, 18th IEEE International Conference on Automated Software Engineering (ASE'03), 2003
Usage of this product signifies your acceptance of the Terms of Use.