IAR visualSTATE incorporates verification of the designed state machines, based on formal verification theories with their roots in low-level hardware design, like integrated circuits etc. This is a brief introduction to the concept of formal verification that shows why you can trust the verification results. The presentation assumes basic knowledge of Finite State Machines.
For more information on the properties that visualSTATE verifies, please see the Verificator.
What is formal verification?
Wikipedia[6] has the following definition of formal verification: In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods of mathematics.
To prove a certain feature of a system, the system is represented by an abstract model that can be manipulated by formal methods; the feature is then proven true or false in this model. This implies that the original system must be possible to translate into an abstract model that has the same properties as the original system. The visualSTATE verification is an example of model checking, which is a set of different methods of algorithmically verifying that a model satisfies a specification.
What does visualSTATE verify?
The visualSTATE Verificator can verify the following properties of a system of interacting state machines:
- State, local and system-wide deadlock 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 are not acted upon
- Unused transitions, i.e. transitions that will never be taken, regardless of the event sequence fed into the system
- Unused actions or assignments
- Unused variables, parameters, and constants.
Some of these properties can be partly checked by a simple syntactic check of the original state machine model, for example unused events. It is easy to check whether a certain event is ever mentioned in the model. However, this is not a complete answer to the question of usage. An event can be unused in a model, even if it is mentioned, if the set of states that acts upon the event is unreachable. To completely answer the question, some form of formal method must be used.
How is the verification performed?
The state machine model is encoded using a data structure called Reduced Ordered Binary Decision Diagrams, or ROBDDs for short. ROBDDs are a form of directed acyclic graphs that can be used to represent Boolean functions and operations on such in an efficient manner. A ROBDD representation of a Boolean function is canonical, that is, there is only one way to encode a specific function. Read more about ROBDDs in [1][2][3].
All aspects of the state machine that are important for verification of the above properties are encoded as ROBDDs. This includes the complete transition relation of the system, the signal queue and all integer variables, integer assignments, and next-state relations. Exactly how this encoding is performed is beyond the scope here, but a description that is close to the method visualSTATE employs can be found in [4].
The ROBDDs and the associated operators form a formal system that can be used to formally answer questions about certain properties of the original state machine system. To answer the questions a traversal of the state space has to be performed. It can be shown that the full state space for a visualSTATE state machine can actually be computed, as long as there is enough memory and CPU time. A traversal of the state space is performed by applying Boolean operators to the ROBDDs.
Checking for unreachable states in a forward-looking algorithm can be performed in the following way:
- Begin with the global system start state.
- Compute the set of reachable next-states, that is, states that are reachable in at most one transition from the start state.
- Form the union of the start state and the computed next-states. Find the set of reachable next-states from the union.
- Repeat until a fixed point is reached, that is, the union of reachable states does not grow any further. The set of unreachable states is the set difference between the reachable set and the full state space.
Checking for deadlocks can be done in a similar fashion by finding states or state configurations that, once entered, block the machine from entering any other state no matter what input is received.
Since the ROBDD encoding is a formal and complete representation of a (finite) state machine system and each property can be expressed as operations on the decision diagrams, it is guaranteed that the verification process can verify each property.
Caveats
The size of the state space is the combinatorial sizes of each state machine in the system, the integer variables, and the signal queue. This implies that the number of possible state configurations can be very large, even for a system of state machines that looks quite innocent on the surface. This is the dreaded state space explosion and it can result in prohibitive amounts of memory and CPU being consumed during verification. There are a number of ways to deal with the problem. visualSTATE has four alternatives to choose from:
- Full verification: As the name implies, this mode uses the complete state space in a forward-looking algorithm. To be able to always use the full mode without restrictions, care has to be taken to keep the state space as small as possible. This includes using as small integer variables as possible, use signals with care and keeping down the number of arithmetic operations on 16-bit and 32-bit entities.
By optionally forcing all variables to be regarded as 8-bit (or any number of bits) by the Verificator, it is sometimes possible to verify even very large state spaces. The downside is that there are probably a number of falsely reported conflicting transitions for such a model.
- Guard mode: This mode excludes parts of the state space by ignoring integer assignments, but includes guard expressions. This might result in some reported transition conflicts that are in fact not conflicting, since a guard might depend on a certain assignment.
- Basic mode: Makes the state space even smaller by also ignoring guard expressions. In the same manner as for guard mode, this might result in some reported transition conflicts that are in fact non-conflicting.
- Compositional mode: This mode takes a completely different approach, by using a backwards-looking algorithm. It starts from each possible goal state in the system and tries to expand the visited state space until the start configuration is reached. By carefully making use of the (absence of) dependencies between machines in the system, the visited state space is kept as small as possible for each goal state.
Currently, this method cannot find state and system dead ends, but it finds local dead ends and performs all of the other checks performed in basic mode. The compositional mode has proven itself to perform very well on extremely large systems with loosely coupled machines, that is, where guards rarely refer to states outside the defining machine. The price is that it does not, at this time, find all the errors that can be found by the full mode. Nevertheless, in some circumstances, due to the size of the complete state space, this is the only way to get any verification results at all.
References
[1] Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, C(35)-8:677-691, August 1986.
[2] Randal E. Bryant, Binary decision diagrams and beyond: enabling technologies for formal verification, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design pp 236-243.
[3] S.B. Akers, "Binary decision diagrams," IEEE Transactions on Computers, Vol. C-27, No. 6 (June, 1978), pp. 509-516.
[4] Jørn Lind-Nielsen, Verification of Large State/Event Systems, IT University of Copenhagen, May 2000, Ph.D. thesis.
[5] Andrzej Wasowski, Code Generation and Model Driven Development for Constrained Embedded Software, IT University of Copenhagen, January 2005, PhD Thesis.
[6] Formal verification. http://en.wikipedia.org/wiki/Formal_verification (Accessed May 3, 2006)