From Hybrid Data-Flow Languages to Hybrid Automata: A Complete Translation

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 lan- guages 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.
Document type :
Conference papers
Thao Dang and Ian Mitchell. Hybrid Systems: Computation and Control, Apr 2012, Beijing, China. ACM, pp.167-176, 2012, HSCC '12 Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control. <10.1145/2185632.2185658>


https://hal.inria.fr/hal-00749891
Contributor : Peter Schrammel <>
Submitted on : Thursday, November 8, 2012 - 3:31:07 PM
Last modification on : Friday, November 16, 2012 - 3:39:18 PM

Files

paper.pdf
fileSource_public_author

Identifiers

Collections

INRIA | LIG | UGA

Citation

Peter Schrammel, Bertrand Jeannet. From Hybrid Data-Flow Languages to Hybrid Automata: A Complete Translation. Thao Dang and Ian Mitchell. Hybrid Systems: Computation and Control, Apr 2012, Beijing, China. ACM, pp.167-176, 2012, HSCC '12 Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control. <10.1145/2185632.2185658>. <hal-00749891>

Export

Share

Metrics

Consultation de
la notice

72

Téléchargement du document

118