Description Class MalfunctionSensor

INTENTION

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

In the case of a malfunction of a sensor, a value is determined depending on a possibly manually entered value by a user and an automatically determined value. If a value has been entered manually this value has priority over the automatically determined value.

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

FORMAL PARAMETERS

Sort	MAL_CONVERTED_DOMAIN

Intention

:

This domain contains the possible values the machine can use as sensor values in the case of a malfunction of the sensor.

SIGNATURE

Object	manualEnteredVal  :  EnteredValue(CHECKED_DOM  =  MAL_CONVERTED_DOMAIN)

Intention	:	This object represents the value entered manually by a user in the case of a malfunction of this sensor. The entered value has to be an element of the domain MAL_CONVERTED_DOMAIN.
Postreferences	:	msref MalfunctionSensor : M_MS1

Time Constant	TinfDelay

Intention	:	This time constant represents the maximal delay between an important event concerning this sensor 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 MalfunctionSensor : R_MS3
		rsref MalfunctionSensor : R_MS4
		rsref MalfunctionSensor : R_MS5
		rsref MalfunctionSensor : R_MS6

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 sensor.
Scope	:	ev
Postreferences	:	rsref MalfunctionSensor : R_MS1
		rsref MalfunctionSensor : R_MS2

Timed Function	automaticDetermValue   MAL_CONVERTED_DOMAIN

Intention	:	This function represents the value of the sensor determined automatically by the machine in the case of a malfunction of the sensor.
Scope	:	mh
Postreferences	:	msref MalfunctionSensor : M_MS1
		rsref OutdoorLightSensor : R_OLS1

Timed Function	valueMal   MAL_CONVERTED_DOMAIN

Intention	:	This function represents the value of the sensor used by the machine in the case of a malfunction of the sensor. It is computed based on the automatically determined and the manually entered value.
Scope	:	mh
Postreferences	:	msref MalfunctionSensor : M_MS1
		msref Sensor : M_S3

Timed Predicate	malDetEnv

Intention	:	This predicate is true iff the sensor 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 sensor 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 Sensor : M_S1
		msref Sensor : M_S2
		msref Sensor : M_S3
		msref Floor : M_F1
		rsref MalfunctionSensor : R_MS3
		rsref MalfunctionSensor : R_MS4
		rsref MalfunctionSensor : R_MS5
		rsref MalfunctionSensor : R_MS6

Timed Predicate	stateManualEnteredValue

Intention	:	This predicate is true iff a value, that should be used in the case of a malfunction of the sensor, has been entered manually by a user.
Scope	:	mh
Postreferences	:	msref MalfunctionSensor : I_MS1
		msref MalfunctionSensor : M_MS1

Timed Predicate	FMInformed

Intention	:	This predicate is true iff the facility manager is informed about an important event concerning this sensor. An important event is either the detection of a malfunction of the sensor or that a malfunction of the sensor has been repaired. The facility manager has to be informed by sending an email.
Scope	:	eh
Postreferences	:	rsref MalfunctionSensor : I_MS3
		rsref MalfunctionSensor : R_MS2
		rsref MalfunctionSensor : R_MS4
		rsref MalfunctionSensor : R_MS6

Timed Predicate	userInformed

Intention	:	This predicate is true iff the user is informed about an important event concerning this sensor. An important event is either the detection of a malfunction or that a malfunction has been repaired. The user is the person who is currently in the area in which the sensor is installed. The user has to be informed by sending an email.
Scope	:	eh
Postreferences	:	rsref MalfunctionSensor : I_MS2
		rsref MalfunctionSensor : R_MS1
		rsref MalfunctionSensor : R_MS3
		rsref MalfunctionSensor : R_MS5

REQUIREMENT SPECIFICATIONS

Property	I_MS2

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

Property	I_MS3

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

Property	R_MS1

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_MS2

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_MS3

Formal	:	( [  malDetMach ]  TinfDelay  userInformed )
NL	:	Whenever the machine assumes that a malfunction of the sensor has occurred, the user is informed about this within $T_\mathit{infDelay}$ milliseconds.

Property	R_MS4

Formal	:	( [  malDetMach ]  TinfDelay  FMInformed )
NL	:	Whenever the machine assumes that a malfunction of the sensor has occurred, the facility manager is informed about this within $T_\mathit{infDelay}$ milliseconds.

Property	R_MS5

Formal	:	( [  malDetMach ]  TinfDelay  userInformed )
NL	:	Whenever the machine assumes that the sensor is working correctly again after it has had a malfunction, the user is informed about this within $T_\mathit{infDelay}$ milliseconds.

Property	R_MS6

Formal	:	( [  malDetMach ]  TinfDelay  FMInformed )
NL	:	Whenever the machine assumes that the sensor is working correctly again after it has had a malfunction, the facility manager is informed about this within $T_\mathit{infDelay}$ milliseconds.

MACHINE SPECIFICATIONS

Property	I_MS1

Formal	:	stateManualEnteredValue
NL	:	Initially no value for the case of a malfunction is entered manually by a user.

Property	M_MS1

Formal	:	(  stateManualEnteredValue                      (  valueMal =  manualEnteredVal. checked )     (  stateManualEnteredValue                      (  valueMal =  automaticDetermValue ) ) )
NL	:	If a value for the status of the sensor in the case of a malfunction has been entered manually this is the value used by the machine in the case of a malfunction of the sensor. Otherwise, the value used by the machine in the case of a malfunction of the sensor is the value determined automatically in the case of a malfunction of the sensor.