Event Driven Monitoring Of Cyber-physical Systems Based On Hybrid Automata

Cyber-Physical Systems (CPS) are considered to be the next-generation embedded systems and have broad application prospects, which involve deep interactions between computation cores, communication networks and physical environments. These systems are inherently complex and often run in the nondeterministic physical environment. This makes the traditional formal verification technology impractical to verify the complete system behaviors. Runtime monitoring, known as a lightweight verification technique, provides a practical way to monitor and verify such systems at runtime. Based on the researches about CPS systems and related software runtime monitoring theories and techniques, this thesis carries out the following researches about monitoring of CPS systems:Firstly, we study the theoretical basis and the existing researches of CPS systems, as well as some software runtime monitoring methods and techniques. Meanwhile, we analysis the major challenges of monitoring CPS systems.Secondly, by drawing lessons from software runtime monitoring, we proposed an event-driven monitoring framework for CPS systems based on the hybrid automata formalism. The framework combines model-based design and formal analysis, aiming to form the monitoring capability early in the system development. It can effectively monitor the safety properties specified by the temporal logic Meta Event Definition Language(MEDL).Thirdly, for the Simulink/Stateflow modeling platform, which is widely used for designing and modeling CPS systems in industry, we proposed a method to translate PEDL/MEDL specification script to monitor models. We design the rules to translate PEDL/MEDL script into Stateflow charts and implement the automated generating tools.Finally, we demonstrate how to use our framework to inject monitoring capabilities into the system model with a typical CPS application case in transportation CPS, the CACC system. Through model simulation, we perform the monitoring process, and monitor the dynamic behavior during runtime. The effectiveness of the proposed framework is verified.