Abstract
This paper sketches a hard real-time programming language featuring operators for expressing timeliness requirements in an abstract, implementation-independent way and presents parts of the design and verification of a provably correct code generator for that language. The notion of implementation correctness used as an implicit specification of the code generator pays attention to timeliness requirements. Hence, formal verification of the code generator design is a guarantee of meeting all deadlines when executing generated code.
This report reflects work that has been partially funded by the Commission of the European Communities under ESPRIT Basic Research Action 7071 “ProCoS II” (Provably Correct Systems II) and by the Deutsche Forschungsgemeinschaft under contract DFG La 426/13-1.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bettina Buth, Karl-Heinz Buth, Martin Fränzle, Burghard v. Karger, Yassine Lakhneche, Hans Langmaack, and Markus Müller-Olm. Provably correct compiler development and implementation. In U. Kastens and P. Pfahler, editors, Compiler Construction, pages 141–155. Springer, 1992. LNCS 641.
Martin Fränzle and Markus Müller-Olm. Drift and Granularity of Time in Real-Time System Implementation. ProCoS II project document [Kiel MF 10/2], Christian-Albrechts-Universität Kiel, Germany, August 1993.
Martin Fränzle and Burghard von Karger. Proposal for a Programming Language Core for ProCoS II. ProCoS II project document [Kiel MF 11/3], Christian-Albrechts-Universität Kiel, Germany, August 1993.
Burghard von Karger. A simple wide-spectrum model for real time systems. ProCoS II project document [OU BvK 9/6], Oxford University Programming Research Group, UK, August 1993.
Markus Müller-Olm. On Translation of TimedPL and Capture of Machine Instruction Timing. ProCoS II project document [Kiel MMO 6/2], Christian-Albrechts-Universität Kiel, Germany, August 1993.
C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall International, 1985.
C.A.R. Hoare. Refinement algebra proves correctness of compiling specifications. In C.C. Morgan and J.C.P. Woodcock, editors, 3rd Refinement Workshop, Workshops in Computing, pages 33–48. Springer-Verlag, 1991.
INMOS ltd. occam 2 Reference Manual. Prentice Hall International, 1988.
INMOS ltd. Transputer Instruction Set — A Compiler Writer's Guide. Prentice Hall International, 1988.
Dines Bjørner, C.A.R. Hoare, Hans Langmaack (Eds.). Provably correct systems. ProCoS I final deliverable, 1993. Available from the Department of Computer Science, Technical University of Denmark, Building 3440, DK-2800 Lyngby.
David Turner. An overview of miranda. SIGPLAN Notices, 1986.
Åke Wikström. Functional Programming Using Standard ML. Series in Computer Science. Prentice-Hall, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fränzle, M., Müller-Olm, M. (1994). Towards provably correct code generation for a hard real-time programming language. In: Fritzson, P.A. (eds) Compiler Construction. CC 1994. Lecture Notes in Computer Science, vol 786. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57877-3_20
Download citation
DOI: https://doi.org/10.1007/3-540-57877-3_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57877-2
Online ISBN: 978-3-540-48371-7
eBook Packages: Springer Book Archive