To specify and verify distributed real-time systems, classical Hoare triples are extended with timing primitives and the interpretation is modified to be able to specify non-terminating computations. For these modified triples a compositional proof system has been formulated. Compositionality supports top-down program derivation, and by using a dense time domain also hybrid systems with continuous components can be designed. This is illustrated by a process control example of a water level monitoring system. First we prove the correctness of a control strategy in terms of a continuous interface. Next, to obtain a discrete interface, a sensor and an actuator are introduced. Using their specifications only, a suitable specification of the control unit is derived. This reduces the design of the system to the conventional problem of deriving a program according to its specification. Finally the control unit is extended, in a modular way, with error detection features.
|Redacteuren||R.L. Grossman, A. Nerode, A.P. Ravn, H. Rischel|
|Plaats van productie||Berlin|
|ISBN van geprinte versie||3-540-57318-6|
|Status||Gepubliceerd - 1993|
|Naam||Lecture Notes in Computer Science|
|ISSN van geprinte versie||0302-9743|