Reachability Analysis and Simulation for Hybridised Event-B Models

The development of cyber-physical systems has become one of the biggest challenges in the field of model-based system engineering. The difficulty stems from the complex nature of cyber-physical systems which have deeply intertwined physical processes, computation and networking system aspects. To provide the highest level of assurance, cyber-physical systems should be modelled and reasoned about at a system-level as their safety depends on a correct interaction between different subsystems. In this paper, we present a development framework of cyber-physical systems which is built upon a refinement and proof based modelling language - Event-B and its extension for modelling hybrid systems. To improve the level of automation in the deductive verification of the resulting hybridised Event-B models, the paper describes a novel approach of integrating reachability analysis in the proof process. Furthermore, to provide a more comprehensive cyber-physical system development and simulation-based validation, we describe mechanism for translating Event-B models of cyber-physical systems to Simulink. The process of applying our framework is evaluated by formally modelling and verifying a cyber-physical railway signalling system.