-----------------------------------------------------------------------
TDS Seminar TDS Seminar TDS Seminar TDS Seminar TDS Seminar TDS Seminar
-----------------------------------------------------------------------

Title:   On Developing A PVS Interface for Abstraction Proofs

Speaker: Sayan Mitra

Place:   NE43-308
Time:    1-2:30pm
Date:    Sept. 19, 2003

Abstract:
                                                   
The Timed Automaton Modeling Environment (TAME) has been developed at
NRL to facilitate specification and verification of timed systems.  It
is a prover interface for PVS;  it consists of (1) a set of theories
which help users specify timed automata, and (2) a set of strategies
which simplify invariant proofs for timed automata. TAME has been
successfully used to verify timed and untimed I/O automata. In this talk
I will discuss the work I did at NRL this summer for extending TAME to
support abstraction proofs. In short, we developed some new theories and
strategies for supporting refinement proofs, and tried these strategies
on two simple examples. As background for this work I will briefly
describe PVS, PVS  strategies, and TAME.