Lecture Notes in Computer Science, 2003, Volume 2623/2003, 113-125, DOI: 10.1007/3-540-36580-X_11

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

Richard J. Boulton, Ruth Hardy and Ursula Martin

View Related Documents

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.
Research supported by QinetiQ and by an EPSRC studentship to the second author.
Affiliation with the University of St Andrews ceased in June 2002.

Fulltext Preview

Image of the first page of the fulltext document