Extended abstract: organizing automaton specifications to achieve faithful representation

We have developed an approach to organizing automaton specifications in which a reference variable captures the essential state and shadow variables are used to facilitate expressiveness. We have applied our approach in specifying automaton models for three different examples: TESLA protocol, SELinux security policies and leader election for IEEE 1394. In all three cases the resulting specification bears an obvious close relationship to the actual system being modeled.