Next: Template Declaration Sensor Up: No Title Previous: Template Declaration NoMalfunctionSensor

Template Declaration MalfunctionSensor

INTENTION

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

The following topics are considered:

A malfunction of a sensor can be detected automatically by the machine or it can be entered manually. To specify this topic the following signature entities manualEnteredMal, T_MalDetDelay, malDetEnv, malDetMach, stateManualEnteredMal, automaticDetMal and the following properties I_A_MS1, I_A_MS3, A_MS1 - A_MS_4, I_M_MS1, M_MS1 - M_MS3 are used.
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. To specify this topic the following signature entities manualEnteredVal, automaticDetermValue, valueMal, stateManualEnteredValue, I_A_MS2, and the following properties M_MS8 are used.
This is our interpretation of stepwise degradation in the case that a sensor has a malfunction.

Postreferences : lsref Sensor : malSens

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 a sensor.

Postreferences : lsref MalfunctionSensor : manualEnteredVal

lsref MalfunctionSensor : automaticDetermValue

lsref MalfunctionSensor : valueMal

Sort	MAL_CONVERTED_DOMAIN

SIGNATURE

Object manualEnteredVal : EnteredValue(VALID_INPUTS = MAL_CONVERTED_DOMAIN)

Intention : This object represents the value that should be used in the case of a malfunction of a sensor. This value is entered manually by a user. The entered value has to be an element of the domain MAL_CONVERTED_DOMAIN.

Prereferences : pdref PD_30

Postreferences : msref MalfunctionSensor : M_MS4

Object	manualEnteredVal : EnteredValue(VALID_INPUTS = MAL_CONVERTED_DOMAIN)

Object manualEnteredMal : EnteredValue(VALID_INPUTS = BINARY)

Intention : This object represents a value entered manually by a person indicating whether a sensor has a malfunction or not.

1 represents that a sensor has a malfunction
0 represents that a sensor has no malfunction
Note that the value of this object is only meaningful if the timed predicate stateManualEnteredMal is true.

Prereferences : pdref FM11

Postreferences : msref MalfunctionSensor : M_MS3

dkref MalfunctionSensor : D_MS1

dkref MalfunctionSensor : D_MS2

msref MalfunctionSensor : M_MS1

msref MalfunctionSensor : M_MS2

Object	manualEnteredMal : EnteredValue(VALID_INPUTS = BINARY)

Time Constant T_MalDetDelay

Intention : This time constant represents the maximal delay between the time point a sensor has a malfunction and the time point the machine assumes a malfunction of this sensor.

Scope : ev

Postreferences : dkref MalfunctionSensor : D_MS1

dkref MalfunctionSensor : D_MS2

dkref MalfunctionSensor : D_MS3

dkref MalfunctionSensor : D_MS4

msref MalfunctionSensor : I_M_MS1

Time Constant	T_MalDetDelay

Timed Function automaticDetermValue MAL_CONVERTED_DOMAIN

Intention : This function represents the value of a sensor determined automatically by the machine in the case of a malfunction of a sensor.

Scope : mh

Prereferences : pdref PD_30

pdref NF1

pdref NF2

pdref NF3

pdref NF4

Postreferences : msref MalfunctionSensor : M_MS4

rsref OutdoorLightSensor : R_OLS1

Timed Function	automaticDetermValue MAL_CONVERTED_DOMAIN

Timed Function valueMal MAL_CONVERTED_DOMAIN

Intention : This function represents the value of a sensor used by the machine in the case of a malfunction of a sensor. It is computed based on the automatically determined and the manually entered value.

Scope : mh

Prereferences : pdref PD_30

Postreferences : msref MalfunctionSensor : M_MS4

msref Sensor : M_S2

Timed Function	valueMal MAL_CONVERTED_DOMAIN

Timed Predicate malDetEnv

Intention : This predicate is true if and only if a 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

Prereferences : pdref PD_30

