Hello, dear friend, you can consult us at any time if you have any questions, add WeChat: THEend8_
CTEC3902 Rigorous Systems Sheet 1 of 8
Faculty of Computing, Engineering & Media (CEM)
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
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:
Tasks to be undertaken:
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.