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

–      if id < myid

•      if non-participant: replace id with myid in message, forward message, mark itself as participant

•      if already a participant: stop forwarding (this way multiple elections are stopped)

–      if id = myid, leader found, leader := myid, send elected message with myid, mark itself as non-participant

•      upon receiving an elected message:

–      if id != myid, leader := id, forward the message, mark itself as non-participant

–      if id = myid, stop forwarding

Eventually, every participant will know the leader (i.e. the largest value among the processes).

Task 1

Build a NuSMV model of the leader election algorithm. You may restrict your model to 4 processes. You should consider the following aspects when constructing your model:

•     How communication between processes is modelled, and in particular whether this is synchronous or asynchronous. The reasons for your choice should be explained in the report.

•     How your model ensures that the values assigned to different participants are different.

•     How your model allows for a process to call an election at any time.

•     Whether your model accurately captures the behaviour of the algorithm. You should explain this briefly in the report. (50%)

Task 2

Use NuSMV’s simulation support to validate your model. (Details of simulation support can be found in     Section 3.5 of the NuSMV manual.) Your report should include the output of a simulation which shows the protocol working as expected in the case of 4 processes with different values. (10%)

Task 3

Use NuSMV’s verification support to establish whether your model satisfies each of the following properties:

1.    It always elects the participant with the highest value as the leader.

2.    Eventually, all the participants know the value of the leader.

For each property, you should explain the output of the verification. If your model does not satisfy a property, explain what is wrong, give a counter example and indicate how it might be corrected. (20%)

Part 2.

Basic use of CBMC

Use CBMC to analyse 'message.c' and 'euclidean-alg.c'. For both files, explain the problem with the code and provide the CBMC command line input which exposes it. For both files, suggest a solution that fixes the problem. (20%)

Report

Your report should be between 2-4 pages in length (excluding appendices), and must contain the following information:

•     For Part 1:

-      a brief description of your model,

-      an explanation of your simulation output,

-      a description of the verification carried out and an interpretation of the verification output.

•     For Part 2:

-      a brief description of the problems in the C code provided and a description of the CBMC options used to discover the problems

-      fixed versions of the C code

The outputs produced by NuSMV and CBMC must be included in a clearly marked appendix.

Marking

-      Part 1: marks will be awarded for clear, uncluttered models that accurately capture the algorithm. For each correctness property, the marks will be awarded for demonstrating your ability to use NuSMV to state and verify the required property, and to explain the outcome.

-      Part 2: marks will be awarded for concise and clear description of the bugs and a clear description of how CBMC was employed for their discovery.

Submission

Your submission should consist of:

•     your report, as a PDF file.

•     your NuSMV model, as a separate file.

•     Fixed versions of the C code (as separate files).

Please submit your answers using the electronic hand-in system (http://handin.ecs.soton.ac. uk) by 5pm on the due date.

Relevant Learning Outcomes

1.    apply automated verification techniques to software

Marking Scheme