Verifying hybrid systems modeled as timed automata: A case study
Myla M. Archer, Constance Heitmeyer · 1997
Abstract. Verifying properties of hybrid systems can be highly complex. To reduce the e ort required to produce a correct proof, the use of mechanical veri cation techniques is promising. Recently, we extended a mechanical veri cation 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 veri cation system, which builds on SRI's Prototype Veri cation 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. 1