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. We are currently investigating the use of problem frames for constructing dependability cases for the BPTC control software. The work described in this paper grew out of the difficulty we encountered with keeping track of a large number of domain properties, relating them appropriately to the requirements and specifications.
Initially, we used problem diagrams simply to describe the BPTC system keeping track of how domains interacted and recording properties about the domains. As
we spent more time interacting with the BPTC engineers, we found that the problem diagrams were not only useful recording information they had told us, but also for indicating what questions to ask. The information they initially
gave us was not enough to build a safety case, yet it was not clear what additional information would be. There simply was not time to get full descriptions of all the parts of the system, so we needed to narrow our questions and focus our inquiry.
Replaced/Superseded by document(s)
A technique is presented for obtaining a specification
from a requirement through a series of incremental steps.
The starting point is a Problem Frame description, involving
a decomposition of the environment into interconnected
domains and a formal requirement on phenomena of those
domains. In each step, the requirement is moved towards
the machine, leaving behind a trail of ‘breadcrumbs’ – partial
domain descriptions representing assumptions about
the behaviors of those domains. Eventually, the transformed
requirement references only phenomena at the interface
of the machine and can therefore serve as a specification.
Each step is justified by a mechanically checkable
implication, ensuring that, if the machine obeys the derived
specification and the domain assumptions are valid, the requirement will hold. The technique is formalized in Alloy
and demonstrated on two examples.