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
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:
The project ran from January 1999 to April 2002, supported by
EPSRC. One postdoctoral research fellow was employed during this time
(Dr Jeremy Bryans).
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
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
Investigate the timed operators introduced in E-LOTOS to determine the
benefits of giving a symbolic semantics for such operators.
Find out more about:
Dr Carron Shankland
Last revision: 18th November 2002