Probabilistic model checking for hybrid systems with hybrid concolic testing and importance sampling

Hybrid systems are dynamic systems that exhibit both continuous and discrete behavior. Many real-world engineering problems can be categorized as hybrid systems, including part of the typical cyber-physical systems. Hybrid systems are known to be hard to analyze and verify as they can both flow with differential equation dynamics and jump like a control graph or similar to program statements. In this master thesis, we investigate the problem of systematically analyzing hybrid systems and build a tool accordingly. Through investigation of related papers, we discover that there are two major problems that arise from hybrid system characteristics. One is to decide the time points when mode jumps happen. This often needs solving the ordinary differential equations with specific guard conditions. It can always be time-consuming with absence of closed form value state functions. The other obstacle lies in the fact that the set of hybrid automata trajectories is often too large. So it is not easy to achieve completeness while checking Bounded Linear Temporal Logic (BLTL) formulas against it. In previous work, a method for analyzing the dynamics of a hybrid automaton H in terms of a Markov Chain M was proposed. Our new algorithm is based on this method. We stress our new algorithm on the problem of rare events with which traditional statistical methods are often hard to deal. We implement our algorithm in a parallel manner to accelerate computing on multi-core machines and compare traces generated by different cores to decide if there exists any guard condition that was never satisfied. Borrowing the idea of hybrid concolic testing in program verification, we call dReach to test this guard's satisfiability. We developed a new importance sampling mechanism based on the satisfiable region retrieved by dReach to improve our efficiency of random testing. We built this new hybrid system checker by the name of HyChecker. We tested several hybrid systems with our tool. Our experiments show that HyChecker has higher efficiency in finding counterexamples without altering the original probabilistic guarantee.MASTER OF ENGINEERING (SCE