CTEC3902 Rigorous Systems Sheet 1 of 8


Faculty of Computing, Engineering & Media (CEM)
Coursework Brief 2019/2020
Module name: Rigorous Systems
Module code: CTEC3902
Title of the Assignment: Coursework
This coursework item is: (delete as appropriate) Summative
This summative coursework will be marked anonymously: (delete
as appropriate)
Yes
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
This coursework is: (delete as appropriate) Individual

This coursework constitutes 100% of the overall module mark.
Date Set: Week 17, Monday 25 January 2021
Date & Time Due: Week 32, Tuesday 11 May 2021, 14:00
Your marked coursework and feedback will be available to
you on:
If for any reason this is not forthcoming by the due date your module
leader will let you know why and when it can be expected. The
Associate Professor Student Experience
(cemstudentexperience@dmu.ac.uk) should be informed of any
issues relating to the return of marked coursework and feedback.

Note that you should normally receive feedback on your coursework by
no later than 20 University working days after the formal hand-in
date, provided that you have met the submission deadline.



9/06/2020
When completed you are required to submit your coursework via:
CTEC3902 Rigorous Systems Sheet 2 of 8

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%.”

Academic Offences and Bad Academic Practices:
These include plagiarism, cheating, collusion, copying work and reuse of your own work, poor
referencing or the passing off of somebody else's ideas as your own. If you are in any doubt about
what constitutes an academic offence or bad academic practice you must check with your tutor.
Further information and details of how DSU can support you, if needed, is available at:
http://www.dmu.ac.uk/dmu-students/the-student-gateway/academic-support-office/academic-
offences.aspx and
http://www.dmu.ac.uk/dmu-students/the-student-gateway/academic-support-office/bad-academic-
practice.aspx

Tasks to be undertaken:
Exercise 1, 2, 3, 4, and 5
Deliverables to be submitted for assessment:
a zip file named .zip containing:
1: your developed Tempura specifications
2: an electronic copy of your report (max 10 pages)
How the work will be marked:
see marking scheme for each exercise
Module leader/tutor name: Vasileios Germanos
Contact details: Email: vasileios.germanos@dmu.ac.uk
CTEC3902 Rigorous Systems Sheet 3 of 8

Please turn over …

Section A
Theoretical Part
Exercise 1. (25 marks total)
Assessment Indicators:
• Correctness
• Conciseness
Give an English and pictorial description of the interval that correspond to each of
the following Interval Temporal Logic formulae.

a) () ∧ ( ) ∧ 3
b) 2 ∧ = 1 ∧ ( )

c) 3; ( ∧ ) ;

d) ((1) ∧(A = 0)); (B = 0 ∧ B gets B + 1 ∧ halt(B = 3))

e) (4) ∧ (P ∧ ) ∧ ( ∧ Q)

Exercise 2. (25 marks total)
Assessment Indicators:
• Correctness
• Elegance (clarity and conciseness)
Give for each of the following intervals the corresponding Interval Temporal Logic
formula.

a)


(3 marks)
= 1 = 2 (3 marks)
(3 marks)
(4 marks)
(7 marks)
(8 marks)
CTEC3902 Rigorous Systems Sheet 4 of 8

Please turn over …


b)


c)


d)


Exercise 3. (20 marks total)
Assessment Indicators:
• Correctness
a) Give the formal semantics of the following Propositional Interval Temporal
Logic formula.
( ∧ );

b) State which of the following ITL formulae are satisfiable and justify your
answer with a specific example.

i) ◇((A) > A)
ii. = 1 ∧ ℎ( = 0)
iii. ( ≔ 2 ∗ )




= 32 = 16 = 8 = 4 = 2
, ¬ , , ¬ , ¬, ¬

(4 marks)
, ¬,

(8 marks)
(10 marks)
(8 marks)
(4 marks)
(4 marks)
(4 marks)
CTEC3902 Rigorous Systems Sheet 5 of 8

