Verifying therapy safety interlock system with spin

Abstract

The ever-increasing reliance of society on computers has led to a need for highly reliable systems. Computer systems perform critical functions in a number of areas ranging from online transaction processing (such as banking systems) to embedded environments (such as nuclear power plant safety control systems). Their development requires a higher level of attention than many others, and the use formal methods is one way to ensure that they are as correct as possible. This paper reports on the successful use of model checking in the design and verification of the Safety Interlock System (SIS) at iThemba LABS. SIS is part of proton therapy control system (TCS) and its main task is to monitor and evaluate the safety conditions in the TCS as a whole. It looks after other dynamic systems and electronic units which may join and leave the whole TCS either predictably or unpredictably, and oversees their distributed interactions. An appropriate design pattern in this kind of setup is the Observer, also known as Publish-Subscribe or Dependents. Although not new, the Observer pattern is receiving increasing interest because of its usefulness in event-driven systems. It encompasses a well-established communications paradigm that allows any number of subjects (publishers) to communicate with any number of observers (subscribers) asynchronously and anonymously via event channels. The study focuses on the development of an abstract communication model between the SIS and the systems it monitors. A number of important correctness properties are verified with the SPIN model checker.