DocumentCode
3557369
Title
Extended abstract: organizing automaton specifications to achieve faithful representation
Author
Leonard, Elizabeth ; Archer, Myla
Author_Institution
Center for High Assurance Comput. Syst., Naval Res. Lab., Washington, DC, USA
fYear
2005
fDate
11-14 July 2005
Firstpage
245
Lastpage
246
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.
Keywords
automata theory; formal specification; formal verification; security of data; IEEE 1394; SELinux security policies; TESLA protocol; automaton specification; formal verification; leader election protocol; reference variable approach; Access protocols; Application software; Authentication; Automata; History; Laboratories; Multicast protocols; Operating systems; Organizing; USA Councils;
fLanguage
English
Publisher
ieee
Conference_Titel
Formal Methods and Models for Co-Design, 2005. MEMOCODE '05. Proceedings. Third ACM and IEEE International Conference on
Print_ISBN
0-7803-9227-2
Type
conf
DOI
10.1109/MEMCOD.2005.1487925
Filename
1487925
Link To Document