TitleVerifying Hybrid Systems Modeled as Timed Automata: A Case Study
Publication TypeConference Paper
Year of Publication1997
AuthorsArcher, M., and C. L. Heitmeyer
Conference NameHART
Conference LocationGrenoble, France
Abstract

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.

Full Text

ArcherHeitmeyer1997b.pdf

NRL Publication Release Number

06-1221.1-2930