Bounded Model Checking of Hybrid Automata Pushdown System

Model checking has been successfully used for checking model design where the specification is given by a temporal logic formula. In this paper, we develop an approach to bounded model checking Linear Temporal Logic (LTL) properties of Hybrid Automata Pushdown System (HAPS) over finite traces. Such HAPS models are suitable formal representations for Cyber/Physical co-verification, verifying software controller with controlled plant together. We convert the LTL formula into a C program, which is interleaved with the execution of the HAPS under analysis. Our approach checks both safety and liveness uniformly within the framework of bounded model checking through symbolic execution. We have realized this approach and applied it to real-world control systems. The evaluation has shown that our approach has major potential in verifying system-level LTL properties of cyber-physical systems.