Hybrid Systems are well-known systems that are widely used in real-time and embed-ded systems. Hybrid Automata are the most commonly used formal language for modeling hybrid system. Researchers always prefer to guarantee the quality of the hybrid system by verifying the reachability property of the corresponding hybrid automaton. There are two basis methods for the reachability verification of hybrid automata:One is symbolic mod-el checking, whose idea is to get the reachable state space by iteratively using geometric computation. The other is bounded model checking, whose idea is to encode the bounded reachability problem into the satisfiability problem, then solve it by using SMT solver. Both of them are feeding the (partly) complete state space to the underlying solver at one time which restricts the size of the problem that can be solved.To control the complexity of single verification, a linear programming based approach had been proposed to check the reachability specification along one abstract path in a linear hybrid automaton (LHA) at a time by translating the reachability problem into the satisfia-bility problem of a linear constraint set. Then a depth-first-search (DFS) is deployed on the graph structure of the LHA to check all the paths with length under the threshold to answer the question of bounded reachability. Though the method has shown good performance and scalability, if the candidate paths to be checked are very huge, the method will still be time consuming. To solve this problem, we give several optimization methods shown as below:· IIS-Guided DFS for efficient bounded reachability analysis. By now, only the abstract path related with the reachability specification will be analyzed by the underlying LP solver. If the path is judged to be infeasible, the IIS technique will be deployed on the infeasible path to locate the path segment which makes this path infeasible to guide the backtracking of the DFS.·Bidirectional DFS for bounded reachability analysis. In many cases, the path segments which make the path infeasible are hidden "deeply" or have many entry points in the graph structure which makes the DFS difficult to find these path segments or has to traverse them time and time again. To solve this problem, we present a backward searching technique for the DFS-style traversing strategy and combine it with the clas-sical forward DFS in our bounded model checker to accelerate the DFS traversing.We implement the methods discussed above into our bounded model checker BACH and release a new version BACH(V4.0). Then compare it with several commonly used model checking tools. The results show that our tool has better performance and scalability. In many cases, our tool can prove the given specification is not satisfiable in general, not only in the given bound.On the other hand, as an extension of the hybrid systems, Cyber-Physical Systems(CPS) are more complex. Many CPS systems retrieve data for key control parameters from envi-ronment frequently while their system structures are highly dynamic as components may join and leave the system randomly. Clearly, the classical offline model checking technique can not handle such problems.Based on the previous methods and tool, we propose an online modeling and verification framework to build the model for the system’s time-bounded short-run future and verify it online to guarantee the safety of CPS. By taking advantage of incremental linear program-ming technique, we present an incremental verification method to accelerate the verification of each period. |