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:

aldebaran –omin 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.