Symbolic model checking is a powerful technique for improving the quality of embedded software because the checking covers all possible behaviors, this is in contrast to tradition software testing which is known to cover only a limited (often very limited) subset of the behaviors. Symbolic model checking provides an exhaustive check covering all combinations of inputs and internal states, this is particularly important for embedded system as, for example, mobile phones, hi-fi equipment, remote controls and interactive simulators. Such systems often have a very limited user interface for detecting the internal state of the system, and therefore many errors do not manifest themselves immediately which makes checking much harder than for general purpose software. Furthermore, the consequences of errors in embedded systems are often severe; it is for example almost impossible to update the software in a washing machine, video or a car once thousands of copies are in daily use.
Symbolic model checking is exploited in the visualSTATE tool developed by Baan VisualSTATE (formerly Beologic A/S). This is a design tool used by many companies for developing embedded software in a variety of embedded applications ranging from simple controllers to very large advanced interactive simulators.
Together with Aalborg University and the Technical University of Denmark, Baan VisualSTATE is now developing a new generation of the visualSTATE tool that will move the limit on the complexity of the embedded software that can be verified by several orders of magnitude. The first result of the cooperation is the recent verification of a design with more than 1400 concurrent state machines in less than an hour on a standard PC. Results such as these will be incorporated in future generations of the visualSTATE tool.
Based on a range of examples taken from the practical applications the
three partners are also investigating ways of enhancing design tools and
their underlying theory. Currently, two research directions are pursued,
one focuses on adding timing information and the other on introducing modularity
in the state transitions systems used for designing embedded software.
Terminology
Embedded software: software used in a dedicated system with a specialized purpose such as controlling an electronical or mechanical device. Often the requirements are very different than tose met in software for a general purpose computer such as a PC or a workstation.
Symbolic model checking is the common name of a class of algorithms that checks a state machine by exercising ALL states of the state space without explicitly enumerating these states and going through them one by one.