Proton Therapy Control System
The Software Design Group at MIT is engaged in a collaborative project with the Northeast Proton Therapy Center (NPTC) in Boston and Ion Beam Applications (IBA) of Belgium, whose purpose is to develop and evaluate ideas for improving the quality and safety of medical software. This collaboration has resulted in three ongoing projects. One involves using Alloy to perform commutativity analysis on the Automatic Beam Scheduler, revealing situations concurrency between human operators can produce unexpected results. A second involves analyzing code dependences to identify and audit code responsible for critical functions. A third involves the development of end-to-end interlocks to ensure that machine settings match prescriptions.
Details and Background
The Northeast Proton Therapy Center (NPTC) is a new radiation therapy facility associated with the Massachusetts General Hospital in Boston. It is one of only two facilities in the United States to offer treatment with protons (rather than electrons or x-rays). Proton beams require much more elaborate and expensive equipment to produce, but can be more tightly conformed, and cause less damage to surrounding tissue. They are thus more suitable for treatments in sensitive areas such as the eye, and for the treatment of tumors in the brains of children, for which collateral damage has more serious long-term consequences. The center occupies a new building adjacent to the hospital, and began treating patients in the fall of 2001.
The Software Design Group in the MIT Lab for Computer Science began a collaboration in April 2002 with NPTC and the developers of the therapy system to investigate better methods for the development of safety critical software. The NPTC system would be used as a challenging example of a modern and complex medical device for the purposes of research; in turn, the results of the research would be used where appropriate to improve the safety and reliability of the system.
The NPTC installation has at its core a cyclotron that generates a beam of protons. The beam is multiplexed amongst several treatment rooms, each with its own gantry and nozzle for positioning the beam. Technicians in a master control room supervise the cyclotron and allocate the beam to treatment rooms. Each treatment room is paired with a treatment control room, in which clinicians enter and execute treatment prescriptions.
The patient is placed on a couch which is electromechanically positioned by staff within the treatment room. The beam emitter is also positioned, and its aim verified by staff using X-rays and lights attached to the emitter. The staff then leave the room, and the treatment is initiated from the treatment control room. Treatment consists of irradiating a specific location on the patient using a beam of protons with a defined lateral and longitudinal distribution.
The machine is considered safety critical primarily due to the potential for overdose --- treating the patient with radiation of excessive strength or duration. The International Atomic Energy Agency lists 80 separate accidents involving radiation therapy in the United States over the past fifty years. The most famous of these accidents are those involving the Therac-25 machine. Faulty software was a primary cause of the Therac-25 failures. More recently, software appears to have been the main factor in similar accidents in Panama in 2001.
The NPTC system was developed in the context of a sophisticated safety program. Unlike the Therac-25, the NPTC system makes extensive use of hardware interlocks, and has a redundant PLC-based system running in parallel with the software control system. Video cameras inside the control room allow the technicians to view internal mechanisms, including a lead beam stop that can be inserted to isolate the treatment room from the cyclotron. The software itself is instrumented with abundant runtime checks, including a heartbeat monitor to ensure continued operation of critical processes. A detailed system-level risk analysis was performed. The software implementation was heavily tested, and manually reviewed against rigorous coding standards.
Separation of Concerns in Critical Systems
Traditionally, a requirements document is structured as a long list of individual "requirements", each describing an anticipated function or user interaction. The result of this approach is that different concerns that should be separated (in the requirements and then subsequently in the design and implementation) are merged together. In a critical system, this is bad, because it makes it hard to ensure that critical concerns are addressed properly, since they are intertwined with less critical ones. We are investigating a new approach based on the identification of "subproblems", whose composition is deferred. As a case study, we are analyzing a part of the design of the proton therapy system that handles the positioning of the gantry for two distinct purposes: determining exact alignments for treatment, and establishing and recording convenient positions for imaging.
Members (Separation of Concerns)
- Robert Seater (SDG)
- Daniel Jackson (SDG)
- Lucy Mendel (SDG)
- Miachael Jackson (Open University)
- Jay Flanz (NPTC)
- Doug Miller (NPTC)
Alloy Model of the Automatic Beam Scheduler
We modeled the proposed Automatic Beam Scheduler algorithm in Alloy, and analyzed the commutativity of the commands. Our results are described in a paper published in ISSTA'04 (see publications). The Alloy model is available for download. Here is a description of the files in the archive:
- main - specification of the ABS
- invariants - commands to check that operations preserved invariants
- tcrTcrEquiv - commands to check diamond equivalence for TCR-TCR pairs
- tcrTcrConnect - commands to check diamond connectivity for TCR-TCR pairs
- mcrTcrEquiv - commands to check diamond equivalence for MCR-TCR pairs
- mcrTcrConnect - commands to check diamond connectivity for MCR-TCR pairs
You should compile and run with the latest Release Candidate of Alloy 3.0. Before compiling with any of last 4 files, you may want to comment out the rest of the commands you don't expect to run; compilation is O(n) in both time and space for n commands, and with some files containing 16 commands it can take a while and will occasionally cause an out-of-memory error to compile the whole file at once.
Members (Beam Scheduler)
- Robert Seater (SDG)
- Greg Dennis (SDG)
- Daniel Jackson (SDG)
- Derek Rayside (SDG)
- Jay Flanz (NPTC)
- Doug Miller (NPTC)
- Hanne Kooy (NPTC)
- Philippe Thirionet (IBA)
- Didier Leyman (IBA)