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.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

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


    Weitere Titelangaben:

    Lect. Notes Control


    Beteiligte:
    Feron, Eric (Herausgeber:in) / Wang, Timothy (Autor:in) / Jobredeaux, Romain (Autor:in) / Herencia, Heber (Autor:in) / Garoche, Pierre-Loïc (Autor:in) / Dieumegard, Arnaud (Autor:in) / Feron, Éric (Autor:in) / Pantel, Marc (Autor:in)


    Erscheinungsdatum :

    17.09.2015


    Format / Umfang :

    44 pages





    Medientyp :

    Aufsatz/Kapitel (Buch)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch




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

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


    A credible autocoding application within a rocket and its payload

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

    Freier Zugriff

    Credible autocoding and verification of a gas turbine engine FADEC

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

    Freier Zugriff

    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