Advanced Topics in Computer Science

This module will be assessed by two components (PART 1 and PART 2). PART 1 carries 70% of the module marks and PART 2 carries 30% of the module marks.

PART 1 (described in this document) consists a series of practical tasks that you will begin in your lab sessions and complete in your own time. There are three tasks that make up PART 1:

a) Formal Model Specification task

b) Formal Model Testing task

c) Formal Model Implementation task

The task, the topic, the associated lab and the allocated marks for each task is given below

LAB 3: Task A (simple) 12 marks

The VDM Specification Language

INITIAL SPECIFICATION

Consider a robot moving across a room (treated like a 6 by 6 grid) in order to exit from a door. The robot always starts at position 1,1. The robot may move left, right, up and down by one grid square at a time. When the robot reaches the door it may exit and another robot immediately enters the room in position 1,1.

Software to monitor the robot is to be developed. Initial analysis of the software has produced the following UML diagram:

Download the template RobotMonitor.rtf specification file from the CN6008 Moodle site and complete the VDM-SL model of this system, using VDMTools to ensure it is free of syntax and type errors.

LAB 4: Task A (advanced) 20 marks

Advanced Features of the VDM Specification Language

To achieve the top end of marks for Task A, develop the simple RobotMonitor specification from Lab 3 further as detailed below:

Add an extra restriction that the Robot cannot make the same move twice. So, for example, if a Robot at (1,1) moves RIGHT to (1,2)

its next move cannot be a move RIGHT again to (1,3). The UML diagram has been adapted to record the last move by making use of an enumerated Move type:

Initially, the robot at 1,1 will have no move allocated to it. Modify your initial RobotMonitor specification accordingly to include a move attribute, again using VDMTools to ensure it is free of syntax and type errors.

LAB 6: Task B

Validating and Verifying Formal Models

Use VDMTools to thoroughly test the RobotMonitor.rtf model you produced in task A - correcting any logical errors you may find. A sampleTestDocumentation.pdf file is available on the CN6008 Moodle site to illustrate how you can document your testing.

SIMPLE TASK (20 marks)

If you were unable to develop the full RobotMonitor specification described in Lab 4 and wish to stick to the simpler specification described in Lab 3, you may use theTestRMSimple.rtf test data file (available on the CN6008 Moodle site) to help carry out your testing. You should add to the test data provided in this file.

ADVANCED TASK (30 marks)

If you developed the advanced RobotMonitor specification described in Lab 4, you may use the TestRMAdvanced.rtf test data file (available on the CN6008 Moodle site) to help carry out your testing. You should add to the test data provided in this file.

LAB 7: Task C

Implementing VDM Specifications

A RobotMonitor class has been discussed in task A & B above. You should have a formal VDM-SL model of this class from task A and this model will have been thoroughly tested in task B. Now, go to the CN6008 Moodle site and download the following files:

1. RobotMonitor.java
2. Move.java
3. VDMException.java
4. RobotMonitorGUI.java
5. RunRobotGUI.java
6. RunRobotText.java

The RobotMonitor.java file is an incomplete Java implementation of the RobotMonitor model discussed above. Complete the implementation of this RobotMonitor.java class, being sure to use defensive programming techniques discussed in lecture 8.

You can test this class by running it alongside the additional classes provided. If you are using a desktop Java IDE (such as NetBeans or eclipse) you can use the GUI interface to test your RobotMonitor.java class by running the RunRobotMonitorGUI.java file. Below is a sample screen shot of how the running application should look once complete:

If you do not have access to a Java IDE such as NetBeans, you may use a web-based Java tool (such as JDoodle). Web-based Java tools such as JDoodle cannot run programs with a GUI interface, so to test your RobotMonitor.java class use the text based tester fie RunRobotMonitorText.java. Below is a sample screen shot of how the running text-based application will look:

SIMPLE TASK (12 marks): Implement the simple VDM-SL specification outlined in Lab 3.
ADVANCED TASK (20 marks): Implement the advanced VDM-SL specification outlined in Lab 4.