Model And Verification Of Cyber Physical System Based On Statecharts With Continuous Variables

With the increasement in the complexity of systems, the systems’ dependence on hardware and the customers’ requirement of systems’ safety and reliability, traditional discrete tools of modeling are not able to meet developers’ needs, especially, when they are modeling Hybrid Systems which combine discrete driven events and time driven events. Cyber Physical System, which develops quickly in these years, is a representative of the Hybrid System. It is constituted by embedded systems, networks and control module and Cyber Physical System is involved in most of aspects of computer science, communication and control, so it is a difficult work to model and verify it.The aim of the thesis is to present a method which is able to model and verify the systems combining discrete driven events and continuous driven events. So we are able to guarantee the safety and reliability of systems.The main contributions of this thesis are followed:1. Proposing Statecharts with Continuous Variables based on original Statecharts and its Statechart Terms to solve the problem that the Statecharts cannot model Hybrid Systems effectively.2. Proposing the method how to transfer the system which is modelled by Statecharts with Continuous Variables to Kripke Structure and using Computation Tree Logic to verify the relevant attributes of the system.3. Using Statecharts with Continuous Variables to model and verify Safety Message inter Linkage Engining System and solve some relevant problems of this system.