EPSRC logo

Details of Grant 

EPSRC Reference: GR/J52716/01
Title: TEMPORAL ASPECTS OF VERIFICATION OF LOTOS SPECIFICATIONS
Principal Investigator: Calder, Professor M
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department: School of Computing Science
Organisation: University of Glasgow
Scheme: Standard Research (Pre-FEC)
Starts: 01 October 1993 Ends: 31 December 1995 Value (£): 77,021
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
Related Grants:
Panel History:  
Summary on Grant Application Form
The objectives of this project are to understand and integrate the roles of different verification and specification styles in the analysis of LOTOS specifications, and to investigate the use of modal and temporal logics for full LOTOS. Since abstract data types are often overlooked in LOTOS, a particular concern is to cover the full language.Progress:Progress has been made in several directions: case studies to motivate the research and as a testbed for results, a new semantics and modal logic for full LOTOS, and guidance on the use of techniques and tools for verification/validation.Several LOTOS specification case studies have been developed in depth, with varying verification/validation requirements. Examples include a login protocol, where the requirement is to show that the protocol satisfies the service; a medical device controller where the requirement is to show that an unsafe state cannot be reached; and aircraft side-stick controllers, where there are requirements to show that a variety of unsafe states cannot be reached and hazardous sequences of states cannot be followed. These studies illustrate a broad spectrum of specification and styles, from resource-oriented (processes model physical entities) to constraint oriented (processes model logical constraints). They cover several application areas and use data types in a variety of ways. Extensive experimentation with tools and verification techniques, particularly using the tools LOLA, PAM and VPAM, has been carried out, with particular reference to the case studies.These studies illustrate that a temporal logic is needed for LOTOS which allows reasoning about processes with data variables. A first step is to define a modal symbolic logic for full LOTOS, which can then be extended to a mu-calculus. It has been found that the standard semantics, which does not distinguish data from events, is not suitable for such a logic and so a new symbolic semantics is needed. A new symbolic semantics has been defined and work on the logic is in progress. This research has been reported at several international and national conferences/workshops. Publications to DateC. Kirkwood, M.Thomas, Experiences with LOTOS Specification and Verification: A Report on Two Case Studies, to appear in IEE WIFT-Workshop on Industrial Strength Formal Methods, IEE 1995. M. Thomas, B.Ormsby, On the Design of Side-Stick Controllers in Fly-by-Wire Aircraft, ACM Applied Computing Review, Vol. 2, no. 1 ACM, 1994. U. Martin, M.Thomas, Verification Techniques for LOTOS, in Proceedings of Formal Methods Europe 94, LNCS Vol. 873, Springer-Verlag 1994. Further papers are in preparation/have been submitted.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Summary
Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:  
Further Information:  
Organisation Website: http://www.gla.ac.uk