OMP6210代写、C++设计编程代写

日期：2022-12-12 08:12

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