Research On Optimization Techniques For Bounded Model Checking Of Hybrid Systems

Hybrid system is a dynamical system that exhibits both discrete and continuous behavior and are widely used for modeling industrial controller systems. Hybrid au-tomata are the most studied formal language for modeling hybrid system. Bounded model checking (BMC) of hybrid automata is an important way to guarantee the re-liability and safety of systems. The basic idea of BMC of hybrid automata is to use SMT (Satisfiability Modulo Theories) techniques to encode the behavior of the system within the threshold into a constraint set and then solve it to check whether the system satisfies the given property. However, as the technique needs to encode the whole state space within the bound firstly, the high complexity restricts the size of the system that can be handled. It is difficult to apply the SMT based technique to industrial systems. Another way to solve the problem is to split the BMC problem of a given hybrid system into several path-oriented reachability problems of each path to control the verification complexity. Based on it, we can enumerate and check all the potential paths to conduct BMC of the whole system. Although the path-oriented BMC has improved the size if the system that can be checked substantially, it needs effective optimization tech-niques to further control the complexity of problems when facing large-scale industrial systems.Based on path-oriented BMC of hybrid systems, in this paper, we tackle problems aimed at optimization techniques for bounded reachability analysis of hybrid systems, including state space reduction, optimized traversing of compositional systems, BMC based global property derivation, verification of nonlinear systems. The main contri-bution of this work addresses the following aspects:● We propose a SAT-HS-LP joint directed solution to reduce the state space under checking. First encode the discrete directed graph into SAT formulas to detect in-feasible paths as early as possible. Then we can locate an infeasible path segment from an infeasible path using irreducible infeasible subset (IIS) technique during the path-oriented BMC procedure. We only need-to enumerate paths which do not contain any detected infeasible path segment in the follow-up traversing, thus reducing the state space. The experiment shows the proposed solution improves the performance and scalability of the path-oriented BMC approach significantly.● We propose a composed IIS path locating based traversing optimization tech-nique for compositional linear hybrid system. By encoding the discrete graph with SMT formulas and then solving it, we can enumerate candidate path sets obeying synchronization condition in the graph structure of compositional sys-tem quickly. We propose to locate a composed infeasible path segment from an infeasible path set based on path synchronization semantic and avoid paths containing such composed infeasible path segments. The experiment shows the proposed approach improves the performance of the BMC approach of compo-sitional linear hybrid systems.● We propose a technique that can derive an unbounded proof argument based on a BMC procedure. During path-oriented BMC of LHA, we can collect a set of infeasible path segments. We find that there may not exist any potentia path to reach the target location when collecting enough infeasible path segments. In this case, the BMC unreachable result can be further extended to global state space, which can be proved automatically using a Linear Temporal Logic (LTL) based approach.● We propose a path-oriented BMC approach and optimization technique for non-linear hybrid automata. By translating the path feasibility problem to the satisfi-ability of a quantified nonlinear constraint set, we can check it with a nonlinear constraint solver. Based on it, we can tackle the BMC problem by enumerating potential paths with depth first search and checking it. Furthermore, we propose an IIS analysis algorithm for nonlinear constrain set, which can be utilized to lo-cate an infeasible path segment from an infeasible path to reduce the state space. Limited by the ability of current underlying tool and nonlinear constraint solver, we can only validate the viability of the proposed approach. The effectiveness of the approach remains further investigated.