by Mark Jorgensen, Christophe Discours, Hubert Garavel

Introduction

The aim of this page is to help the reader to discover the CADP toolbox as easily as possible through the EUCALYPTUS graphical user interface.

The CADP toolbox comes complete with a set of demonstrations that illustrate the different functionnalities of the toolset. You may find these demonstrations in the directory: $CADP/demos.

A lot of documentation is also provided in directory $CADP/doc. We recommend you read first the papers on LOTOS if you are not familiar with this language.

Getting Started

We will start off by using CADP on one of the demonstrations that are provided with the toolset. In this case, we will study the alternating bit protocol which is the basis of $CADP/demos/demo_02.

The first thing to do is to copy the directory containing the demonstration to a place where you can work on it, such as /tmp :

        cp -r $CADP/demos/demo_02 /tmp
        chmod -R +w+x /tmp/demo_02
        cd /tmp/demo_02

Next, start the EUCALYPTUS Graphical Interface.

        xeuca

The following window appears :

The left-hand window, where you can see icons representing the different files, present in the current directory is a contextual menu. In other words, if you click on a file, the different operations that are possible on this file appear in a menu. You choose the operation you want to do, by selecting it with the mouse, and the interface runs the different tools that enable the operation. The execution of the selected operation as well as the results of it appear in the right-hand window.

In this directory, you will find a LOTOS description of the alternating bit protocol in file bitalt_protocol.lotos. Our aim is to verify this protocol.

The alternating bit protocol

The purpose of this protocol is the sure transmission of data across a faulty network, where messages may be lost. This protocol belongs to the transport layer of the ISO model (Fourth layer). Seen from the layer above, this protocol assures a reliable transmission of Messages from T (Transmitter) to R (Receiver) : messages are never lost, and they are received in the same order they were sent.

The protocol consists in :
• the Receiver acknowledges every message it receives by sending an acknowledgement message.
• The messages contain a control bit. The control bit of an acknowledgement message is the same as the control bit of the message received.
• The control bit alternates every time a new message is sent.

To modelise this system in LOTOS, we will need four processes :

• The Receiver process receives the messages
• The Transmittrer process sends the messages
• The Medium1 process modelises the physical medium on which Data is sent from T to R. It may lose Messages. It may notify message loss to the Receiver.
• The Medium2 process modelises the physical medium on which Data is sent from R to T. It may lose Messages. It may notify message loss to the Transmitter.

The different communications between the processes are summarized in the following schematic :

Describing this system in LOTOS is straightforward. The description may be found in file bitalt_protocol.lotos :

specification ALTERNATING_BIT_PROTOCOL [PUT, GET] : noexit 
library BITALT endlib
behaviour
   hide SDT, RDT, RDTe, RACK, SACK, SACKe in
      (
         (
         TRANSMITTER [PUT, SDT, SACK, SACKe] (0 of BIT)
         |||
         RECEIVER [GET, RDT, RDTe, RACK] (0 of BIT)
         )
      |[SDT, RDT, RDTe, RACK, SACK, SACKe]|
         (
         MEDIUM1 [SDT, RDT, RDTe]
         |||
         MEDIUM2 [RACK, SACK, SACKe]
         )
      )

where
(*---------------------------------------------------------------------------*)
   process TRANSMITTER [PUT, SDT, SACK, SACKe] (B:BIT) : noexit :=
      PUT ?M:MSG;            (* A message has been received from the higher layer *) 
         TRANSMIT [PUT, SDT, SACK, SACKe] (B, M)
   where
      process TRANSMIT [PUT, SDT, SACK, SACKe] (B:BIT, M:MSG) : noexit :=
         SDT !M !B;           (* send the message *)
            (
            SACK !B;          (* correct control bit *)
               TRANSMITTER [PUT, SDT, SACK, SACKe] (not (B))
            []
            SACK !(not (B));  (* uncorrect control bit => retransmission *)
               TRANSMIT [PUT, SDT, SACK, SACKe] (B, M)
            []
            SACKe;            (* The message has been lost => retransmission *)
               TRANSMIT [PUT, SDT, SACK, SACKe] (B, M)
            []
            i;                (* timeout => retransmission *)
               TRANSMIT [PUT, SDT, SACK, SACKe] (B, M)
            )
      endproc
   endproc

(*---------------------------------------------------------------------------*)

   process RECEIVER [GET, RDT, RDTe, RACK] (B:BIT) : noexit :=
      RDT ?M:MSG !B;          (* correct control bit*)
         GET !M;              (* deliver the message to the higher level*)
            RACK !B;          (* send a correct acknowledgment *)
               RECEIVER [GET, RDT, RDTe, RACK] (not (B))
      []
      RDT ?M:MSG !(not (B));  (* uncorrect control bit => *)
         RACK !(not (B));     (* send an uncorrect acknowledgement *)
            RECEIVER [GET, RDT, RDTe, RACK] (B)
      []
      RDTe;                   (* the message has been lost => *)
         RACK !(not (B));     (* send an uncorrect acknowledgement *)
            RECEIVER [GET, RDT, RDTe, RACK] (B)
      []
      i;                      (* timeout => *)
         RACK !(not (B));     (* send an uncorrect acknowledgement *)
            RECEIVER [GET, RDT, RDTe, RACK] (B)
   endproc
   
