Description Class MalfunctionActuator

INTENTION

This class provides all definitions to describe the behavior of an actuator if it has a malfunction.

The facility manager as well as the user are informed about a malfunction.

SIGNATURE

Time Constant	TinfDelay

Intention

:

This time constant represents the maximal delay between an important event concerning this actuator a user or the facility manager has to be informed about (e.g. a malfunction or the repair of a malfunction) and the time point the user or the facility manager is informed.

Time Constant	Tinfo

Intention

:

This time constant represents the maximal time span a user or the facility manager is informed about an important event concerning this actuator.

Timed Predicate	malDetEnv

Intention

:

This predicate is true iff the actuator existing in the real world has a malfunction. Note that this predicate represents the value as it exists in the real world. This value is not visible for the machine.

Timed Predicate	malDetMach

Intention

:

This predicate is true iff the machine assumes that the actuator existing in the real world has a malfunction. Note that this predicate represents the value as it seen by the machine.

Timed Predicate	FMInformed

Intention

:

This predicate is true iff the facility manager is informed about an important event concerning this actuator. An important event is either the detection of a malfunction of the actuator or that a malfunction of the actuator has been repaired. The facility manager has to be informed by sending an email.

Timed Predicate	userInformed

Intention

:

This predicate is true iff the user is informed about an important event concerning this actuator. An important event is either the detection of a malfunction of the actuator or that a malfunction of the actuator has been repaired. The user has to be informed by sending an email.

REQUIREMENT SPECIFICATIONS

Property	I_MA1

NL

:

Initially the user is not informed about an important event concerning this actuator.

Property	I_MA2

NL

:

Initially the facility manager is not informed about an important event concerning this actuator.

Property	R_MA1

NL

:

Whenever a user becomes informed he is informed for at most $T_\mathit{info}$ milliseconds. By this requirement it is expressed, that the user is not informed permanently, but that the information is a kind of signal, e.g. an email.

Property	R_MA2

NL

:

Whenever the facility manager becomes informed he is informed for at most $T_\mathit{info}$ milliseconds. By this requirement it is expressed, that the facility manager is not informed permanently, but that the information is a kind of signal, e.g. an email.

Property	R_MA3

NL

:

Whenever the machine assumes that a malfunction of the actuator has occurred, the user is informed about this within $T_\mathit{infDelay}$ milliseconds.

Property	R_MA4

NL

:

Whenever the machine assumes that a malfunction of the actuator has occurred, the facility manager is informed about this within $T_\mathit{infDelay}$ milliseconds.

Property	R_MA5

NL

:

Whenever the machine assumes that the actuator is working correctly again after it has had a malfunction, the user is informed about this within $T_\mathit{infDelay}$ milliseconds.

Property	R_MA6

NL

:

Whenever the machine assumes that the actuator is working correctly again after it has had a malfunction, the facility manager is informed about this within $T_\mathit{infDelay}$ milliseconds.