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.