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.
Scope	:	ev
Postreferences	:	rsref MalfunctionActuator : R_MA3
		rsref MalfunctionActuator : R_MA4
		rsref MalfunctionActuator : R_MA5
		rsref MalfunctionActuator : R_MA6

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.
Scope	:	ev
Postreferences	:	rsref MalfunctionActuator : R_MA1
		rsref MalfunctionActuator : R_MA2

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.
Scope	:	eh

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.
Scope	:	mh
Postreferences	:	msref Actuator : M_A1
		rsref MalfunctionActuator : R_MA3
		rsref MalfunctionActuator : R_MA4
		rsref MalfunctionActuator : R_MA5
		rsref MalfunctionActuator : R_MA6

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.
Scope	:	eh
Postreferences	:	rsref MalfunctionActuator : I_MA2
		rsref MalfunctionActuator : R_MA2
		rsref MalfunctionActuator : R_MA4
		rsref MalfunctionActuator : R_MA6

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.
Scope	:	eh
Postreferences	:	rsref MalfunctionActuator : I_MA1
		rsref MalfunctionActuator : R_MA1
		rsref MalfunctionActuator : R_MA3
		rsref MalfunctionActuator : R_MA5

REQUIREMENT SPECIFICATIONS

Property	I_MA1

Formal	:	userInformed
NL	:	Initially the user is not informed about an important event concerning this actuator.

Property	I_MA2

Formal	:	FMInformed
NL	:	Initially the facility manager is not informed about an important event concerning this actuator.

Property	R_MA1

Formal	:	( [  userInformed ]  Tinfo  userInformed )
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

Formal	:	( [  FMInformed ]  Tinfo  FMInformed )
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

Formal	:	( [  malDetMach ]  TinfDelay  userInformed )
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

Formal	:	( [  malDetMach ]  TinfDelay  FMInformed )
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

Formal	:	( [  malDetMach ]  TinfDelay  userInformed )
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

Formal	:	( [  malDetMach ]  TinfDelay  FMInformed )
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.