Determining the specification of a control system from that of its environment

  1. Lookup NU author(s)
  2. Professor Cliff Jones
Author(s)Hayes I, Jackson M, Jones C
Editor(s)Araki, K., Gnesi, S., Mandrioli, D.
Publication type Conference Proceedings (inc. Abstract)
Conference NameInternational Symposium of Formal Methods Europe (FME)
Conference LocationPisa, Italy
Year of Conference2003
Source Publication Date8-14 September 2003
Series TitleLecture Notes in Computer Science
Full text for this publication is not currently held within this repository. Alternative links are provided below where available.
Well understood methods exist for developing programs from given specifications. A formal method identifies proof obligations at each development step: if all such proof obligations are discharged, a precisely defined class of errors can be excluded from the final program. For a class of "closed" systems such methods offer a gold standard against which less formal approaches can be measured.For "open" systems -those which interact with the physical world- the task of obtaining the program specification can be as challenging as the task of deriving the program. And, when a system of this class must tolerate certain kinds of unreliability in the physical world, it is still more challenging to reach confidence that the specification obtained is adequate. We argue that widening the notion of software development to include specifying the behaviour of the relevant parts of the physical world gives a way to derive the specification of a control system and also to record precisely the assumptions being made about the world outside the computer.
Notes(A development of this paper has now been submitted (different title, different order of authors) to Acta Informatica - I obviously hope it will replace this item pre-RAE.) The technique described here is a major outcome of the 6-year DIRC project. It's importance is that it shows how to determine the specification of the technical part of a larger (possibly socio-technical) system. The technicalities required that we brought together work from all three authors.
ActionsLink to this publication
Library holdingsSearch Newcastle University Library for this item