Extended Abstract: Organizing Automaton Specifications to Achieve Faithful Representation
Abstract
In using models for verification, an important question is how faithful a model is to the thing modeled. In 2002 and 2003, we specified two applications as automaton models: the TESLA multicast stream authentication protocol and a portion of the Security-Enhanced Linux (SELinux) operating system. Both models used a single reference variable to capture essentially all of the information about the actual state of the system. Additional state variables in the models were defined to provide access to some of the reference variable information in a form that made specifying system transitions and reasoning about the system easier. Having used the same organizational approach to advantage in defining automaton models for two different applications, we wondered if this approach would have benefits in other applications. We decided to specify the well-known IEEE 1394 leader election algorithm (Tree Identify Protocol) using this modeling technique to see if it would provide any benefit.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 2005
- Accession Number
- ADA465569
Entities
People
- Elizabeth Leonard
- Myla M. Archer
Organizations
- United States Naval Research Laboratory