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.
In this project our key advances are:
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.
[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. |