Overview: The Northeast Proton Therapy Center

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 direct the beam to the allocated treatment room. 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 electro-mechanically positioned by staff within the treatment room. The beam delivery nozzle 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 and controlled 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.

Previous Work: Analyzing the Emergency Stop Feature [2]

Andrew Rae, Prasad Ramanan, Daniel Jackson, Jay Flanz & Didier Leyman

We analyzed the (software) emergency shutdown feature of the NPTC therapy control system using a directed form of code review based on module dependences. Dependences between modules are labeled by particular assumptions; this allows one to trace through the code, and identify those fragments responsible for critical features. An "assumption tree" is constructed in parallel, showing the assumptions which each module makes about others. The root of the assumption tree is the critical feature of interest, and its leaves represent assumptions which, if not valid, might cause the critical feature to fail. The analysis revealed some unexpected assumptions that motivated improvements to the code.

Previous Work: Design-Level Commutativity Analysis [3]

Greg Dennis, Robert Seater, Derek Rayside & Daniel Jackson

The NPTC therapy control system is a distributed multi-user system. Each treatment room has a corresponding control room, in addition to the master control room. All of these users share, and can update, a single queue that controls which room gets the beam next.

Suppose that user A issues queue-updating command alpha at (almost) the same instant as user B issues queue-updating command beta. If the command sequence alpha-beta leaves the queue in the same state as the command sequence beta-alpha, we say that alpha and beta commute.

However, if the sequence alpha-beta leaves the system in a different state than the sequence beta-alpha, one or more of the users of the system may be surprised by the subsequent behaviour of the system. These kinds of surprises are to be avoided in general, but in safety critical environments in particular.

We reduced the problem of checking commutativity of two operations to a constraint solving problem. We express each operation as a constraint in the Alloy modelling notation [1]. The assertion that two operations commute is itself a constraint, whose negation is satisfied by scenarios in which commutativity fails. The Alloy Analyzer translates constraints to boolean formulas, and solves them with the aid of off-the-shelf SAT solvers. Usually, when two operations do not commute, a violating scenario is found in a few seconds. This analysis is carried out at design time.

Current Work: Treatment Points

Derek Rayside & Daniel Jackson

Recently, the medical physicists at NPTC have decided that they would like to implement new ways of directing the beam at tumours, such as raster scanning. (They refer to these as new treatment modalities as conceptual "treatment points".) The hardware is physically capable of these new treatment modalities, but the software does not currently support them.

Adding the treatment point concept to the therapy control system will require extensive changes to the software. We are currently conducting analyses to determine:

• which parts of the software need to be changed
• how those changes will affect the rest of the system
• that the system will retain its current level of safety after the changes are implemented

Current Work: Software Interlocks

Derek Rayside & Daniel Jackson

We are exploring the idea of an end-to-end check on the therapy control system: given the settings of the beam at the time of treatment delivery, compute what the prescription should have been, and compare that with the patient database. Such a system, operating in real time, would guard against a number of potential safety concerns, such as: treatment over-dose, treatment under-dose, equipment malfunction, mistaken patient identity, and so on.

Research Funding

This research was supported by: grant 0086154 ('Design Conformant Software') from the ITR program of the National Science Foundation; grant 6895566 ('Safety Mechanisms for Medical Software') from the ITR program of the National Science Foundation; and by the High Dependability Computing Program from NASA Ames cooperative agreement NCC-2-1298.

References

[1] Alloy Language and Analyzer. Software Design Group, CSAIL, MIT. http://alloy.mit.edu

[2] Andrew Rae, Prasad Ramanan, Daniel Jackson and Jay Flanz. Critical Feature Analysis of a Radiotherapy Machine. International Conference of Computer Safety, Reliability and Security (SAFECOMP 2003). Edinburgh, Scotland, UK, September 2003.

[3] Greg Dennis, Robert Seater, Derek Rayside, and Daniel Jackson. Automating Commutativity Analysis at the Design Level. International Symposium on Software Testing and Analysis (ISSTA 2004). Boston, MA, USA, July 2004.