The Open UniversitySkip to content
 

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

Hayes, Ian J.; Jackson, Michael A. and Jones, Cliff B. (2003). Determining the specification of a control system from that of its environment. In: International Symposium of Formal Methods: Proceedings of FME2003, 8-14 Sept 2003, Pisa, Italy, Springer Berlin, pp. 154–169.

URL: http://springerlink.metapress.com/content/531u4w0h...
DOI (Digital Object Identifier) Link: http://dx.doi.org/10.1007/b13229
Google Scholar: Look up in Google Scholar

Abstract

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.

Item Type: Conference Item
ISBN: 3-540-40828-2, 978-3-540-40828-4
Extra Information: Lecture Notes in Computer Science, Volume 2805/2003 ISBN 978-3-540-40828-4
Academic Unit/Department: Mathematics, Computing and Technology > Computing & Communications
Interdisciplinary Research Centre: Centre for Research in Computing (CRC)
Item ID: 7577
Depositing User: Users 7283 not found.
Date Deposited: 01 May 2007
Last Modified: 02 Dec 2010 19:59
URI: http://oro.open.ac.uk/id/eprint/7577
Share this page:

Actions (login may be required)

View Item
Report issue / request change

Policies | Disclaimer

© The Open University   + 44 (0)870 333 4340   general-enquiries@open.ac.uk