Attributed Automata: A Formal Model for Protocol Specification

Attributed Automata: a Formal Model for Protocol Specification The report considers the concept of attributed automaton (AA) and its general properties from the viewpoint of software engineering. The main attention is paid to the possibilities of usage of AA for specification of distributed software systems. This is discussed on an example of modeling the alternating bit protocol. In this respect, the role of AA is to permit a formal model for reasoning about general properties of a concrete communication protocol as well as to give the implementable specifications of protocols. The implementation of AA model of the communication protocol in the NUT system is presented. Contents 1 Introduction 2 2 Attributed Automata 5 2.1 Definition and Properties of Attributed Automata : : : : : : 5 2.2 Expressive power of AA : : : : : : : : : : : : : : : : : : : : : 8 2.3 Systems of AA : : : : : : : : : : : : : : : : : : : : : : : : : : 8 3 Modeling of Alternating Bit Protocol 11 4 Modeling Prot..