On supporting science journalism
If you're enjoying this article, consider supporting our award-winning journalism by subscribing. By purchasing a subscription you are helping to ensure the future of impactful stories about the discoveries and ideas shaping our world today.
Modern medical devices rely on software for almost every aspect of their operation. In a machine used for cancer therapy, even the "emergency stop" button is not an actual electrical switch but a software program: hitting it causes about 15,000 lines of code to execute and shut the system down--unless, of course, there is a bug or design flaw in the software. That is where Alloy comes in--it analyzes programs to find the design problems.
Working with the developers of a cancer-therapy system, for example, we have used Alloy to explore the design of some of its features. In one case, we took a design for a new scheduling system that determines the treatment room to which the beam is sent. We set Alloy to look for scenarios in which interactions between the operator in the main control room and the therapists in the treatment rooms would produce unexpected results. Alloy found various scenarios that had not been anticipated originally.
In another case, we applied Alloy to the design of an elaborate protocol for positioning the patient under the proton beam, which turned out to have a subtle and unexpected consequence: the angle of the gantry crept around over time, even when it was not being intentionally adjusted. With a small Alloy model we showed how, by choosing the right abstractions, this problem could be reduced to the same, rather simple problem as that for designing a car accessory system that remembers driver-seat positions. In fact, the therapy system has many safeguards and the gantry movement was not a dangerous problem. But if the correct abstractions had been used from the start, the design would have been much simpler and operating the software considerably easier.