Description Class Sensor

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.
Postreferences	:	dkref OutdoorLightSensor : D_OLS1
		dkref OutdoorLightSensor : D_OLS2
		dkref BinarySensor : D_BS1
		dkref BinarySensor : D_BS2
		dkref BinarySensor : D_BS3
		dkref LightSensor : D_L1
		dkref DoorContact : D_DC1
		dkref MotionDetector : D_MD1
		dkref ControlledLight : D_CL1
		dkref ControlledLight : D_CL2
		dkref AreaLight : D_AL2
		msref Sensor : M_S2
		msref ControlledLight : M_CL1
		rsref AreaLight : R_AL1
		rsref AreaLight : R_AL2
		rsref HallwaySection : R_HS1
		rsref HallwaySection : R_HS2
		rsref Floor : R_F1

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).
Postreferences	:	msref Sensor : M_S1
		msref Sensor : M_S2
		msref Sensor : M_S3
		msref Floor : M_F1
		rsref OutdoorLightSensor : R_OLS1

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.
Postreferences	:	msref Sensor : M_S1

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.
Scope	:	mh
Postreferences	:	msref Sensor : M_S2
		msref Sensor : M_S3
		msref AreaLight : M_AL7
		msref HallwaySection : M_HS3
		msref BasicRoom : M_BaR1

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.
Scope	:	mh
Postreferences	:	msref Sensor : I_S1
		msref Sensor : M_S1

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.
Scope	:	mh
Postreferences	:	msref Sensor : M_S1

MACHINE SPECIFICATIONS

Property	I_S1

Formal	:	stateManualEnteredMal
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

Formal	:	(  malSens. malDetMach       (  stateManualEnteredMal  manualEnteredMal. checked = 1 )       (  stateManualEnteredMal  automaticDetMal ) )
NL	:	The machine assumes a malfunction of the sensor iff 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.

Property	M_S2

Formal	:	(  malSens. malDetMach             usedValue =  noMalSens. convertedEntity )
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

Formal	:	(  malSens. malDetMach  usedValue =  malSens. valueMal )
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.