pdref FM11

Postreferences : dkref MalfunctionSensor : D_MS1

dkref MalfunctionSensor : D_MS2

dkref MalfunctionSensor : I_D_MS3

dkref MalfunctionSensor : D_MS3

dkref MalfunctionSensor : D_MS4

Timed Predicate	malDetEnv

Timed Predicate	malDetMach

Timed Predicate stateManualEnteredValue

Intention : This predicate is true if and only if a value, that should be used in the case of a malfunction of a sensor, has been entered manually by a user.

Scope : ev

Prereferences : pdref PD_30

Postreferences : msref MalfunctionSensor : M_MS4

dkref MalfunctionSensor : I_D_MS2

Timed Predicate	stateManualEnteredValue

Timed Predicate stateManualEnteredMal

Intention : This predicate is true if and only if it has been manually entered whether there is a malfunction of a sensor or whether there is no malfunction of it.
Note the difference between this predicate and the object manualEnteredMal.

Scope : ev

Prereferences : pdref FM11

Postreferences : dkref MalfunctionSensor : I_D_MS1

msref MalfunctionSensor : M_MS3

dkref MalfunctionSensor : D_MS1

dkref MalfunctionSensor : D_MS2

Timed Predicate	stateManualEnteredMal

Timed Predicate automaticDetMal

Intention : This predicate is true if and only if a malfunction of a sensor has been detected automatically, i.e. not by entering it manually.

Scope : ev

Prereferences : pdref FM11

Postreferences : msref MalfunctionSensor : M_MS3

dkref MalfunctionSensor : D_MS1

dkref MalfunctionSensor : D_MS2

DOMAIN KNOWLEDGE

Timed Predicate	automaticDetMal

Property I_D_MS1

Formal : stateManualEnteredMal

NL : Initially it has not been entered manually whether there is a malfunction of a sensor or whether there is no malfunction of it.

Property	I_D_MS1

Property I_D_MS2

Formal : stateManualEnteredValue

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

Property	I_D_MS2

Property I_D_MS3

Formal : malDetEnv

NL : Initially a sensor has no malfunction.

Property	I_D_MS3

Property D_MS1

Formal : ( malDetEnv _{T_MalDetDelay}
     ( stateManualEnteredMal automaticDetMal )
     ( stateManualEnteredMal
       _{manualEnteredMal. checkTime} ( manualEnteredMal. entered = ``1'' ) ) )

NL : Whenever a sensor existing in the real world has constantly a malfunction for at least T_MalDetDelay milliseconds then within this time the conditions are fulfilled that the machine assumes a malfunction of this sensor, i.e.,

either the machine has detected a malfunction automatically and it is not entered manually whether there is a malfunction or not
or it is entered manually whether there is a malfunction or not and in the last manualEnteredMal.checkTime milliseconds it has been entered that there is a malfunction, i.e. manualEnteredMal.entered = "1".

Property	D_MS1

Property D_MS2

Formal : ( malDetEnv _{T_MalDetDelay}
     ( stateManualEnteredMal automaticDetMal )
     ( stateManualEnteredMal
       _{manualEnteredMal. checkTime} ( manualEnteredMal. entered ``1'' ) ) )

NL : Whenever a sensor existing in the real world has constantly no malfunction for at least T_MalDetDelay milliseconds then within this time the conditions are fulfilled that the machine assumes no malfunction of this sensor, i.e.,

either the machine has not detected a malfunction automatically and it is not entered manually whether there is a malfunction or not
or it is entered manually whether there is a malfunction or not and in the last manualEnteredMal.checkTime milliseconds it has not been entered that there is a malfunction, i.e. manualEnteredMal.entered $\not=$ "1".

Property	D_MS2

Property D_MS3

Formal : ( _{T_MalDetDelay} malDetEnv )

NL : Each time malDetEnv becomes valid, it will be constantly valid for at least T_MalDetDelay milliseconds.

