Verifying hybrid systems modeled as timed automata: A case study

Verifying properties of hybrid systems can be highly complex. To reduce the effort required to produce a correct proof, the use of mechanical verification techniques is promising. Recently, we extended a mechanical verification system, originally developed to reason about deterministic real-time automata, to verify properties of hybrid systems. To evaluate our approach, we applied our extended proof system to a solution, based on the Lynch-Vaandrager timed automata model, of the Steam Boiler Controller problem, a hybrid systems benchmark. This paper reviews our mechanical verification system, which builds on SRI's Prototype Verification System (PVS), and describes the features we added to handle hybrid systems. It also discusses some errors we detected in applying our system to the benchmark problem. We conclude with a summary of insights we acquired in using our system to specify and verify hybrid systems.