A Hoare Logic for Single-Input Single-Output Continuous-Time Control Systems

Richard J. Boulton, Ruth Hardy, Ursula Martin

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

This paper presents a Hoare-style logic for reasoning about the frequency response of control systems in the continuous-time domain. Two properties, the gain (amplitude) and phase shift, of a control system are considered. These properties are for a sinusoidal input of variable frequency. The logic operates over a simplified form of block diagram, including arbitrary transfer functions, feedback loops, and summation of signals. Reasoning is compositional, i.e. properties of a system can be deduced from properties of its subsystems. A prototype tool has been implemented in a mechanised theorem prover.
Original languageEnglish
Title of host publicationHybrid Systems: Computation and Control
Subtitle of host publication6th International Workshop, HSCC 2003 Prague, Czech Republic, April 3–5, 2003 Proceedings
Number of pages13
ISBN (Electronic)978-3-540-36580-8
Publication statusPublished - 2003
Event6th HSCC International Workshop: Hybrid Systems: Computation and Control - Prague, Czech Republic
Duration: 3 Apr 20035 Apr 2003

Publication series

NameLecture Notes in Computer Science


Workshop6th HSCC International Workshop
Abbreviated titleHSCC '03
Country/TerritoryCzech Republic
Internet address


Dive into the research topics of 'A Hoare Logic for Single-Input Single-Output Continuous-Time Control Systems'. Together they form a unique fingerprint.

Cite this