An application of a prototype credible autocoding and verification tool-chain

We present the usage of a prototype that is the result of our research efforts in the translation of control theory into code semantics and the automatic verification of control software using those generated semantics. We demonstrate an application of tool-chain for a jet engine, produced by the lightweight jet engine manufacturer Price Induction, running in closed-loop with its Full Authority Digital Controller (FADEC) hardware. The framework for the tool is based on the model-based development paradigm but with integration of formal methods into the development process to support the claim of correctness of the auto-generated code. The prototype is a two parts tool-chain. The credible autocoding part is designed to translate a Simulink model of a control system into an annotated C program. The annotations, which express control semantics of the system, are generated during the autocoding process and embedded into the C program as comments. The control semantics are formal expressions of the safety and performance requirements of the control system and their proofs. The second part, the verification backend, which in general runs independently of the first part, checks the correctness of the annotations with respect to the code.