System declarations

1

2

//Template instantiations

system Carrier_Agent,Path;

Global declarations

1

2

3

4

5

//Global declarations

const int N = 2; //number of carrier agents

typedef int [0,N-1] id_carrier;

chanappr[N], stop[N], leave[N];

urgent chan go[N];

Carrier agent declarations

1

2

3

4

5

6

7

8

9

10

11

12

13

14

15

16

17

18

19

20

21

id_carrier list[N+1];

int[0,N] len;

// Postcondition: Put an element at the end of the queue

void enqueue(id_carrier element)

{list[len++] = element;}

// Postcondition: Removes the front element of the queue

void dequeue()

{

int i = 0;

len -= 1;

while (i < len)

{list[i] = list[i + 1];

i++;}

list[i] = 0;

}

// Postcondition: Returns the front element of the queue

id_carrier front()

{return list[0];}

// Postcondition: Returns the last element of the queue

id_carrier tail()

{return list[len - 1];}

Formal verification using UPPAAL verifier

1

2

3

4

5

6

7

//Collion Detection on Crossing Area

E<> Carrier_Agent(1).Crossing imply not Carrier_Agent(0).Crossing

//Reachability

E<> Carrier_Agent(1).Crossing

//Check Deadlock For System

A[] not deadlock