Assignment Formal Methods

Instructions and notes: 1. This assignment is to be attempted on an individual basis and will contribute 40% to your course grade. The total marks for this assignment is 40. 2. This assignment consists of three tasks: a. Producing a formal specification in VDM. b. Implementing part of the specification in SPARK. c. Delivering a 10-minute presentation to highlight your solution. 3. The deadline for submission is the 15 of May 2012. For any late submission, a penalty of 5 marks per day will be imposed. 4. Any act of plagiarism will be dealt with severely. 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.2 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.