Composed IIS Paths Based Path-oriented Reachability Analysis Of Composed Linear Hybrid Automata

Cyber-physical systems are widely used in safety-critical systems,so it is very important to ensure their correctness and safety.Hybrid automata consist of discrete state transitions and continuous dynamics.The combination of discrete logical state transitions and continuous dynamics in hybrid automata makes it possible to model and verify Cyber-physical systems.However,due to the complex state space,even reachability analysis of the safety problems of hybrid automata is extremely difficult.Due to a large amount of communication cooperative behaviors of different com-ponents,compositional hybrid automata can be used to model CPS.Compositional hy-brid automata are composed of multiple single hybrid automata through the shared la-bel,and its behavior is more complex than a single hybrid automaton.The state-of-the-art techniques do not scale well to model checking of compositional hybrid automata.Therefore,how to improve the scale of model checking of compositional hybrid au-tomata and improve the verification efficiency are very worthy of attention and re-search.This paper systematically studied the following problems about reachability analysis of compositional linear hybrid automata:1.Mixed semantics based bounded model checking of compositional linear hy-brid automata.This paper proposes a mixed semantics which means enumer-ating candidate paths through step semantics and check reachability of these paths through shallow semantics.Firstly,encoding the discrete graph structure of com-positional automaton to SAT problem to traverse graph.Then checking reachability of the candidate path through linear programming.In order to reduce the number of paths traversed,this paper gives the definition of three atypical paths that are consistent under shallow synchronization semantics and different under traditional interleaving semantics.Meanwhile,the coding method for avoiding atypical paths in the path traversal phase is proposed in this paper.2.Multiple-IIS based bounded model checking of compositional linear hybrid au-tomata.IIS techniques can be used to reduce a large number of paths during graph structure traversal period,effectively mitigates path explosion problems.However,different IIS path segment performs very different on reducing paths.In order to take advantage of IIS to reduce more paths,this paper proposes shared label cut based multiple IIS location techniques.This method uses multiple IIS techniques to extract multiple IIS paths from an unsatisfiable constraint set.Then,in order to locate the extracted IIS path to a more precise range,we propose a shared la-bel cut based IIS locating method.This method abstracts IIS on different subpaths by splitting the path through shared label.We implement this method and exper-imented with benchmarks that are widely used in the industry.The experimental results show that the scale of the verification has been greatly improved,and the performance is better than the relevant tools in the field.3.IIS path based unbounded reachability proof of compositional linear hybrid automata.The above method has made some progress in bounded model check-ing of compositional linear hybrid automata,but in practice,it is often necessary to check the unbounded specification of systems.This paper proposes an IIS path based method which derives unbounded reachability of compositional linear hy-brid automata during bounded model checking procedure.Firstly,we design an algorithm to transform IIS path to LTL specification.Secondly,we transform three kinds of atypical paths to LTL specification to avoid them.However,this method will generate a huge LTL specificaiton so that solver cannot work out in effective time.Aiming to this problem,we propose a localization method of LTL specifica-tion.When the system model satisfies this form of LTL protocol proposed by the method,our method can give an unbounded proof.In many widely used bench-marks,our method can get unbounded proof result in short time.