TitleTAME: A Specialized Specification and Verification System for Timed Automata
Publication TypeConference Paper
Year of Publication1996
AuthorsArcher, M., and C. L. Heitmeyer
Conference NameWork in Progress session at RTSS
Conference LocationWashington, D.C.
Abstract

Assuring the correctness of specifications of real-time systems can involve significant human effort. The use of a mechanical theorem prover to encode such specifications and to verify their properties could significantly reduce this effort. A barrier to routinely encoding and mechanically verifying specifications has been the need first to master the specification language and logic of a general theorem proving system. Our approach to overcoming this barrier is to provide mechanical support for producing specifications and verifying proofs, specialized for particular mathematical models and proof techniques. We are currently developing a mechanical verification system called TAME (Timed Automata Modeling Environment) that provides this specialized support using SRI's Prototype Verification System (PVS). Our system is intended to permit steps in reasoning similar to those in hand proofs that use model-specific techniques. TAME has recently been used to detect errors in a realistic example.

Full Text

ArcherHeitmeyer1996b.pdf

NRL Publication Release Number

06-1221.1-2932