Research On Hybrid Automata Model Checking And Its Application

Hybrid system is a type of complex system with both discrete and continuous behaviors and is widely used in real-time control area.Since most of the real-time control systems are safety-critical,it is essential to use hybrid automata to model the system's behavior and to check the safety of it correspondingly.However,it has been very difficult to verify the safety property of the hybrid automata.Even for a special class of hybrid automata,the Linear Hybrid Automata(LHA),the reachability verification is undecidable.The size of problem that can be answered by LHA model checking is very limited.Therefore,it is important for us to:1)control the complexity of the verification of the hybrid automata,2)to expand the scale of problems of LHA model checking,3)and to apply these models to real case problems.My thesis studies the following problems about the hybrid automata:.First,we did the path-oriented method reachability analysis for the composition-al linear hybrid automata(LHA).It is well-known that the verification of the compositional automata is very complex and this greatly restricts the size of the problem that can be solved.Thus,we proposed a path-oriented reachability anal-ysis optimization technique based on classical STEP semantics.By introducing tau transitions in the graph structure of the model,we can conduct a pure SAT encoding of the graph structure of the composed system and make the SAT-based path enumeration easier.We also presented a set of optimization techniques that can alleviate the path explosion problem caused by tau transitions.Further exper-iments showed that the efficiency of our method performs so much better than the original model that we can handle a nuclear rod benchmark with 21 rods within just 1 second..Secondly,we researched on the derivation of unbounded reachability proof for L-HA during bounded model checking procedure.Bounded model checking(BM-C)is much easier to conduct in a certain bound,but cannot guarantee the safety beyond the bound.In my thesis,we proposed an incremental buchi automata construction based optimization technique to derive,in some cases,a proof of un-bounded reachability argument of LHA from a BMC procedure.By conducting incremental biichi automata construction from the IIS path segments discovered in the BMC procedure and on-the-fly check for unbounded proof,it can stop the BMC procedure as soon as the unbounded argument is derived.The experiment showed that the proposed method highly improved the performance of deriving unbound proof from BMC,even better than pure BMC procedure in some case..Finally,we studied how to systematically check and fix the event-driven Internet of Thing Systems based on hybrid automata.IoT system is closely related to the personal and property safety of the users,so the confidence of IoT system is very important.But with the increasing complexity of the IoT devices and the nature of non-expert users in the field,it is hard to ensure the safety of the system.In my thesis,we introduced a new automatic technique based on hybrid automata that can be used to assist non-expert IoT users in the confidence checking of the HA,IoT systems.With the devices users have and the corresponding IFTTT ruls,we can automatically built and checked the LHA model.We also present a quantifier elimination process based on the counterexample found to synthesize the fixed suggestions for the users.At last,we implemented a platform called MenShen:it can handle a complex system composed of 45 devices and 65 rules easily.The fixed suggestions made by our tools are highly praised by our users,with more than 80%satisfaction in the user study.