Essay: Exploring Meta Keys, System Specifications, and Tempura for HAL

What are Meta Keys and Description?

The learning outcomes that are assessed by this coursework are:

1. Reason with a document written in a formal specification language

2. Use a formal notation to develop, analyse and critically review

a (small-scale) system specification

3. Animate a specification using an appropriate practical tool and discuss the results

When completed you are required to submit your coursework via:

Blackboard through an assignment submission portal If you need any support or advice on completing this coursework please visit the Student Matters tab on the Faculty of Technology Blackboard page.

Late submission of coursework policy: Late submissions will be processed in accordance with current University regulations which state: “the time period during which a student may submit a piece of work late without authorisation and have the work capped at 40% [50% at PG level] if passed is 14 calendar days. Work submitted unauthorised more than 14 calendar days after the original submission date will receive a mark of 0%. These regulations apply to a student’s first attempt at coursework. Work submitted late without authorisation which constitutes reassessment of a previously failed piece of coursework will always receive a mark of 0%.”

• Ability to translate informal textual system description into formal description

• Ability to justify system design decisions

• Ability to analyse a formal system specification

The following is a description of a smart freezer security system (HAL). Smart freezers are used in labs for storing experimental samples. HAL consists of sensors,

actuators and a control system. The following sensors and actuators are present:

• Contamination checkers CCi (0 ≤ i ≤ 1), these can be on or off. CC0 indicates the checker for the top drawer shelf and CC1 the checker for the bottomdrawer shelf. The freezer in this scenario has two drawer shelves. When a checker is in mode on, a contamination sensor is activated to analyse the drawer.

• Door sensors Di (0 ≤ i ≤ 1), indicating whether the doors are open or not. The freezer has two doors (one for each drawer shelf).

• Temperature sensor TEMPi (0 ≤ i ≤ 1), indicating whether the temperature inside each drawer is the proper one.

• Switch S, indicating whether one is in the lab or away.

• Alarm A, this can be on or off.

Give a Tempura specification of HAL. Log decisions on how you resolve any ambiguity. Use the following 24-hour scenarios to illustrate your answer with output from your Tempura program:

i) Normal working day at lab: the user works in the lab, sets labPat  and Check pattern but HAL does not detect anything wrong.

ii) The forgotten open door: the user finished his experiment, put the samples in the freezer and is about to go away. He/she has set the awayPat pattern. The user presses the switch S to tell HAL to switch to away mode. However, HAL complains that it cannot switch to away mode as the user has forgotten to close the door D0. The user has to close the door and then try switch S again.

iii) A malfunction of the freezer: the user has a day off and is away from  the lab all day and sets the awayPat pattern. Suddenly, at 23:40 the temperature sensor TEMP0 detects an increase of the temperature inside the freezer and the alarm sounds