Name
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. |
Year | DOI | Venue |
|---|---|---|
2003 | 10.1007/3-540-36580-X_11 | HSCC |
Keywords | Field | DocType |
phase shift,arbitrary transfer function,single-input single-output continuous-time control,variable frequency,hoare-style logic,continuous-time domain,control system,frequency response,hoare logic,feedback loop,block diagram,mechanised theorem prover,theorem prover,transfer function | Frequency response,Control theory,Hoare logic,Automated theorem proving,Transfer function,Function block diagram,Control system,Predicate logic,Block diagram,Mathematics | Conference |
Volume | ISSN | ISBN |
2623 | 0302-9743 | 3-540-3-540-00913-2 |
Citations | PageRank | References |
14 | 0.92 | 5 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Richard J. Boulton | 1 | 255 | 23.64 |
| Ruth Hardy | 2 | 15 | 1.62 |
| Ursula Martin | 3 | 127 | 16.38 |