The Clinical Neutron Therapy System (CNTS) project is building a new control system for a clinical cyclotron in the Cancer Center. It provides new capabilities to the Cancer Center’s neutron radiation therapy program. It is also an example of the application of formal methods (in particular the Z notation and the SMV model checker) in software development.
The new control software and hardware for the isocentric treatment unit were completed in July 1999 and are now in use treating patients.
This report provides an overview and summary of the control system project:
These recent reports describe the new control system in detail:
This brief conference paper describes how we used formal software development methods in this project:
Here is a large portion of the formal specification itself:
More about the project appears in the following reports and papers, and in a textbook.
- TR 90-12-01 CNTS control system specification, part 1
- TR 90-12-02 Technical description of CNTS
- TR 91-02-02 Using formal models to plan control system testing (Dose Monitor Controller)
- TR 92-05-01 CNTS control system specification, part 2
- TR 95-08-03 CNTS control system specification, part 3
- TR 95-12-01 Formal specification of control software (Z notation)
- FM 90 Formal specifications for a clinical cyclotron control system
- PAC 91 Control system specification for a cyclotron and neutron therapy facility
- ZUM 92 Formal specification and development of control system input/output
- FME 93 Specifying a safety-critical control system in Z (also published as TSE 95)
- ZUM 95 Formal development of a graphical user interface for a radiation therapy machine
- AAS 97 Modelling, checking and implementing a control program for a rad. therapy machine
- ZUM 97 Experience with Z developing a control program for a radiation therapy machine
- ZUM 98 Analyzing a real-time program with Z (and the SMV model checker)