A compositional approach to the design of hybrid systems

J.J.M. Hooman

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

Abstract

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.
Original languageEnglish
Title of host publicationHybrid systems
EditorsR.L. Grossman, A. Nerode, A.P. Ravn, H. Rischel
Place of PublicationBerlin
PublisherSpringer
Pages121-148
ISBN (Print)3-540-57318-6
DOIs
Publication statusPublished - 1993

Publication series

NameLecture Notes in Computer Science
Volume736
ISSN (Print)0302-9743

Fingerprint Dive into the research topics of 'A compositional approach to the design of hybrid systems'. Together they form a unique fingerprint.

Cite this