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.

DOMAIN KNOWLEDGE

Property	D_AL1

NL

:

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

Property	D_AL2

NL

:

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

REQUIREMENT SPECIFICATIONS

Property	R_AL1

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_AL2

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_AL3

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.

MACHINE SPECIFICATIONS

Property	I_AL1

NL

:

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

Property	I_AL2

NL

:

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

Property	M_AL1

NL

:

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

Property	M_AL2

NL

:

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

Property	M_AL3

NL

:

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

Property	M_AL4

NL

:

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

Property	M_AL5

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_AL6

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_AL7

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

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

NL

:

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