How do you test that your state machine design model and embedded application does not contain any of the following problematic properties?
- State, Local and System wide dead lock conditions Conflicting transitions between states
- Unreachable states, i.e. states that cannot be entered by any sequence of events from the environment
- Unused events or signals, i.e. stimuli to the system that is not acted upon
- Unused transitions, i.e. transitions that will never fire, regardless of the event sequence fed into the system
- Unused actions or assignments
- Unused variables, parameters and constants.
Each of these properties, if present in the application, is a potential sign of an inconsistent design or - even worse - a design with fatal logical gaps.
Fighting the state space explosion
Even for a moderately complex application, the task of exhaustively testing by hand for all of the above properties can be intimidating, or virtually impossible. It is simply not possible in the general case to use a traditional black box, or even white box, approach to achieve 100% test coverage of all design elements in a defendable amount of time. The combinatorial number of state, event and transition combinations for a state machine, or a system of state machines in the same application, rises very fast as the machine, or system of machines, grows.
Formal verification and model driven design
The way out of the test dilemma is to complement traditional test strategies with methods based on formal verification. The design model is checked from a purely formal point of view, utilizing theory based on theorem proving and graph theory.
The visualSTATE® verificator utilizes these formal methods and combines them with a highly efficient abstract internal representation of the system; thus drastically reducing the time and memory consumption normally associated with formal verification techniques. By using the visualSTATE verificator, you can hereby discover design mistakes early. Mistakes of a kind that can be impossible to devise realistic test plans for.
Verifying custom design properties
In addition to testing for all of the formal design properties listed above, the visualSTATE verificaftor can be used to test for custom properties of the design; this is achieved by expressing the desired verification properties as one or more UML state machines in their own right, parallel to the application design. (Eg. "Can the system ever be brought into a state change directly from StateA to StateC, through StateB?", or "Can StateMachine1 ever be in StateD at the same time as StateMachine2 is in StateE?" etc.)
Since the verification is performed on the design model, it can be performed throughout the entire development cycle. In this way it is possible to catch errors as soon as they are introduced, instead of waiting until a customer discovers them the hard way.
If problematic states are discovered in the state machine model, an event sequence can be automatically generated that shows how the system can be brought into this state. (If the state is reachable.) This event sequence can later be used as an input test vector in the functional testing and validation of the application. An important property of the generated event sequence is that it is the shortest possible sequence to reach that state.
By combining the formal verification of the Verificator, the test tools in the Validator and the powerful in-target debug and simulation features, iterative testing and verification ensures that the system design can truly be seen as an executable representation of the application.
Example 1: State dead end
This example shows a single state machine with a dead end.
visualSTATE model with a state dead end.
visualSTATE will report the following verification result on the design in the figure above:
CHECKING FOR STATE DEAD ENDS
State dead end(s) (Warnings):
B
A state dead end is a state that cannot be left once it has been entered. The state machine will stay in the state until the state machine is reset.
Explanation
State B is a state dead end because it has no transitions leaving it that enter other states.
Example 2: Local dead ends
This example illustrates a system with two state machines M0 and M1. M0 has the local dead end {B, C}. M1 has the local dead ends {B, C}.
| M0 |
|
M1 |
 |
|
|
visualSTATE System consisting of the two state machines M0 and M1. M0 has the local dead end {B , C} . M1 has the local dead ends {B , C} and D.
visualSTATE will report the following verification result on the design shown in this example:
CHECKING FOR LOCAL DEAD ENDS
Local dead end(s) for 'M_0_M0' (Warning):
Local dead end 1:
B
C
Local dead end(s) for 'M_1_M1' (Warning):
Local dead end 1:
D
Local dead end 2:
B
C
A local dead end is a combination of states from one or more state machines that prevents a state machine from changing state. Please check transitions with state conditions.
Explanation
The system has three local dead ends. If the event Event1 occurs before the event Event2 , then the system will enter the state {B , C} which is a local dead end both for state machine M0 and state machine M1. If Event2 occurs first, then the state machine M1 will enter the local dead end D.
Note that all state and system dead ends will also be local dead ends. In systems that do not contain guard expressions, a dead end is most probably caused by some state condition.
Example 3: System dead ends
This system consists of two state machines M0 and M1. M1 has one system dead end.
| M0 |
|
M1 |
 |
|
 |
visualSTATE System with one System dead end {B , F}.
visualSTATE will report the following verification result on the design shown above:
CHECKING FOR SYSTEM DEAD ENDS
Printing system dead end(s) (Warnings):
System dead end 1:
B
F
A system dead end is a combination of states from all the state machines, which prevents the complete system from changing state. Please check transitions with state conditions.
Explanation
The verification finds that state {B , F} is a system dead end. The system dead end will be reached by any sequence of events where both Event1 and Event3 occur before the events Event3 and Event4.
Example 4: Transition conflicts
The following example shows a simple visualSTATE system with transition conflicts.
Simple system with transition conflicts.
When verifying the design shown in this example, visualSTATE will report the following result:
CHECKING CONFLICTS
Conflicting Transitions: (Error)
A: Event1() /
-> B
A: Event1() /
-> C
If guard expressions are used in the transitions above please check these guard expressions manually to ensure that they are mutually exclusive.
Explanation
Upon receiving the event Event1, the system will be in a conflict; should it enter state B or state C? The conflict may be resolved by adding guard expressions, state conditions or by letting one of the transitions be triggered by some other event.
Example 5: Force state actions and conflicts
The following example shows how the use of force state actions might lead to transition conflicts. The system consists of the state machines M0 (containing states A and B), and M1 (containing states C, D and E).
| M0 |
|
M1 |
 |
|
 |
visualSTATE system consisting of two state machines named M0 and M1.
If you verify the design in this example, visualSTATE will report the following result:
CHECKING CONFLICTS
Conflicting Transitions: (Error)
A:
Event1() / D
-> B
C:
Event1() /
-> E
If guard expressions are used in the transitions above please check these guard expressions manually to ensure that they are mutually exclusive.
Explanation
A conflict in M1 is found. The force state action on the transition from A to B leads to a transition conflict. The question is: should state machine M1 enter state D or state E upon receiving the event Event1?
Example 6: Hierarchy and conflicts
It can be difficult to detect conflicts in a hierarchical system. The example shown here is simple but illustrates that transitions at a deeply nested level may conflict with transitions at the topmost level.
Hierarchical system with a conflict.
If you verify this design, visualSTATE will report the following:
Conflicting Transitions: (Error)
A: Event1() /
-> B
C: Event1() /
-> D
If guard expressions are used in the transitions above please check these guard expressions manually to ensure that they are mutually exclusive.
Explanation
When the event Event1 is received, the two transitions A -> B and C -> D conflict. The question is: should the system enter state A.D or state B ?