Title :
Evaluating symbolic traversal algorithms applied to asynchronous concurrent systems
Author :
Solé, Marc ; Pastor, Enric
Author_Institution :
Dept. of Comput. Archit., Catalonia Tech. Univ., Barcelona, Spain
Abstract :
Symbolic reachability analysis based on binary decision diagrams (BDDs) is a technique that allows the implementation of efficient invariant checking algorithms, and improves the performance of CTL/LTL verification. However, in practice it is well known that the BDD blowup problem limits the size of the systems that can be successfully verified. Along the years multiple variants of the basic reachability scheme have been introduced. However, most of them perform nicely only on synchronous systems or under the assumption that the transition relation (TR) can be effectively decomposed as a conjunction. This paper intends to demonstrate that the reachability algorithms based on these premises do not fit properly on asynchronous concurrent systems. Therefore it justifies developing alternative reachability algorithms for concurrent systems, or even for mixed synchronous/asynchronous schemes.
Keywords :
binary decision diagrams; computational complexity; concurrency control; formal verification; reachability analysis; search problems; temporal logic; CTL verification; LTL verification; asynchronous concurrent systems; binary decision diagrams; invariant checking; symbolic reachability analysis; symbolic traversal; synchronous systems; synchronous/asynchronous scheme; transition relation; Binary decision diagrams; Boolean functions; Computational complexity; Computer architecture; Concurrent computing; Data structures; Explosions; Reachability analysis; State-space methods; System testing;
Conference_Titel :
Application of Concurrency to System Design, 2004. ACSD 2004. Proceedings. Fourth International Conference on
Print_ISBN :
0-7695-2077-4
DOI :
10.1109/CSD.2004.1309133