TY - GEN
T1 - An application of a prototype credible autocoding and verification tool-chain
AU - Wang, Timothy
AU - Jobredeaux, Romain
AU - Pakmehr, Mehrdad
AU - Vivies, Martin
AU - Feron, Eric
N1 - Publisher Copyright:
© 2014 IEEE.
PY - 2014/12/8
Y1 - 2014/12/8
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84919824979&partnerID=8YFLogxK
U2 - 10.1109/DASC.2014.6979438
DO - 10.1109/DASC.2014.6979438
M3 - Conference contribution
AN - SCOPUS:84919824979
T3 - AIAA/IEEE Digital Avionics Systems Conference - Proceedings
SP - 2E41-2E414
BT - 2014 IEEE/AIAA 33rd Digital Avionics Systems Conference, DASC
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 33rd Digital Avionics Systems Conference, DASC 2014
Y2 - 5 October 2014 through 9 October 2014
ER -