Extended Abstract: Organizing Automaton Specifications to Achieve Faithful Representation
NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
Pagination or Media Count:
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.
- Computer Programming and Software
- Computer Systems Management and Standards