Protocol engineering

Protocol engineering is the application of systematic methods to the development of communication protocols. It uses many of the principles of software engineering, but it is specific to the development of distributed systems.

History

When the first experimental and commercial computer networks were developed in the 1970s, the concept of protocols was not yet well developed. These were the first distributed systems. In the context of the newly adopted layered protocol architecture (see OSI model), the definition of the protocol of a specific layer should be such that any entity implementing that specification in one computer would be compatible with any other computer containing an entity implementing the same specification, and their interactions should be such that the desired communication service would be obtained. On the other hand, the protocol specification should be abstract enough to allow different choices for the implementation on different computers.

It was recognized that a precise specification of the expected service provided by the given layer was important.^[1] It is important for the verification of the protocol, which should demonstrate that the communication service is provided if both protocol entities implement the protocol specification correctly. This principle was later followed during the standardization of the OSI protocol stack, in particular for the transport layer.

It was also recognized that some kind of formalized protocol specification would be useful for the verification of the protocol and for developing implementations, as well as test cases for checking the conformance of an implementation against the specification.^[2] While initially mainly finite-state machine were used as (simplified) models of a protocol entity,^[3] in the 1980s three formal specification languages were standardized, two by ISO ^[4] and one by ITU.^[5] The latter, called SDL, was later used in industry and has been merged with UML state machines.

Principles

Layered protocol architecture: More abstract view – showing the communication service provided.

The following are the most important principles for the development of protocols:^[1]

Layered architecture: A protocol layer at the level n consists of two (or more) entities that have a service interface through which the service of the layer is provided to the users of the protocol, and which uses the service provided by a local entity of level (n-1).
The service specification of a layer describes, in an abstract and global view, the behavior of the layer as visible at the service interfaces of the layer.
The protocol specification defines the requirements that should be satisfied by each entity implementation.
Protocol verification consists of showing that two (or more) entities satisfying the protocol specification will provide at their service interfaces the specified service of that layer.
The (verified) protocol specification is used mainly for the following two activities:

The development of an entity implementation. Note that the abstract properties of the service interface are defined by the service specification (and also used by the protocol specification), but the detailed nature of the interface can be chosen during the implementation process, separately for each entity.
Test suite development for conformance testing. Protocol conformance testing checks that a given entity implementation conforms to the protocol specification. The conformance test cases are developed based on the protocol specification and are applicable to all entity implementations. Therefore standard conformance test suites have been developed for certain protocol standards.^[3]

Methods and tools

Tools for the activities of protocol verification, entity implementation and test suite development can be developed when the protocol specification is written in a formalized language which can be understood by the tool. As mentioned, formal specification languages have been proposed for protocol specification, and the first methods and tools where based on finite-state machine models. Reachability analysis was proposed to understand all possible behaviors of a distributed system, which is essential for protocol verification. This was later complemented with model checking. However, finite-state descriptions are not powerful enough to describe constraints between message parameters and the local variables in the entities. Such constraints can be described by the standardized formal specification languages mentioned above, for which powerful tools have been developed.

It is in the field of protocol engineering that model-based development was used very early. These methods and tools have later been used for software engineering as well as hardware design, especially for distributed and real-time systems. On the other hand, many methods and tools developed in the more general context of software engineering can also be used of the development of protocols, for instance model checking for protocol verification, and agile methods for entity implementations.

Constructive methods for protocol design

Most protocols are designed by human intuition and discussions during the standardization process. However, some methods have been proposed for using constructive methods possibly supported by tools to automatically derive protocols that satisfy certain properties. The following are a few examples:

Semi-automatic protocol synthesis:^[6] The user defines all message sending actions of the entities, and the tool derives all necessary reception actions (even if several messages are in transit).
Synchronizing protocol:^[7] The state transitions of one protocol entity are given by the user, and the method derives the behavior of the other entity such that it remains in states that correspond to the former entity.
Protocol derived from service specification:^[8] The service specification is given by the user and the method derives a suitable protocol for all entities.
Protocol for control applications:^[9] The specification of one entity (called the plant - which must be controlled) is given, and the method derives a specification of the other entity such that certain fail states of the plant are never reached and certain given properties of the plant's service interactions are satisfied. This is a case of supervisory control.

