OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Compilation of synchronous observers as code contracts

Dieumegard, Arnaud and Garoche, Pierre-Loïc and Kahsai, Temesghen and Taillar, Alice and Thirioux, Xavier Compilation of synchronous observers as code contracts. (2015) In: 30th Annual ACM Symposium on Applied Computing (SAC 2015), 13 April 2015 - 17 April 2015 (Salamanca, Spain).

[img] (Document in English)

PDF (Author's version) - Depositor and staff only - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
361kB

Official URL: https://doi.org/10.1145/2695664.2695819

Abstract

Synchronous languages have long been the standard formalism for modeling and implementing embedded control software in critical domains like avionics, automotive or railway system development. Those languages are equipped with qualified compilers that generate the target final embedded code. An extensively used technique to define the expected behavior is the use of synchronous observers. Those observers are typically used for simulation and testing purposes. However, the information contained in those observers is lost during the compilation process. This makes the verification of expected behavior at code level difficult, since it requires the re-specification of the observer. In this paper, we propose an integrated process in which functional properties expressed at the model level through synchronous observers are compiled as code-level contracts. We also show how these specifications, both at model level and code level could be analyzed via SMT-based model checking, static analysis and runtime verification. We have implemented these techniques in a tool chain targeting embedded systems modeled in Simulink.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to ACM. The definitive version is available at http://dl.acm.org This papers appears in Proceedings of the 30th Annual ACM Symposium on Applied Computing ISBN: 978-1-4503-3196-8. The original PDF is available at: https://dl.acm.org/citation.cfm?id=2695819
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Other partners > Carnegie Mellon University - CMU (USA)
Université de Toulouse > Institut National Polytechnique de Toulouse - INPT (FRANCE)
Other partners > National Aeronautics and Space Administration - NASA (USA)
French research institutions > Office National d'Etudes et Recherches Aérospatiales - ONERA (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UPS (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
Statistics:download
Deposited By: IRIT IRIT
Deposited On:04 Apr 2019 14:54

Repository Staff Only: item control page