Formal specification of control software for a radiation therapy machine (revised)

Jonathan Jacky, Michael Patrick and Jonathan Unger

January, 1997


This report presents a formal (mathematical) specification for the operator's console of a computer-controlled radiation therapy machine equipped with a multileaf collimator. This formal specification, rather than the prose specification, serves as the primary reference source for programming and test planning.

Specified functions include selecting treatment setups from a database of stored prescriptions, setting up prescriptions on the treatment machine manually or semi-automatically, checking that the setup conforms to the prescription (with provision for overriding certain settings, with operator confirmation), safety interlocking and essential user interface features. The specification supports physics and experimental procedures as well as normal patient treatments.

The specification is expressed in the Z notation. It formalizes the requirements in a thorough informal (English prose) specification. Its organization suggests a detailed design.

Download (76 pages): PDF (440 kb)