Assignment

Closed Posted May 1, 2012 Paid on delivery
Closed Paid on delivery

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

particular lab.

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.

TASK 1

Develop a VDM specification for the access control system as described above. Your

specification must be comprehensive enough to cover all the described requirements

and constraints.

TASK 2

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

procedures.

Using the SPARK Examiner and Simplifier, prove that your implementation is free

from run-time errors.

Freelance

Project ID: #1600746

About the project

Remote project Active Jun 5, 2012