Next: Description Class HallwaySection Up: No Title Previous: Group BuildingUnits

Description Class AreaLight

INTENTION

This class provides all definitions to describe the general aspects of lights in an area. An area is here the generalization of rooms and hallways. In more detail this class provides:

A set of lights that can be conrolled by the machine. The concrete number of controlled lights can be specified by instantiating the parameter numLights.
The specification of the behavior of the system concerning the aspect safety. Here safety means that there is sufficient light to move. This class provides the requirements concerning the case that safe light has to be established. Other cases can be considered in derived classes.
The specification of the behavior of the system concerning the case that the facility manager controls the light using a control panel.
The specification of the behavior of the system concerning the case that the light is controlled manually.

FORMAL PARAMETERS

Function numLights NAT

Intention : This parameter represents the number of lights in an area that are controlled by the machine.

Function	numLights NAT

SIGNATURE

Object	occ : Occupancy

Object light : ControlledLight[ numLights]

Intention : These objects represent the lights in area that are controlled by the machine.

Postreferences : dkref AreaLight : D_AL2

lsref RoomLight : light

msref AreaLight : M_AL7

msref AreaLight : M_AL8

msref AreaLight : M_AL9

rsref AreaLight : R_AL1

rsref AreaLight : R_AL2

rsref HallwaySection : R_HS1

rsref HallwaySection : R_HS2

rsref Floor : R_F1

Object	light : ControlledLight[ numLights]

Object lCPFM : AreaLightCtrlPanelFM

Intention : This object represents the light control panel containing the entities for which the facility manager can enter a value.

Postreferences : lsref RoomLight : lCPFM

msref AreaLight : M_AL5

rsref AreaLight : R_AL1

Object	lCPFM : AreaLightCtrlPanelFM

Time Constant T_AL1

Intention : This time constant represents the maximal time delay for the following two situations:

between the time point an area becomes occupied and the time point at which safe light is established;
between the time point an area becomes unoccupied and the time point the machine controlled lights are off.

Scope : ev

Postreferences : dkref AreaLight : D_AL1

msref AreaLight : M_AL1

rsref AreaLight : R_AL1

rsref AreaLight : R_AL2

rsref AreaLight : R_AL3

Time Constant	T_AL1

Time Constant T_AL2

Intention : This time constant represents the maximal delay between the time point the machine assumes an occupation of an area and the time point the machine has set the corresponding actuators to establish safe light.

Scope : ev

Postreferences : dkref AreaLight : D_AL1

msref AreaLight : M_AL2

msref AreaLight : M_AL7

Time Constant	T_AL2

Timed Predicate lightFMControlled

Intention : This predicate is true iff the light is controlled by the facility manager using the control panel.

Scope : eh

Postreferences : msref AreaLight : I_AL2

rsref AreaLight : R_AL1

rsref AreaLight : R_AL2

Timed Predicate	lightFMControlled

Timed Predicate allLightsOff

Intention : This predicate is true iff all lights in an area that are controlled by the machine are off.

Scope : eh

Postreferences : dkref AreaLight : D_AL2

Timed Predicate	allLightsOff

Timed Predicate safeLight

Intention : This predicate is true, iff there is sufficient light to move safely.

Scope : eh

Postreferences : rsref AreaLight : R_AL3

Timed Predicate	safeLight

Timed Predicate noSaveLight

Intention : This predicate is true iff the light intensity in an area that is occupied can be less than the light intensity needed to establish safe light. This is for example the case if the light is controlled manually.

Scope : mh

Postreferences : msref AreaLight : I_AL1

msref AreaLight : M_AL7

msref HallwaySection : M_HS2

msref RoomLight : M_RL4

rsref AreaLight : R_AL3

Timed Predicate	noSaveLight

Timed Predicate manualControl

Intention : This predicate is true iff the machine assumes that the light in this area is controlled manually.

Scope : mh

Postreferences : msref AreaLight : M_AL8

msref AreaLight : M_AL9

msref HallwaySection : M_HS2

msref RoomLight : M_RL4

msref RoomLight : M_RL8

msref RoomLight : M_RL9

