Assessment Indicators:
· Correctness
· Conciseness
Give an English and pictorial description of the interval that correspond to each of the following Interval Temporal Logic formulae.
Copyright By PowCoder代写 加微信 powcoder
Assessment Indicators:
· Correctness
· Elegance (clarity and conciseness)
Give for each of the following intervals the corresponding Interval Temporal Logic formula.
Assessment Indicators:
· Correctness
a) Give the formal semantics of the following Propositional Interval Temporal Logic formula. (10 marks)
Assessment Indicators:
· Clear English
· Correctness
· Elegance (clarity and conciseness)
a) 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)
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, an astronaut in the space station wanting to enter the airlock via door D0 and an astronaut 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: an astronaut in the airlock cannot 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 space station: An astronaut enters 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: An astronaut 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.
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.
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com