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: | Pierre-Loïc Garoche, Temesghen Kahsai, Xavier Thirioux |
---|---|
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 |
Similar Items
-
Synthesizing Modular Invariants for Synchronous Code
by: Pierre-Loic Garoche, et al.
Published: (2014-12-01) -
Solving non-linear Horn clauses using a linear Horn clause solver
by: Bishoksan Kafle, et al.
Published: (2016-07-01) -
PKind: A parallel k-induction based model checker
by: Temesghen Kahsai, et al.
Published: (2011-10-01) -
Horn Clauses for Communicating Timed Systems
by: Hossein Hojjat, et al.
Published: (2014-12-01) -
Higher-order constrained horn clauses for verification
by: Cathcart Burn, T, et al.
Published: (2017)