Lessons from the Formal Development of a Radiation Therapy Machine Control Program

  • Jonathan Jacky
Part of the Formal Approaches to Computing and Information Technology (FACIT) book series (FACIT)


Formal methods work best where traditional programming methods do not work very well: problems that are too difficult to solve by intuition or too novel to solve by modifying some existing program or design. We are developing the control program for the therapy operator’s console for a unique radiation therapy machine. This is not a pilot study or demonstration project; we will use this program to administer neutron therapy at our clinic. The program is safety-critical; it could contribute to delivering a treatment that differs from the prescribed one, irradiating the wrong volume within the patient or delivering the wrong dose (there are also hardware protection mechanisms that work independently of the control program). Errors in medical software can have serious consequences (Jacky, 1996; Leveson and Turner,1993; Leveson, 1995), and our experience shows that development methods typically used in this field are only partially effective at eliminating errors (Jacky and White, 1990). We decided to try a more rigorous method.


Control Program Formal Description State Schema Operation Schema Controller Process 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag London 1999

Authors and Affiliations

  • Jonathan Jacky

There are no affiliations available

Personalised recommendations