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

Richard J. Boulton; Ruth Hardy; Ursula Martin

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
, Ursula Martin

School of Informatics

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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 language	English
Title of host publication	Hybrid Systems: Computation and Control
Subtitle of host publication	6th International Workshop, HSCC 2003 Prague, Czech Republic, April 3–5, 2003 Proceedings
Pages	113-125
Number of pages	13
ISBN (Electronic)	978-3-540-36580-8
DOIs	https://doi.org/10.1007/3-540-36580-X_11
Publication status	Published - 2003
Event	6th HSCC International Workshop: Hybrid Systems: Computation and Control - Prague, Czech Republic Duration: 3 Apr 2003 → 5 Apr 2003 http://www-hscc03.imag.fr/

Publication series

Name	Lecture Notes in Computer Science
Volume	2623

Workshop

Workshop	6th HSCC International Workshop
Abbreviated title	HSCC '03
Country/Territory	Czech Republic
City	Prague
Period	3/04/03 → 5/04/03
Internet address	http://www-hscc03.imag.fr/

Access to Document

10.1007/3-540-36580-X_11

https://link.springer.com/chapter/10.1007%2F3-540-36580-X_11?LI=true

Cite this

@inproceedings{b52c63bba908464ea6f53598ab03a012,

title = "A Hoare Logic for Single-Input Single-Output Continuous-Time Control Systems",

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.",

author = "Boulton, \{Richard J.\} and Ruth Hardy and Ursula Martin",

year = "2003",

doi = "10.1007/3-540-36580-X\_11",

language = "English",

isbn = "978-3-540-00913-9",

series = "Lecture Notes in Computer Science",

pages = "113--125",

booktitle = "Hybrid Systems: Computation and Control",

note = "6th HSCC International Workshop : Hybrid Systems: Computation and Control, HSCC '03 ; Conference date: 03-04-2003 Through 05-04-2003",

url = "http://www-hscc03.imag.fr/",

}

Boulton, RJ, Hardy, R & Martin, U 2003, A Hoare Logic for Single-Input Single-Output Continuous-Time Control Systems. in Hybrid Systems: Computation and Control: 6th International Workshop, HSCC 2003 Prague, Czech Republic, April 3–5, 2003 Proceedings. Lecture Notes in Computer Science, vol. 2623, pp. 113-125, 6th HSCC International Workshop, Prague, Czech Republic, 3/04/03. https://doi.org/10.1007/3-540-36580-X_11

A Hoare Logic for Single-Input Single-Output Continuous-Time Control Systems. / Boulton, Richard J.; Hardy, Ruth; Martin, Ursula.
Hybrid Systems: Computation and Control: 6th International Workshop, HSCC 2003 Prague, Czech Republic, April 3–5, 2003 Proceedings. 2003. p. 113-125 (Lecture Notes in Computer Science; Vol. 2623).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

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

AU - Boulton, Richard J.

AU - Hardy, Ruth

AU - Martin, Ursula

PY - 2003

Y1 - 2003

N2 - 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.

AB - 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.

U2 - 10.1007/3-540-36580-X_11

DO - 10.1007/3-540-36580-X_11

M3 - Conference contribution

SN - 978-3-540-00913-9

T3 - Lecture Notes in Computer Science

SP - 113

EP - 125

BT - Hybrid Systems: Computation and Control

T2 - 6th HSCC International Workshop

Y2 - 3 April 2003 through 5 April 2003

ER -

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

Abstract

Publication series

Workshop

Access to Document

Fingerprint

Cite this