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

    27 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 → …

    Cite this

    Fränzle, M., Müller-Olm, M., & Fritzson, P. A. (Ed.) (1994). Towards provably correct code generation for a hard real-time programming language. In Compiler Construction (CC 94) (Vol. 786, pp. 294-308). Springer Verlag.
    Fränzle, Martin ; Müller-Olm, Markus ; Fritzson, Peter A. (Editor). / Towards provably correct code generation for a hard real-time programming language. Compiler Construction (CC 94). Vol. 786 Springer Verlag, 1994. pp. 294-308
    @inproceedings{87dd108fa5904991bfdc163a6bbebfde,
    title = "Towards provably correct code generation for a hard real-time programming language",
    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.",
    author = "Martin Fr{\"a}nzle and Markus M{\"u}ller-Olm and Fritzson, {Peter A.}",
    year = "1994",
    language = "English",
    volume = "786",
    pages = "294--308",
    booktitle = "Compiler Construction (CC 94)",
    publisher = "Springer Verlag",
    address = "Germany",

    }

    Fränzle, M, Müller-Olm, M & Fritzson, PA (ed.) 1994, Towards provably correct code generation for a hard real-time programming language. in Compiler Construction (CC 94). vol. 786, Springer Verlag, pp. 294-308, Proceedings of the 5th International Conference on Compiler Construction, 01/01/1994.

    Towards provably correct code generation for a hard real-time programming language. / Fränzle, Martin; Müller-Olm, Markus; Fritzson, Peter A. (Editor).

    Compiler Construction (CC 94). Vol. 786 Springer Verlag, 1994. p. 294-308.

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

    TY - GEN

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

    AU - Fränzle, Martin

    AU - Müller-Olm, Markus

    A2 - Fritzson, Peter A.

    PY - 1994

    Y1 - 1994

    N2 - 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.

    AB - 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.

    M3 - Article in proceedings

    VL - 786

    SP - 294

    EP - 308

    BT - Compiler Construction (CC 94)

    PB - Springer Verlag

    ER -

    Fränzle M, Müller-Olm M, Fritzson PA, (ed.). Towards provably correct code generation for a hard real-time programming language. In Compiler Construction (CC 94). Vol. 786. Springer Verlag. 1994. p. 294-308