DIET: Developing Implementation and Extending Theory A Symbolic Approach to Reasoning about LOTOS

Computer failures can be spectacular, and occasionally fatal, therefore we must find ways of making these systems more reliable. Formal methods can contribute to achieving this, but the chosen formalism must reflect the real world system accurately, otherwise any results proved about the mathematical model may not apply to the real system. Also, since only small studies can be analysed by hand, good tool support is required. Lastly, in order to assist and guide software engineers applying formal methods it is important to have a selection of case studies on which to draw.

The DIET project addresses these points by extending the support available for a particular formal method (LOTOS). The main tasks of the project are to:

Prove key theories of the formal framework (adequacy of the logic, consistency of new semantics with standard semantics), giving a strong theoretical base to the work.
Develop implementations of model checkers for symbolic modal logic and Full (symbolic) LOTOS. We draw on different paradigms, each yielding different benefits. These are: CADP (an existing model checker for concrete LOTOS), Ergo (a theorem prover), and Maude (a term rewriting environment).
Carry out several case studies to demonstrate the effectivemess of the theory and the implemented tools, and to provide guidance for practitioners wishing to adopt this approach.
Extend the theory and implementation to include features of the model mu-calculus, specifically those allowing looping properties to be described.
Investigate the timed operators introduced in E-LOTOS to determine the benefits of giving a symbolic semantics for such operators.

The project ran from January 1999 to April 2002, supported by EPSRC. One postdoctoral research fellow was employed during this time (Dr Jeremy Bryans).

Find out more about:

Research

Teaching

Personal

Home

Dr Carron Shankland Email: ces@cs.stir.ac.uk

Last revision: 18th November 2002