|
The objectives of this project are to investigate the inadequacies of the LOTOS sub language ACT ONE used for specifying abstract data types; to investigate verification procedures for relations between LOTOS specifications; to develop a safety-critical application for testing the results of the above; and to submit suggestions for improvement to the LOTOS community.Progress:Progress has been made in several directions, inspired mainly by specification case studies.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. There studies illustrate a broad spectrum of specification and styles and employ data types in a variety of ways. The inadequacies of ACT ONE as a specification language are highlighted in these studies. However, at the same time, the power of expressiveness deriving from the abstract data types, and their effects on the simplification of the verification requirement, are also demonstrated. The results of these case studies, in the way of proposals for changes to ACT ONE and requirements for a data type language, have been presented at internation meetings of LOTOS users in UK and Europe. Another outcome is a new symbolic semantics for LOTOS which separates the concerns of data and events. The semantics permits processes parameterised over data, and separates the two proof systems: data and events, such that future changes to the data types sub-language can be easily incorporated into the language. Publications to Date:1. C.Kirkwood, M. Thomas, Experiences with LOTOS Specification and Verification: A Report on Two Case Studies, to appear in IEEE WIFT Workshop on Industrial Strength Formal Methods, IEEE 1995.2. M. Thomas, The Story of the Therac-25 in LOTOS, High Integrity Systems Journal, Vol. 1, no. 1, Oxford University Press, 1994. 3. 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. 4. M. Thomas, A Proof of Incorrectness using LP: the Editing Problems from the Therac-25, High Integrity Systems Journal, Vol. 1, no. 1, Oxford University Press, 1994.5. U. Martin, M. Thomas, Verification Techniques for LOTOS, in Proceedings of Formal Methods Europe 94, LNCS Vol. 873, Springer-Verlag 1994.6. M. Thomas,Order, Disorder and Chaos in Complex Systems: The role of formal methods in safety-critical computer software, in Proceedings of SCOS Conference Organisations and Symbols of Transformation, Barcelona, 1993.
|