We modeled and tested an embedded controller that will be incorporated into a medical process control application. The controller (including customized software) was developed by others, and its original documentation does not include a functional speci cation that is su ciently complete and accurate for our needs. We proposed a functional speci cation of certain important controller behaviors, based on the available documentation and behavior that we had observed. We used Petri nets for our speci cation notation. From the Petri net, we derived a series of tests intended to reveal whether our provisional speci cation accurately characterized controller behavior. The method for deriving the tests from the Petri net is described. The tests systematically traverse the Petri net and also present faults that should be handled in a reasonable way. Performing the tests revealed several errors in our initial speci cation. We modi ed our speci cation until it was consistent with all observed behaviors, covering a wide range of situations. Department of Computer Science and Engineering, FR-35, University of Washington, Seattle WA 98195. Supported in part by National Institutes of Health grant number LM04174 from the National Library of Medicine

Particle radiotherapy facilities are highly capital intensive and must operate over decades to recoup the original investment. We describe the successful, long-term operation of a neutron radiotherapy center at the University of Washington, which has been operating continuously since September 1984. To date, 2836 patients have received neutron radiotherapy. The mission of the facility has also evolved to include the production of unique radioisotopes that cannot be made with the low-energy cyclotrons more commonly found in nuclear medicine departments. The facility is also used for neutron damage testing for industrial devices. In this paper, we describe the challenges of operating such a facility over an extended time period, including a planned maintenance and upgrade program serving diverse user groups, and summarize the major clinical results in terms of tumor control and normal tissue toxicity. Over time, the mix of patients being treated has shifted from common tumors such as prostate cancer, lung cancer, and squamous cell tumors of the head and neck to the rarer tumors such as salivary gland tumors and sarcomas due to the results of clinical trials. Current indications for neutron radiotherapy are described and neutron tolerance doses for a range of normal tissues presented.

The fast neutron therapy facility at the University of Washington has been in routine clinical use for 25 years. 50.5 MeV protons produce neutrons in a beryllium target mounted on an isocentric gantry. Beam shaping is accomplished with a 40-leaf collimator. Dosimetry measurements for treatment planning and calibration are performed with tissue equivalent ion chambers. A layered phantom of alternating Solid Water® and Plastic Water® slabs has been developed for rapid dose verification measurements. The neutron field in the room has been used for radiation testing of electronic components.

The Idaho National Laboratory (INL), the University of Washington (UW) Neutron Therapy Center, the University of Essen (Germany) Neutron Therapy Clinic, and the Northern Illinois University(NIU) Institute for Neutron Therapy at Fermilab have been collaborating in the development of fast-neutron therapy (FNT) with concurrent neutron capture (NCT) augmentation [1,2]. As part of this effort, we have conducted measurements to produce suitable benchmark data as an aid in validation of advanced three-dimensional treatment planning methodologies required for successful administration of FNT/NCT. Free-beam spectral measurements as well as phantom measurements with Lucite{trademark} cylinders using thermal, resonance, and threshold activation foil techniques have now been completed at all three clinical accelerator facilities. The same protocol was used for all measurements to facilitate intercomparison of data. The results will be useful for further detailed characterization of the neutron beams of interest as well as for validation of various charged particle and neutron transport codes and methodologies for FNT/NCT computational dosimetry, such as MCNP [3], LAHET [4], and MINERVA [5].

We are developing a control program for a unique radiation therapy machine. The program is safety-critical, executes several concurrent tasks, and must meet real-time deadlines. Development employs both formal and traditional methods: we produce an informal specification in prose (supplemented by tables, diagrams and a few formulas) and a formal description in Z. The Z description includes an abstract level that expresses overall safety requirements and a concrete level that serves as a detailed design, where Z paragraphs correspond to data structures, functions and procedures in the code. We validate the Z texts against the prose specification by inspection. We derive most of the code from the Z texts by intuition and verify it by inspection but a small amount of code is derived and verified more formally. We have produced about 250 pages of informal specification and design description, about 1200 lines of Z and about 6000 lines of code. Experiences developing a large Z specification and writing the program are reported, and some errors we discovered and corrected are described.

A control program has been developed for use with an existing radiation therapy machine used to treat cancer patients with neutrons. The system is safety-critical, multitasking, meets real-time deadlines and replaces existing control system hardware and software in use since 1984. The program allows therapists to treat patients in a safe and timely manner. The system controls various wedges, filters, and a collimator that shape the therapy beam dose distribution. It checks the actual machine state against a database of prescribed machine setups, and records accumulating dose for each patient across multiple treatment sessions, and updates logs used for patient record keeping and machine quality assurance. Development involved both formal and traditional methods, including extensive use of the Z formal specification language. Since the therapy equipment is in daily clinical use with the original control system, access to real machine hardware is very limited. This limited access necessitated the use of portable components such as X windows and ANSI C to allow for most development and testing to be done on a general purpose workstation and operating system. The program was written only in ANSI C using minimal support (X Windows, the real time operating system, and ANSI C libraries) to reduce the dependence on other third party products and software. This was done to ensure stability over the lifespan of the system and for quality control of safety critical functions. Experiences with testing the program and actual clinical use is reported.