Formal Development for a Radiation Therapy Machine

Jon Jacky, University of Washington

Clinical Neutron Therapy System at UWMC

Pictures here.


Formal methods are not mainstream.
What justifies unusual development effort?

Radiation therapy machine control system!

Culture and environment

We had an unusually supportive culture and working environment:

Formal development product

We produced a formal specification that serves two purposes:

  1. Mathematical model
  2. Detailed design document

State-based safety analysis

Tutorial and exercises here.

Answers to exercises here.

Z Notation

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.


safe_: \power SETUP
match_: SETUP \rel SETUP
prescription: FIELD \pfun SETUP

\begin{schema}{ TherapyMachine }

beam: BEAM
measured, prescribed: SETUP

\begin{schema}{ SafeTreatment }

match(measured, prescribed)
prescribed \in ran prescription

\forall TherapyMachine @ beam = ON \implies 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.

Some project metrics

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.

Further reading

Jon Jacky,