Software Dependability for Proton Therapy
The Software Design Group at MIT is engaged in a collaborative project with the Burr Proton Therapy Center (BPTC) 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.
This work is supported by the National Science Foundation ITR Programme (Safety Mechanisms for Medical Software, Award number 0325283).
1. End-to-End Dependability Analysis
- Robert Seater. Chapter 4: BPTC Case Study. Building Dependability Arguments for Software Intensive Systems. PhD Thesis (Draft Chapter), Massachusetts Institute of Technology, September 2008 (PDF) (PS)
- Daniel Jackson. A Direct Path To Dependable Software. Communications of the Association for Computing Machinery (CACM). 2008. (PDF)
- Robert Seater, Daniel Jackson, and Rohit Gheyi. Requirement Progression in Problem Frames: Deriving Specifications from Requirements. Requirements Engineering Journal (REJ'07). 2007. (PDF) (PS)
- Robert Seater and Daniel Jackson. Requirement Progression in Problem Frames Applied to a Proton Therapy System. 14th IEEE International Requirements Engineering Conference (RE'06). September 2006. Minneapolis, MN. (PDF) (PS)
- Robert Seater and Daniel Jackson. Problem Frame Transformations: Deriving Specifications from Requirements. Second International Workshop on Applications and Advances in Problem Frames (IWAAPF'06), associated with the International Conference on Software Engineering (ICSE'06). Shanghai, China. May, 2006. (PDF) (PS)
Members (Dependability)
- Robert Seater (MIT SDG)
- Daniel Jackson (MIT SDG)
- Ed Crawley (MIT)
- Rob Miller (MIT)
- Jay Flanz (BPTC)
2. 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.
- Daniel Jackson & Michael Jackson. Separating Concerns in Requirements Analysis: An Example. M. Butler, C. Jones, A. Romanovsky, E. Troubitsyna (editors). Chapter of Rigorous development of complex fault tolerant systems. Springer-Verlag. (PDF)
- Andrew Rae, Daniel Jackson, Prasad Ramanan, Jay Flanz, and Didier Leyman. Critical feature analysis of a radiotherapy machine. Reliability Engineering & System Safety Volume 89, Issue 1, Elsevier Science, July 2005, Pages 48-56. (link)
Members (Separation of Concerns)
- Robert Seater (SDG)
- Daniel Jackson (SDG)
- Lucy Mendel (SDG)
- Andrew Rae (SDG)
- Miachael Jackson (Open University)
- Jay Flanz (BPTC)
- Doug Miller (BPTC)
3. Alloy Model of the Automatic Beam Scheduler
- Greg Dennis, Robert Seater, Derek Rayside, Daniel Jackson. Automating Commutativity Analysis at the Design Level. International Symposium on Software Testing and Analysis, Boston, MA, July 2004. (PS) (PDF)
We modeled the proposed Automatic Beam Scheduler algorithm in Alloy, and analyzed the commutativity of the commands. That 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
These files are compatible with Alloy v3. You can download current and past versions of Alloy from the Alloy website.
Members (Beam Scheduler)
- Robert Seater (SDG)
- Greg Dennis (SDG)
- Daniel Jackson (SDG)
- Derek Rayside (SDG)
- Jay Flanz (BPTC)
- Doug Miller (BPTC)
- Hanne Kooy (BPTC)
- Philippe Thirionet (IBA)
- Didier Leyman (IBA)