Abstract | ||
---|---|---|
Hybrid systems are used to model embedded computing systems interacting with their physical environment. There is a conceptual mismatch between high-level hybrid system languages like Simulink, which are used for simulation, and hybrid automata, the most suitable representation for safety verification. Indeed, in simulation languages the interaction between discrete and continuous execution steps is specified using the concept of zero-crossings, whereas hybrid automata exploit the notion of staying conditions. We describe a translation from a hybrid data-flow language to logico-numerical hybrid automata that points out this issue carefully. We expose various zero-crossing semantics, propose a sound translation, and discuss to which extent the original semantics is preserved. |
Year | DOI | Venue |
---|---|---|
2012 | 10.1145/2185632.2185658 | HSCC |
Keywords | Field | DocType |
hybrid system,high-level hybrid system language,hybrid data-flow language,complete translation,various zero-crossing semantics,sound translation,continuous execution step,conceptual mismatch,simulation language,original semantics,hybrid automaton,verification,hybrid systems,data flow,embedded computing,static analysis | Automata theory,Computer science,Automaton,Flow (psychology),Static analysis,Theoretical computer science,Exploit,Hybrid data,Hybrid system,Semantics | Conference |
Citations | PageRank | References |
8 | 0.50 | 20 |
Authors | ||
2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Peter Schrammel | 1 | 134 | 19.10 |
Bertrand Jeannet | 2 | 641 | 29.06 |