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

Timothy Wang, Romain Jobredeaux, Mehrdad Pakmehr, Martin Vivies, Eric Feron

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

4 Scopus citations


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.

Original languageEnglish (US)
Title of host publication2014 IEEE/AIAA 33rd Digital Avionics Systems Conference, DASC
PublisherInstitute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)9781479950010
StatePublished - Dec 8 2014
Event33rd Digital Avionics Systems Conference, DASC 2014 - Colorado Springs, United States
Duration: Oct 5 2014Oct 9 2014

Publication series

NameAIAA/IEEE Digital Avionics Systems Conference - Proceedings
ISSN (Print)2155-7195
ISSN (Electronic)2155-7209


Conference33rd Digital Avionics Systems Conference, DASC 2014
Country/TerritoryUnited States
CityColorado Springs

Bibliographical note

Publisher Copyright:
© 2014 IEEE.

ASJC Scopus subject areas

  • Aerospace Engineering
  • Electrical and Electronic Engineering


Dive into the research topics of 'An application of a prototype credible autocoding and verification tool-chain'. Together they form a unique fingerprint.

Cite this