next up previous

Final Report of the COST-247 Action

A LOTOS Verification Case Study

Muffy Thomas

University of Glasgow
Dept. of Computer Science
UK-G12 8QQ Glasgow
United Kingdom
Tel: +44 141 330 4969


This talk presents the results of a case study of the high-level design of a control device for a dual-mode linear accelerator, based on the Therac-25. The specification language LOTOS is used throughout. First, a basic LOTOS design is developed, and analysed for safety properties using both property testing (with LOLA), reasoning with the cred relation (with PAM), and using the modal mu-calculus (with CAESAR toolkit). Second, state is added in the form of abstract data types as parameters to the processes. These model the shield and beam entities. This design is also analysed, using property testing and the modal mu-calculus. In each case, we discuss what can and can't be proved, the benefits of the tools, and the contribution of the exercise to the safety case.

This presentation has been given during the COST-247 3rd Management Committee Meeting (Evry, France, September 19--20, 1994).

COST-247 Working Group(s): 1-2

This Page was prepared by Mark Jorgensen.

Back to the VASY Home page