Verification of Systems and Circuits Using LOTOS, Petri Nets, and CCS

CHAPTER 8

Verification of Communication Protocols

8.1 INTRODUCTION

Communication protocols are intended to provide reliable communications over unreliable communication channels. In particular, we will be concerned with point-to-point unidirectional communication systems, transmitting messages from a Sender or Transmitter station to a Receiver station over an unreliable data channel. We assume that the Receiver station has facilities to confirm the receipt of a message, by sending an acknowledgement back to the Sender station over an acknowledge channel, which, in the general case, may also be unreliable.

We will assume various scenarios of possible failures, and indicate methods to overcome such failures. In particular, we are interested in verifying that the specified communication systems indeed provide reliable communication over the type of unreliable channels that we will specify in the sequel.

8.2 TWO SIMPLE COMMUNICATION PROTOCOLS

In Section 6.8.6 we introduced a very simple communication protocol (VSP), with the main purpose of illustrating the use of CCS and the associated Concurrency Workbench (CWB-NC). In this section we again use CCS and CWB-NC to present another simple communication protocol (SCP), which is a reduced version of the simple protocol used as the example in introducing CWB-NC (see Section 6.8). We also describe another version of this simple communication protocol (SCP1) based on Petri nets.

8.2.1 Simple Communication Protocol SCP

To become familiar with ...