|Title||Reusable PVS Proof Strategies for Proving Abstraction Properties of I/O Automata|
|Publication Type||Conference Paper|
|Year of Publication||2004|
|Authors||Mitra, S., and M. Archer|
|Conference Name||Fourth International Workshop on Strategies in Automated Deduction (STRATEGIES 2004)|
|Conference Location||Cork, 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.
|NRL Publication Release Number|| |