Area: Computer Science & Engineering
Research Title: Model Checking in Software Engineering
Keywords: concurrent systems, formal methods, software engineering
Concurrency is concerned with systems of multiple, simultaneously active computing components that interact with one another. While each component may be demonstrably correct, it is often difficult to predict what the behaviour will be when components interact. Concurrency bugs are particularly difficult to remove because they are often not reproducible. Problems that can arise include timing and sequencing problems, live-lock and dead-lock. These problems can lead to poor performance, unpredictable behaviour and system failure. In applications that are commercially or safety “critical”, the results can be disastrous.
Model checking is a technique that can be used to detect concurrency problems. Classical model checking (see for example GPVW95, Kato99) is a brute-force technique that involves a complete state search of a finite-state (Buchi) automaton that represents the physical (concurrent) system together with the property that the user wishes to verify. The property is expressed is a temporal logic. The technique is well-known, and is used for example in the very popular model-checking tool SPIN (Holz97).
In this research, model checking of industrial size systems will be investigated with a view to making the technique more readily accessible to software engineers. This will involve defining more user-friendly but formal language to describe the finite-state automaton that models the system and the properties. This language can then be translated to input for SPIN (for example), which is then used to check the given properties of the system.
The new language should be related to semi-formal notations that are typically used in a software development setting to express the required functionality of the system. Two of the most popular notations used in software development are entity-relationship diagrams and data-flow diagrams. These notations are problematical because there is no semantic check of correctness, and properties cannot be checked. In this work, these diagrammatic notations will be translated to the new, more formal language, which in turn will be translated to input for an off- the-shelf model checker like SPIN. The former translation may need to be carried out interactively because the semi-formal notation may contain ambiguities and inconsistencies. These translators will comprise a tool that software designers can use to model how a system should behave. This model can be verified by the model checker and act as a specification of the system. Also included in the scope of this research is investigating whether this technology can be integrated with CASE tools that are used in industry.
A fundamental goal of this research is to make modelling an industrial system and verifying at the specification stage `easy’ for software engineers.
R. Gerth, D. Peled, Y.Vardi, and P.Wolper. “Simple on-the-fly automatic verification of linear temporal logic”. In P. Dembinski and M. Sredniawa, editors, Proceedings of the IFIP WG6.1 International Symposium on Protocol Specification, Testing, and Verification, XV, Warsaw, Poland, June 1995. Chapman & Hall.
J.-P. Katoen. Concepts, algorithms and tools for model checking. Arbeitsberichte der Informatik Vol. 32~1, University of Erlangen- Nuernberg, 1999.