Verified Code Generation for a Visual Modeling Tool

Date

2024-8-23

Author

Çelebi, Ebru

Metadata

Show full item record

This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

Item Usage Stats

86
views

63
downloads

Cite This

This thesis introduces a verified code generator for the IMODE tool, which enables users to model a sequential computation visually and to generate executable code from the model that will be part of a safety critical software system. The generated code must carry out exactly the computation modeled without any side effects and must be compliant to the applicable safety critical software standards. The code generator goes through the following stages: (i) It takes its model input from the IMODE XML save files, (ii) checks the input model for well-formedness, (iii) annotates it with logical expressions that capture the input-output relationships effected by the model elements, (iv) generates code in a subset of C, (v) verifies the generated code using Hoare logic, adopting the pre- and post-conditions derived from the annotated model, and, finally, (vi) outputs the verified code. To ensure the correctness of the code generator itself, the Agda programming language, a functional programming language with dependent types, has been used for implementation. Using the Agda's integrated theorem prover, the code generator is proved adhering to the correct-by-construction approach.

Subject Keywords

Model-Based Design Tool, Verified Code Generator, Correct by Construction, Hoare Logic

URI

https://hdl.handle.net/11511/111011

Collections

Graduate School of Natural and Applied Sciences, Thesis