CSC8105讲解、辅导CS/Python编程设计、辅导software留学生、讲解Python/Java设计

CSC8105: Coursework Project

(2018/2019)

Aims

To assess student’s ability to model and validate high-level prototypes of software used to

implement communicating systems.

To become familiar with a computer-aided tool for the specification and verification of communicating

systems.

General

There are four arrays of N byte values each, A, B, C and D, stored in processes P rA, P rB,

P rC and P rD, respectively. These values are used to calculate a password. Your have been

asked to design a validated communication scheme to produce an array R of N byte values (the

password), to be stored in process Rcv. The new array (the password being calculated) should

satisfy R[i] = max{A[i], B[i], C[i], D[i]} for all 0 ≤ i < N. The connectivity of the five process

network is given in the diagram below.

PrA PrB

PrD PrC

Rcv

It is assumed that:

message passing is the only means of interprocess communication;

process Rcv is not allowed to carry out any calculations involving the data received;

message passing is assumed to be asynchronous, i.e. it is carried out using buffered channels,

which are assumed to be error-free in Task 1;

a single message can carry at most one byte data value used in calculations;

the four outer processes can communicate and the design should allow data received, say, by

P rA from P rD, to be forwarded to P rB (unless P rA is certain that P rB does not need this

data);

any of the four outer processes can calculate and send the values of array R to Rcv.

Project Tasks

(1) Develop a highly concurrent symmetric solution to the above problem, using as few message

exchanges as possible. Write a PROMELA program which would provide a validation model

for your solution. Formulate the relevant correctness requirements and verify, using SPIN,

that they are indeed satisfied. Start with N = 2 (or even N = 1) and see what is the largest

value of N for which the validation task can still be carried out in ‘reasonable’ time.

(2) It turned out that the channels outgoing from PrA can duplicate messages. Modify your

solution to cope with these problems. Again, formulate correctness requirements and validate

them using SPIN.

Marking Scheme

Task 1 (75% in total): design: 25%, PROMELA code: 40%, and validation results and

explanations: 10%.

Task 2 (25% in total): design: 10%, PROMELA code: 10%, and validation results and

explanations: 5%.

Submission

The assignment must be submitted to NESS in a single .zip file by

8.45am on Monday, 26th November 2018

In your submission you should provide, for each of the two tasks:

PROMELA program;

brief explanations of how your solution works;

validation results produced by SPIN.

Hint

The following can be used as rough template while working on your solution. Note that P rA has

my id equal to 0, P rB has my id equal to 1, etc.

#define N 2

byte init_data[8];

proctype proc (byte my_id, next_id, previous_id; chan to_next, from_previous, to_receiver)

{ byte my_data[N]; byte i=0;

/* declare more variables */

/* initialise the array for this process */

do

:: i<N -> my_data[i] = init_data[my_id*N + i]; i++

:: i==N -> break

od;

/*add communication etc */}

proctype receiver (chan from_A, from_B, from_C, from_D)

{ byte result[N] ;

/* declare more variables */

/* add communication etc */}

init {

chan AtoB = [N] of { byte }; chan BtoC = [N] of { byte }; chan CtoD = [N] of { byte };

chan DtoA = [N] of { byte }; chan AtoR = [N] of { byte }; chan BtoR = [N] of { byte };

chan CtoR = [N] of { byte }; chan DtoR = [N] of { byte };

atomic

{

init_data[0]=2; init_data[1]=0; init_data[2]=5; init_data[3]=8;

init_data[4]=4; init_data[5]=1; init_data[6]=3; init_data[7]=9;

run proc (0,1,3,AtoB,DtoA,AtoR); run proc (1,2,0,BtoC,AtoB,BtoR);

run proc (2,3,1,CtoD,BtoC,CtoR); run proc (3,0,2,DtoA,CtoD,DtoR);

run receiver(AtoR,BtoR,CtoR,DtoR)}}