TitleExtended Abstract: Organizing Automaton Specifications to Achieve Faithful Representation
Publication TypeConference Paper
Year of Publication2005
AuthorsLeonard, E., and M. Archer
Conference NameThird ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'05)
Conference LocationVerona, Italy
Abstract

This extended abstract describes a general technique for organizing an automaton model of a system (or protocol) that is useful in the context of theorem proving, which we call the reference variable method. In this technique, a (usually complex) reference variable is used to capture the state. In cases when reasoning about the reference variable directly is complicated, auxiliary, shadow variables with provable relationships to the reference variable are used in formalizing properties of the automaton. The shadow variables are updated simultaneously with the reference variable when state transitions occur, and invariants are used to establish the relationships maintained. Proofs of properties relating shadow variables can often be done in an abstraction that omits the reference variable. This technique produces a natural specification in which the connection of the system model to the actual system is clear, and can be useful even when shadow variables are not used. Particularly when shadow variables are used, the technique provides the advantage that different abstractions can be related easily to ensure that they are abstractions of the same system. To illustrate the potential usefulness of the technique, we describe how we applied it in three examples.

Full Text

LeonardArcher2005.pdf

NRL Publication Release Number

05-1226-2046