|
The first step in analyzing model specifications is usually to determine all possible circumstances and sequences of events that can arise in the system. This task is performed by a state space generator, which conducts a brute-force enumeration of every possible state or configuration that a system can enter. By examining the resulting set of reachable states and the connections between them (the state graph), it is possible for a correctness analyser to detect sequences of events that lead to unsafe states or undesirable situations (such as a deadlock in a communications protocol or a collision between two trains). Given the rate of movement between states, the information can also be used by a steady state solver to produce performance statistics.