Title :
Unfolding enhancements speed FSM based simulation
Author_Institution :
RMIT Univ., Melbourne, VIC
Abstract :
Simulation of real systems such as communications protocols can prove a system will work before any implementation, and test all possible operational states faster and more cheaply than could be achieved with a real physical system. This checking is usually performed by creating a reachability tree that shows all possible outcomes starting from one initial state and checking that all sequences result in an acceptable outcome. Examining the full reachability tree of a system described by Finite State Machines (FSMs) or Petri nets can guarantee the discovery of all incorrect behavior, but can take excessive computing time. Unfolding the reachability tree of a system described by Petri nets has been shown to dramatically reduce the simulation time. This paper shows several advantages if this unfolding is applied to an FSM model of a system instead. Such an approach allows fast discovery of deadlock, and livelock caused by true livelock or by unfairness in the simulation The unfolding method is extended to show how a system can be tested for all possible ldquounexpected inputsrdquo and ldquoany initial staterdquo, both of which are essential when analyzing the robustness of real world protocols. The method is applied to a communications protocol called 2-wire TIA where the simulation speed up was estimated to be a factor of 1.8 billion.
Keywords :
Petri nets; finite state machines; formal verification; protocols; reachability analysis; 2-wire TIA; FSM; Petri net; communication protocol; deadlock discovery; finite state machine; formal verification; reachability tree; simulation; Analytical models; Automata; Computational modeling; Explosions; Petri nets; Protocols; Robustness; System recovery; System testing; Vehicle crash testing;
Conference_Titel :
Industrial Informatics, 2008. INDIN 2008. 6th IEEE International Conference on
Conference_Location :
Daejeon
Print_ISBN :
978-1-4244-2170-1
Electronic_ISBN :
1935-4576
DOI :
10.1109/INDIN.2008.4618236