In a context of heightened safety requirements for safety-critical embedded systems and ever-increasing costs of verification and validation, we describe a fully automated, credible autocoding chain for control systems. This chain generates code, along with guarantees of high level functional properties, which cans be independently verified. The platform relies on domain specific knowledge and formal analysis methods to bridge the semantic gap between domain experts and code verification experts. First, a graphical dataflow language is extended with annotation symbols, enabling the control engineer to express high level properties of its control law within the framework of a familiar block-diagram language. A public-domain autocoder is enhanced not only to generate the code implementing the initial design, but also to carry high level properties down to annotations at the level of the code. Finally, using customized code analysis tools, certificates are generated, which guarantee the correctness of the annotations with respect to the code, and can be verified using existing static analysis tools. For now, we limit the conclusions to the bounded-input bounded-output characteristic of linear controllers, however the approach appears readily extendable to a broader array of properties and systems.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

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


    Additional title:

    Lect. Notes Control


    Contributors:


    Publication date :

    2015-09-17


    Size :

    44 pages





    Type of media :

    Article/Chapter (Book)


    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

    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


    Autocoding sicherheitsrelevanter Software in der Luftfahrt

    Reiners, Dieter | TIBKAT | 1999

    Free access