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.
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.
