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.

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.