OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Hierarchical State Machines as Modular Horn Clauses

Garoche, Pierre-Loïc and Kahsai, Temesghen and Thirioux, Xavier Hierarchical State Machines as Modular Horn Clauses. (2016) In: 3rd Workshop on Horn Clauses for Verification and Synthesis (HCVS 2016), 3 April 2016 (Eindhoven, Netherlands).

(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.4204/EPTCS.219.2


In model based development, embedded systems are modeled using a mix of dataflow formalism, that capture the flow of computation, and hierarchical state machines, that capture the modal beahviour of the system. For safety analysis, existing approaches rely on a compilation scheme that transform the original model (dataflow and state machines) into a pure dataflow formalism. Such compilation often result in loss of important structural information that capture the modal behaviour of the system. In previous work we have developed a compilation technique from a dataflow formalism into modular Horn clauses. In this paper, we present a novel technique that faithfully compile hierarchical state machines into modular Horn clauses. Our compilation technique preserves the structural and modal behavior of the system, making the safety analysis of such models more tractable.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to EPTCS: Electronic Proceedings in Theoretical Computer Science ISSN: 2075-2180 http://published.eptcs.org/
HAL Id:hal-02092915
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)
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)
Laboratory name:
Deposited On:04 Apr 2019 13:18

Repository Staff Only: item control page