A compositional approach to the design of hybrid systems

J.J.M. Hooman

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureHoofdstukAcademicpeer review


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.
Originele taal-2Engels
TitelHybrid systems
RedacteurenR.L. Grossman, A. Nerode, A.P. Ravn, H. Rischel
Plaats van productieBerlin
ISBN van geprinte versie3-540-57318-6
StatusGepubliceerd - 1993

Publicatie series

NaamLecture Notes in Computer Science
ISSN van geprinte versie0302-9743

Vingerafdruk Duik in de onderzoeksthema's van 'A compositional approach to the design of hybrid systems'. Samen vormen ze een unieke vingerafdruk.

Citeer dit