CSC8105: Coursework Project (2016/2017) 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 com- municating systems. General There are four arrays of N boolean 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 boolean values, to be stored in process Rcv. The new array (the password being calculated) should satisfy R[i] = (A[i]∧ B[i])∨ (C[i]∧ D[i]) for all 0 ≤ i < N (note that ∨ denotes logical OR, and ∧ logical AND). 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 in order to derive the values of R; • message passing is assumed to be asynchronous, i.e. it is carried out using buffered channels, which are initially assumed to be error-free; • a message can carry at most one boolean 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 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 lose messages, but that the total number of messages sent from PrA to PrB and lost will not be greater than some given number K). 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, 28th November 2016 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 bit init_data[8]; proctype proc (byte my_id, next_id, previous_id; chan to_next, from_previous, to_receiver) { bit my_code[N]; byte i=0; /* declare more variables */ /* initialise the array for this process */ do :: i my_code[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) { bit result[N] ; /* declare more variables */ /* add communication etc */} init { chan AtoB = [N] of { bit }; chan BtoC = [N] of { bit }; chan CtoD = [N] of { bit }; chan DtoA = [N] of { bit }; chan AtoR = [N] of { bit }; chan BtoR = [N] of { bit }; chan CtoR = [N] of { bit }; chan DtoR = [N] of { bit }; atomic { init_data[0]=1; init_data[1]=0; init_data[2]=1; init_data[3]=1; init_data[4]=1; init_data[5]=0; init_data[6]=1; init_data[7]=0; 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