Abstract:

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.