AN ALGEBRA OF REGULAR MACRONETS FOR FORMAL SPECIFICATION OF COMMUNICATION PROTOCOLS

The paper addresses the formal model for formal description techniques of communication protocols based on Petri nets. As a starting point we take an algebra of regular Petri nets (RPN) proposed by V. Kotov. This algebra is generalized in order to enhance an adequacy of protocol representation. A generalization of RPN called regular macronets (RMN) is described. We also define a set of operations on macronets which are generalizations of those in RPN. In particular, in order to describe such constructions as reset, restart, disconnection, etc., we introduce a new net operation called disruption. The notion of bisimulation equivalence is reformulated for RMNs. It is shown that this equivalence is a congruence with respect to all net operations. Finally, we give an informal comparison of our approach with related ones. We illustrate an application of the introduced formalism with the aid of the ISO transport protocol.