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

RJ Boulton, R Hardy, Ursula Hilda Mary Martin, O Maler (Editor), A Pnueli (Editor)

Research output: Other contribution

16 Citations (Scopus)

Abstract

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
PublisherSpringer-Verlag
ISBN (Print)0302-9743
Publication statusPublished - 2003

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