Property	D_MS3

Property D_MS4

Formal : ( _{T_MalDetDelay} malDetEnv )

NL : Each time malDetEnv becomes invalid, it will be constantly invalid for at least T_MalDetDelay milliseconds.

Property	D_MS4

MACHINE SPECIFICATIONS

Property I_M_MS1

Formal : _{T_MalDetDelay} malDetMach

NL : The first T_MalDetDelay milliseconds the machine assumes that a sensor has no malfunction.

Property	I_M_MS1

Property M_MS1

Formal : ( manualEnteredMal. nearestValue(``1'') = 1 )

NL : A manually entered ``1'' (as a string) concerning whether a sensor has a malfunction or not is always converted to a 1 as a natural number, i.e. as an element of the domain BINARY.

Property	M_MS1

Property M_MS2

Formal : ( s STRING :
( s ``1'' manualEnteredMal. nearestValue(s) = 0 ) )

NL : Each manually entered string concerning whether a sensor has a malfunction or not that differs from ``1'' (as a string) is always converted to a 0 as a natural number, i.e. as an element of the domain BINARY.

Property	M_MS2

Property M_MS3

Formal : ( malDetMach
( stateManualEnteredMal manualEnteredMal. checked = 1 )
( stateManualEnteredMal automaticDetMal ) )

NL : The machine assumes a malfunction of a sensor if and only if one of the following conditions is fulfilled:

a malfunction has been entered manually or
it has not been entered manually whether there is a malfunction or not and a malfunction has been detected automatically.

Prereferences : pdref FM11

Property	M_MS3

Property M_MS4

Formal : ( stateManualEnteredValue
                     ( valueMal = manualEnteredVal. checked )
    ( stateManualEnteredValue
                     ( valueMal = automaticDetermValue ) ) )

NL : If a value for the status of a 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 a sensor.
Otherwise, the value used by the machine in the case of a malfunction of a sensor is the value determined automatically in the case of a malfunction of a sensor.

Prereferences : pdref PD_30

Property	M_MS4

Next: Template Declaration Sensor Up: No Title Previous: Template Declaration NoMalfunctionSensor

Forest-System
2000-09-06

Intention	:	This domain contains the possible values the machine can use as sensor values in the case of a malfunction of a sensor.
Postreferences	:	lsref MalfunctionSensor : manualEnteredVal
		lsref MalfunctionSensor : automaticDetermValue
		lsref MalfunctionSensor : valueMal

Intention	:	This object represents the value that should be used in the case of a malfunction of a sensor. This value is entered manually by a user. The entered value has to be an element of the domain MAL_CONVERTED_DOMAIN.
Prereferences	:	pdref PD_30
Postreferences	:	msref MalfunctionSensor : M_MS4

Intention	:	This object represents a value entered manually by a person indicating whether a sensor has a malfunction or not. 1 represents that a sensor has a malfunction 0 represents that a sensor has no malfunction Note that the value of this object is only meaningful if the timed predicate stateManualEnteredMal is true.
Prereferences	:	pdref FM11
Postreferences	:	msref MalfunctionSensor : M_MS3
		dkref MalfunctionSensor : D_MS1
		dkref MalfunctionSensor : D_MS2
		msref MalfunctionSensor : M_MS1
		msref MalfunctionSensor : M_MS2

Intention	:	This time constant represents the maximal delay between the time point a sensor has a malfunction and the time point the machine assumes a malfunction of this sensor.
Scope	:	ev
Postreferences	:	dkref MalfunctionSensor : D_MS1
		dkref MalfunctionSensor : D_MS2
		dkref MalfunctionSensor : D_MS3
		dkref MalfunctionSensor : D_MS4
		msref MalfunctionSensor : I_M_MS1

Intention	:	This function represents the value of a sensor determined automatically by the machine in the case of a malfunction of a sensor.
Scope	:	mh
Prereferences	:	pdref PD_30
		pdref NF1
		pdref NF2
		pdref NF3
		pdref NF4
