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

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

doi:10.1109/DASC.2014.6979438

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

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

Electrical and Computer Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

4 Scopus citations

Abstract

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 language	English (US)
Title of host publication	2014 IEEE/AIAA 33rd Digital Avionics Systems Conference, DASC
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	2E41-2E414
ISBN (Electronic)	9781479950010
DOIs	https://doi.org/10.1109/DASC.2014.6979438
State	Published - Dec 8 2014
Event	33rd Digital Avionics Systems Conference, DASC 2014 - Colorado Springs, United States Duration: Oct 5 2014 → Oct 9 2014

Publication series

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

Conference

Conference	33rd Digital Avionics Systems Conference, DASC 2014
Country/Territory	United States
City	Colorado Springs
Period	10/5/14 → 10/9/14

Bibliographical note

Publisher Copyright:
© 2014 IEEE.

ASJC Scopus subject areas

Aerospace Engineering
Electrical and Electronic Engineering

Access to Document

10.1109/DASC.2014.6979438

Cite this

Wang, T., Jobredeaux, R., Pakmehr, M., Vivies, M., & Feron, E. (2014). An application of a prototype credible autocoding and verification tool-chain. In 2014 IEEE/AIAA 33rd Digital Avionics Systems Conference, DASC (pp. 2E41-2E414). Article 6979438 (AIAA/IEEE Digital Avionics Systems Conference - Proceedings). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/DASC.2014.6979438

@inproceedings{6ff65ed8af6944378b829d02e3a5cf09,

title = "An application of a prototype credible autocoding and verification tool-chain",

abstract = "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.",

author = "Timothy Wang and Romain Jobredeaux and Mehrdad Pakmehr and Martin Vivies and Eric Feron",

note = "Publisher Copyright: {\textcopyright} 2014 IEEE.; 33rd Digital Avionics Systems Conference, DASC 2014 ; Conference date: 05-10-2014 Through 09-10-2014",

year = "2014",

month = dec,

day = "8",

doi = "10.1109/DASC.2014.6979438",

language = "English (US)",

series = "AIAA/IEEE Digital Avionics Systems Conference - Proceedings",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "2E41--2E414",

booktitle = "2014 IEEE/AIAA 33rd Digital Avionics Systems Conference, DASC",

address = "United States",

}

Wang, T, Jobredeaux, R, Pakmehr, M, Vivies, M & Feron, E 2014, An application of a prototype credible autocoding and verification tool-chain. in 2014 IEEE/AIAA 33rd Digital Avionics Systems Conference, DASC., 6979438, AIAA/IEEE Digital Avionics Systems Conference - Proceedings, Institute of Electrical and Electronics Engineers Inc., pp. 2E41-2E414, 33rd Digital Avionics Systems Conference, DASC 2014, Colorado Springs, United States, 10/5/14. https://doi.org/10.1109/DASC.2014.6979438

An application of a prototype credible autocoding and verification tool-chain. / Wang, Timothy; Jobredeaux, Romain; Pakmehr, Mehrdad et al.
2014 IEEE/AIAA 33rd Digital Avionics Systems Conference, DASC. Institute of Electrical and Electronics Engineers Inc., 2014. p. 2E41-2E414 6979438 (AIAA/IEEE Digital Avionics Systems Conference - Proceedings).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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

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 -

Wang T, Jobredeaux R, Pakmehr M, Vivies M, Feron E. An application of a prototype credible autocoding and verification tool-chain. In 2014 IEEE/AIAA 33rd Digital Avionics Systems Conference, DASC. Institute of Electrical and Electronics Engineers Inc. 2014. p. 2E41-2E414. 6979438. (AIAA/IEEE Digital Avionics Systems Conference - Proceedings). doi: 10.1109/DASC.2014.6979438

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

Abstract

Publication series

Conference

Bibliographical note

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this