Myla Archer: TAME: A Kinder, Gentler Version of PVS for Proving Properties of Automata

Abstract: TAME is a PVS interface that uses specification templates and special PVS strategies to simplify the process of specifying and proving properties of automata using PVS. An automatic SCR-to-TAME translator and strategies especially developed for proving properties of SCR automata make it possible for a user of the SCR toolset to prove many invariant properties of their specifications automatically. For more general automata, TAME supports interactive proofs of properties using proof steps similar to high level proof steps commonly used in hand proofs. As a result, TAME can be used to mechanically check informal hand proofs, and to create proofs that can be understood at a high level. The TAME strategies provide generic support for proving invariant properties of automata, and have been applied to many examples, most recently to the correctness proof of the basic version of the TESLA multicast stream authentication protocol. Development of generic support in TAME for proving simulation relations between automata is planned, but will require the completion of certain extensions to PVS.

CV: Myla Archer is a research computer scientist in the Software Engineering Section of the Center for High Assurance Computer Systems at NRL. Prior to coming to NRL in 1995, she taught mathematics at Wheaton College (Norton, MA) and was on the Computer Science Faculty at the University of California, Davis. Her research interests include formal methods, verification, theorem proving, computer security, and programming languages. She is the principal developer of TAME.