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

Project Achievements

Download the Individual Grant Review.

The focus for this project was to build up a symbolic framework for reasoning about LOTOS. This framework pictured below is based around a symbolic semantics for Full LOTOS (see the AMAST 1997 paper and the FORTE 2001 paper) using Symbolic Transition Systems (STS) as defined by Hennessy and Lin. It also includes an HML-like logic (FULL) (see the Computer Journal paper) and symbolic bisimulation (see the FORTE 2001 paper and the Glasgow and Stirling technical reports). Although we focus on the use of LOTOS as a specification language, any similar process algebra can be represented in a symbolic framework. The Symbolic Framework

In this project our key advances are:

Proof of the relation between symbolic and standard bisimulation
LOTOS is a standardised language, therefore it is important that the meaning of the semantics is retained while gaining the benefit of a more convenient compact notation using symbolic transition systems. This result means that if two closed processes are bisimilar under the standard bisimulation relation, then they are bisimilar under symbolic bisimulation (this will be reported in a later paper). This relation is shown by the heavy arrow in the framework picture.
Proof of adequacy of FULL with respect to symbolic bisimulation
This result shows that if two processes are bisimilar then they satisfy the same logical properties (see the Computer Journal paper and the FME 2001 paper). Conversely, if the processes are not bisimilar then there is a logical property which captures the difference between them. This is an important result because it shows that our symbolic framework is self-consistent in this sense. The logic differentiates exactly the same sets of processes as the bisimulation relation. This result is represented by the dashed arrows in framework picture.
Three prototype model checking tools for the logic
The three tools are built on top of existing tools, and all exploit different paradigms. The first (see the Bryans and Shankland FORTE 2001 paper) is built on top of CADP, and is useful because although the semantics in this case is not really symbolic, our tool can be part of an established suite of tools for reasoning about LOTOS specifications. The second (see the Robinson/Shankland AVIS paper) is built on top of the theorem prover Ergo. This implements a truly symbolic semantics, and gives access to theorem proving tactics for reasoning about the data part of specifications. The third (see the Bryans/Verdejo/Shankland AVIS paper) is built in a term rewriting system Maude. This also implements a symbolic semantics, and gives access to term rewriting techniques for dealing with data.
Extended version of FULL
The FULL logic has some nice theoretical properties, described above; however, for practical specification purposes a more expressive logic is required. A particular flaw in FULL is the inability to describe properties with loops. FULL* (a forthcoming paper by Bryans/Morel/Shankland will detail this) is an extended version of FULL which can describe such properties. Prototype implementation has been carried out in CADP.
Case studies
To demonstrate the functionality of our symbolic framework it is important to carry out case studies. Some small case studies exist, but these are not yet fully written up and published.

Collaborations have arisen through the tool development work with Alberto Verdejo (UCM, Spain) and Peter Robinson (SVRC, Australia). These are ongoing: Mr Verdejo is implementing other parts of the symbolic framework in Maude as part of his thesis, and an extended version of the Ergo paper is in preparation. New collaborations also arose in the theoretical work: Savi Maharaj (Stirling) contributed as much as a co-investigator (see the Computer Journal paper, the FME 2001 paper, and the TPHOLS paper) and Lionel Morel (IMAG, France) continues to work with us on a paper describing FULL*.

Related work, extending tool support for the framework by developing and implementing an algorithm for symbolic bisimulation is being carried out by Brian Ross (Glasgow), who is a student of Prof. Calder.

Publications of the project

