Formal Development for a Radiation Therapy Machine

Jon Jacky, University of Washington
jon@u.washington.edu

Clinical Neutron Therapy System at UWMC

Pictures here.

Unique machine, best treatment for certain rare cancers
Built by NCI for research, now in routine use
Begin treating patients 1984
Maintained, upgraded by UWMC staff
Replacement control system anticipated from the start
Funded by hospital (patients etc.), not research grants or education
New control system begins treating patients 1999, in use today

Motivation

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

Radiation therapy machine control system!

Safety-critical, fatal accidents a real possibility
Limited opportunities for testing, unique machine already in use
Novel design, all new code, no previous performance record

Culture and environment

We had an unusually supportive culture and working environment:

Culture of safety, legal and personal responsibility
Long experience, deep understanding of application and other staff (1981 - 1999)
Respect for science, correctness, precision, mathematical modeling
Not much schedule pressure

Formal development product

We produced a formal specification that serves two purposes:

Mathematical model
- Justify and check design
- Support safety analysis
Detailed design document
- State variables in the model become program variables
- Operations in the model become functions

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.

[SETTING, VALUE, FIELD]

SETUP == SETTING $\fun$ VALUE

BEAM ::= OFF | ON

$\begin{axdef}$
		safe_: $\power$ SETUP
		match_: SETUP $\rel$ SETUP
		prescription: FIELD $\pfun$ SETUP
	$\end{axdef}$

$\begin{schema}{$		TherapyMachine



		beam: BEAM
		measured, prescribed: SETUP

	$\end{schema}$

$\begin{schema}{$		SafeTreatment



		TherapyMachine

	$\where$

		safe(measured)
		match(measured, prescribed)
		prescribed $\in$ ran prescription

	$\end{schema}$

$\forall$ TherapyMachine

beam = ON $\implies$ SafeTreatment

The 2000 line detailed formal specification that we analyzed and coded from is elaborated from this.

Implementation

Safe system design throughout --- not just formal specification

Careful hardware/software/system design
Minimize software complexity in embedded program

Time-tested, lowest-common-denominator technology, minimize dependencies

C, Xlib, TCP/IP, VxWorks
Nothing else! No database, No window manager etc.
VME hardware

Traditional technology for this application domain.

Some project metrics

Rough measures of effort and quality

About 300 page requirements (prose, pictures, tables)
About 70 page, 2000 line formal specification
About 16000 lines C
About 500 pages manuals and other docs
Requirements were significant effort, spread over many years
Most work except requirements done in 3 years, 2-3 people

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.