msref RoomLight : M_RL10

msref RoomLight : M_RL11

Timed Predicate	manualControl

Function evalSaveLight : NAT ( numLights ) BINARY

Intention : This function represents the computation that results in the decision which light has to be on in order to achieve safe light in an area. evalSaveLight[i]=i means that the i-th light has to be on.

Scope : mh

Postreferences : msref AreaLight : M_AL7

DOMAIN KNOWLEDGE

Function	evalSaveLight : NAT ( numLights ) BINARY

Property D_AL1

Formal : ( T_AL2 < T_AL1 )

NL : The time constant $T\_\mathit{AL}_2$ is allways smaller than the time constant $T\_\mathit{AL}_1$ .

Property	D_AL1

Property D_AL2

Formal : ( allLightsOff n NAT ( numLights ) :
light[n]. ls. noMalSens. envEntity = 0 )

NL : The predicate allLightsOff is true iff all lights that are controlled by the machine are off.

Property	D_AL2

REQUIREMENT SPECIFICATIONS

Property R_AL1

Formal : ( lightFMControlled occ. occUsed _{T_AL1}
n NAT ( numLights ) :
( light[n]. ls. noMalSens. envEntity = lCPFM. lightOn. checked ) )

NL : Whenever the light is controlled by the facility manager using the control panel and the area is unoccupied for at least $T\_\mathit{AL}_1$ milliseconds, the status of the machine controlled lights equals within this time the status as it is determined by the facility manager.

Property	R_AL1

Property R_AL2

Formal : ( lightFMControlled occ. occUsed _{T_AL1}
n NAT ( numLights ) :
( light[n]. ls. noMalSens. envEntity = 0 ) )

NL : Whenever the light is not controlled by the facility manager using the control panel and the area is unoccupied for at least $T\_\mathit{AL}_1$ milliseconds, all machine controlled lights are off within this time and remains off at least as long as the precondition is true.

Property	R_AL2

Property R_AL3

Formal : ( noSaveLight occ. occUsed _{T_AL1} safeLight )

NL : Whenever safe light has to be established and the area is occupied for at least $T\_\mathit{AL}_1$ milliseconds, the light is sufficient to move safely within this time span and remains sufficient to move safely at least as long as the precondition is true.

Property	R_AL3

MACHINE SPECIFICATIONS

Property I_AL1

Formal : noSaveLight

NL : Initially safe light has to be established if an area is occupied.

Property	I_AL1

Property I_AL2

Formal : lightFMControlled

NL : Initially the light is not controlled by the facility manager using his control panel.

Property	I_AL2

Property M_AL1

Formal : ( T_AL1 = 50 )

NL : The value of $T\_\mathit{AL}_1$ is always 50 miliiseconds.

Property	M_AL1

Property M_AL2

Formal : ( T_AL2 = 30 )

NL : The value of $T\_\mathit{AL}_2$ is always 30 miliiseconds.

Property	M_AL2

Property M_AL3

Formal : ( occ. noMalOcc. dt1 = 1000 )

NL : The first time delay used to determine occupancy concerning the light control is always 1 second.

Property	M_AL3

Property M_AL4

Formal : ( occ. noMalOcc. dt2 = 0 )

NL : The second time delay used to determine occupancy concerning the light control is always 0 second.

Property	M_AL4

Property M_AL5

Formal : ( occ. noMalOcc. dt3 = lCPFM. unoccDelay. checked )

NL : The third time delay used to determine occupancy concerning the light control corresponds always with the value entered by the facility manager for the time a certain area has to be unoccupied continuously before the lights are switched off.

Property	M_AL5

Property M_AL6

Formal : ( occ. malOcc. automaticDetermValue )

NL : The value determined automatically by the machine for occupancy concerning the light control in the case of a malfunction of some sensors used to determine occupancy concerning the light control is occupancy.

Property	M_AL6

Property M_AL7

Formal : ( noSaveLight occ. occUsed n NAT (  numLights ) :
           ( evalSaveLight(n) = 1 light[n]. ls. usedValue = 0
                _{T_AL2} light[n]. pulse. noMalAct. adjustedEntity = 1 ) )