Postreferences	:	msref MalfunctionSensor : M_MS4
		rsref OutdoorLightSensor : R_OLS1

Intention	:	This predicate is true if and only if a 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
Prereferences	:	pdref PD_30
		pdref FM11
Postreferences	:	dkref MalfunctionSensor : D_MS1
		dkref MalfunctionSensor : D_MS2
		dkref MalfunctionSensor : I_D_MS3
		dkref MalfunctionSensor : D_MS3
		dkref MalfunctionSensor : D_MS4

Intention	:	This predicate is true if and only if it has been manually entered whether there is a malfunction of a sensor or whether there is no malfunction of it. Note the difference between this predicate and the object manualEnteredMal.
Scope	:	ev
Prereferences	:	pdref FM11
Postreferences	:	dkref MalfunctionSensor : I_D_MS1
		msref MalfunctionSensor : M_MS3
		dkref MalfunctionSensor : D_MS1
		dkref MalfunctionSensor : D_MS2

Formal	:	stateManualEnteredMal
NL	:	Initially it has not been entered manually whether there is a malfunction of a sensor or whether there is no malfunction of it.

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

Formal	:	( malDetEnv _{T_MalDetDelay} ( stateManualEnteredMal automaticDetMal ) ( stateManualEnteredMal _{manualEnteredMal. checkTime} ( manualEnteredMal. entered = ``1'' ) ) )
NL	:	Whenever a sensor existing in the real world has constantly a malfunction for at least T_MalDetDelay milliseconds then within this time the conditions are fulfilled that the machine assumes a malfunction of this sensor, i.e., either the machine has detected a malfunction automatically and it is not entered manually whether there is a malfunction or not or it is entered manually whether there is a malfunction or not and in the last manualEnteredMal.checkTime milliseconds it has been entered that there is a malfunction, i.e. manualEnteredMal.entered = "1".

Formal	:	( _{T_MalDetDelay} malDetEnv )
NL	:	Each time malDetEnv becomes valid, it will be constantly valid for at least T_MalDetDelay milliseconds.

Formal	:	( _{T_MalDetDelay} malDetEnv )
NL	:	Each time malDetEnv becomes invalid, it will be constantly invalid for at least T_MalDetDelay milliseconds.

Formal	:	_{T_MalDetDelay} malDetMach
NL	:	The first T_MalDetDelay milliseconds the machine assumes that a sensor has no malfunction.

Formal	:	( manualEnteredMal. nearestValue(``1'') = 1 )
NL	:	A manually entered ``1'' (as a string) concerning whether a sensor has a malfunction or not is always converted to a 1 as a natural number, i.e. as an element of the domain BINARY.

Formal	:	( s STRING : ( s ``1'' manualEnteredMal. nearestValue(s) = 0 ) )
NL	:	Each manually entered string concerning whether a sensor has a malfunction or not that differs from ``1'' (as a string) is always converted to a 0 as a natural number, i.e. as an element of the domain BINARY.

Formal	:	( malDetMach ( stateManualEnteredMal manualEnteredMal. checked = 1 ) ( stateManualEnteredMal automaticDetMal ) )
NL	:	The machine assumes a malfunction of a sensor if and only if one of the following conditions is fulfilled: a malfunction has been entered manually or it has not been entered manually whether there is a malfunction or not and a malfunction has been detected automatically.
Prereferences	:	pdref FM11

Formal	:	( stateManualEnteredValue ( valueMal = manualEnteredVal. checked ) ( stateManualEnteredValue ( valueMal = automaticDetermValue ) ) )
NL	:	If a value for the status of a 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 a sensor. Otherwise, the value used by the machine in the case of a malfunction of a sensor is the value determined automatically in the case of a malfunction of a sensor.
Prereferences	:	pdref PD_30