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.

Download