CSC8105: Project (May 2021)
The first N bits of a password are stored in process PrA, the middle N bits in process PrB ,
and the last N bits in process PrC . You have been asked to design a communication scheme for
assembling the password in process Rcv assuming the following network connectivity.
PrA
PrB PrC
Rcv
It is assumed that:
• message passing is the only means of interprocess communication;
• Rcv accepts the complete password from just one of the three outer processes, and any of
these three processes should be able to send the complete password to Rcv ;
• 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 single message can carry at most one bit of the password;
• the three outer processes can communicate and the design should allow data received, say,
by PrA from PrC , to be forwarded to PrB (unless PrA is certain that PrB does not need
this data).
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.
Use simulation features of SPIN with different seed values to debug your PROMELA pro-
gram.
Formulate the relevant correctness requirements and include them in your submitted solution.
(2) It turned out that the channels connected to Rcv can duplicate messages. Modify your
solution to cope with this problem. Again, use simulation features of SPIN with different
seed values to debug your PROMELA program.
Marking Scheme
• Task 1 (75% in total): design: 25%, PROMELA code: 40%, and simulation results and
explanations: 10%.
• Task 2 (25% in total): design: 10%, PROMELA code: 10%, and simulation results and
explanations: 5%.
Submission
The assignment must be submitted in a single .zip file. In your submission you should provide, for
each of the two tasks:
• PROMELA program;
• brief explanations of how your solution works;
• simulation results produced by SPIN with different seed values.
Appendix
The following can be used as a rough template while working on your solution. Note that PrA has
my id equal to 0, PrB has my id equal to 1, and PrC has my id equal to 2.
#define N 2
#define L 6
bit init_data[L]; /* password */
proctype proc (byte my_id, next_id, previous_id;
chan to_next, from_previous, to_receiver)
{ bit my_pswd[N]; byte i=0;
/* here declare more variables */
/* initialise local part of the password for this process */
do
:: i my_pswd[i] = init_data[my_id*N + i]; i++
:: else -> break
od;
/* here add communication statements etc */
}
proctype receiver (chan from_A, from_B, from_C)
{ bit result[L] ;
/* here declare more variables */
/* here add communication statements etc */
}
init {
chan AtoB = [N] of { bit }; chan BtoC = [N] of { bit }; chan CtoA = [N] of { bit };
chan AtoR = [L] of { bit }; chan BtoR = [L] of { bit }; chan CtoR = [L] of { bit };
atomic
{
init_data[0]=1; init_data[1]=0; init_data[2]=1; /* try also other passwords */
init_data[3]=1; init_data[4]=1; init_data[5]=0;
run proc (0,1,2,AtoB,CtoA,AtoR);
run proc (1,2,0,BtoC,AtoB,BtoR);
run proc (2,0,1,CtoA,BtoC,CtoR);
run receiver(AtoR,BtoR,CtoR)
}}

欢迎咨询51作业君