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


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
CountryCzech Republic
Internet address

Fingerprint 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