Extended abstract: organizing automaton specifications to achieve faithful representation

E. Leonard; M. Archer

doi:10.1109/MEMCOD.2005.1487925

Previous
Next
Table of Contents

Formal Methods and Models for Co-Design, ACM/IEEE International Conference on

Extended abstract: organizing automaton specifications to achieve faithful representation

Year: 2005, Pages: 245-246

DOI Bookmark: 10.1109/MEMCOD.2005.1487925

Authors

E. Leonard, Center for High Assurance Comput. Syst., Naval Res. Lab., Washington, DC, USA
M. Archer, Center for High Assurance Comput. Syst., Naval Res. Lab., Washington, DC, USA

Abstract

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.

Like what you’re reading?

Already a member?

Get this article FREE with a new membership!