Synthesizing controllers from duration calculus

Martin Fränzle, Bengt Jonsson (Editor), Joachim Parrow (Editor)

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    32 Downloads (Pure)


    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.
    Original languageEnglish
    Title of host publicationFormal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT 96)
    PublisherSpringer Verlag
    Publication date1996
    ISBN (Print)3-540-61648-9
    Publication statusPublished - 1996
    EventProceedings of the 4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems -
    Duration: 1 Jan 1996 → …


    ConferenceProceedings of the 4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems
    Period01/01/1996 → …


    Dive into the research topics of 'Synthesizing controllers from duration calculus'. Together they form a unique fingerprint.

    Cite this