Research Proposal - Sample Only

Source: http://www.cse.unsw.edu.au/postgrad/research/sample.html

Title of research: Model Checking in Software Engineering

Name of student: Alex A. Aardvark

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.

References