|
Back to list of 2002/03 seminars Abstract for Seminar
There are well documented methods for developing programs from their specifications; a formal method identifies proof obligations at each step of development; if all such proof obligations are discharged, there is a precise notion of errors which cannot be present in the final program. For a class of " closed " systems such methods offer a gold standard against which one can measure less formal approaches. For the interesting class of systems which interact --via sensors and actuators-- with the physical world, the issue of how to obtain a starting specification can be as challenging as how to derive a program from that specification. Being confident that the specification is appropriate is yet more challenging for systems which should tolerate (certain classes of)errors in, say, the sensors. This paper argues that widening the notion of system to specify first the behaviour of the physical system provides a route to deriving the specification of a control system and recording precisely assumptions made about physical components.
|