NL : Whenever safe light has to be established and the area is occupied the necessary actuators, i.e. pulse lines, are set within $T\_\mathit{AL}_2$ milliseconds to establish safe light.

Property M_AL8

Formal : ( manualControl
n NAT ( numLights ) : ( light[n]. manualControl )
occ. occUsed )

NL : The machine assumes that the light is controlled manually in an area iff at least one light in this area is controlled manually and the area is occupied.

Property M_AL9

Formal : ( manualControl
n NAT ( numLights ) :
( [ light[n]. pulse. noMalAct. adjustedEntity = 1 ] ) )

NL : If the light in an area is controlled manually, the settings of all lights remain unchanged.

Next: Description Class HallwaySection Up: No Title Previous: Group BuildingUnits

Forest-System
1999-06-10

Intention	:	This object represents the part of the definition of area light defining whether a room is occupied or not.
Postreferences	:	msref AreaLight : M_AL3
		msref AreaLight : M_AL4
		msref AreaLight : M_AL5
		msref AreaLight : M_AL6
		msref AreaLight : M_AL7
		msref AreaLight : M_AL8
		msref HallwaySection : M_HS3
		msref RoomLight : M_RL5
		msref RoomLight : M_RL6
		msref RoomLight : M_RL7
		msref RoomLight : M_RL8
		msref RoomLight : M_RL9
		msref RoomLight : M_RL10
		msref RoomLight : M_RL12
		msref RoomLight : M_RL13
		msref RoomLight : M_RL14
		rsref AreaLight : R_AL1
		rsref AreaLight : R_AL2
		rsref Floor : R_F1
		msref BasicRoom : M_BaR1
		rsref AreaLight : R_AL3

Intention	:	These objects represent the lights in area that are controlled by the machine.
Postreferences	:	dkref AreaLight : D_AL2
		lsref RoomLight : light
		msref AreaLight : M_AL7
		msref AreaLight : M_AL8
		msref AreaLight : M_AL9
		rsref AreaLight : R_AL1
		rsref AreaLight : R_AL2
		rsref HallwaySection : R_HS1
		rsref HallwaySection : R_HS2
		rsref Floor : R_F1

Intention	:	This object represents the light control panel containing the entities for which the facility manager can enter a value.
Postreferences	:	lsref RoomLight : lCPFM
		msref AreaLight : M_AL5
		rsref AreaLight : R_AL1

Intention	:	This time constant represents the maximal time delay for the following two situations: between the time point an area becomes occupied and the time point at which safe light is established; between the time point an area becomes unoccupied and the time point the machine controlled lights are off.
Scope	:	ev
Postreferences	:	dkref AreaLight : D_AL1
		msref AreaLight : M_AL1
		rsref AreaLight : R_AL1
		rsref AreaLight : R_AL2
		rsref AreaLight : R_AL3

Intention	:	This predicate is true iff the light is controlled by the facility manager using the control panel.
Scope	:	eh
Postreferences	:	msref AreaLight : I_AL2
		rsref AreaLight : R_AL1
		rsref AreaLight : R_AL2

Intention	:	This predicate is true iff all lights in an area that are controlled by the machine are off.
Scope	:	eh
Postreferences	:	dkref AreaLight : D_AL2

Intention	:	This predicate is true, iff there is sufficient light to move safely.
Scope	:	eh
Postreferences	:	rsref AreaLight : R_AL3

Intention	:	This predicate is true iff the light intensity in an area that is occupied can be less than the light intensity needed to establish safe light. This is for example the case if the light is controlled manually.
Scope	:	mh
Postreferences	:	msref AreaLight : I_AL1
		msref AreaLight : M_AL7
		msref HallwaySection : M_HS2
		msref RoomLight : M_RL4
		rsref AreaLight : R_AL3

Intention	:	This predicate is true iff the machine assumes that the light in this area is controlled manually.
Scope	:	mh
Postreferences	:	msref AreaLight : M_AL8
		msref AreaLight : M_AL9
		msref HallwaySection : M_HS2
		msref RoomLight : M_RL4
		msref RoomLight : M_RL8
		msref RoomLight : M_RL9
		msref RoomLight : M_RL10
		msref RoomLight : M_RL11

