Description Class Floor

INTENTION

This class is the main class. It contains and combines all the objects belonging to the considered system. These objects are

• the rooms of the floor
• the hallway sections of the floor
• the parts of the staircases belonging to the floor
• the outdoor light sensors
• the outdoor temperature sensor

DOMAIN KNOWLEDGE

Property	D_F1

NL

:

The two rooms with room numbers 435 and 433 are connected by a door.

Property	D_F2

NL

:

The two rooms with room numbers 433 and 431 are connected by a door.

Property	D_F3

NL

:

The two rooms with room numbers 425 and 423 are connected by a door.

Property	D_F4

NL

:

The two rooms with room numbers 423 and 421 are connected by a door.

Property	D_F5

NL

:

The two rooms with room numbers 418 and 416 are connected by a door.

Property	D_F6

NL

:

The two rooms with room numbers 416 and 414 are connected by a door.

Property	D_F7

NL

:

The eastern and middle hallway section are connected by a door.

Property	D_F8

NL

:

The middle and western hallway section are connected by a door.

REQUIREMENT SPECIFICATIONS

Property	R_F1

NL

:

Whenever some outdoor light sensors are not working correctly and the hallway is occupied for at least $T_{\mathit{malReact}}$ time units, then eventually within this time span, the light in the hallway is on and remains on at least as long as the precondition is true.

Property	R_F2

NonFormal

:

If a malfunction occurs, the control system supports the facility manager by finding the reason.

Property	R_F3

NonFormal

:

The system provides reports on current and past energy consumption.

Property	R_F4

NonFormal

:

All malfunctions and unusual conditions are stored and reported on request.

Property	R_F5

NonFormal

:

All hardware connections have to be made according to DIN standards.

Property	R_F6

NonFormal

:

No hazardous condition for persons, inventory or building are allowed.

Property	R_F7

NonFormal

:

The system issues warnings on unreasonable inputs.

MACHINE SPECIFICATIONS

Property	M_F1

NL

:

The machine assumes that some outdoor light sensor has a malfunction iff one of the six outdoor light sensors has a malfunction.

Property	M_F2

NL

:

Whenever the machine assumes that some outdoor light sensors are not working correctly, then the standard light scene is the standard fault light scene, i.e. all ceiling lights are on.