Access Restriction

Author Garoche, Pierre-Loïc ♦ Kahsai, Temesghen ♦ Thirioux, Xavier
Source Hyper Articles en Ligne (HAL)
Content type Text
File Format PDF
Language English
Subject Keyword Compilation technique ♦ info ♦ Computer Science [cs]/Hardware Architecture [cs.AR] ♦ Computer Science [cs]/Cryptography and Security [cs.CR] ♦ Computer Science [cs]/Embedded Systems ♦ Computer Science [cs]/Human-Computer Interaction [cs.HC] ♦ Computer Science [cs]/Logic in Computer Science [cs.LO] ♦ Computer Science [cs]/Modeling and Simulation ♦ Computer Science [cs]/Programming Languages [cs.PL] ♦ Computer Science [cs]/Software Engineering [cs.SE]
Abstract 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.
Educational Use Research
Learning Resource Type Proceeding
Publisher Date 2016-01-01
Volume Number 219
Page Count 14
Starting Page 15
Ending Page 28