Reusable PVS Proof Strategies for Proving Abstraction Properties of I/O Automata
Abstract
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jul 04, 2004
- Accession Number
- ADA465029
Entities
People
- Myla Archer
- Sayan Mitra
Organizations
- Massachusetts Institute of Technology