This assignment consists of three tasks:
a. Producing a formal specification in VDM.
b. Implementing part of the specification in SPARK.
Read the following scenario:
Telco Research is a research organization involved in the R&D of telecommunication
products and technologies. It has a number of research labs within its building. Telco
Research is looking to develop its own access control system for its research lab.
Access to each lab is to be secured by biometric fingerprint authentication. The access
control system has the following requirements and constraints:
a. The system must maintain an access control list that keeps information on the
research lab(s) that a researcher is allowed to access. Entry to a lab must be
governed by this access control list.
b. There is a database of researchers. For each researcher, the following
information is kept in the database: ID, name and research group. Only
researchers in this database are allowed to access the labs.
c. No researcher can be in two labs at the same point in time.
d. For safety reasons, each lab has a capacity in terms of the maximum number
of researchers that can be allowed in the lab at any one point in time.
e. The system must support at least the following processes:
i. Updating of the access control list: adding permission for new
researchers, revoking the access of a particular researcher to a
ii. A researcher entering and leaving a research lab.
iii. Query functionality to check the location of a particular staff (which
lab) at a point in time.
iv. Adding and removing entries into the database of researchers.
Develop a VDM specification for the access control system as described above. Your
specification must be comprehensive enough to cover all the described requirements
Implement, using SPARK, the operations corresponding to requirement e. ii. (A
researcher entering and leaving a research lab). This implementation must correspond
to the formal specification that you have developed in TASK 1. In order to achieve a
running program, you may define any other necessary structures, types, functions or
Using the SPARK Examiner and Simplifier, prove that your implementation is free
from run-time errors.