Font Size: a A A

Safety Verification Of Hybrid Systems Based On Formal Method

Posted on:2016-12-24Degree:MasterType:Thesis
Country:ChinaCandidate:Q LiFull Text:PDF
GTID:2308330461975909Subject:Software engineering
Abstract/Summary:PDF Full Text Request
Hybrid systems are combinations of discrete events and dynamic systems. Typical examples of hybrid systems are cyber physical system, intelligent control system and etc. Hybrid system is one of the most important and cutting-edge systems studied in the information technology field. It’s of great value to study how to model the hybrid systems and verify whether the system meet the safety properties.Formal verification method is a good fit for modeling, analyzing and verifying hybrid systems. We use abstraction method and differential dynamic logic, combined with Coq and KeYmaera tool separately to model and analyze two practical hybrid systems. And successfully verified their safety properties.Abstraction method first divides the state space of a linear hybrid system into several parts, and then transforms it to the reachability problem of a graph. This paper applies the abstraction method in the Coq system, which is an interactive theorem-proofing tool with some existing libraries implemented in it, and implements the formal verification of hybrid system with abstraction method in Coq system. Then uses the abstraction method to model and verify a thermostat system in Coq.Differential dynamic logic is applied to model and analyze the VCCR system, which is a subsystem of the space life support system. Based on hybrid program, the model of VCCR system is built with its safety property defined. Using the KeYmaera tool, a safety verification tool of hybrid system, the safety property of the system is verified.Finally, the results confirm the advantages of formal verification of hybrid systems and prospects of the further research are discussed.
Keywords/Search Tags:Hybrid system, formal verification, abstract method, differential dynamic logic, life support system, VCCR system, thermostat system, Coq system, KeYmaera tool
PDF Full Text Request
Related items