Abstract
Given the considerable ongoing research interest in collaborative multidisciplinary modelling and co-simulation, it is worth considering the features of model-based techniques and tools that deliver benefits to cyber-physical systems developers. The European project “Integrated Tool Chain for Model-based Design of Cyber-Physical Systems” (INTO-CPS) has developed a well-founded tool chain for CPS design, based on the Functional Mock-up Interface standard, and supported by methodological guidance. The focus of the project has been on the delivery of a sound foundation, an open chain of compatible and usable tools, and a set of accessible guidelines that help users adapt the technology to their development needs.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
FMI essentially defines a standardised interface to be used in computer simulators to develop complex CPSs.
- 2.
- 3.
- 4.
- 5.
- 6.
- 7.
- 8.
- 9.
- 10.
- 11.
- 12.
For SysML we have only formalised the subset we need in a co-simulation setting [1].
- 13.
- 14.
This library can be viewed at github.com/isabelle-utp/utp-main.
References
Amálio, N., Payne, R., Cavalcanti, A., Woodcock, J.: Checking SysML models for co-simulation. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 450–465. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47846-3_28
Armstrong, A., Gomes, V., Struth, G.: Building program construction and verification tools from algebraic principles. Form. Asp. Comput. 28(2), 265–293 (2015)
Bagnato, A., Brosse, E., Quadri, I., Sadovykh, A.: The INTO-CPS cyber-physical system profile. In: DeCPS Workshop on Challenges and New Approaches for Dependable and Cyber-Physical System Engineering Focus on Transportation of the Future. Vienna, Austria, June 2017
Banks, M.J., Jacob, J.L.: Unifying theories of confidentiality. In: Qin, S. (ed.) UTP 2010. LNCS, vol. 6445, pp. 120–136. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16690-7_5
Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS (LNAI), vol. 6989, pp. 12–27. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24364-6_2
Blochwitz, T., Otter, M., Arnold, M., Bausch, C., Elmqvist, H., Junghanns, A., Mauss, J., Monteiro, M., Neidhold, T., Neumerkel, D., Olsson, H., Peetz, J.V., Wolf, S., Clau, C.: The functional mockup interface for tool independent exchange of simulation models. In: Proceedings of 8th International Modelica Conference, pp. 105–114 (2011)
Bresciani, R., Butterfield, A.: A UTP semantics of pGCL as a homogeneous relation. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 191–205. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-30729-4_14
Broman, D., Brooks, C., Greenberg, L., Lee, E.A., Masin, M., Tripakis, S., Wetter, M.: Determinate composition of FMUs for co-simulation. In: 13th International Conference on Embedded Software (EMSOFT), Montreal, September 2013. http://chess.eecs.berkeley.edu/pubs/1002.html
Broman, D., Greenberg, L., Lee, E.A., Masin, M., Tripakis, S., Wetter, M.: Requirements for hybrid cosimulation standards. In: Proceedings of 18th ACM International Conference on Hybrid Systems: Computation and Control (HSCC), pp. 179–188. ACM (2015)
Cavalcanti, A., Woodcock, J.: A tutorial introduction to CSP in Unifying Theories of Programming. In: Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) PSSE 2004. LNCS, vol. 3167, pp. 220–268. Springer, Heidelberg (2006). https://doi.org/10.1007/11889229_6
Cavalcanti, A., Woodcock, J., Amálio, N.: Behavioural models for FMI co-simulations. In: ICTAC (2016, in press)
Couto, L.D., Basagianis, S., Mady, A.E.D., Ridouane, E.H., Larsen, P.G., Hasanagic, M.: Injecting formal verification in FMI-based co-simulation of cyber-physical systems. In: Cerone, A., Roveri, M. (eds.) SEFM 2017 Workshops. LNCS, vol. 10729, pp. 282–297. Springer, Cham (2017)
Derler, P., Lee, E.A., Sangiovanni-Vincentelli, A.: Modeling cyber-physical systems. Proc. IEEE (special issue on CPS) 100(1), 13–28 (2012)
The Electron website. http://electron.atom.io/ (2016)
Fitzgerald, J., Gamble, C., Larsen, P.G., Pierce, K., Woodcock, J.: Cyber-physical systems design: formal foundations, methods and integrated tool chains. In: FormaliSE: FME Workshop on Formal Methods in Software Engineering. ICSE 2015, Florence, Italy, May 2015
Fitzgerald, J., Gamble, C., Payne, R., Lam, B.: Exploring the cyber-physical design space. In: Proceedings of INCOSE International Symposium on Systems Engineering, Adelaide, Australia, vol. 27, pp. 371–385 (2017). http://dx.doi.org/10.1002/j.2334-5837.2017.00366.x
Fitzgerald, J., Gamble, C., Payne, R., Larsen, P.G., Basagiannis, S., Mady, A.E.D.: Collaborative model-based systems engineering for cyber-physical systems, with a building automation case study. In: INCOSE International Symposium, vol. 26, no. 1, pp. 817–832 (2016)
Fitzgerald, J., Larsen, P.G., Verhoef, M. (eds.): Collaborative Design for Embedded Systems - Co-modelling and Co-simulation. Springer, Berlin (2014). http://link.springer.com/book/10.1007/978-3-642-54118-6
Foldager, F., Larsen, P.G., Green, O.: Development of a driverless lawn mower using co-simulation. In: Cerone, A., Roveri, M. (eds.) SEFM 2017 Workshops. LNCS, vol. 10729, pp. 328–342. Springer, Cham (2017)
Foster, S., Thiele, B., Cavalcanti, A., Woodcock, J.: Towards a UTP semantics for Modelica. In: Proceedings of 6th International Symposium on Unifying Theories of Programming, June 2016 (to appear)
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, Cham (2015). https://doi.org/10.1007/978-3-319-14806-9_2
Foster, S., Zeyda, F., Woodcock, J.: Unifying heterogeneous state-spaces with lenses. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 295–314. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46750-4_17
Fritzson, P.: Principles of Object-Oriented Modeling and Simulation with Modelica 2.1. Wiley-IEEE Press, January 2004
Gotel, O.C., Finkelstein, A.C.: An analysis of the requirements traceability problem. In: Proceedings of 1st International Conference on Requirements Engineering, pp. 94–101, April 1994
Hoare, T., Jifeng, H.: Unifying Theories of Programming. Prentice Hall, Upper Saddle River (1998)
Holt, J., Ingram, C., Larkham, A., Stevens, R.L., Riddle, S., Romanovsky, A.: Convergence report 3. Technical report, COMPASS Deliverable, D11.3, September 2014
Holt, J., Perry, S., Payne, R., Bryans, J., Hallerstede, S., Hansen, F.O.: A model-based approach for requirements engineering for systems of systems. IEEE Syst. J. 9(1), 252–262 (2015). https://doi.org/10.1109/JSYST.2014.2312051
Immler, F.: Formally verified computation of enclosures of solutions of ordinary differential equations. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 113–127. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06200-6_9
Klein, G., et al.: seL4: Formal verification of an OS kernel. In: Proceedings of 22nd Symposium on Operating Systems Principles (SOSP), pp. 207–220. ACM (2009)
Larsen, P.G., Fitzgerald, J., Woodcock, J., Lecomte, T.: Chapter 8: Collaborative modelling and simulation for cyber-physical systems. In: Trustworthy Cyber-Physical Systems Engineering. Chapman and Hall/CRC, Boca Raton (2016). ISBN 9781498742450
Larsen, P.G., Fitzgerald, J., Woodcock, J., Nilsson, R., Gamble, C., Foster, S.: Towards semantically integrated models and tools for cyber-physical systems design. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 171–186. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47169-3_13
Mengist, A., Pop, A., Asghar, A., Fritzson, P.: Traceability support in openmodelica using open services for lifecycle collaboration (OSLC). In: Kofránek, J., Casella, F. (eds.) Proceedings of 12th International Modelica Conference, pp. 823–830. Modelica Association and Linköping University Electronic Press, 15–17 May 2017
Moreau, L., Groth, P.: PROV-overview. Technical report, World Wide Web Consortium (2013). http://www.w3.org/TR/2013/NOTE-prov-overview-20130430/
Neghina, M., Zamrescu, C.B., Larsen, P.G., Lausdahl, K., Pierce, K.: A discrete event-first approach to collaborative modelling of cyber-physical systems. In: Fitzgerald, J., Tran-Jørgensen, P.W.V., Oda, T. (ed.) 15th Overture Workshop: New Capabilities and Applications for Model-based Systems Engineering, Newcastle, UK, September 2017
Nielsen, C.B., Larsen, P.G., Fitzgerald, J., Woodcock, J., Peleska, J.: Model-based engineering of systems of systems. ACM Comput. Surv. 48(2) (September 2015). http://dl.acm.org/citation.cfm?id=2794381
Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9
Palmieri, M., Bernardeschi, C., Masci, P.: Co-simulation of semi-autonomous systems: the Line Follower Robot case study. In: Cerone, A., Roveri, M. (eds.) SEFM 2017 Workshops. LNCS, vol. 10729, pp. 421–435. Springer, Cham (2017)
Pedersen, N., Lausdahl, K., Sanchez, E.V., Larsen, P.G., Madsen, J.: Distributed co-simulation of embedded control software with exhaust gas recirculation water handling system using INTO-CPS. In: Proceedings of 7th International Conference on Simulation and Modeling Methodologies, Technologies and Applications (SIMULTECH 2017), Madrid, Spain, pp. 73–82, July 2017. ISBN 978-989-758-265-3
Peleska, J.: Industrial-strength model-based testing - state of the art and current challenges. In: Petrenko, A.K., Schlingloff, H. (eds.) Proceedings Eighth Workshop on Model-Based Testing, MBT 2013. EPTCS, Rome, Italy, vol. 111, pp. 3–28, 17 March 2013. http://arxiv.org/abs/1303.0379
Penzenstadler, B., Eckhardt, J.: A requirements engineering content model for cyber-physical systems. In: RESS, pp. 20–29 (2012)
Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Log. Comput. 20(1), 309–352 (2010)
Platzer, A.: Logical Analysis of Hybrid Systems. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14509-4
Santos, T., Cavalcanti, A., Sampaio, A.: Object-orientation in the UTP. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol. 4010, pp. 18–37. Springer, Heidelberg (2006). https://doi.org/10.1007/11768173_2
Tang, X., Woodcock, J.: Travelling processes. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 381–399. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27764-4_20
Wei, K.: Reactive designs of interrupts in Circus Time. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) ICTAC 2013. LNCS, vol. 8049, pp. 373–390. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39718-9_22
Wenzel, M., Wolff, B.: Building formal method tools in the isabelle/isar framework. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 352–367. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74591-4_26
Wiesner, S., Gorldt, C., Soeken, M., Thoben, K.-D., Drechsler, R.: Requirements engineering for cyber-physical systems. In: Grabot, B., Vallespir, B., Gomes, S., Bouras, A., Kiritsis, D. (eds.) APMS 2014. IAICT, vol. 438, pp. 281–288. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44739-0_35
Woodcock, J., Cavalcanti, A.: A tutorial introduction to designs in unifying theories of programming. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) IFM 2004. LNCS, vol. 2999, pp. 40–66. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24756-2_4
Zeyda, F., Ouy, J., Foster, S., Cavalcanti, A.: Formalised cosimulation models. In: Cerone, A., Roveri, M. (eds.) SEFM 2017 Workshops. LNCS, vol. 10729, pp. 451–466. Springer, Cham (2017)
Acknowledgment
The work presented here is partially supported by the INTO-CPS project funded by the European Commission’s Horizon 2020 programme under grant agreement number 664047. We would like to thank all the participants of those projects for their efforts making this a reality.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG
About this paper
Cite this paper
Larsen, P.G., Fitzgerald, J., Woodcock, J., Gamble, C., Payne, R., Pierce, K. (2018). Features of Integrated Model-Based Co-modelling and Co-simulation Technology. In: Cerone, A., Roveri, M. (eds) Software Engineering and Formal Methods. SEFM 2017. Lecture Notes in Computer Science(), vol 10729. Springer, Cham. https://doi.org/10.1007/978-3-319-74781-1_26
Download citation
DOI: https://doi.org/10.1007/978-3-319-74781-1_26
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-74780-4
Online ISBN: 978-3-319-74781-1
eBook Packages: Computer ScienceComputer Science (R0)