An Operational Semantics for Hybrid Systems Involving Behavioral Abstraction

Simon Bliudze
École Polytechnique Fådårale de Lausanne, Lausanne, Switzerland

Sébastien Furic
LMS Imagine S.A., Roanne, France

Ladda ner artikelhttp://dx.doi.org/10.3384/ecp14096693

Ingår i: Proceedings of the 10th International Modelica Conference; March 10-12; 2014; Lund; Sweden

Linköping Electronic Conference Proceedings 96:73, s. 693-706

Visa mer +

Publicerad: 2014-03-10

ISBN: 978-91-7519-380-9

ISSN: 1650-3686 (tryckt), 1650-3740 (online)


We discuss the challenges of building a simulation framework for hybrid systems; in particular the well-known Zeno effect and correct composition of models idealised by abstracting irrelevant behavioural details (e.g. the bounce dynamics of a bouncing ball or the process of fuse melting in an electrical circuit). We argue that the cornerstone of addressing these challenges is the definition of a semantic framework with an appropriate underlying model of time. Using two simple examples; we illustrate the properties of such a model and explain why existing models are not sufficient. Finally; we propose a new Zeno-free semantic model that allows mixing discrete and continuous behaviour in a rigorous way and provides for the compositional behavioural abstraction. Although it is based on non-standard analysis; we explain how our semantic model can be used to develop hybrid system simulators.


Hybrid Modeling Languages; Non-Standard Analysis; Models of Signals; Behavioral Abstraction; Operational Semantics


[1] Albert Benveniste, Timothy Bourke, Benoit Caillaud, and Marc Pouzet. Non-standard semantics of hybrid systems modelers. Journal of Computer and System Sciences, 78:877–910, May 2012. doi: 10.1016/j.jcss.2011.08.009.

[2] Simon Bliudze and Daniel Krob. Modelling of complex systems: Systems as dataflow machines. Fundamenta Informaticae, 91:1–24, 2009. doi: 10.3233/FI-009-0001.

[3] Timothy Bourke and Marc Pouzet. Zélus: A synchronous language with ODEs. In 16th International Conference on Hybrid Systems: Computation and Control (HSCC’13), pages 113–118, Philadelphia, USA, March 2013.

[4] Stephen L Campbell, Jean-Philippe Chancelier, and Ramine Nikoukhah. Modeling and Simulation in Scilab/Scicos with ScicosLab 4.4. Springer, 2010. ISBN 978-1-4419-5527-2.

[5] François E. Cellier, Ernesto Kofman, Gustavo Migoni, and Mario Bortolotto. Quantized state system simulation. Proceedings of Grand Challenges in Modeling and Simulation (GCMS’08), pages 504–510, 2008.

[6] J. Eker, J. W. Janneck, E. A. Lee, J. Liu, X. Liu, J. Ludvig, S. Neuendorffer, S. Sachs, and Y. Xiong. Taming heterogeneity: The Ptolemy approach. Proceedings of the IEEE, 91(1):127–144, 2003.

[7] Goran Frehse, Colas Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler. SpaceEx: Scalable verification of hybrid systems. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification, volume 6806 of Lecture Notes in Computer Science, pages 379–395. Springer Berlin Heidelberg, 2011. doi: 10.1007/ 978-3-642-22110-1_30.

[8] Peter Fritzson. Introduction to modeling and simulation of technical and physical systems with Modelica. Wiley-IEEE Press, 2011. ISBN 978-1-118-01068-6.

[9] Sébastien Furic. Enforcing model composability in Modelica. In Proceedings of the 7th International Modelica Conference, Como, Italy, pages 868–879, 2009.

[10] Boris Golden, Marc Aiguier, and Daniel Krob. Modeling of complex systems II: A minimalist and unified semantics for heterogeneous integrated systems. Applied Mathematics and Computation, 218(16):8039–8055, 2012.

[11] Thomas A. Henzinger. The theory of hybrid automata. In Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, LICS’96, pages 278–292. IEEE Society Press, 1996.

[12] H. Jerome Keisler. Foundations of Infinitesimal Calculus. On-line Edition, 2007. URL http://www.math.wisc.edu/~keisler/foundations.html.

[13] Michal Kone?cný,Walid Taha, Jan Duracz, Adam Duracz, and Aaron Ames. Enclosing the behavior of a hybrid system up to and beyond a Zeno point. In Cyber-Physical Systems, Networks, and Applications (CPSNA), 2013 IEEE 1st International Conference on, pages 120–125, 2013. doi: 10.1109/CPSNA.2013.6614258.

[14] Edward A. Lee and Haiyang Zheng. Operational semantics of hybrid systems. In Manfred Morari and Lothar Thiele, editors, Hybrid Systems: Computation and Control, volume 3414 of Lecture Notes in Computer Science, pages 25–53. Springer Berlin Heidelberg, 2005. ISBN 978-3-540-25108-8. doi: 10.1007/978-3-540-31954-2_2.

[15] Abraham Robinson. Non Standard Analysis. North Holland, 1966.

[16] Heinrich Rust. Operational Semantics for Timed Systems: A Non-standard Approach to Uniform Modeling of Timed and Hybrid Systems, volume 3456 of Lecture Notes in Computer Science. Springer, 2005. ISBN 3-540-25576-1. doi: 10.1007/978-3-540-32008-1.

[17] Bernard P. Zeigler and Jong Sik Lee. Theory of quantized systems: formal basis for DEVS/HLA distributed simulation environment. In SPIE Proceedings, volume 3369, pages 49–58, 1998.

Citeringar i Crossref