Applying TAME to I/O Automata: A User's Perspective
Abstract
Mechanical theorem provers have been shown to expose proof errors, some of them serious, that humans miss. Mechanical provers will be applied more widely if they are easier to use. The tool TAME (Timed Automata Modeling Environment) provides an interface to the prover PVS to simplify specifying and proving properties of automata models. Originally designed for reasoning about Lynch-Vaandrager (LV) timed automata, TAME has since been adapted to other automata models. This paper shows how TAME can be used to specify and verify properties of I/O automata, a class of untimed automata. It also describes the experiences of a new TAME user (the first author) who used TAME to check Lamport-style hand proofs of invariants for two applications: Romijn's solution to the RPC-Memory Problem and the verification by Devillers et. al. of the tree identify phase of the IEEE 1394 bus protocol. For the latter application, the TAME mechanization of the hand proofs is compared with the more direct PVS proofs. Improvements to TAME in response to user feedback are discussed.
Document Details
- Document Type
- Technical Report
- Publication Date
- Apr 10, 2000
- Accession Number
- ADA375903
Entities
People
- Constance Heitmeyer
- Elvinia Riccobene
- Myla M. Archer
Organizations
- United States Naval Research Laboratory