Books

Ming T. Liu, Protocol Engineering, Advances in Computers, Volume 29, 1989, Pages 79-195.
G.J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, 1991.
H. König, Protocol Engineering, Springer, 2012.
M. Popovic, Communication Protocol Engineering, CRC Press, 2nd Ed. 2018.
P. Venkataram, S.S. Manvi, B.S. Babu, Communication Protocol Engineering, 2014.

References

^ ^a ^b G. v. Bochmann and C. A. Sunshine, Formal methods in communication protocol design, IEEE Tr. COM-28, No. 4 (April 1980), pp. 624-631.
^ See the series of conferences on Protocol Specification Testing and Verification (PSTV) since 1981.
^ ^a ^b G. v. Bochmann, D. Rayner and C. H. West, Some notes on the history of protocol engineering, Computer Networks journal, 54 (2010), pp 3197–3209.
^ C. A. Vissers, G. v. Bochmann and R. L. Tenney, Formal description techniques, Proceedings of the IEEE, vol. 71, 12, pp. 1356-1364, Dec. 1983.
^ G.J. Dickson ; P.E. de Chazal, Status of CCITT description techniques and application to protocol specification, Proceedings of the IEEE, vol. 71, 12, pp. 1346-1355 (1983).
^ P. Zafiropulo, C. West, H. Rudin, D. Cowan, D. Brand : Towards analyzing and synthesizing protocols, IEEE Transactions on Communications ( Volume: 28, Issue: 4, Apr 1980 )
^ M.G. Gouda and Y.T. Yu, Synthesis of communicating Finite State Machines with guaranteed progress, IEEE Trans. on Comm., vol. Com-32, No. 7, July 1984, pp. 779-788.
^ M.F. Al-hammouri and G.v. Bochmann, Realizability of service specifications, Proc. System Analysis and Modelling (SAM) conference 2018, Copenhagen, LNCS, Springer.
^ G. v. Bochmann, Using logic to solve the submodule construction problem, Journal on Discrete Event Dynamic Systems, Vol. 23 (1), Springer, March 2013, pp. 27-59.

[Boch1980-1] G. v. Bochmann and C. A. Sunshine, Formal methods in communication protocol design, IEEE Tr. COM-28, No. 4 (April 1980), pp. 624-631.

[2] See the series of conferences on Protocol Specification Testing and Verification (PSTV) since 1981.

[Boch2010-3] G. v. Bochmann, D. Rayner and C. H. West, Some notes on the history of protocol engineering, Computer Networks journal, 54 (2010), pp 3197–3209.

[4] C. A. Vissers, G. v. Bochmann and R. L. Tenney, Formal description techniques, Proceedings of the IEEE, vol. 71, 12, pp. 1356-1364, Dec. 1983.

[5] G.J. Dickson ; P.E. de Chazal, Status of CCITT description techniques and application to protocol specification, Proceedings of the IEEE, vol. 71, 12, pp. 1346-1355 (1983).

[6] P. Zafiropulo, C. West, H. Rudin, D. Cowan, D. Brand : Towards analyzing and synthesizing protocols, IEEE Transactions on Communications ( Volume: 28, Issue: 4, Apr 1980 )

[7] M.G. Gouda and Y.T. Yu, Synthesis of communicating Finite State Machines with guaranteed progress, IEEE Trans. on Comm., vol. Com-32, No. 7, July 1984, pp. 779-788.

[8] M.F. Al-hammouri and G.v. Bochmann, Realizability of service specifications, Proc. System Analysis and Modelling (SAM) conference 2018, Copenhagen, LNCS, Springer.

[9] G. v. Bochmann, Using logic to solve the submodule construction problem, Journal on Discrete Event Dynamic Systems, Vol. 23 (1), Springer, March 2013, pp. 27-59.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]