TAME: Using PVS strategies for special-purpose theorem proving

TAME (Timed Automata Modeling Environment), an interface to the theorem pro ving system PVS, is designed for proving properties of three classes of aut omata: I/O automata, Lynch-Vaandrager timed automata, and SCR automata. TAM E provides templates for specifying these automata, a set of auxiliary theo ries, and a set of specialized PVS strategies that rely on these theories a nd on the structure of automata defined using the templates. Use of the TAM E strategies simplifies the process of proving automaton properties. partic ularly state and transition invariants. TAME provides two types of strategi es: strategies for "automatic" proof and strategies designed to implement " natural" proof steps, i.e., proof steps that mimic the high-level steps in typical natural language proofs. TAME's "natural" proof steps can be used b oth to mechanically check hand proofs in a straightforward way and to creat e proof scripts that can he understood without executing them in the PVS pr oof checker. Several new PVS features can be used to obtain better control and efficiency in user-defined strategies such as those used in TAME. This paper describes the TAME strategies, their use, and how their implementatio n exploits the structure of specifications and various PVS features, It als o describes several features, currently unsupported in PVS. that would eith er allow additional "natural" proof steps in TAME or allow existing TAME pr oof steps to be improved. Lessons learned from TAME relevant to the develop ment of similar specialized interfaces to PVS or other theorem provers are discussed.