INTENTION
This class provides all definitions to describe the behavior of a sensor. It is composed of the behavior of a sensor if there is no malfunction and the case that there is a malfunction.
A malfunction of a sensor can be detected automatically by the machine or it can be entered manually.
FORMAL PARAMETERS
Sort | ENV_DOMAIN |
---|
Intention | : | This domain contains the possible values of the measured phenomenon existing in the real world in the case that a sensor has no malfunction. |
Sort | MEASURED_DOMAIN |
---|
Intention | : | This domain contains the possible analogously measured values in the case that a sensor has no malfunction. |
Sort | CONVERTED_DOMAIN |
---|
Intention | : | This domain contains the possible digitally converted measured values in the case that a sensor has no malfunction. |
SIGNATURE
Object | noMalSens : NoMalfunctionSensor(ENV_DOMAIN = ENV_DOMAIN, MEASURED_DOMAIN = MEASURED_DOMAIN, CONVERTED_DOMAIN = CONVERTED_DOMAIN) |
---|
Intention | : | This object represents the part of the sensor describing the behavior of the sensor if it has no malfunction, i.e. if the machine assumes that it has no malfunction. |
Object | malSens : MalfunctionSensor(MAL_CONVERTED_DOMAIN = CONVERTED_DOMAIN) |
---|
Intention | : | This object represents the part of the sensor describing the behavior of the sensor if it has a malfunction, i.e. if the machine assumes that it has a malfunction.
The possible digitally converted measured values (CONVERTED_ DOMAIN) are used as the possible values the machine can use as sensor values in the case of a malfunction of the sensor (MAL_CONVERTED_DOMAIN). |
Object | manualEnteredMal : EnteredValue(CHECKED_DOM = BINARY) |
---|
Intention | : | This object represents a value entered manually by a person concerning a malfunction of the sensor. 1 stands for a malfunction, 0 stands for no malfunction.
Note that the value of this object is only meaningful if the timed predicate stateManualEnteredMal is true. |
Timed Function | usedValue CONVERTED_DOMAIN |
---|
Intention | : | This function models the current value used by the machine as the value of the sensor. This depends on whether there is a malfunction of the sensor or not. |
Timed Predicate | stateManualEnteredMal |
---|
Intention | : | This predicate is true iff it has been manually entered whether there is a malfunction of the sensor or whether there is no malfunction of it.
Note the difference between this predicate and the object manualEnteredMal. |
Timed Predicate | automaticDetMal |
---|
Intention | : | This predicate is true iff a malfunction of the sensor has been detected automatically, i.e. not by entering it manually. |
Property | I_S1 |
---|
NL | : | Initially it has not been entered manually whether there is a malfunction of the sensor or whether there is no malfunction of it. |
Property | M_S1 |
---|
NL | : | The machine assumes a malfunction of the sensor iff one of the following conditions is fulfilled:
|
Property | M_S2 |
---|
NL | : | Whenever the machine assumes that the sensor is working correctly the value used by the machine corresponds with the digitally converted version of the measured value. |
Property | M_S3 |
---|
NL | : | Whenever the machine assumes that the sensor is not working correctly the value used by the machine corresponds with the value computed for this case. |