Lessons from the Formal Development of a Radiation Therapy Machine Control Program
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.
KeywordsControl Program Formal Description State Schema Operation Schema Controller Process
Unable to display preview. Download preview PDF.