Abstract
Model-based design tools supporting the Functional Mockup Interface (FMI) standard, often employ specification languages ideal for modelling specific domain problems without capturing the overall behavior of a Cyber-Physical System (CPS). These tools tend to handle some important CPS characteristics implicitly, such as network communication handshakes. At the same time, formal verification although a powerful approach, is still decoupled to FMI co-simulation processes, as it can easily lead to infeasible explorations due to state space explosion of continuous or discrete representations. In this paper we exploit co-modelling and co-simulation concepts combined with the injection of formal verification results indirectly in a model-based design workflow that will enable verification engineering benefits in a heterogeneous, multi-disciplinary design process for CPSs. We demonstrate the approach using a Heating, Ventilation and Air Conditioning (HVAC) case study where communication delays may affect the CPS system’s analysis. We model discrete events based on the Vienna Development Method Real-Time dialect, Continuous Time phenomena using Modelica, and communications using PROMELA. Results are considered and inspected both at the level of constituent models and the overall co-simulation.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
The User component is a basic abstraction used only to enable requests to the system during co-simulation.
References
Amalio, N., Cavalcanti, A., Miyazawa, A., Payne, R., Woodcock, J.: Foundations of the SysML for CPS modelling. Technical report, INTO-CPS Deliverable, D2.2a, December 2016
Bernardeschi, C., Masci, P., Pfeifer, H.: Early prototyping of wireless sensor network algorithms in PVS. In: Harrison, M.D., Sujan, M.-A. (eds.) SAFECOMP 2008. LNCS, vol. 5219, pp. 346–359. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-87698-4_29
Bernardeschi, C., Masci, P., Pfeifer, H.: Analysis of wireless sensor network protocols in dynamic scenarios. In: Guerraoui, R., Petit, F. (eds.) SSS 2009. LNCS, vol. 5873, pp. 105–119. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-05118-0_8
Blochwitz, T.: Functional Mock-up Interface for Model Exchange and Co-Simulation, July 2014. https://www.fmi-standard.org/downloads
Brosse, E., Quadri, I.: SysML and FMI in INTO-CPS. Technical report, INTO-CPS Deliverable, D4.2c, December 2016
Derler, P., Lee, E.A., Sangiovanni-Vincentelli, A.L.: Addressing modeling challenges in cyber-physical systems. Technical report UCB/EECS-2011-17, EECS Department, University of California, Berkeley, March 2011. http://www.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-17.html
Duflot, M., Kwiatkowska, M.Z., Norman, G., Parker, D.: A formal analysis of bluetooth device discovery. STTT 8(6), 621–632 (2006)
Elmqvist, H., Mattsson, S.E.: An introduction to the physical modelling of language modelica. In: Proceedings of the 9th European Simulation Symposium, Technical report, October 1997
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., Larsen, P.G., Basagiannis, S., Mady, A.E.D.: Collaborative model-based systems engineering for cyber-physical systems - a case study in building automation. In: Proceedings of INCOSE International Symposium on Systems Engineering, Edinburgh, Scotland, July 2016
Fitzgerald, J., Gamble, C., Payne, R., Pierce, K.: Method Guidelines 2. Technical report, INTO-CPS Deliverable, D3.2a, December 2016
Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)
Kleijn, C.: Modelling and simulation of fluid power systems with 20-sim. Int. J. Fluid Power 7(3), 57–60 (2006)
Lamport, L.: Real-time model checking is really simple. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 162–175. Springer, Heidelberg (2005). https://doi.org/10.1007/11560548_14
Larsen, P.G., Battle, N., Ferreira, M., Fitzgerald, J., Lausdahl, K., Verhoef, M.: The overture initiative - integrating tools for VDM. SIGSOFT Softw. Eng. Notes 35(1), 1–6 (2010). https://doi.org/10.1145/1668862.1668864
Larsen, P.G., Fitzgerald, J., Woodcock, J., Fritzson, P., Brauer, J., Kleijn, C., Lecomte, T., Pfeil, M., Green, O., Basagiannis, S., Sadovykh, A.: Integrated tool chain for model-based design of cyber-physical systems: the INTO-CPS project. In: CPS Data Workshop, Vienna, Austria, April 2016
Larsen, P.G., Lausdahl, K., Battle, N., Fitzgerald, J., Wolff, S., Sahara, S., Verhoef, M., Tran-Jørgensen, P.W.V., Oda, T.: The VDM-10 language manual. Technical report TR-2010-06, The Overture Open Source Initiative, April 2010
MathWorks, October 2011. Simulink official website: http://www.mathworks.com/
Ölveczky, P.C., Thorvaldsen, S.: Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in real-time maude. Theor. Comput. Sci. 410(2–3), 254–280 (2009)
Ouy, J., Lecomte, T., Christiansen, M.P., Henriksen, A.V., Green, O., Hallerstede, S., Larsen, P.G., ger, C.J., Basagiannis, S., Couto, L.D., din Mady, A.E., Ridouanne, H., Poy, H.M., Alcala, J.V., König, C., Balcu, N.: Case Studies 2, Public Version. Technical report, INTO-CPS Public Deliverable, D1.2a, December 2016
Philips Semiconductors Corporation: SCC2691 UART data sheet. Technical report, May 2006
Timothy, S.: A survey of control technologies in the building automation industry. In: Proceedings of the IFAC 16th World Congress, Prague, Czech Republic, pp. 13–96 (2005)
Verhoef, M., Larsen, P.G., Hooman, J.: Modeling and validating distributed embedded real-time systems with VDM++. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 147–162. Springer, Heidelberg (2006). https://doi.org/10.1007/11813040_11
Acknowledgments
This work is supported by the INTO-CPS H2020 project: Integrated Tool Chain for Model-based Design of Cyber-Physical Systems. Funded by the European Commission-H2020, Project Number: 664047.
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
Couto, L.D., Basagiannis, S., Ridouane, E.H., Mady, A.ED., Hasanagic, M., Larsen, P.G. (2018). Injecting Formal Verification in FMI-Based Co-simulations of Cyber-Physical Systems. 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_20
Download citation
DOI: https://doi.org/10.1007/978-3-319-74781-1_20
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)