Title :
Combining simulation and guided traversal for the verification of concurrent systems
Author :
Pastor, Enric ; Peña, Marco A.
Author_Institution :
Dept. of Comput. Archit., Tech. Univ. of Catalonia, Barcelona, Spain
Abstract :
We present a hybrid methodology that combines simulation and symbolic traversal in order to improve invariant checking. The methodology concentrates on concurrent systems, whose peculiarities are not fully exploited by other existing techniques for hybrid verification. Our approach exploits the information obtained from simulations to improve the knowledge of the state space, effectively guiding symbolic traversal.
Keywords :
asynchronous circuits; binary decision diagrams; causality; concurrency theory; distributed processing; formal verification; invariance; protocols; reachability analysis; state-space methods; symbol manipulation; BDD; asynchronous circuits; asynchronous concurrent systems; combining simulation/guided traversal; concurrent system verification; distributed systems; event causality; hybrid verification; invariant checking; network protocols; reachability analysis; state space methods; symbolic traversal; Analytical models; Asynchronous circuits; Computational complexity; Computational modeling; Computer architecture; Computer simulation; Discrete event simulation; Feedback; Reachability analysis; State-space methods;
Conference_Titel :
Design, Automation and Test in Europe Conference and Exhibition, 2003
Print_ISBN :
0-7695-1870-2
DOI :
10.1109/DATE.2003.1253780