Please turn over …

Section B
Practical Part
Exercise 4. (5 marks total)
Assessment Indicators:
• Clear English
• Correctness
• Elegance (clarity and conciseness)
Give an English description of the interval that corresponds to the following
Tempura formulae
a) Give an English description of the interval that corresponds to the following
Tempura formula.
/* run */ define test1()={
exists I: {halt(I=9) and I=-1 and
chopstar(skip and I:=I+2) and
always output(I)
}
}. (5 marks)









CTEC3902 Rigorous Systems Sheet 6 of 8

Please turn over …

Exercise 5. (25 marks total)
Assessment Indicators:
• 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 lock system HAL for entering and exiting a
research lab, where experiments with hazardous chemicals are contacted. HAL
consists of sensors, actuators, and a control system. The following sensors and
actuators are present:
• Doors D0 and D1.
• Buttons B0, B1, B2, and B3.
• Infrared sensor I.










The procedure for exiting the office is as follows.
• Press button B1, if it is safe then door D1 will open and one can enter the
cleaning area via door D1.
• Door D1 will close immediately when button B3 is pressed or after 5 seconds
when sensor I detects that a person is present in the cleaning area.
• Press button Β0, if it is safe then door D0 will open and one can exit the
cleaning area via door D0.
• Door D0 will close immediately when button B2 is pressed or after 10
seconds when I sensor detects that a person is not present in the cleaning
area
lab office
B0
B2
I
D0
B3
B1
D1
cleaning area
CTEC3902 Rigorous Systems Sheet 7 of 8

Please turn over …

The procedure for entering the office is as follows.
• Press button B2, the door opens, and one can enter the cleaning area via
door D0.
• Door D0 will close immediately when button B0 is pressed or after 7 seconds
when sensor I detects a person present in the cleaning are.
• Press button B3, if it is safe then door D1 will open and one can exit the
cleaning area via door D1.
• Door D1 will close immediately when button B1 is pressed or after 6 seconds
when sensor I detects that a person is not present in the cleaning area.

Be aware of the following constraints.
• The office has 3 scientists. At any point in time at least 1 scientist should be
in the office.
• There is only space for 1 person in the cleaning area.
• If both doors D0 and D1 are open, then contaminated air will escape from
the lab this needs to be avoided at all time.
• It is possible that more than one button is pressed at the same time, for
example, a scientist in the lab wanting to enter the cleaning area via door D0
and a scientist in the office wanting to enter the cleaning area via door D1.
You need to resolve this type of conflict by giving priority to a particular
button press. Note: a scientist in the cleaning area can not press
simultaneously buttons B0 and B3.
The control system HAL determines whether doors Di are open or closed
depending on the state of the infrared sensor and the buttons Bj.
a) Give a Tempura specification of HAL. A template solution is available on
Blackboard. Use the following scenarios to illustrate your answer with
output from your Tempura program:

i) A short visit at lab: A scientist leaves the office via the cleaning area
using above exit procedure for a short visit at the lab and comes back
after 10 minutes and re-enters the office via the cleaning area using
the enter procedure.
CTEC3902 Rigorous Systems Sheet 8 of 8


ii) The enter / exit conflict: A scientist is outside the office and wants to
enter the office via the cleaning area. At the same time, a scientist
inside the office wants to leave it via the cleaning area. Note: you
need give priority to one scientist who can use the cleaning area first.

The following marking scheme will be used
Environment: User/Sensors
Tempura + 2 scenarios : 06-08
Tempura + 1 scenario : 03-05
English : 00-02
Controller: HAL
Tempura + 2 scenarios : 06-08
Tempura + 1 scenario : 03-05
English : 00-02
Integration
Tempura : 02-04
English : 00-02
(20 marks)
b) The system that you have specified needs to satisfy certain safety
conditions.

Give one example of a safety condition that your system should satisfy and
formulate it in ITL/Tempura.
(5 marks)