OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Automated analysis of Stateflow models

Bourbouh, Hamza and Garoche, Pierre-Loïc and Garion, Christophe and Gurfinkel, Arie and Kahsai, Temesghen and Thirioux, Xavier Automated analysis of Stateflow models. (2017) In: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2017), 7 May 2017 - 12 May 2017 (Maun, Botswana).

(Document in English)

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

Official URL: https://doi.org/10.29007/b8gq


Stateflow is a widely used modeling framework for embedded and cyberphysical systems where control software interacts with physical processes. In this work, we present a framework and a fully automated safety verification technique for Stateflow models. Our approach is two-folded: (i) we faithfully compile Stateflow models into hierarchical state machines, and (ii) we use automated logic-based verification engine to decide the validity of safety properties. The starting point of our approach is a denotational semantics of Stateflow. We propose a compilation process using continuation-passing style (CPS) denotational semantics. Our compilation technique preserves the structural and modal behavior of the system. The overall approach is implemented as an open source toolbox that can be integrated into the existing Mathworks Simulink/Stateflow modeling framework. We present preliminary experimental evaluations that illustrate the effectiveness of our approach in code generation and safety verification of industrial scale Stateflow models.

Item Type:Conference or Workshop Item (Paper)
Additional Information:This papers appears in EPiC Series in Computing Volume 46 ISSN: 2398-7340. The original PDF is available at: https://easychair.org/publications/paper/fPz
HAL Id:hal-02092930
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 - Toulouse INP (FRANCE)
Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE-SUPAERO (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 - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Other partners > University of Waterloo (CANADA)
Laboratory name:
ANR Agence nationale de la recherche - CNES Centre national d'études spatiales - NASA National Aeronautics and Space Administration
Deposited On:03 Apr 2019 12:56

Repository Staff Only: item control page