Gesellschaft fr Informatik e.V.

Lecture Notes in Informatics


INFORMATIK 2005, Informatik LIVE! Band 1, Beiträge der 35 Jahrestagung der Gesellschaft für Informatik e.V. (GI), 19. bis 22. September 2005 in Bonn P-67, 303-305 (2005).


2005


Editors

Armin B. Cremers, Rainer Manthey, Peter Martini, Volker Steinhage (eds.)


Contents

Enhancing BMC-based Protocol Verification Using Transition-By-Transition FSM Traversal

M. D. Nguyen , D. Stoffel and W. Kunz

Abstract


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.


Full Text: PDF

ISBN 3-88579-396-2


Last changed 24.01.2012 21:50:50