VVS - Verification and Validation of large State-systems
by Niels Bo Theilgaard, Kim Guldstrand Larsen, Henrik Reif Andersen and Jørgen Staunstrup
A consortium consisting of Aalborg University, Technical University of Denmark and the Danish company Beologic A/S is working on new symbolic model checking techniques that will move the limits on the complexity of the embedded software that can be verified by several orders of magnitude. The techniques will be incorporated in new generations of the visualSTATE tool developed and sold by Beologic A/S. The tool is currently used by more than 100 companies for developing embedded software throughout the world. 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. The cooperation started in March 1997, and it involves several people at each of the partners.
The goal of the cooperation is to move the limits of the complexity of what can be verified using symbolic model checking tools by several orders of magnitude. Beologic A/S and their customers find that symbolic model checking is a powerful technique for improving the quality of embedded software because the checking covers all possible behaviours, this is in contrast to tradition software testing which is known to cover only a limited (often very limited) subset of the behaviours. 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.
The first phase of the project consists of adapting state of the art model checking techniques such as Reduced Order Binary Decision Diagrams (ROBDDs) to Beologic's visualSTATE tool. This already enhances the power of the tool significantly. Based on a thorough analysis of a large number of examples from Beologic's customers new techniques have been developed, and recently a design with more than 1400 concurrent state machines was verified in less than an hour on a standard PC. The diagram shows the structure of the 1400 concurrent state machines.
Currently, two research directions are pursued to increase the power of the techniques even further; one focuses on adding timing information and the other on introducing modularity in the state transitions systems used for designing embedded software.
The cooperation between a research oriented company and the two academic groups in Aalborg and Lyngby has been very positive. Through the analysis of real-world examples, new fruitful research directions have been identified leading to a significant increase of the power of the visualSTATE tool provided by Beologic. This enhances the applicability of the tools at Beologic's customers leading to the ultimate goal of the project which is increased quality of the software in embedded applications. For more information on VVS, see http://www.it.dtu.dk/~jst/vvs
Please contact:
Niels Bo Theilgaard - Beologic A/S
Tel: +45 8625 1111
E-mail: nbt@beologic.dkKim Guldstrand Larsen - Aalborg University
Tel: +45 9635 8893
E-mail: kgl@cs.auc.dkHenrik Reif Andersen and Jørgen Staunstrup - Technical University of Denmark
Tel: +45 4525 3761 and +45 4525 3740
E-mail: hra@it.dtu.dk, jst@it.dtu.dk