Intention	:	This function represents the computation that results in the decision which light has to be on in order to achieve safe light in an area. evalSaveLight[i]=i means that the i-th light has to be on.
Scope	:	mh
Postreferences	:	msref AreaLight : M_AL7

Formal	:	( T_AL2 < T_AL1 )
NL	:	The time constant $T\_\mathit{AL}_2$ is allways smaller than the time constant $T\_\mathit{AL}_1$ .

Formal	:	( allLightsOff n NAT ( numLights ) : light[n]. ls. noMalSens. envEntity = 0 )
NL	:	The predicate allLightsOff is true iff all lights that are controlled by the machine are off.

Formal	:	( lightFMControlled occ. occUsed _{T_AL1} n NAT ( numLights ) : ( light[n]. ls. noMalSens. envEntity = lCPFM. lightOn. checked ) )
NL	:	Whenever the light is controlled by the facility manager using the control panel and the area is unoccupied for at least $T\_\mathit{AL}_1$ milliseconds, the status of the machine controlled lights equals within this time the status as it is determined by the facility manager.

Formal	:	( lightFMControlled occ. occUsed _{T_AL1} n NAT ( numLights ) : ( light[n]. ls. noMalSens. envEntity = 0 ) )
NL	:	Whenever the light is not controlled by the facility manager using the control panel and the area is unoccupied for at least $T\_\mathit{AL}_1$ milliseconds, all machine controlled lights are off within this time and remains off at least as long as the precondition is true.

Formal	:	( noSaveLight occ. occUsed _{T_AL1} safeLight )
NL	:	Whenever safe light has to be established and the area is occupied for at least $T\_\mathit{AL}_1$ milliseconds, the light is sufficient to move safely within this time span and remains sufficient to move safely at least as long as the precondition is true.

Formal	:	noSaveLight
NL	:	Initially safe light has to be established if an area is occupied.

Formal	:	lightFMControlled
NL	:	Initially the light is not controlled by the facility manager using his control panel.

Formal	:	( T_AL1 = 50 )
NL	:	The value of $T\_\mathit{AL}_1$ is always 50 miliiseconds.

Formal	:	( T_AL2 = 30 )
NL	:	The value of $T\_\mathit{AL}_2$ is always 30 miliiseconds.

Formal	:	( occ. noMalOcc. dt1 = 1000 )
NL	:	The first time delay used to determine occupancy concerning the light control is always 1 second.

Formal	:	( occ. noMalOcc. dt2 = 0 )
NL	:	The second time delay used to determine occupancy concerning the light control is always 0 second.

Formal	:	( occ. noMalOcc. dt3 = lCPFM. unoccDelay. checked )
NL	:	The third time delay used to determine occupancy concerning the light control corresponds always with the value entered by the facility manager for the time a certain area has to be unoccupied continuously before the lights are switched off.

Formal	:	( occ. malOcc. automaticDetermValue )
NL	:	The value determined automatically by the machine for occupancy concerning the light control in the case of a malfunction of some sensors used to determine occupancy concerning the light control is occupancy.

Formal	:	( noSaveLight occ. occUsed n NAT ( numLights ) : ( evalSaveLight(n) = 1 light[n]. ls. usedValue = 0 _{T_AL2} light[n]. pulse. noMalAct. adjustedEntity = 1 ) )
NL	:	Whenever safe light has to be established and the area is occupied the necessary actuators, i.e. pulse lines, are set within $T\_\mathit{AL}_2$ milliseconds to establish safe light.

Formal	:	( manualControl n NAT ( numLights ) : ( light[n]. manualControl ) occ. occUsed )
NL	:	The machine assumes that the light is controlled manually in an area iff at least one light in this area is controlled manually and the area is occupied.

Formal	:	( manualControl n NAT ( numLights ) : ( [ light[n]. pulse. noMalAct. adjustedEntity = 1 ] ) )
NL	:	If the light in an area is controlled manually, the settings of all lights remain unchanged.