TitleReusable PVS Proof Strategies for Proving Abstraction Properties of I/O Automata
Publication TypeConference Paper
Year of Publication2004
AuthorsMitra, S., and M. Archer
Conference NameFourth International Workshop on Strategies in Automated Deduction (STRATEGIES 2004)
Conference LocationCork, Ireland

Recent modifications to PVS support a new technique for defining abstraction properties relating automata in a clean and uniform way. This definition technique employs specification templates that can support development of generic high level PVS strategies that set up the standard subgoals of these abstraction proofs and then execute the standard initial proof steps for these subgoals. In this paper, we describe an abstraction specification technique and associated abstraction proof strategies we are developing for I/O automata. The new strategies can be used together with existing strategies in the TAME (Timed Automata Modeling Environment) interface to PVS; thus, our new templates and strategies provide an extension to TAME for proofs of abstraction. We illustrate how the extended set of TAME templates and strategies can be used to prove example I/O automata abstraction properties taken from the literature.

Full Text


NRL Publication Release Number