Template Declaration MalfunctionOccupancy

INTENTION

This class provides all definitions to describe the behavior of the system concerning the detection of occupancy in an area in the case that some sensors used to determine occupancy have a malfunction.

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

Most of the entities introduced in this description class have to be refined in the description classes where they are used.

Postreferences

:

lsref Occupancy : malOcc

SIGNATURE

Object	manualEnteredOcc  :  EnteredValue(VALID_INPUTS  =  BINARY)

Intention	:	This object represents the value concerning occupancy entered manually by a user in the case of a malfunction of some sensors used to determine occupancy. manualEnteredOcc.checked = 1 means occupancy, manualEnteredOcc.checked = 0 means no occupancy. Note that the value of this object is only meaningful if the predicate stateManualEnteredOcc is true.
Prereferences	:	pdref FM11
Postreferences	:	msref MalfunctionOccupancy : M_MO2
		msref MalfunctionOccupancy : I_M_MO1

Object	manualEnteredMal  :  EnteredValue(VALID_INPUTS  =  BINARY)

Intention	:	Manually entered value concerning a malfunction of the sensors determining occupancy entered by a user. 1 means that some sensors used to determine occupancy have a malfunction, 0 means that no sensor used to determine occupancy has a malfunction. Note that the value of this object is only meaningful if the timed predicate stateManualEnteredMal is true.
Prereferences	:	pdref FM11
Postreferences	:	msref MalfunctionOccupancy : M_MO1
		msref MalfunctionOccupancy : I_M_MO5

Timed Predicate	malOccDetEnv

Intention	:	This predicate is true if and only if some sensors existing in the real world used to determine occupancy have 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 NF4

Timed Predicate	malOccDetMach

Intention	:	This predicate is true if and only if the machine assumes that some sensors used to determine occupancy have a malfunction. Note that this predicate represents the value as it seen by the machine.
Scope	:	mh
Prereferences	:	pdref NF4
Postreferences	:	msref Occupancy : M_O1
		msref MalfunctionOccupancy : I_M_MO2
		msref MalfunctionOccupancy : M_MO1

Timed Predicate	stateManualEnteredOcc

Intention	:	This predicate is true if and only if it has been entered manually whether there is occupancy or not.
Scope	:	mh
Prereferences	:	pdref FM11
		pdref PD_30
Postreferences	:	msref MalfunctionOccupancy : I_M_MO3
		msref MalfunctionOccupancy : M_MO2

Timed Predicate	automaticDetermValue

Intention	:	This predicate represents the occupancy determined automatically by the machine in the case of a malfunction of the sensors used to determine occupancy. If this predicate is true this means occupancy. If it is false this means no occupancy.
Scope	:	mh
Prereferences	:	pdref NF4
		pdref PD_30
Postreferences	:	msref MalfunctionOccupancy : M_MO2
		msref Area : M_A4
		msref MalfunctionOccupancy : I_M_MO4

Timed Predicate	occMal

Intention	:	This predicate represents the occupancy used by the machine in the case of a malfunction of the sensors used to determine occupancy. If this predicate is true this means occupancy. If it is false this means no occupancy.
Scope	:	mh
Prereferences	:	pdref NF4
		pdref PD_30
Postreferences	:	msref MalfunctionOccupancy : M_MO2
		msref Occupancy : M_O1

Timed Predicate	stateManualEnteredMal

Intention	:	This predicate is true if and only if it has been manually entered whether there is a malfunction of the sensors used to determine occupancy or whether there is no malfunction of them.
Scope	:	mh
Prereferences	:	pdref FM11
Postreferences	:	msref MalfunctionOccupancy : M_MO1
		msref MalfunctionOccupancy : I_M_MO6

Timed Predicate	automaticDetMal

Intention	:	This predicate is true if and only if a malfunction of the sensors used to determine occupancy has been detected automatically, i.e. not by entering it manually.
Scope	:	mh
Prereferences	:	pdref FM11
Postreferences	:	msref MalfunctionOccupancy : M_MO1
		msref MalfunctionOccupancy : I_M_MO7

MACHINE SPECIFICATIONS

Property	I_M_MO1

Formal	:	manualEnteredOcc. checked = 0
NL	:	Initially the value concerning occupancy entered manually is 0.

Property	I_M_MO2

Formal	:	malOccDetMach
NL	:	Initially the machine does not assume that some sensors used to determine occupancy have a malfunction.

Property	I_M_MO3

Formal	:	stateManualEnteredOcc
NL	:	Initially no value for occupancy in the case of a malfunction is entered manually.

Property	I_M_MO4

Formal	:	automaticDetermValue
NL	:	Initially the value for the automatically determined occupancy in the case of a malfunction of the sensors used to determine occupancy is false.

Property	I_M_MO5

Formal	:	manualEnteredMal. checked = 0
NL	:	Initially the value of the manually entered value concerning a malfunction of the sensors used to determine occupancy is 0.

Property	I_M_MO6

Formal	:	stateManualEnteredMal
NL	:	Initially no value for occupancy in the case of a malfunction is entered manually.

Property	I_M_MO7

Formal	:	automaticDetMal
NL	:	Initially no malfunction of the sensors used to determine occupancy is detected automatically.

Property	M_MO1

Formal	:	(  malOccDetMach            ( (  stateManualEnteredMal                manualEnteredMal. checked = 1 )              (  stateManualEnteredMal  automaticDetMal ) ) )
NL	:	The machine assumes a malfunction of some sensors used to determine occupancy if and only if one of the following conditions is fulfilled: a malfunction has been entered manually or it has not been entered manually that there is no malfunction and a malfunction has been detected automatically.
Prereferences	:	pdref FM11
		pdref PD_30

Property	M_MO2

Formal	:	(  stateManualEnteredOcc                      (  occMal  manualEnteredOcc. checked = 1 )    (  stateManualEnteredOcc                      (  occMal  automaticDetermValue ) ) )
NL	:	If a value for the status of occupancy has been entered manually this is the value used for occupancy in the case of a malfunction of some sensors used to determine occupancy. Otherwise, the value used for occupancy in the case of a malfunction of the sensors used to determine occupancy corresponds with the value determined automatically.
Prereferences	:	pdref PD_30