Research On Optimization Techniques For Bounded Model Checking Of Hybrid Systems  Posted on:20170506  Degree:Doctor  Type:Dissertation  Country:China  Candidate:D B Jie  Full Text:PDF  GTID:1108330485974105  Subject:Computer Science and Technology  Abstract/Summary:  PDF Full Text Request  Hybrid system is a dynamical system that exhibits both discrete and continuous behavior and are widely used for modeling industrial controller systems. Hybrid automata are the most studied formal language for modeling hybrid system. Bounded model checking (BMC) of hybrid automata is an important way to guarantee the reliability 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 pathoriented 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 pathoriented BMC has improved the size if the system that can be checked substantially, it needs effective optimization techniques to further control the complexity of problems when facing largescale industrial systems.Based on pathoriented 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 contribution of this work addresses the following aspects:● We propose a SATHSLP joint directed solution to reduce the state space under checking. First encode the discrete directed graph into SAT formulas to detect infeasible 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 pathoriented BMC procedure. We only needto enumerate paths which do not contain any detected infeasible path segment in the followup traversing, thus reducing the state space. The experiment shows the proposed solution improves the performance and scalability of the pathoriented BMC approach significantly.● We propose a composed IIS path locating based traversing optimization technique 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 system 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 compositional linear hybrid systems.● We propose a technique that can derive an unbounded proof argument based on a BMC procedure. During pathoriented 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 pathoriented BMC approach and optimization technique for nonlinear hybrid automata. By translating the path feasibility problem to the satisfiability 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 locate 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.  Keywords/Search Tags:  Hybrid System, Linear Hybrid Automata, Nonlinear Hybrid Automa ta, Bounded Reachability Analysis, SATBased Path Traversing, Satisfiability Modulo Theories, Linear Temporal Logic, Irreducible Infeasible Subset  PDF Full Text Request  Related items 
 
