Analysis of communication protocols via protocol projections
A. Udaya Shankar · 1982
The method of projections is presented as a new approach to reduce the complexity of analyzing nontrivial communication protocols. A protocol system consists of protocol entities that interact by exchanging messages through communication channels. Our method provides an approach to break up a protocol analysis problem into smaller analysis problems, and is intended for protocols with several distinguishable functions. A faithful image protocol is constructed for each function by individually examining the entities of the original protocol system. An image protocol system is specified just like a real protocol, and is said to be faithful if it preserves all safety and liveness properties of the original protocol system concerning the projected function. Image protocols are simpler than the original protocol and can thus be more easily analyzed. The method is first described using an abstract protocol model in which protocol entities are specified by states and state transitions. Then, we describe a protocol model in which the entities are specified by programs. For this model faithful image protocols can be constructed easily without having to examine individual state transitions (in most cases). Thus, the model can be applied to complex multi-function protocols. The model includes real-life protocol features such as multi-field messages and timers to realize time-dependent logical behavior. We use this model to specify and verify a version of the High-level Data Link Control (HDLC) protocol. The HDLC protocol specified uses the basic repertoire of HDLC commands and responses (except for the CMDR response), and includes poll/final cycles for connection management and checkpointing, sliding windows for data transfer, and ready/not ready messages for flow control. The HDLC protocol has three distinguishable functions: connection management, and one-way data transfers between the protocol entities. For each of these functions, we construct an image protocol and obtain inductively complete invariant assertions that state various desirable logical safety properties. We then show that by introducing a minor modification to HDLC, it can be made well-structured and faithful image protocols of a much smaller size can be constructed for each of these functions.