Hierarchical State Machines as Modular Horn Clauses
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 behavior of the system. For safety analysis, existing approaches rely on a compilation scheme that transform the o...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2016-07-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1607.04457v1 |
| _version_ | 1818682966388244480 |
|---|---|
| author | Pierre-Loïc Garoche Temesghen Kahsai Xavier Thirioux |
| author_facet | Pierre-Loïc Garoche Temesghen Kahsai Xavier Thirioux |
| author_sort | Pierre-Loïc Garoche |
| collection | DOAJ |
| description | 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 behavior 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. |
| first_indexed | 2024-12-17T10:27:14Z |
| format | Article |
| id | doaj.art-e2e686540154408f8cee217a9ef1cc0c |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-17T10:27:14Z |
| publishDate | 2016-07-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-e2e686540154408f8cee217a9ef1cc0c2022-12-21T21:52:37ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802016-07-01219Proc. HCVS2016152810.4204/EPTCS.219.2:1Hierarchical State Machines as Modular Horn ClausesPierre-Loïc Garoche0Temesghen Kahsai1Xavier Thirioux2 DTIM, UFT, Onera - The French Aerospace Lab Nasa Ames / CMU IRIT/ENSEEIHT, UFT, CNRS 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 behavior 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.http://arxiv.org/pdf/1607.04457v1 |
| spellingShingle | Pierre-Loïc Garoche Temesghen Kahsai Xavier Thirioux Hierarchical State Machines as Modular Horn Clauses Electronic Proceedings in Theoretical Computer Science |
| title | Hierarchical State Machines as Modular Horn Clauses |
| title_full | Hierarchical State Machines as Modular Horn Clauses |
| title_fullStr | Hierarchical State Machines as Modular Horn Clauses |
| title_full_unstemmed | Hierarchical State Machines as Modular Horn Clauses |
| title_short | Hierarchical State Machines as Modular Horn Clauses |
| title_sort | hierarchical state machines as modular horn clauses |
| url | http://arxiv.org/pdf/1607.04457v1 |
| work_keys_str_mv | AT pierreloicgaroche hierarchicalstatemachinesasmodularhornclauses AT temesghenkahsai hierarchicalstatemachinesasmodularhornclauses AT xavierthirioux hierarchicalstatemachinesasmodularhornclauses |