O'Reilly logo

Verification of Systems and Circuits Using LOTOS, Petri Nets, and CCS by Rakefet Kol, Michael Yoeli

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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 ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required