OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Preserving Functional Correctness of Cyber-Physical System Controllers: From Model to Code

Davy, Guillaume and Garion, Christophe and Garoche, Pierre-Loic and Roux, Pierre and Thirioux, Xavier Preserving Functional Correctness of Cyber-Physical System Controllers: From Model to Code. (2018) In: Forum on Specification & Design Languages (FDL 2018), 10 September 2018 - 12 September 2018 (Munich, Germany).

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: http://doi.org/10.1109/FDL.2018.8524044


In this paper, we outline a methodology allowing to support the formal verification of functional properties for generated code. When relying on a code generator, a model is directly mapped into the target embedded code in C for instance. At model level, a specification can be associated to the model and used to assess the validity of the model with respect to its requirements. At code level, other means can be used to ensure similar goals. We present here a framework which builds a semantics layer connecting model specification to code specification, as well as associated proof evidences. This approach has been designed and developed in the context of dataflow languages such as Simulink, SCADE or Lustre, typically used in the design of cyber-physical system controllers, but it could also be revisited in other contexts. The model is analyzed by SMT-based model checking and convex optimization-based static analysis. At code level, deductive techniques, such as implemented in Frama-C, are used to prove the functional correctness. Our approach combines static analysis with refinement to drive the proof at code level, relying on analysis results obtained at model level.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to the IEEE (Institute of Electrical and Electronics Engineers). This paper is available at : https://ieeexplore.ieee.org/document/8524044 “© 2018 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE-SUPAERO (FRANCE)
French research institutions > Office National d'Etudes et Recherches Aérospatiales - ONERA (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
Deposited On:25 Jan 2019 14:59

Repository Staff Only: item control page