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.
Key Publication
Towards Concolic Testing for Hybrid Systems.
FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings.
People
