Synthesizing controllers from duration calculus |
|
| Abstract | Duration Calculus is a logic for reasoning about requirements for real-time systems at a high level of abstraction from operational detail, which qualifies it as an interesting starting point for embedded controller design. Such a design activity is generally thought to aim at a control device the physical behaviours of which satisfy the requirements formula, i.e. the refinement relation between requirements and implementations is taken to be trajectory inclusion. Due to the abstractness of the vocabulary of Duration Calculus, trajectory inclusion between control requirements and controller designs is undecidable even for fully synchronous controllers, rendering automatic verification and automatic synthesis impossible wrt. trajectory inclusion. In this paper, besides reviewing these results, we are giving evidence that trajectory inclusion is in general an overly restrictive refinement relation for embedded controller design and exploit this fact for developing an automatic procedure for controller synthesis from specifications formalized in Duration Calculus. As far as we know, this is the first positive result concerning feasibility of automatic synthesis from dense-time Duration Calculus. |
| Type | Conference paper [With referee] |
| Conference | Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT 96) |
| Editors | Bengt Jonsson and Joachim Parrow |
| Year | 1996 Vol. 1135 pp. 168-187 |
| Publisher | Springer Verlag |
| Series | Lecture Notes in Computer Science |
| Electronic version(s) | [ps] |
| Publication link | http://www.imm.dtu.dk/~mf/ftrtft96.ps.Z |
| BibTeX data | [bibtex] |
| IMM Group(s) | Computer Science & Engineering |