PVS strategies for proving abstraction properties of automata

Sayan Mitra, Myla Archer

Research output: Contribution to journalConference articlepeer-review

Abstract

Abstractions are important in specifying and proving properties of complex systems. To prove that a given automaton implements an abstract specification automaton, one must first find the correct abstraction relation between the states of the automata, and then show that this relation is preserved by all corresponding action sequences of the two automata. This paper describes tool support based on the PVS theorem prover that can help users accomplish the second task, in other words, in proving a candidate abstraction relation correct. This tool support relies on a clean and uniform technique for defining abstraction properties relating automata that uses library theories for defining abstraction relations and templates for specifying automata and abstraction theorems. The paper then describes how the templates and theories allow development of generic, high level PVS strategies that aid in the mechanization of abstraction proofs. These strategies first set up the standard subgoals for the abstraction proofs and then execute the standard initial proof steps for these subgoals, thus making the process of proving abstraction properties in PVS more automated. With suitable supplementary strategies to implement the "natural" proof steps needed to complete the proofs of any of the standard subgoals remaining to be proved, the abstraction proof strategies can form part of a set of mechanized proof steps that can be used interactively to translate high level proof sketches into PVS proofs. Using timed I/O automata examples taken from the literature, this paper illustrates use of the templates, theories, and strategies described to specify and prove two types of abstraction property: refinement and forward simulation.

Original languageEnglish (US)
Pages (from-to)45-65
Number of pages21
JournalElectronic Notes in Theoretical Computer Science
Volume125
Issue number2
DOIs
StatePublished - Mar 15 2005
Externally publishedYes
EventProceedings of the 5th International Workshop on Strategies in Automated Deduction -
Duration: Jul 4 2004Jul 4 2004

Keywords

  • Abstraction
  • Forward Simulation
  • I/O Automata
  • Mechanical Theorem Proving
  • Refinement
  • Strategies

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'PVS strategies for proving abstraction properties of automata'. Together they form a unique fingerprint.

Cite this