[BCM+02] J. Bryans, M. Calder, S. Maharaj, B. Ross, and C. Shankland. Report on Developing a Symbolic Framework for Reasoning about Full LOTOS. In preparation, 2002.
[BHS02] J. Bryans, R. Hardy, and C. Shankland. A Symbolic Approach to the RPC case study. In preparation, 2002.
[BMS02] J. Bryans, L. Morel, and C. Shankland. Extending FULL with * operations. In preparation, 2002.
[BS01] J. Bryans and C. Shankland. Implementing a modal logic over data and processes using XTL. In M. Kim, B. Chin, S. Kang, and D. Lee, editors, {\em Proceedings of FORTE 2001, 21st International Conference on Formal Techniques for Networked and Distributed Systems}, pages 201--218. Kluwer Academic Publishers, 2001.
[BVS01a] J. Bryans, A. Verdejo, and C. Shankland. Using Rewriting Logic to implement the modal logic FULL. In R. Bharadwaj, editor, {\em {AVIS'01: First International Workshop on Automated Verification of Infinite-State Systems}. Naval Research Laboratory Technical Memorandum, 2001.
[BVS01b] J. Bryans, A. Verdejo, and C. Shankland. Using Rewriting Logic to implement the modal logic FULL. In D. Nowak, editor, {\em {AVoCS'01: Workshop on Automated Verification of Critical Systems}, 2001. Oxford University Computing Laboratory technical report PRG-RR-01-07.
[CMS01] M. Calder, S. Maharaj, and C. Shankland. An Adequate Logic for Full LOTOS. In J. Oliveira and P. Zave, editors, {\em {Formal Methods Europe'01}, LNCS 2021, pages 384--395. Springer-Verlag, 2001.
[CMS02] M. Calder, S. Maharaj, and C. Shankland. A Modal Logic for Full LOTOS based on Symbolic Transition Systems. {\em The Computer Journal}, 45(1):55--61, 2002.
[CS00] M. Calder and C. Shankland. A Symbolic Semantics and Bisimulation for Full LOTOS. Technical Report CSM-159, University of Stirling, 2000.
[CS01a] M. Calder and C. Shankland. A Symbolic Semantics and Bisimulation for Full LOTOS. In M. Kim, B. Chin, S. Kang, and D. Lee, editors, {\em Proceedings of FORTE 2001, 21st International Conference on Formal Techniques for Networked and Distributed Systems}, pages 184--200. Kluwer Academic Publishers, 2001.
[CS01b] M. Calder and C. Shankland. A Symbolic Semantics and Bisimulation for Full LOTOS. Technical Report TR-2001-77, University of Glasgow, 2001. Extended version of FORTE 2001 paper.
[HS00] R. Hardy and C. Shankland. Battleships: A Case Study using Symbolic Transition Systems. Draft manuscript, 2000.
[Mah01a] S. Maharaj. A PVS-Assisted Proof of Adequacy for a Logic for Full LOTOS. In preparation, 2001.
[Mah01b] S. Maharaj. A PVS Theory of Symbolic Transition Systems. In Richard J Boulton and Paul B Jackson, editors, {\em {Supplemental Proceedings of Theorem Proving in Higher Order Logics 2001, September 2001}, pages 255--266, 2001. Published Informatics Research Report, Division of Informatics, University of Edinburgh.
[RC02] B. Ross and M. Calder. Computing Symbolic Bisimulations for Full LOTOS. Submitted to FACS, 2002.
[RS01a] P. Robinson and C. Shankland. Implementing the modal logic FULL using Ergo. In R. Bharadwaj, editor, {\em {AVIS'01: First International Workshop on Automated Verification of Infinite-State Systems}. Naval Research Laboratory Technical Memorandum, 2001.
[RS01b] P. Robinson and C. Shankland. Implementing the modal logic FULL using Ergo. In D. Nowak, editor, {\em {AVoCS'01: Workshop on Automated Verification of Critical Systems}, 2001. Oxford University Computing Laboratory technical report PRG-RR-01-07.
[Sha02] C. Shankland. Classic Case Studies using Symbolic Transition Systems. In preparation, 2002.
[ST97] C. Shankland and M. Thomas. Symbolic Bisimulation for Full LOTOS. In M. Johnson, editor, {\em Algebraic Methodology and Software Technology, Proceedings of AMAST 97}, LNCS 1349, pages 479--493. Springer-Verlag, 1997.
[Ver02a] A. Verdejo. A tool for Full LOTOS in Maude. Technical Report 123-02, Dpto. Sistemas Informaticos y Programacion, Universidad Complutense de Madrid, April 2002.
[Ver02b] A. Verdejo. Building tools for LOTOS Symbolic Semantics in Maude. In {\em Proceedings of FORTE 2002, 22nd International Conference on Formal Techniques for Networked and Distributed Systems}, 2002. To appear.
[Ver02c] A. Verdejo. LOTOS Symbolic Semantics in Maude. Technical Report 122-02, Dpto. Sistemas Informaticos y Programacion, Universidad Complutense de Madrid, January 2002.
Historical documents about the project:
[] Research   [] Teaching   [] CV   [] Personal   [Home] Home
Dr Carron Shankland    Email: ces@cs.stir.ac.uk [email me]    Last revision: 1st September 2002