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 behaviour 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.