Research On Formal Verification Methods Of CAN-based Cyber-Physical Systems

Cyber-physical systems are widely used in many important areas, such as automobile, medicaland energy, etc. Controller area network (CAN) is a field bus, which has been applied invehicle-based Cyber-physical systems. In the above CAN-based Cyber-physical systems, it is veryimportant to ensure the safety and reliability; however, the current verification methods have someproblems, such as non-standardization in verification process, and the deficiency of performanceanalysis.In order to take effective verification of CAN-based Cyber-physical systems and improve theconfidence of reliability, this thesis, firstly, proposes a formal verification framework forCyber-physical systems. In the framework, models of the components in the system are proposedand then formed into the formal logic model of the whole system according to their interaction, andthe functional correctness verification and performance analysis are taken. Then, a method ofbuilding the timed automata of CAN-based Cyber-physical systems is proposed, and each timedautomaton is described formally. And finally, the CAN-based automotive Cyber-physical systems isdetailed modeled in UPPAAL, and functional correctness verification and performance analysis aretaken under different environment configuration.The case study work shows that the formal verification framework and the timed automatamodel proposed in this paper are feasible and effective. They standardize the verification process.Also, it can take verification of function and performance of a system effectively. Thus, it canensure the safety and reliability of CAN-based Cyber-physical systems.