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

Martin Fränzle, Markus Müller-Olm, Peter A. Fritzson (Editor)

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

    33 Downloads (Pure)

    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.
    Original languageEnglish
    Title of host publicationCompiler Construction (CC 94)
    Volume786
    PublisherSpringer Verlag
    Publication date1994
    Pages294-308
    Publication statusPublished - 1994
    EventProceedings of the 5th International Conference on Compiler Construction -
    Duration: 1 Jan 1994 → …

    Conference

    ConferenceProceedings of the 5th International Conference on Compiler Construction
    Period01/01/1994 → …

    Fingerprint Dive into the research topics of 'Towards provably correct code generation for a hard real-time programming language'. Together they form a unique fingerprint.

    Cite this