Lecturer: Prof Michael Butler
Due: 4pm Friday 18 May 2007
Errors in software can be time-consuming, expensive and possibly
life-threatening. Many problems result from faulty specification and design of
systems. A variety of methods are used in industry to attempt to avoid such
problems. These methods can be classified as structured, object-oriented and
formal. Formal methods involve the application of mathematics, usually set
theory and logic, to the specification, design and verification of software
(and hardware) systems.
D5 involves
producing a specification of a software system using the B notation. B is a formal method based on set
theory and logic.
See http://en.wikipedia.org/wiki/B-Method
This
coursework will contribute 25% towards the total for the unit. It is intended
to familiarise you with specification using the B-Method and the ProB tool.
ProB Tool: http://www.stups.uni-duesseldorf.de/ProB/
We
consider the access control system within a high-security building where access
is controlled on a per room basis.
Each individual employed by the organisation is authorised to engage in
a range of activities which varies between individuals. Each room in the building is designed
for a specific set of activities.
Individuals only have access to that room if they are authorised to
engage in each activity that the room
is designed for. Individuals should
only be in one room at any one time.
1.
Produce a B
model of the above access policy and its enforcement using the following steps:
a.
Produce a
bullet list of informally described access constraints from the above
description.
b.
Introduce
appropriate types, variables and invariants which model these constraints in a
B machine.
c.
Introduce
the following operations
i.
an
individual enters a room,
ii.
an
individual leaves a room,
iii.
add an
activity to an individual’s authorisation list
iv.
add an
activity to an room
d.
For each of
the constraints in (a), justify informally why it is modelled in your B
machine.
2.
Animate and
model-check your B model using the ProB tool. Include a printout of a run of your
specification using the B animator in your report. Write a short report (approx 15 lines)
on your experience with ProB, explaining whether and how it helped with
constructing the B specification.
Instructions
You
should submit a report (Word or PDF), one per group, giving your answer to each
of the tasks above (B model and supporting text). The report should be
word-processed so you may find it useful to install the B
ttf font. You should also include the machine readable version you used in
the ProB tool. You should use the automated handin facilities found on the
student Web pages at:
https://handin.ecs.soton.ac.uk/
If
you feel there are any ambiguities in the requirements feel free to make your
own interpretation, but make sure any interpretations you make are clearly
indicated in the report. Make sure
your group's number is clearly marked on your report. You should avoid
discussing your solutions with other groups.