Abstract
Abstract
This thesis provides a verified code generator for IMODE tool, where a logical model-based design can be made, using correct by construction and Hoare logic methods. IMODE tool is developed to generate code from model-based designs for safety critical software systems that must be compliant to the DO-178 and similar standards. Generated code should not contain any errors or side effects, should completely represent the design that user made in the tool. This code generation process also needs to be certified by another standard named DO-330. Verification processes contain a high number of test cases, intense test runs for each change in the code. Code generator takes inputs from IMODE XML save files, checks them if there is no problem that prevents generating code, such as missing connections, type inconsistencies or cycles in the model, which is essentially a directed graph, then outputs the result either as an error message or the generated code. To lessen the load of verification process, Agda programming language has been used for the code generator. Thanks to Agda dependent type theory and safety options, code generator is proved of its partial correctness. Using Hoare logic, it is proved that the annotation of an IMODE model is a logical expression that captures the relationship between the inputs and outputs of the model are the same as the generated code.