Towards provably correct code generation for a hard real-time programming language

3Citations
Citations of this article
4Readers
Mendeley users who have this article in their library.

This article is free to access.

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.

Cite

CITATION STYLE

APA

Fränzle, M., & Müller-Olm, M. (1994). Towards provably correct code generation for a hard real-time programming language. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 786 LNCS, pp. 294–308). Springer Verlag. https://doi.org/10.1007/3-540-57877-3_20

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free