(*---------------------------------------------------------------------------*)

   process MEDIUM1 [SDT, RDT, RDTe] : noexit :=
      SDT ?M:MSG ?B:BIT;   (* reception of a message *)
         (
         RDT !M !B;        (* correct transmission *)
            MEDIUM1 [SDT, RDT, RDTe]
         []
         RDTe;             (* loss with warning *)
            MEDIUM1 [SDT, RDT, RDTe]
         []
         i;                (* silent loss *)
            MEDIUM1 [SDT, RDT, RDTe]
         )
   endproc

(*---------------------------------------------------------------------------*)

   process MEDIUM2 [RACK, SACK, SACKe] : noexit :=
      RACK ?B:BIT;   (* reception of an acknowledgement *)
         (
         SACK !B;    (* correct transmission *)
            MEDIUM2 [RACK, SACK, SACKe]
         []
         SACKe;      (* loss with warning *)
            MEDIUM2 [RACK, SACK, SACKe]
         []
         i;          (* silent loss *)
            MEDIUM2 [RACK, SACK, SACKe]
         )
   endproc

endspec

We would like to check that this protocol fulfills its task which is the reliable transmission of messages. This service we expect from the protocol can be expressed in LOTOS, as follows (file bitalt_service.lotos):

specification ALTERNATING_BIT_SERVICE [PUT, GET] : noexit 
library BITALT endlib
behaviour
   SERVICE [PUT, GET]
where
   process SERVICE [PUT, GET] : noexit :=
      PUT ?M:MSG;  (* send the message *)
         GET !M;   (* receive the message *)
            SERVICE [PUT, GET]
   endproc
endspec

The CADP toolbox enables us to check that the first lotos description bitalt_protocol.lotos is equivalent to the service we expect from the protocol bitalt_service.lotos. We will now see how to do so.

Step 1 : LTS generation

First we generate the LTS (Labelled Transition System) corresponding to the protocol from the bitalt_protocol.lotos file. To do so, just click on the icon representing the file, and choose "Generate labelled transition system...".

The following window appears. In this window click on OK.

During the generation, a status window pops up and indicates how far the generation has reached. Once the generation is completed, click on the "done" button in this window to carry on.

Step 2 : LTS Visualization

A file called bitalt_protocol.bcg is created: it contains the LTS. We may visualise this LTS, just click on Visualise / Draw in 2 Dimensions.

This will show you the following graph:

As you can see, the LTS has many states and transitions, so the graph is very dense. We can try to simplify the graph, which we will do in the next step.

Step 3 : LTS reduction

To reduce the LTS, just click on the file containing the LTS, (bitalt_protocol.bcg) and select Reduce... .

The following window appears :

In this window, you may choose the tool you want to use to reduce the LTS (Aldebaran or Fc2tools), you may choose the algorithm to use, and the equivalence to use for the reduction.

As far as our demonstration goes, select:

• Aldebaran for the tool to use
• Strong Equivalence for the comparison relation
• Standard for the decision method.

If instead we choose the following parametres:

• Aldebaran for the tool to use
• Observationnal Equivalence for the comparison relation
• Standard for the decision method.

While this graph is simpler than the previous ones, its visualisation is still not obvious. We may edit it to look nicer, by clicking on Visualise / Edit in 2 Dimensions.

Step 4 : LTS generation

Go back to step 1, and generate this time the LTS for file bitalt_service.lotos. This LTS is very small, so we won't need to reduce it.

Step 5 : LTS comparison

Now we will compare the LTS representing the protocol with the LTS representing the service we expect from it. To do so just click on the file bitalt_protocol_bmin.bcg and select Compare... .

The following window appears:

In this window, you may choose the tool you want to use to compare the LTS (Aldebaran or Fc2tools), you may choose the algorithm to use (Decision Method: Standard, Binary Decision Diagrams ...), and the relation to use for the comparison (Strong Equivalence Bisimulation, Observationnal equivalence bisimulation, ...), and you may choose the LTS you want to compare the current LTS to. As far as our demonstration goes, select:

• bitalt_service.bcg for the LTS to compare to.
• Aldebaran for the tool to use
• Observationnal Equivalence for the comparison relation
• Standard for the decision method.

and then click on OK. The result of the comparison appears on the right-hand window :



The result is TRUE, which means that the protocol renders the expected service.