Behavioural models for FMI co-simulations. (English) Zbl 1482.68135

Sampaio, Augusto (ed.) et al., Theoretical aspects of computing – ICTAC 2016. 13th international colloquium, Taipei, Taiwan, ROC, October 24–31, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9965, 255-273 (2016).
Summary: Simulation is a favoured technique for analysis of cyber-physical systems. With their increase in complexity, co-simulation, which involves the coordinated use of heterogeneous models and tools, has become widespread. An industry standard, FMI, has been developed to support orchestration; we provide the first behavioural semantics of FMI. We use the state-rich process algebra, Circus, to present our modelling approach, and indicate how models can be automatically generated from a description of the individual simulations and their dependencies. We illustrate the work using three algorithms for orchestration. A stateless version of the models can be verified using model checking via translation to CSP. With that, we can prove important properties of these algorithms, like termination and determinism, for example. We also show that the example provided in the FMI standard is not a valid algorithm.
For the entire collection see [Zbl 1347.68012].


68Q60 Specification and verification (program logics, model checking, etc.)
68Q55 Semantics in the theory of computing
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: DOI Link


[1] Abrial, J.R.: Modeling in Event-B-System and Software Engineering. Cambridge University Press, Cambridge (2010) · Zbl 1213.68214
[2] Bastian, J., Clauß, C., Wolf, S., Schneider, P.: Master for co-simulation using FMI. In: Modelica Conference (2011)
[3] Bradfield, J., Stirling, C.: Verifying temporal properties of processes. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 115–125. Springer, Heidelberg (1990). doi: 10.1007/BFb0039055
[4] Broman, D., et al.: Determinate composition of FMUs for co-simulation. In: ACM SIGBED International Conference on Embedded Software. IEEE (2013)
[5] Broman, D., et al.: Requirements for hybrid cosimulation standards. In: 18th International Conference on Hybrid Systems: Computation and Control, pp. 179–188. ACM (2015) · Zbl 1366.68352
[6] Butterfield, A., Sherif, A., Woodcock, J.: Slotted-circus. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 75–97. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-73210-5_5 · Zbl 05523876
[7] Cavalcanti, A.L.C., Clayton, P., O’Halloran, C.: From control law diagrams to ada via \[ {\mathsf Circus} \] . Formal Aspects Comput. 23(4), 465–512 (2011) · Zbl 1226.68028
[8] Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: A refinement strategy for \[ {\mathsf Circus} \] . Formal Aspects Comput. 15(2–3), 146–181 (2003) · Zbl 1093.68555
[9] Denil, J., et al.: Explicit semantic adaptation of hybrid formalisms for FMI co-simulation. In: Spring Simulation Multi-Conference (2015)
[10] Derler, P., Lee, E.A., Vincentelli, A.S.: Modeling cyber-physical systems. Proc. IEEE 100(1), 13–28 (2012)
[11] Feldman, Y.A., Greenberg, L., Palachi, E.: Simulating Rhapsody SysML blocks in hybrid models with FMI. In: Modelica Conference (2014)
[12] FMI development group: Functional mock-up interface for model exchange and co-simulation, 2.0. (2014). https://www.fmi-standard.org
[13] Foster, S., et al.: Towards a UTP semantics for Modelica. In: Unifying Theories of Programming. LNCS. Springer (2016) · Zbl 1483.68053
[14] Foster, S., Zeyda, F., Woodcock, J.: Isabelle/UTP: a mechanised theory engineering framework. In: Naumann, D. (ed.) UTP 2014. LNCS, vol. 8963, pp. 21–41. Springer, Heidelberg (2015). doi: 10.1007/978-3-319-14806-9_2 · Zbl 1457.68061
[15] Gheorghe, L., et al.: A formalization of global simulation models for continuous/discrete systems. In: Summer Computer Simulation Conference, pp. 559–566. Society for Computer Simulation International (2007)
[16] Gibson-Robinson, T., et al.: FDR3–a modern refinement checker for CSP. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 187–201 (2014) · Zbl 1392.68300
[17] Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985) · Zbl 0637.68007
[18] Kübler, R., Schiehlen, W.: Two methods of simulator coupling. Math. Comput. Modell. Dynamical Syst. 6(2), 93–113 (2000) · Zbl 0962.65107
[19] The MathWorks Inc: Simulink. www.mathworks.com/products/simulink
[20] Oliveira, M., Cavalcanti, A.: From \[ \mathsf {Circus} \] to JCSP. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 320–340. Springer, Heidelberg (2004). doi: 10.1007/978-3-540-30482-1_29
[21] Oliveira, M.V.M., Cavalcanti, A.L.C., Woodcock, J.C.P.: A UTP semantics for \[ {\mathsf Circus} \] . Formal Aspects Comput. 21(1–2), 3–32 (2009) · Zbl 1165.68048
[22] Pohlmann, U., et al.: Generating functional mockup units from software specifications. In: Modelica Conference (2012)
[23] Roscoe, A.W.: Understanding concurrent systems. In: Texts in Computer Science. Springer (2011) · Zbl 1211.68205
[24] Savicks, V., et al.: Co-simulating event-b and continuous models via FMI. In: Summer Simulation Multiconference, pp. 37:1–37:8. Society for Computer Simulation International (2014)
[25] Tripakis, S.: Bridging the semantic gap between heterogeneous modeling formalisms and FMI. In: International Conference on Embedded Computer Systems: Architectures, Modeling, and Simulation, pp. 60–69. IEEE (2015)
[26] Woodcock, J.C.P., Davies, J.: Using Z-Specification, Refinement, and Proof. Prentice-Hall, New York (1996) · Zbl 0855.68060
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.