Lecture 5

 

Introductory Applications

 

In this lecture we illustrate how BLA as well as LOTOS/CADP may be applied to the verification of digital systems.

 

5.1          The “Very Simple Protocol” Again

 

We introduced the above protocol informally in Lecture1. Now let us formalize our approach, using BLA first. We define:

 

PSEND = *[PUT;msg;ack]

PREC = *[msg;GET;ack]

SPROT = PSEND || PREC

 

We wish to show that SPROT\{msg,ack} == *[PUT;GET].

Here, ‘\’ is the hiding operator. P\L is obtained from the process P by replacing all the actions in L (a subset of Act(P)) by ‘i’.

 

Using BLA we may proceed as follows.

                 SPROT= PSEND || PREC =

                           PUT;*[msg;ack;PUT] || PREC =

                           PUT;msg;(*[ack;PUT;msg] || *[GET;ack;msg])=

                           PUT;msg;GET; ack;SPROT

Thus,

                            SPROT = *[PUT;msg;GET;ack]

and

                            SPROT\{msg,ack} == *[PUT;GET]

 

Alternatively, we may use Basic LOTOS/CADP. Here is the relevant LOTOS-file vsprot.lotos.

 

===========================================

specification vsprot[PUT,GET]:noexit behaviour

        hide msg,ack in

(

 PSEND[PUT,msg,ack]

     |[msg,ack]|

 PREC[msg,GET,ack]

)

where

   process PSEND[PUT,msg,ack]:noexit:=

        PUT;msg;ack;PSEND[PUT,msg,ack]

   endproc

   process PREC[msg,GET,ack]:noexit:=

       msg;GET;ack;PREC[msg,GET,ack]

   endproc

endspec

 

===========================================

 

Exercise Ex5.1

Convert the above LOTOS program into the corresponding aut-file  

vsprot.aut and then issue the command:

                         aldebaranomin vsprot.aut

You should get an LTS representing *[PUT;GET] .

 

5.2   Up-Down  Counters

  

In this section we consider up-down transition counters. They count input transitions (level changes) within a given range. We denote by UP the level input whose transitions increment the count, and by DOWN the level input whose transitions decrement the count. We denote by ‘up’  the (up- or down-) transition of UP, and by ‘down’  any transition of DOWN.

For the time being we consider up-down transition counters without associating outputs which would indicate the present count state. The issue of outputs will be taken up later on.

Let udcntk  denote an up-down transition counter capable of counting within the range 0-k.  Below we show a process graph, where Proc0 = Pudcnt3 represents udcnt3.

 

                                Proc0

                       down↑       ↓up

                                Proc1

                       down↑       ↓up

                                Proc2

                       down↑       ↓up

                                Proc3

 

It turns out that Pudcnt3 may also be represented by udc3\{x,y}, where udc3 is specified below.  In a later chapter we use this representation to obtain a hardware implementation of Pudcnt3.

 

           udc3[up,down] = (*[up;x] || *[x;y]) || *[y;down]

 

Exercise Ex5.2

Use CADP to show that Pudcnt3 and udc3\{x,y} are  obs.  equivalent.

 

5.2.2           Direct Verification

 

We wish to prove directly that udc3\{x,y} is indeed obs.equivalent to the above specified process Pudcnt3.

 

Let     proc0:= udc3

          proc1:= *[up;x] || *[x;y] || *[down;y]

          proc2:= *[up;x] || *[y;x] || *[down;y]

          proc3:= *[x;up] || *[y;x] || *[down;y]

One easily verifies  the following:

         proc0 = up;x;y;proc1

         proc1 = down;proc0 [ ] up;x;proc2

         proc2 = down;y;proc1 [ ] up;proc3

        proc3 = down;y;x;proc2

Thus, after hiding x and y, udc3\{x,y} becomes obs. equivalent to Pudcnt3, with procj, as specified above,  corresponding to Procj of Pudcnt3.

 

5.3                 Further Reading

 

Further applications of BLA and LOTOS/CADP will be discussed in Lectures 6-9.