Dieumegard, Arnaud and Toom, Andres and Pantel, Marc
Block Library Driven Translation Validation for Dataflow Models in Safety Critical Systems.
(2016)
In: FMICS - AVoCS 2016 (Joint 21st International Workshop on Formal Methods for Industrial Critical Systems / 16th International Workshop on Automated Verification of Critical Systems), 26 September 2016 - 28 September 2016 (Pisa, Italy).
|
(Document in English)
PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader 382kB |
Official URL: https://doi.org/10.1007/978-3-319-45943-1_8
Abstract
Model driven engineering is widely used in the development of complex and safety critical systems. Systems' designs are specified and validated in domain specific modeling languages and software code is often produced by autocoding. Thus the correctness of the final systems depend on the correctness of those tools. We propose an approach for the formal verification of code generation from dataflow languages, such as SIMULINK, based on translation validation. It relies on the BLOCKLIBRARY DSL for the formal specification and verification of the structure, semantics and variability of the complex block libraries found in these languages. These specifications are then used here for deriving model and block-specific semantic contracts that will be woven into the generated C code. We present two different approaches for performing the block matching and weaving step. Finally, we rely on the FRAMA-C toolset and state-of-the-art SMT solvers for verifying the annotated code.
Item Type: | Conference or Workshop Item (Paper) |
---|---|
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 > 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) Other partners > IB Krates OÜ (ESTONIA) Other partners > IRT Saint Exupéry - Institut de Recherche Technologique (FRANCE) Other partners > Tallinn University of Technology - TTU (ESTONIA) |
Laboratory name: | |
Statistics: | download |
Deposited On: | 14 May 2020 07:09 |
Repository Staff Only: item control page