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...

Full description

Saved in:
Bibliographic Details
Main Author: Kong, Pingfan
Other Authors: Liu Yang
Format: Theses and Dissertations
Language:English
Published: 2016
Subjects:
Online Access:https://hdl.handle.net/10356/65915
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Nanyang Technological University
Language: English
id sg-ntu-dr.10356-65915
record_format dspace
spelling sg-ntu-dr.10356-659152023-03-04T00:47:06Z Probabilistic model checking for hybrid systems with hybrid concolic testing and importance sampling Kong, Pingfan Liu Yang School of Computer Engineering Parallel and Distributed Computing Centre DRNTU::Engineering::Computer science and engineering::Mathematics of computing::Probability and statistics DRNTU::Engineering::Computer science and engineering::Theory of computation::Mathematical logic and formal languages 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) 2016-01-15T02:01:27Z 2016-01-15T02:01:27Z 2016 Thesis Kong, P. (2016). Probabilistic model checking for hybrid systems with hybrid concolic testing and importance sampling. Master's thesis, Nanyang Technological University, Singapore. https://hdl.handle.net/10356/65915 10.32657/10356/65915 en 44 p. application/pdf
institution Nanyang Technological University
building NTU Library
continent Asia
country Singapore
Singapore
content_provider NTU Library
collection DR-NTU
language English
topic DRNTU::Engineering::Computer science and engineering::Mathematics of computing::Probability and statistics
DRNTU::Engineering::Computer science and engineering::Theory of computation::Mathematical logic and formal languages
spellingShingle DRNTU::Engineering::Computer science and engineering::Mathematics of computing::Probability and statistics
DRNTU::Engineering::Computer science and engineering::Theory of computation::Mathematical logic and formal languages
Kong, Pingfan
Probabilistic model checking for hybrid systems with hybrid concolic testing and importance sampling
description 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.
author2 Liu Yang
author_facet Liu Yang
Kong, Pingfan
format Theses and Dissertations
author Kong, Pingfan
author_sort Kong, Pingfan
title Probabilistic model checking for hybrid systems with hybrid concolic testing and importance sampling
title_short Probabilistic model checking for hybrid systems with hybrid concolic testing and importance sampling
title_full Probabilistic model checking for hybrid systems with hybrid concolic testing and importance sampling
title_fullStr Probabilistic model checking for hybrid systems with hybrid concolic testing and importance sampling
title_full_unstemmed Probabilistic model checking for hybrid systems with hybrid concolic testing and importance sampling
title_sort probabilistic model checking for hybrid systems with hybrid concolic testing and importance sampling
publishDate 2016
url https://hdl.handle.net/10356/65915
_version_ 1759855933742120960