Fm

SCHOOL OF COMPUTING AND TECHNOLOGY Submission instructions • Cover sheet to be attached to the front of the assignment • Question paper to be attached to assignment • All pages to be numbered sequentially • Assignment to be stapled ONLY ONCE in the top left-hand corner • Assignment NOT to be placed in a folder, plastic sleeve of any kind or bound in any other form. • Computer discs to be attached to the work in an envelope or purpose made sleeve adhered to the rear

Module code

Module title

Module leader

Assignment tutor

Assignment title

Assignment number

Weighting

EEM117

Formal Methods

Aaron Kans

Aaron Kans

Secure Messaging Service

1

25%

Handout date

8 June 2009

Submission date

11 August 2009

Instructions:

This work is expected to be word processed to a professional standard. You should submit a printed copy of your work as well as an electronic copy on disc.

MSc CSE Formal Methods: Coursework The Secure Messaging Service

An application is required to provide a secure messaging service for agents assigned to classified missions. Agents send each other message s detailing his\her mission. The messages are kept in the appropriate agent's individual inbox. Once a message is read, it is deleted from that agent's inbox. A single message can be sent to many agents.

Agents must enter a code name and password in order to read and send messages. The application must offer at least the following two services:

sendMessage Takes the code name and password of an agent, as well as the code names of all message recipients. The title of the message is also supplied, along with the details of the mission itself. As long as a valid code name and password has been entered for the agent, the message is stored in the inbox of each recipient. This operation returns a collection of all invalid code names supplied as message recipients. To maintain confidentiality, message in the recipient's inbox do not reveal the code names of other recipients of this mission or the sender of the message, they simply reveal the message title and details of the mission.

readMessage Takes the code name and password of an agent and, as long as the code name and password are valid, returns the next message in the given agent's inbox. The messages are to be read in the order in which they were sent. Once the message has been read it is deleted from the agent's inbox.

The following UML analysis has been arrived at for the SMS application:

SMS agents: Agent[*] sendMessage (CodeName, Password, CodeName[*], Title, Mission) : CodeName[*] readMessage (CodeName, Password ): Message Deliverables

2

Deliverables 1.

Produce UML diagrams for any types in the UML class that require further analysis. 6 marks

2.

Formally model the data in this system in VDM-SL, remember to include an initialisation clause and to consider any invariants and type definitions that may be necessary. 16 marks

3.

Formally specify, in VDM-SL, the two operations described above using the model you specified in part (2) above. Extra credit will be given for making good use of comments, functions and let...in clauses where appropriate. 20 marks

4.

Now assume that message can be allocated a priority: NORMAL or HIGH. Messages are still to be read in the order in which they were sent but HIGH priority messages are always read before LOW priority messages. Briefly explain how your SMS specification would need to be modified in order to incorporate this notion of a message priority (you do not need to re-specify the SMS class) 8 marks (TOTAL 50)

3