代写 CSC8105: Coursework Project

程序代写 CS代考

Aims

CSC8105: Coursework Project (2018/2019)

  • 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 com- municating systems.

    General

    There are four arrays of N byte values each, A, B, C and D, stored in processes PrA, PrB, PrC and PrD, 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.

    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. (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. (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.

PrA

PrB

Rcv

PrD

PrC

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 PrA has myidequal to0, PrB hasmyidequal to1, 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)}}

Related Posts