Hierarchical State Machines as Modular Horn Clauses
This addresses a specific problem in model-based development for embedded systems, offering an incremental improvement over prior compilation methods.
The paper tackles the problem of safety analysis for embedded systems modeled with hierarchical state machines, where existing compilation approaches lose structural information about modal behavior. The authors present a novel compilation technique that faithfully preserves this structural and modal information in modular Horn clauses, making safety analysis more tractable.
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.