COMP6210 Assignment Instructions
Instructions
Part 1 of this assignment requires you to construct a NuSMV model of a leader election algorithm and use NuSMV to verify some of its properties. Part 2 of the assignment requires you to use CBMC to discover flaws in two simple C programs, fix these issues and use CBMC to check that your solution is indeed a fix.
You are also required to write a brief report describing:
– For Part 1: your modelling decisions and the verification carried out, including an interpretation of the results.
– For Part 2: the problems with the C programs.
Part 1. Leader Election in a Ring
A Ring-Based Election Algorithm
The aim of this distributed algorithm is to elect a leader among a number of participant processes arranged in a (logical) ring. Each participant can only send messages to the next participant in the ring. Each participant has a unique value, different from all the other participants. The participant with the largest value must be elected as a leader. The algorithm works as follows:
• initially, every process is a non-participant
• any process can call an election:
– marks itself as participant
– places its id in an election message
– sends this message to neighbour (next process in the ring)
• upon receiving an election message:
– if id > myid, forward the message, mark itself as participant
– ifid