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.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

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


    Contributors:


    Publication date :

    2014-10-01


    Size :

    2042458 byte




    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    Credible autocoding and verification of a gas turbine engine FADEC

    Wang, Timothy / Jobredeaux, Romain / Pakmher, Mehrdad et al. | IEEE | 2014

    Free access

    A credible autocoding application within a rocket and its payload

    Cohen, Raphael / Jobredeaux, Romain / Feron, Eric | IEEE | 2015

    Free access

    From Design to Implementation: An Automated, Credible Autocoding Chain for Control Systems

    Wang, Timothy / Jobredeaux, Romain / Herencia, Heber et al. | Springer Verlag | 2015


    A credible autocoding application within a rocket and its payload

    Cohen, Raphael / Bui Long, Anh-Toan / Jobredeaux, Romain et al. | IEEE | 2015


    Autocoding in Automotive Software Development

    Furst, S. / Institution of Electrical Engineers / IEE Microelectronics and Embedded Systems Professional Network et al. | British Library Conference Proceedings | 2005