Template Declaration Area

INTENTION

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

• A set of ceiling light groups that can be controlled by the machine. The concrete number of controlled ceiling light groups 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 ceiling light groups using the facility manager control panel.
• The specification of the behavior of the system concerning the case that the ceiling light groups are controlled manually.

Postreferences	:	lsref HallwaySection : Area
		lsref Room : Area

FORMAL PARAMETERS

Function	numLights  NAT

Intention	:	This parameter represents the number of lights in an area that are controlled by the machine.
Postreferences	:	lsref Area : light
		lsref Area : evalSaveLight
		rsref Area : R_A1
		rsref Area : R_A2
		msref Area : M_A5
		msref Area : M_A6
		msref Area : M_A7
		msref Area : M_A8

Function	numPB  NAT

Intention

:

This parameter represents the number of push buttons that can be used by a person to control a ceiling light group in an area by bypassing the machine. The default number is 1, i.e., if nothing else is specified there is one such push button.

SIGNATURE

Object	occFM  :  Occupancy

Intention	:	This object represents the part of the light control concerning occupancy in an area as it is seen by the facility manager. Note that in the case of rooms there is also a second version of the aspect occupancy concerning the handling of light scenes (see description class Room, object occRoom.
Prereferences	:	pdref FM2
		pdref FM3
		pdref FM4
		pdref FM5
		pdref FM6
Postreferences	:	msref Area : M_A4
		msref HallwaySection : M_HS3
		rsref Area : R_A3
		msref Room : M_R11
		dkref HallwaySection : D_HS1
		rsref Floor : R_F1
		rsref Area : R_A1
		rsref Area : R_A2
		msref Area : M_A3
		msref Area : M_A5
		msref Area : M_A6
		msref Area : M_A7

Object	light  :  CeilingLightGroup[ numLights]

Intention	:	These objects represent the ceiling light groups in an area that are controlled by the machine.
Prereferences	:	akref BD_8
		akref BD_14
		akref BD_19
Postreferences	:	lsref Room : light
		rsref Floor : R_F1
		rsref Area : R_A1
		rsref Area : R_A2
		msref Area : M_A5
		msref Area : M_A6
		msref Area : M_A7
		msref Area : M_A8
		rsref HallwaySection : R_HS1
		rsref HallwaySection : R_HS2
		msref HallwaySection : M_HS4
		msref HallwaySection : M_HS5

Object	CPFM  :  AreaCtrlPanelFM

Intention	:	This object represents the facility manager control panel containing the entities for which the facility manager can enter a value.
Prereferences	:	pdref FM4
		pdref FM5
		pdref FM6
Postreferences	:	rsref Area : R_A1
		msref Area : M_A3
		msref HallwaySection : M_HS4
		msref Room : M_R14
		msref Floor : M_F5

Time Constant	T_A1

NL	:	occupation-to-safelight delay
Intention	:	This time constant represents the maximal time delay for the following situations: between the time point the facility manager switches off all ceiling light groups in an unoccupied area and the time point all ceiling light groups in this area are off, see Property R_A1. between the time point an area becomes unoccupied and the time point the machine controlled lights are off, see Property R_A2. between the time point an area becomes occupied and the time point at which safe light is established, see Property R_A3. This time constant is used to state requirement specifications.
Scope	:	ev
Prereferences	:	pdref U1
		pdref U13
		pdref FM2
		pdref FM3
		pdref FM6
Postreferences	:	msref Area : M_A1
		msref Area : M_A9
		rsref Area : R_A3
		rsref Area : R_A1
		rsref Area : R_A2
		msref HallwaySection : M_HS5

Time Constant	T_A2

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. This time constant is used to state machine specifications.
Scope	:	mh
Prereferences	:	pdref U1
		pdref U13
Postreferences	:	msref Area : M_A2
		msref Area : M_A9
		msref Area : M_A5
		msref Area : M_A6
		msref HallwaySection : M_HS5

Timed Function	dayLight   LIGHT_VALUES

Intention	:	This function represents the day light that the machine assumes to be available in an area.
Scope	:	mh
Prereferences	:	pdref FM1
Postreferences	:	msref Area : M_A5
		msref Room : M_R8
		msref Room : M_R8b

Timed Predicate	safeLight

NL	:	safe light
Intention	:	This predicate is true if and only if there is sufficient light to move safely.
Scope	:	eh
Prereferences	:	pdref U1
		pdref U13
Postreferences	:	rsref Area : R_A3

Timed Predicate	noSaveLight

Intention	:	This predicate is true if and only if 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 ceiling light groups are controlled manually.
Scope	:	mh
Prereferences	:	pdref U1
Postreferences	:	msref Area : I_M_A1
		msref HallwaySection : M_HS2
		msref Room : M_R3
		rsref Area : R_A3
		msref Area : M_A5

Timed Predicate	manualControl

Intention	:	This predicate is true if and only if the machine assumes that the ceiling light groups light in this area are controlled manually.
Scope	:	mh
Prereferences	:	pdref PD_30
Postreferences	:	msref HallwaySection : M_HS2
		msref Room : M_R3
		msref Area : M_A7
		msref Area : M_A8
		msref Room : M_R8
		msref Room : M_R8b
		msref Room : M_R9
		msref Room : M_R10

Timed Predicate	sensorActMalFct

Intention	:	This predicate is true if and only if a sensor or an actuator that is solely used by a room has a malfunction.
Scope	:	mh
Prereferences	:	pdref U8

Function	evalSaveLight  : NAT (  numLights ) ,  LIGHT_VALUES  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]=1 means that the i-th light has to be on. This computation depends at least from the current day light that the machine assumes to be available in an area.
Scope	:	mh
Prereferences	:	pdref U1
		pdref U13
		pdref FM1
