OMP6210 Assignment Instructions
Module: Automated Software Verification
Assignment: Practical application of NUSMV and CBMC Weighting: 20%
Deadline: 09/12/2022 Feedback: 30/12/2022 Effort: 30 hours
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
Criterion Description Total
Ability to model systems
in NuSMV
Working NuSMV model and brief description of key
modelling decisions
50%
Ability to use NuSMV in
simulation mode
NuSMV output showing appropriate simulation of your
model
10%
Ability to formalise
correctness properties
Formal description of the two correctness properties in
Task 3, to be used by NuSMV
10%
Ability to use NuSMV in
verification mode
NuSMV output showing appropriate verification of the
two correctness properties in Task 3
10%
Ability to diagnose
issues with C code using
CBMC
Evidence of using CBMC on the C code provided
(command line options and a clear description of the
problem)
10%
Ability to fix basic
software errors using
CBMC
Successfully fixing the errors in the C programs
provided
10%
Late submissions will be penalised at 10% per working day. Work submitted more than 5 days late will receive a mark of
zero. Your attention is drawn to the University regulations concerning Academic Integrity.
COMP6210 Assignment Feedback