HyChecker

Hybrid systems exhibit both continuous and discrete behavior. They are hard to analyze, as they can both flow (described by differential equations) and jump (described by program-like statements). Many real-world systems including the so-called cyber-physical systems can be categorized as hybrid systems. In this work, we propose to analyze hybrid systems using a combination of random sampling and symbolic execution, which we refer to as concolic sampling. We formally prove that such a combination is more effective than random sampling. Furthermore, we analyze the cost of different sampling methods and propose to dynamically switch between random sampling and symbolic execution so as to reduce the overall cost. Our method has been implemented and made available as a web-based checker named HyChecker . HyChecker has been evaluated with benchmark hybrid systems and a water treatment system in order to test its effectiveness.

For experiments details, please visit Here.

For each benchmark source codes, please visit the links below:

Thermodynamic, Navigation, Traffic, SWaT.

For viewing HyChecker tool source codes, please visit Here.

For downloading HyChecker source codes, please visit Here.

For try with HyChecker online verison, visit Here. (In case of server unstable, please visit Here.)