Jon Jacky, University of Washington
Formal methods are not mainstream.
What justifies unusual development effort?
Radiation therapy machine control system!
We had an unusually supportive culture and working environment:
We produced a formal specification that serves two purposes:
Tutorial and exercises here.
Answers to exercises here.
Specification language for expressing very large boolean expressions (CNTS spec is 2000 lines).
Tutorial and links here.
Good Z style emphasizes invariants (the "value added" that isn't easily expressed in most programming languages)
Specify a radiation therapy machine on the back of an envelope!
The therapy beam can only turn on or remain on when the actual setup of the machine matches a stored prescription that the operator has selected and approved.
|[SETTING, VALUE, FIELD]|
|SETUP == SETTING VALUE|
|BEAM ::= OFF | ON|
|match_: SETUP SETUP|
|prescription: FIELD SETUP|
|measured, prescribed: SETUP|
|prescribed ran prescription|
|TherapyMachine beam = ON SafeTreatment|
The 2000 line detailed formal specification that we analyzed and coded from is elaborated from this.
Safe system design throughout --- not just formal specification
Time-tested, lowest-common-denominator technology, minimize dependencies
Traditional technology for this application domain.
Rough measures of effort and quality
About 10 errors, < 1 error/KLOC, compare to > 2 error/KLOC other projects we've done (without formal spec).
Errors not serious, easily corrected, no patients mistreated, no treatments delayed
Model (formal spec) not quite accurate. Insufficient granularity in timing.
One (potentially) safety-critical failure occurs after 3 years in use!
No harm done, detected immediately. Hardware failure involved.