Konferenzbeitrag
Enhancing BMC-based protocol verification using transition-by-transition FSM traversal
Lade...
Volltext URI
Dokumententyp
Text/Conference Paper
Zusatzinformation
Datum
2005
Autor:innen
Zeitschriftentitel
ISSN der Zeitschrift
Bandtitel
Verlag
Gesellschaft für Informatik e.V.
Zusammenfassung
We present a technique to automatically derive reachability information from designs to enhance Bounded Model Checking style verification. The method is well suited for typical protocol applications where the operation is controlled by a main finite state machine (FSM) interacting with a hierarchy of sub-FSMs. The algorithm traverses the global state space of the design based on single transitions of the main finite state machine. This transition-by-transition decomposition of the state space distinguishes our approach from previous ones. The experimental results clearly show the value of the new method. In our experiments, false negatives could be completely avoided and the overall verification effort was drastically reduced.