Provides a unified framework for the specification of communication protocols. This framework enables one to integrate different formalisms within algebraic specifications, permitting the description of the dynamic aspects of distributed systems, such as temporal logic, Petri nets and process algebra. These integrations provide different languages, allowing specifications which may include both the data aspects and the behavioral aspects of protocols. In addition, this paper gives a unified semantics for the different languages based on algebra and event structures. Finally, we illustrate our framework by specifying the Alternating Bit Protocol using the different behavioral formalisms.
展开▼