Towards Concolic Testing for Hybrid Systems
This work addresses the problem of verifying hybrid systems, which is crucial for safety-critical applications like water treatment, but it appears incremental as it builds on existing concolic testing ideas.
The paper tackled the challenge of verifying hybrid systems by combining random sampling and symbolic execution, proposing an algorithm that dynamically switches between them to reduce cost and implementing it in a tool called HyChecker, which was evaluated on benchmark systems and a water treatment system.
Hybrid systems exhibit both continuous and discrete behavior. Analyzing hybrid systems is known to be hard. Inspired by the idea of concolic testing (of programs), we investigate whether we can combine random sampling and symbolic execution in order to effectively verify hybrid systems. We identify a sufficient condition under which such a combination is more effective than random sampling. Furthermore, we analyze different strategies of combining random sampling and symbolic execution and propose an algorithm which allows us to dynamically switch between them so as to reduce the overall cost. Our method has been implemented 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.