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

fYear

2003

fDate

2003

Firstpage

1158

Lastpage

1159

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Design, Automation and Test in Europe Conference and Exhibition, 2003

ISSN

1530-1591

Print_ISBN

0-7695-1870-2

Type

conf

DOI

10.1109/DATE.2003.1253780

Filename

1253780