Abstract
Duration Calculus, as introduced in [ZHR91], 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.
This report reflects work that has been partially funded by the Deutsche Forschungsgemeinschaft under contract DFG La 426/13-2.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
J. R. Büchi and L. H. Landweber. Solving sequential conditions by finite-state strategies. Trans. Amer. Math. Soc., 138:295–311, 1969.
Ahmed Bouajjani, Yassine Lakhnech, and Riadh Robbana. From duration calculus to linear hybrid automata. In Pierre Wolper, editor, Computer Aided Verification (CAV '95), volume 939 of Lecture Notes in Computer Science. Springer-Verlag, 1995.
Martin Fränzle. A discrete model of VLSI dynamics in hybrid control applications. ProCoS Technical Report Kiel MF 17/3, Christian-Albrechts Universität Kiel, Germany, April 1995.
Martin Fränzle. Controller Design from Temporal Logic: Undecidability need not matter. Dissertation, Institut für Informatik und Prakt. Mathematik der Christian-Albrechts-Universität Kiel, Germany, to appear 1996.
Michael R. Hansen. Model-checking discrete duration calculus. Formal Aspects of Computing, 6(6A):826–845, 1994.
Jifeng He, C. A. R. Hoare, Martin Fränzle, Markus Müller-Olm, Ernst-Rüdiger Olderog, Michael Schenke, Michael R. Hansen, Anders P. Ravn, and Hans Rischel. Provably correct systems. In Langmaack et al. [LdRV94], pages 288–335.
Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya. What's decidable about hybrid automata. In Proceedings of the Twenty-Seventh Annual ACM Symposium on the Theory of Computing, pages 373–382. ACM, 1995.
Michael R. Hansen and Ernst-Rüdiger Olderog. Constructing circuits from decidable duration calculus. Unpublished Note, Fachbereich Informatik, Universität Oldenburg, Germany, June 1993.
H. Langmaack, W.-P. de Roever, and J. Vytopil, editors. Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT '94), volume 863 of Lecture Notes in Computer Science. Springer-Verlag, 1994.
Ben Moszkowski. A temporal logic for multi-level reasoning about hardware. IEEE Computer, 18(2):10–19, 1985.
Anders P. Ravn, Hans Rischel, and Kirsten M. Hansen. Specifying and verifying requirements of real-time systems. IEEE Transactions on Software Engineering, 19(1):41–55, January 1993.
Claude E. Shannon. The mathematical theory of communication. In The Mathematical Theory of Communication, pages 3–91. The University of Illinois Press: Urbana, 1949.
Jens Ulrik Skakkebæk and Peter Sestoft. Checking validity of duration calculus formulas. ProCoS Technical Report ID/DTH JUS 3/1, Technical University of Denmark, March 1994.
Wolfgang Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 4, pages 133–191. North-Holland, 1990.
Thomas Wilke. Specifying timed state sequences in powerful decidable logics and timed automata. In Langmaack et al. [LdRV94], pages 694–715.
Zhou Chaochen, C. A. R. Hoare, and Anders P. Ravn. A calculus of durations. Information Processing Letters, 40(5):269–276, 1991.
Zhou Chaochen, Michael R. Hansen, and Peter Sestoft. Decidability and undecidability results for duration calculus. In P. Enjalbert, A. Finkel, and K. W. Wagner, editors, Symposium on Theoretical Aspects of Computer Science (STACS 93), volume 665 of Lecture Notes in Computer Science, pages 58–68. Springer-Verlag, 1993.
Zhou Chaochen, Zhang Jingzhong, Yang Lu, and Li Xiaoshan. Linear duration invariants. In Langmaack et al. [LdRV94], pages 86–109.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fränzle, M. (1996). Synthesizing controllers from Duration Calculus. In: Jonsson, B., Parrow, J. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 1996. Lecture Notes in Computer Science, vol 1135. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61648-9_40
Download citation
DOI: https://doi.org/10.1007/3-540-61648-9_40
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61648-1
Online ISBN: 978-3-540-70653-3
eBook Packages: Springer Book Archive