Reference no: EM133191492

CTEC3902 Rigorous Systems - De Montfort University

Section A - Theoretical Part

Exercise 1.
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) ¬P ∧ (fin P) ∧ skip³

b) skip²∧A = 2∧(A gets - A)

c) (skip ∧ fin(A=0)) ; (B=1 ∧ skip)

d) (P ∧ empty) ; skip ; skip²

e) A=1 ∧ (A gets A + 2) ∧ halt(A=7)

f) (len(2)∧"[]" (A=2) );(B=2∧B gets B - 1∧halt(B=0) )

g) len(4)∧(Q ;(skip⇒¬Q)*)

Exercise 2.

Assessment Indicators:
Correctness
Elegance (clarity and conciseness)
Give for each of the following intervals the corresponding Interval Temporal Logic formula.

 

Exercise 3.
Assessment Indicators:
Correctness
Give the formal semantics of the following Propositional Interval Temporal Logic formula.
(P∧skip);skip

Section B

Practical Part

Exercise 4.
Assessment Indicators:
Clear English
Correctness
Elegance (clarity and conciseness)
Give an English description of the interval that corresponds to the following Tempura formulae
Give an English description of the interval that corresponds to the following Tempura formula.
/* run */ define test1()={
exists I: {halt(I=18) and I=-2 and
chopstar(skip and I:=I+2) and
always output(I)
}
}.

Exercise 5.
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 an airlock system HAL for entering and exiting a space station. 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 entering the space station is as follows.
Press button B1, if it is safe then door D1 will open and one can enter the airlock 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 airlock.
Press buttonΒ0, if it is safe then door D0 will open and one can exit the airlock 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 airlock.
The procedure for exiting the space station is as follows.
Press button B2, the door opens, and one can enter the airlock 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 airlock.
Press button B3, if it is safe then door D1 will open and one can exit the airlock 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 airlock.

Be aware of the following constraints.
The space station has 3 scientists. At any point in time at least 1 astronaut should be in the space station.
There is only space for 1 person in the airlock.
If both doors D0 and D1 are open, then air will escape from space station, this needs to be avoided at all times.
It is possible that more than one button is pressed at the same time, for example, anastronaut in the space station wanting to enter the airlock via door D0 and anastronaut wanting to enter the airlock via door D1. You need to resolve this type of conflict by giving priority to a particular button press. Note: anastronaut in the airlockcannot 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.
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:

A short visit at space station: Anastronautenters the airlock via D1 using above entering procedure for a short visit at the space station and comes back after 10 minutes and re-exits the space station via the airlock using the exiting procedure.

ii) The enter / exit conflict: Anastronaut is outside in the space and wants to enter the space station via the airlock. At the same time, an astronaut inside the airlock wants to leave it and go out to the space. Note: you need give priority to one astronaut who can use the airlock 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

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.