Postreferences	:	msref Area : M_A5

REQUIREMENT SPECIFICATIONS

Property	R_A1

Formal	:	(  CPFM. lightOff. checked = 1  occFM. occUsed  T_A1       n NAT (  numLights ) :            (  light[n]. sl. noMalSens. envEntity = 0 ) )
NL	:	Whenever the light is switched off by the facility manager using the facility manager control panel and the area is unoccupied for at least T_A_1 milliseconds, all ceiling light groups are off within this time and remain off at least as long as the preconditions are fulfilled.

Property	R_A2

Formal	:	(  occFM. occEnv  T_A1       n NAT (  numLights ) :            (  light[n]. sl. noMalSens. envEntity = 0 ) )
NL	:	Whenever an area is unoccupied for at least T_A1 milliseconds, all ceiling light groups in this area are off within this time and remain off at least as long as the area is unoccupied.
Propreferences	:	dkref HallwaySection : D_HS1
		dkref ToggleActuator : D_TA1
		msref Area : M_A6
		msref HallwaySection : M_HS3
		msref Occupancy : M_O1
		msref NoMalfunctionOccupancy : M_NMO1
		dkref CeilingLightGroup : D_CLG1
		msref HallwaySection : M_HS5

Property	R_A3

Formal	:	(  noSaveLight  occFM. occUsed  T_A1  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.
Prereferences	:	pdref U1
		pdref U13

MACHINE SPECIFICATIONS

Property	I_M_A1

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

Property	M_A1

Formal	:	(  T_A1 = 50 )
NL	:	The value of T_AL_1 is always 50 milliseconds.

Property	M_A2

Formal	:	(  T_A2 = 30 )
NL	:	The value of T_AL_2 is always 30 milliseconds.

Property	M_A3

Formal	:	(  occFM. noMalOcc. delay =  CPFM. unoccDelay. checked )
NL	:	The time delay used to determine occupancy as it is seen by the facility manager corresponds always with the value entered by the facility manager for the time an area has to be unoccupied continuously before the lights are switched off.

Property	M_A4

Formal	:	(  occFM. malOcc. automaticDetermValue )
NL	:	The value determined automatically by the machine for occupancy as it is seen by the facility manager in the case of a malfunction of some sensors used to determine occupancy is always true, i.e., occupancy is assumed.
Prereferences	:	pdref NF4

Property	M_A5

Formal	:	(  noSaveLight  occFM. occUsed n NAT (  numLights ) :            (  evalSaveLight(n,  dayLight) = 1  light[n]. sl. usedValue = 0                  T_A2  light[n]. pulse. noMalAct. adjustedEntity = 1 ) )
NL	:	Whenever safe light has to be established in an area and this area is occupied then for all ceiling light groups in this area it holds: if a ceiling light group has to be on in order to achieve safe light and this ceiling light group is off then within T_A2 milliseconds a pulse to this ceiling light group is sent.
Prereferences	:	pdref U1

Property	M_A6

Formal	:	(  occFM. occUsed            n NAT (  numLights ) :            (  light[n]. sl. usedValue = 1                  T_A2  light[n]. pulse. noMalAct. adjustedEntity = 1 ) )
NL	:	Whenever the machine assumes no occupancy of an area then for all ceiling light groups in the area it holds: if a ceiling light group is on then within T_A2 milliseconds a pulse is sent.
Prereferences	:	pdref FM3
		pdref FM2
Propreferences	:	rsref Area : R_A2

Property	M_A7

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

Property	M_A8

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 ceiling light groups remain unchanged.

Property	M_A9

Formal	:	(  T_A2 <  T_A1 )
NL	:	The time constant T_AL_2 is always smaller than the time constant T_AL_1.