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.

This is a three year EPSRC funded project with one postdoctoral research fellow (Dr Jeremy Bryans).

Work on the project has proceeded in three main directions:

refining the symbolic framework, tightening up definitions, dealing more clearly with loops in the transition systems, proving properties of the new semantics with respect to the standard semantics, and of the logic with respect to the bisimulation relation. Joint work with Muffy Calder of the University of Glasgow and Savi Maharaj of the University of Stirling.
The semantics is detailed in a FORTE 2001 paper. There's a fuller version of this paper (with examples) published as a Glasgow technical report. The logic is detailed in a forthcoming Computer Journal paper. The relationship between the logic and a bisimulation over symbolic transition systems is detailed in a FME 2001 paper.
developing implementations of a model checker for symbolic temporal logic (called FULL) and Full (Symbolic) LOTOS. Three different implementations have been developed:
- CADP: based on the standard semantics, and the logic XTL. Joint work with Jeremy Bryans. The implementation is detailed in a FORTE 2001 paper. We're hoping to extend this work with the help of an honours student in Autumn 01.
- Ergo: based on the theorem proving tool Ergo, implementing the symbolic semantics and proving the validity of FULL properties with respect to symbolic transition systems. Joint work with Peter Robinson at the SVRC. An overview of the implementation is given in a AVIS 2001 paper.
- Maude: based on rewriting logic, implementing a translation from LOTOS to symbolic transition systems, and proving the validity of HML properties with respect to those systems. Joint work with Alberto Verdejo. An overview of the implementation is given in a AVIS 2001 paper.
carry out several case studies to demonstrate the effectiveness of the theory and the implemented tool, and to provide guidance for practitioners wishing to adopt this approach.

Historical documents about the project:

Research

Teaching

Personal

Home

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

Last revision: 20th August 2001