Co-simulation and verification of cyber-physical systems using logic models

This thesis proposes a methodology to validate and formally verify Cyber-Physical Systems (CPS) exploiting logic for formal models, emerging standard technologies for co-simulation and theorem proving technology for verification. Co-simulation enables the global simulation of a complex system by composing the simulations of its parts, created with different tools without the need to formalize the whole system with a formal language, which, if feasible, is a time-consuming task. The same models of components can successively be used for verifying properties of the whole system. The proposed methodology also allows to build early prototypes of human-machine interfaces based on formal methods, supporting the work of formal methods experts in charge of analyzing safety-critical aspects of user interfaces in CPS. Formal methods experts usually need to engage with domain experts that may not fully understand the mathematical details of formal analysis. Co-simulation with human-machine interfaces mitigates the barriers mentioned above, providing a speed-up in the design phase of the CPS and improving the validation of formal models. The framework presented in this thesis extends an existing prototyping toolkit, based on the Prototype Verification System (PVS), with novel functionalities for automatic generation of interactive prototypes supporting the Functional Mock-up Interface (FMI), a de-facto standard technology for co-simulation. The architecture of the framework is presented, along with verification of fundamental aspects of its functionalities. The framework is the core element for the integration of formal models, co-simulation and verification. The PVS theorem prover can be used to verify safety properties of the system under analysis. Finally, this thesis provides a collection of case studies to show the possibilities offered by the proposed methodology and the developed framework for model-based design of CPS from different application domains.