Most system failures do not stem from incorrect system requirements or from components that fail to meet their individual specifications. Rather, they come about when the component specification are insufficient to enforce the system requirement because of implicit (but incorrect) assumptions about the system's environment [3, 4, 5]. As software is increasingly deployed in contexts in which it controls multiple, complex physical devices, this issue is likely to grow in importance. Consequently, our research has focused on techniques for constructing an argument that the component specifications do indeed ensure the system requirement, and on exposing the environmental assumptions upon which that argument relies.
Our research group has been involved in an ongoing collaboration with the Burr Proton Therapy Center (BPTC), a radiation therapy facility associated with the Massachusetts General Hospital in Boston, investigating improved methods for ensuring software dependability. The BPTC system is considered to be 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 [6]. The most infamous of these accidents are those involving the Therac-25 machine [5, 7], in whose failures faulty software was a primary cause. More recently, software appears to have been the main factor in similar accidents in Panama in 2001 [8].
The BPTC system was developed in the context of a sophisticated safety program including a detailed risk analysis. Unlike the Therac-25, the BPTC system makes extensive use of hardware interlocks, monitors, and redundancies. The software itself is instrumented with abundant runtime checks, heavily tested, and manually reviewed. However, concerns about the dependability of the software control systems remain and have been the focus and motivation of our work. Our focus has been on investigating concerns raised by the engineers who maintain the control software. For example: Could a patient be delivered a different patient's treatment? Given that the correct treatment is selected, is it correctly translated and transmitted to the hardware? When a dose of radiation is delivered to a patient, is it accurately logged?
Recently, we have been investigating the use of Problem Frames for constructing dependability cases for the BPTC control software. The Problem Frames approach offers a framework for describing the interactions amongst software and other system components [9, 10]. It helps the developer understand the context in which the software problem resides, and which of its aspects are relevant to the design of a solution [11, 12, 13]. A requirement is an end-to-end constraint on phenomena from the problem world, which are not necessarily controlled or observed by the machine. During subsequent development, the requirement is typically decomposed into a specification (of a machine to be implemented) and a set of domain assumptions (about the behavior of physical devices and operators that interact directly or indirectly with the machine). This process is called ''Requirement Progression''.
Our work [1, 2] aims to create a strategy by which requirement progression can be performed systematically by a series of incremental transformations. For example, given a system requirement that the log accurately reflect the radiation delivered to the patient and a Problem Frame description of how the log and patient (indirectly) interact, an analyst can systematically derive a specification on the Treatment Control System (TCS) that is sufficient to enforce that requirement. In the process of performing that derivation, the analyst leaves behind a trail of ''breadcrumbs'' in the form of domain assumptions. The analyst is guaranteed that, so long as those assumptions hold, the derived specification for the TCS is sufficient to enforce the system requirement.
For example, the following is a Problem Frames style description of the logging requirement that might be used in a system such as the BPTC. The requirement, formalized in the Alloy language, says that the log must accurately reflect the number of bursts of radiation delivered to the patient with a margin of error of 1 burst. This means that if the treatment is interrupted at any point, the log will permit the treatment to be resumed at a later date.
The terms used in that diagram are related to phenomena in the real world according to the following designations:
d = # DoseUnit........Upon the completion of treatment, the
patient's body has exactly d units of
radiation.
e = # Entry...........Upon the completion of treatment, there are
exactly e entries in the log.
b in DelivBurst.......At some point during the treatment, a burst
of radiation was delivered, associated with
the burst b.
b in ReqBurst.........At some point during the treatment a request
was made for burst b to be delivered.
b in AckBurst.........At some point during the treatment, an
acknowledgement was made that burst b was
delivered.
b in ReqWrite.........At some point during the treatment, there
was a request for burst b to be written.
b in AckWrite.........At some point during the treatment, there
was an acknowledgement that burst b was
written.
After applying our incremental technique, we derive the following argument diagram. The argument diagram involves a specification on the software domain (the treatment control system) and a set of explicit assumptions about the behaviors of the other domains. The analyst is guaranteed that the spoftware specification will be sufficiently strong to ensure the system requirement as long as the domain assumptions hold.
We are building safety cases for key aspects of the BPTC. Doing so has an immediate benefit to the hospital staff and patients who rely on those safety properties on a daily basis. As with any complex system, knowing that the components of the BPTC operate correctly is not enough; one wants to know that system as a whole has certain properties.
We are doing more than just a case study; we are developing a general approach for building auditable safety cases. That is, arguments that are not only sound but which can be verified by an outside source. For systems like the BPTC, this is essential -- they no only want to know that the system will operate safely, but they also need that argument to be verifiable by an outside authority.
Requirements Engineering asks the question ''If these components obey these requirements, will the system as a whole have this property?''. Program Analysis asks the question ''How confident are we that this piece of software obeys its requirement?''. A full safety argument about a software-heavy system (such as medical devices like the BPTC) must incorporate both sides -- they must argue that the properties we can establish about the software components are sufficient to guarantee other properties about the system as a whole. Our ongoing project is the unification of these two fields in the construction of end-to-end safety arguments.
[1] Robert Seater and Daniel Jackson. Requirement Progression in Problem Frames Applied to a Proton Therapy System. In Proceedings of the 14th IEEE International Requirements Engineering Conference (RE'06). Minneapolis, MN, USA. September, 2006.
[2] Robert Seater and Daniel Jackson. Problem Frame Transformations: Deriving Specifications from Requirements. In Proceedings of the Second International Workshop on Applications and Advances in Problem Frames (IWAAPF'06), page 71. Shanghai, China. May, 2006.
[3] T. E. Bell and T. A. Thayer. Software Requirements: are they really a problem? In Proceedings of the 2nd International Conference on Software Engineering (ICSE'67), pages 61--68. IEEE Society Press. San Fransisco, CA. 1967.
[4] Sol Greenspan, John Mylopoulos, and Alex Borgida. On Formal Requirements Modeling Languages: RML Revisited. In Proceedings of the 16th International Conference on Software Engineering (ICSE'94), pages 135--147. IEEE Computer Society Press. Sorento, Italy. 1994.
[5] Nancy G. Leveson. Safeware: System Safety and Computers. Addison-Wesley Longman Publishing Co., Inc. Boston, MA. 1995. ISBN 0-201-11972-2.
[6] Robert C. Ricks, Mary Ellen Berger, Elizabeth C. Holloway, and Ronald E. Goans. REACTS Radiation Accident Registry: Update of Accidents in the United States. International Radiation Protection Association. 2000.
[7] Nancy G. Leveson and C. Turner. An investigation of the Therac-25 accidents. In IEEE Computer. Vol 7, num 26, pages 18--41. 1993.
[8] Food and Drug Administration. FDA Statement on Radiation Overexposures in Panama. http://www.fda.gov/cdrh/ocd/panamaradexp.html.
[9] Michael Jackson. Software Requirements and Specifications: a lexicon of practice, principles and prejudice. Addison-Wesley. 1995.
[10] Michael Jackson. Problem Frames: analyzing and structuring software development problems. Addison-Wesley Longman Publishing Co., Inc. Boston, MA. 2001. ISBN 0-201-59627-X.
[11] Charles B. Haley, Robin C. Laney, and Bashar Nuseibeh. Using Problem Frames and Projections to Analyze Requirements for Distributed Systems. In Proceedings of the 10th International Workshop on Requirements Engineering: Foundation for Software Quality (REFSQ'04), pages 203--217. Essener Informatik Beitrage. Editors B. Regnell, E. Kamsties, and V. Gervasi. 2004.
[12] Michael Jackson. Problem Analysis Using Small Problem Frames. In South African Computer Journal. Vol. 22, pages 47--60. March, 1999.
[13] Robin C. Laney, Leonor Barroca, Michael Jackson, and Bashar Nuseibeh. Composing Requirements Using Problem Frames. In Proceedings of the 12th International Conference on Requirements Engineering (RE'04). Kyoto, Japan. IEEE Computer Science Press, pages 121--131. 2004.