Synthesizing controllers from duration calculus



AbstractDuration 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.
TypeConference paper [With referee]
ConferenceFormal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT 96)
EditorsBengt Jonsson and Joachim Parrow
Year1996    Vol. 1135    pp. 168-187
PublisherSpringer Verlag
SeriesLecture Notes in Computer Science
Electronic version(s)[ps]
Publication linkhttp://www.imm.dtu.dk/~mf/ftrtft96.ps.Z
BibTeX data [bibtex]
IMM Group(s)Computer Science & Engineering