Article | Proceedings of the 11th International Modelica Conference, Versailles, France, September 21-23, 2015 | Co-Simulation of Hybrid Systems with SpaceEx and Uppaal
Göm menyn

Title:
Co-Simulation of Hybrid Systems with SpaceEx and Uppaal
Author:
Sergiy Bogomolov: IST Austria, Austria Marius Greitschus: University of Freiburg, Germany Peter G. Jensen: Aalborg University, Denmark Kim G. Larsen: Aalborg University, Denmark Marius Mikučionis: Aalborg University, Denmark Thomas Strump: University of Freiburg, Germany Stavros Tripakis: Aalto University, Finland, and University of California, Berkeley, USA
DOI:
10.3384/ecp15118159
Download:
Full text (pdf)
Year:
2015
Conference:
Proceedings of the 11th International Modelica Conference, Versailles, France, September 21-23, 2015
Issue:
118
Article no.:
017
Pages:
159-169
No. of pages:
11
Publication type:
Abstract and Fulltext
Published:
2015-09-18
ISBN:
978-91-7685-955-1
Series:
Linköping Electronic Conference Proceedings
ISSN (print):
1650-3686
ISSN (online):
1650-3740
Publisher:
Linköping University Electronic Press, Linköpings universitet


Export in BibTex, RIS or text

The Functional Mock-up Interface (FMI) is an industry standard which enables co-simulation of complex heterogeneous systems using multiple simulation engines. In this paper, we show how to use FMI in order to co-simulate hybrid systems modeled in the model checkers SpaceEx and Uppaal. We show how FMI components can be automatically generated from SpaceEx and Uppaal models. We also validate the co-simulation approach by comparing the simulations of a room heating benchmark in two cases: first, when a single model is simulated in SpaceEx; and second, when the model is split in two submodels, and co-simulated using SpaceEx and Uppaal. Finally, we perform a measurement experiment on a composite model to show a potential for statistical model checking using stochastic co-simulations.

Keywords: FMI; hybrid system; timed automaton

Proceedings of the 11th International Modelica Conference, Versailles, France, September 21-23, 2015

Author:
Sergiy Bogomolov, Marius Greitschus, Peter G. Jensen, Kim G. Larsen, Marius Mikučionis, Thomas Strump, Stavros Tripakis
Title:
Co-Simulation of Hybrid Systems with SpaceEx and Uppaal
DOI:
http://dx.doi.org/10.3384/ecp15118159
References:

D.E. Nadales Agut, Dirk A. van Beek, and J.E. Rooda. Syntax and semantics of the compositional interchange format for hybrid systems. The Journal of Logic and Algebraic Programming, 82(1):1 – 52, 2013. ISSN 1567-8326. doi: 10.1016/j.jlap.2012.07.001.


R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138(1):3–34, 1995.


Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.


Stanley Bak, Sergiy Bogomolov, and Taylor T. Johnson. HYST: a source transformation and translation tool for hybrid automaton models. In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC, Seattle, WA, USA, April 14-16, 2015, pages 128–133. ACM, 2015.


Jens Bastian, Christoph ClauĂź, SusannWolf, and Peter Schneider. Master for Co-Simulation Using FMI. In 8th International Modelica Conference, 2011.


Harsh Beohar, D. E. Nadales Agut, Dirk A. van Beek, and Pieter J. L. Cuijpers. Hierarchical states in the compositional interchange format. In Luca Aceto and Pawel Sobocinski, editors, Proceedings Seventh Workshop on Structural Operational Semantics, SOS 2010, Paris, France, 30 August 2010., volume 32 of EPTCS, pages 42–56, 2010. doi: 10.4204/EPTCS.32.4.


T. Blochwitz, M. Otter, M. Arnold, C. Bausch, C. ClauĂź, H. Elmqvist, A. Junghanns, J. Mauss, M. Monteiro, T. Neidhold, D. Neumerkel, H. Olsson, J.-V. Peetz, and S. Wolf. The Functional Mockup Interface for Tool independent Exchange of Simulation Models. In 8th International Modelica Conference, Dresden, Germany, March 2011. Modelica Association.


D. Broman, C. Brooks, L. Greenberg, E. A. Lee, S. Tripakis, M. Wetter, and M. Masin. Determinate Composition of FMUs for Co-Simulation. In 13th ACM & IEEE International Conference on Embedded Software (EMSOFT’13), 2013.


D. Broman, L. Greenberg, E. A. Lee, M. Masin, S. Tripakis, and M. Wetter. Requirements for Hybrid Cosimulation Standards. In Hybrid Systems: Computation and Control (HSCC), 2015.


Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikucionis, Danny Bøgsted Poulsen, Jonas van Vliet, and Zheng Wang. Statistical model checking for networks of priced timed automata. In Uli Fahrenberg and Stavros Tripakis, editors, Formal Modeling and Analysis of Timed Systems, volume 6919 of Lecture Notes in Computer Science, pages 80–96. Springer Berlin Heidelberg, 2011.


Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikucionis, and Danny Bøgsted Poulsen. Uppaal SMC tutorial. International Journal on Software Tools for Technology Transfer, 2015.


J. Eker, J. Janneck, E. 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, January 2003.


Ansgar Fehnker and Franjo Ivancic. Benchmarks for hybrid systems verification. In In Hybrid Systems: Computation and Control (HSCC), pages 326–341. Springer, 2004.


Y. A. Feldman, L. Greenberg, and E. Palachi. Simulating Rhapsody SysML Blocks in Hybrid Models with FMI. In 10th Modelica Conference, pages 43–52, 2014.


Goran Frehse, Colas Le 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 Shaz Qadeer Ganesh Gopalakrishnan, editor, 23rd International Conference on Computer Aided Verification (CAV), LNCS. Springer, 2011.


Kim G. Larsen, Paul Pettersson, and Wang Yi. Uppaal in a nutshell. International Journal on Software Tools for Technology Transfer, 1(1-2):134–152, 1997.


Alessandro Pinto, Alberto L. Sangiovanni-Vincentelli, Luca P. Carloni, and Roberto Passerone. Interchange formats for hybrid systems: review and proposal. In Hybrid Systems: Computation and Control, HSCC. Springer, 2005.


Alessandro Pinto, Luca P. Carloni, Roberto Passerone, and Alberto Sangiovanni-Vincentelli. Interchange format for hybrid systems: Abstract semantics. In Joao P. Hespanha and Ashish Tiwari, editors, Hybrid Systems: Computation and Control, volume 3927 of LNCS, pages 491–506. Springer Berlin Heidelberg, 2006.


Uwe Pohlmann, Wilhelm Schäfer, Hendrik Reddehase, Jens Röckemann, and Robert Wagner. Generating Functional Mockup Units from Software Specifications. In 9th Modelica Conference, pages 765–774, 2012.


Stavros Tripakis. Bridging the Semantic Gap Between Heterogeneous Modeling Formalisms and FMI. In International Conference on Embedded Computer Systems: Architectures, Modeling and Simulation – SAMOS XV, 2015.

Proceedings of the 11th International Modelica Conference, Versailles, France, September 21-23, 2015

Author:
Sergiy Bogomolov, Marius Greitschus, Peter G. Jensen, Kim G. Larsen, Marius Mikučionis, Thomas Strump, Stavros Tripakis
Title:
Co-Simulation of Hybrid Systems with SpaceEx and Uppaal
DOI:
http://dx.doi.org/10.3384/ecp15118159
Note: the following are taken directly from CrossRef
Citations:
No citations available at the moment


Responsible for this page: Peter Berkesand
Last updated: 2017-02-21