Injecting Formal Verification in FMI-Based Co-simulations of Cyber-Physical Systems

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