|
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.
|