Jonathan Jacky, Ruedi Risler, Ira Kalet, Peter Wootton,
Alexandra Barke, Stan Brossard, and Ralph Jackson
It is usually considered an essential element of good practice in engineering to produce a specification for a system before building it. However, it has been found to be quite difficult to produce useful specifications of large software systems. We have nearly completed a comprehensive specification for the computer control system of a cyclotron and treatment facility that provides particle beams for cancer treatments with fast neutrons, production of medical isotopes, and physics experiments. We describe the control system as thoroughly as is practical using standard technical English, supplemented by tables, diagrams, and some algebraic equations. This specification comprises over 300 single-spaced pages. A more precise and compact specification might be achieved by making greater use of formal mathematical notations instead of English. We have begun work on a formal specification of our system, using the Z and Petri net notations.