Browse by author
Lookup NU author(s): Emeritus Professor Cliff JonesORCiD, Professor Michael Jackson
Well understood methods exist for developing programs from formal specifications. Not only do such methods offer a precise check that certain sorts of deviations from their specifications are absent from implementations but they can also increase the productivity of the development process by careful use of layers of abstraction and refinement in design. These methods, however, presuppose a specification from which to begin the development. For tasks that are fully described in terms of the symbolic values within a machine, inventing a specification is not difficult but there is an increasing demand for systems in which programs interact with an external physical world. Here, the task of fixing the specification for the “silicon package” can be more challenging than the development itself. Such applications include control programs that attempt to bring about changes in the physical world via actuators and measure things in that external (to the silicon package) world via sensors. Furthermore, most systems of this class must tolerate failures in the physical components outside the computer: it then becomes even harder to achieve confidence that the specification is appropriate. This paper offers a systematic way to derive the specification of a control program. Furthermore, our approach leads to recording assumptions about the physical world. We also discuss separating the detection and management of faults from system operation in the absence of faults. This discussion is linked to the distinction between “normal” and “radical” design. This report is a preprint of a paper that will appear in an LNCS volume — please cite that publication [JHJ07].
Author(s): Jones CB, Hayes IJ, Jackson MA
Publication type: Report
Publication status: Published
Series Title: School of Computing Science Technical Report Series
Year: 2007
Pages: 31
Print publication date: 01/08/2007
Source Publication Date: August 2007
Report Number: 1045
Institution: School of Computing Science, University of Newcastle upon Tyne
Place Published: Newcastle upon Tyne
URL: http://www.cs.ncl.ac.uk/publications/trs/papers/1045.pdf
