%---------------------------------------------------------------------------- Requirements Specification ??? 1.3 : %---------------------------------------------------------------------------- Organizational Aspects: ProjectName : Light_32_4 Authors : Peper, Kronenburg Status : after composition of 1.2 Declarations: Formalized Requirements: % ----------------------------------------------------------------------------- # The requirement specification for any kind of room ReqSpec Room (outdoorLightSensorFault) Intention : Contains the requirements speicification common to any kind of room. Declaration: Predicates : outdoorLightSensorFault : the outdoor light sensor does not work correctly U11, NF1a, NF1b, NF2 roomOccupied : the room is occupied by a person U1, U2, U3, U4, FM3, FM6 safeLight : light is sufficient to move safely U1 lightScene : a light scene is chosen U1 switchPushed : the switch is pushed down U5i, U5ii lightOn : The corresponding light is completely on U5i, U5ii lightOff : The corresponding light is completely off U5i userInformed : the user is informed U11 lightOff : all lights are off FM1, FM3, FM6 fmLightOff : the facility manager has turned the light off FM6 sensorFault : the motion detector does not work correctly NF4a, NF4b standardIsCeilingLightsOn : the standard light scene is "all ceiling lights on". NF2 Domains: LS : the possible light scenes - at least { on, off, ambient } U2, U3, U4, U6, U7, U16i, U16ii OL : outdoor light values NF1a, NF1b MV : the motion values, at least { occupied } NF4a, NF4b Functions: appliedLightScene : LS the light scene "l" is applied by the system U2, U3, U4, U6, U7 chosenLightScene : LS the light scene "l" was last selected at the control panel U2, U3, U6, U7 cpCeilingLight : LS the ceiling light scene set by the control panel U16i ceilingight : LS the ceiling light scene set by the system U16i cpLightLevel : LS the ambient light level set by the control panel U16ii lightLevel : LS the ceiling light level U16ii outdoorLight : OL the outdoor light value returned by the sensor NF1a outdoorLightValue : OL the outdoor light value used by the system NF1a, NF1b lastCorrectLight : OL the last correct outdoor light value returned by the sensor NF1b motion : MV the motion detector value returned by the sensor NF4a motionValue : MV the motion detector value used by the system NF4a, NF4b Constants : T_U1 : The time delay between occupation of a room, when no light scene is chosen, and the establishment of a safe light scene U1 T_U3a : the time delay during which the reoccupation of a room leads to reestablishing the previous light scene U3 T_U3b : the time delay between a sufficiently often occupation and the application of the chosen light scene U3 T_U4a : the time delay during which the reoccupation of a room leads to reestablishing the previous light scene U4 T_U4b : the time delay between a sufficiently long non-occupation and the application of the standard light scene U4 TU5 : The maximal time between pushing the switch and switching off the light. U5i TU5 : The maximal time between pushing the switch and switching on the light. U5ii T_U6 ; time delay between selection and application of a certain light scene U6 T_U7 ; time delay between selection and application of a certain light scene U7 T_U16 : the time delay between setting and applying a certain light level U16i T_U16 : the time delay between setting and applying a certain light level U16ii T3 : the time delay between a sufficiently long non-occupation of the room and switching off the light FM3 T_FM6 : the time delay between a sufficiently long non-occupation of the room or hallway, if the f.m. has turned the light off and actually switching off the light. FM6 T_NF1a: the time delay between a correct sensor operation and the corresponding system behaviour NF1a T_2 : the time delay between outdoorLightValue and outdoorLight NF1a T_NF1b: the time delay between a sensor fault and the corresponding system behaviour NF1b T_NF4a: the time delay between a correct sensor operation and the corresponding system behaviour NF4a T_2 : the time delay between motion and motionValue NF4a % ----------------------------------------------------------------------------- Formalization: U1: Formal : \always ( roomOccupied \and \not lightScene \delImp_{T_U1} safeLight ) NL : Whenever the room is occupied and no light scene is chosen for at least time T_{U1}, the light becomes sufficient to move safely within this time span. and remains sufficient to move safely at least as long as the precondition is true. References : PD-Sec3.1.1/U1 PatternInst : DelayedImplication (roomOccupied \and \not lightScene, safeLight, T_U1) CustomerReq : Is it desired that a light scene "Dark" is applicable to an occupied room, thus suppressing the safe light condition? It is assumed that the "dark" light scene is allowed. U2: Formal : \always ( \forall l: (roomOccupied and chosenlightScene=l) \delImp_{T_U2} appliedLightScene=l) NL : Whenever the room is occupied and light scene l is chosen for at least time T_{U1}, this light scene l is applied within this time span. and remains applied at least as long as the precondition is true. References : PD-Sec3.1.1/U2 PatternInst : ConditionalContinuity (roomOccupied, lightScene) CustomerReq : Does this even exclude any change of the light scene during the room occupation? What is the meaning of "lightScene"? ANY light scene is chosen or a CERTAIN light scene is chosen? "ANY" is supposed. U3: Formal : \always ( ( [roomOccupied] \and \sometimesInThePast_{(0, T_U3a]} roomOccupied \and chosenLightScene=l) \imp \eventually_{T_U3b} appliedLightScene=l) NL : Whenever the room becomes occupied now and was occupied sometimes within the last T_U3a minutes and the light scene l was last chosen, the light scene l is applied within T_U3b time units. References : PD-Sec.3.1.1/U3 CustomerReq : Or is the last APPLIED light scene to be reestablished? Is it possible that another light scene is chosen between the last occupation and the reoccupation? U4: Formal : \always ( [roomOccupied] \and \alwaysInThePast_{(0,TU4a]} \not roomOccupied) \imp \eventually_{T_U4b} appliedLightScene="standard") NL : Whenever the room becomes occupied now and was not occupied during the last T_U4a minutes, the light scene 'standard' is applied within T_U4b time units. References : PD-Sec.3.1.1/U4 U5i: Formal : \always ( [switchPushed] \and lightOn \imp \eventually_{\leq TU5i} lightOff ) NL : Whenever the switch becomes pushed and the light is completely on, the light is completely off within TU5 time units. References : PD-Sec.3.1.1/U5(i) CustomerReq : How long should the light be switched off? Is this defined by U2? U5ii: Formal : \always ( [switchPushed] \and \not lightOn \imp \eventually_{\leq TU5} lightOn ) NL : Whenever the switch becomes pushed and the light is not completely on, the light is completely on within TU5 time units. References : PD-Sec.3.1.1/U5(ii) CustomerReq : How long should the light be switchend on? Is this defined by U2? U6: Formal : \always ( \forall l: chosenLightScene = l \delEquiv_{T_U6} appliedLightScene = l ) NL : Whenever the light scene "l" was last selected at the control panel, the light scene "l" is applied within T_U6 time units. NonFormal : by using the control panel. References : PD-Sec.3.1.1/U6 U7: Formal : \always ( chosenLightLevel = l \delEquiv_{\leq T_U7} appliedLightLevel = l ) NL : Whenever the light level "l" was last selected at the control panel, the light level "l" is applied within T_U7 time units. NonFormal : by using the control panel. References : PD-Sec.3.1.1/U7 U8: NonFormal : For each room a default light scene can be set (not by using the control panel). References : PD-Sec3.1.1/U8 U9: NonFormal : For each room a default ambient light level can be set (not by using the control panel). References : PD-Sec3.1.1/U9 U10: NonFormal : The value T1 can be set for each room seperately (not by using the control panel). References : PD-Sec3.1.1/U10 U11: Formal : \always ( outdoorLightSensorFault \delEquiv_{T_{U11}} userInformed ) NL : Whenever the outdoor sensor does not work correctly for at least time T_{U11}, the user is informed within time T_{U11} and remains informed as long as the precondition is true. And conversely, whenever the outdoor light sensor works correctly for at least time T_{U11}, the user is no longer informed within time T_{U11} and is not informed as long as this precondition is true. References : PD-Sec3.1.1/U11 PatternInst : DelayedEquivalence (outdoorLightSensorFault, userInformed) CustomerReq : What is the meaning of 'the user is informed'? U15: NonFormal : In all other rooms the control panel should be installed near a door to the hallway. References : PD-Sec3.1.1/U15 U16i: Formal : \always ( \forall l: cpCeilingLight=l \delEquiv_{T_{U16}} ceilingLight=l ) NL : Whenever the ceiling light switch in the control panel is l the ceiling light will be l within T_U16 time units and stays l as long as the precondition is true. NonFormal : The ceiling light switch is contained in the control panel. References : PD-Sec3.1.1/U16(i) PatternInst : DelayedEquivalence (cpTaskLight, taskLight, T_U16) CustomerReq : What does ceilingLight="ambient" mean ? U16ii: Formal : \always ( cpLightLevel \delEquiv_{T_{U16}} lightLevel ) NL : Whenever the light level in the control panel is set to "l" the light level will be "l" within T_U16 time units and stays "l" as long as the precondition is true. NonFormal : The ambient light level setting is contained in the control panel. References : PD-Sec3.1.1/U16(ii) PatternInst : DelayedEquivalence (cpLightLevel, lightLevel, T_U16) FM1: Formal : \always ( lightOff ) NL : the light is always off References : PD-Sec3.1.2/FM1 Comment : Waiting for conflicts ... CustomerReq : This requirement is expected to have lowest priority in case of potential conflicts. Was this your intention? FM3: Formal : \always ( \not roomOccupied \delImp_{T3 min} lightOff ) NL : Whenever the room is continuously not occupied for at least T3 minutes, then the light is off within this time span and remains off at least as long as the room is not occupied. References : PD-Sec3.1.2/FM2 PatternInst : DelayedImplication (roomOccupied, lightOff, T2) FM5: NonFormal : The value T3 can be set for each room separatly. References : PD-Sec3.1.2/FM5 Comment : Is this achieved by instantiating T3 for each room? FM6: Formal : \always ( fmLightOff \and \not occupied \delImp_{\leq T_{FM6}} lightOff ) NL : Whenever the facility manager has turned the light off and the hallway/room is not occupied for at least T_FM6 time units, then eventually within this time span, the light is off and remains so at least as long as the facility manager has turned the light off and the hallway/room is not occupied. References : PD-Sec3.1.2/FM6 PatternInst : DelayedImplication (fmLightOff \and \not occupied, lightOff, T_FM6) NF1a: Formal : \always ( (\not outDoorLightSensorFault \delImp_{T_NF1a} (\forall v : outdoorLightValue=v \delCopy_{T_2} outdoorLight=v)) ) NL : Whenever the outdoor light sensor does work correctly for at least T_NF1a time units, then eventually within this time span, the outdoor light value used by the system is equal to the outdoor light value returned by the sensor with a maximal delay of T_2 time units. References : PD-Sec3.1.3/NF1 Comment : Additional requirement covering the "normal case". New operator is currently developed. NF1b: Formal : \always ( (outDoorLightSensorFault \delImp_{T_NF_1b} outdoorLightValue=lastCorrectLight ) ) NL : Whenever the outdoor light sensor does not work correctly for at least T_NF1b time units, the outdoor light value used by the system is equal to the last correct light value returned by the sensor, and this remains so at least as long as the precondition is true. References : PD-Sec3.1.3/NF1 NF2: Formal : \always ( outDoorLightSensorFault \delImp_{T_NF2} standardIsCeilingLightsOn NL : Whenever the outdoor light sensor does not work correctly for at least T_NF2 time units, then eventually within this time span, the standard light scene is "all ceiling lights on" and remains so at least as long as the outdoor light sensor does not work correctly. References : PD-Sec3.1.3/NF2 PatternInst : DelayedImplication (outDoorLightSensorFault, standardLightScene = "all ceiling lights on", T_NF2) CustomerReq : Is the standard light scene in this case to be applied? "No" is supposed. NF4a: Formal : \always ( (\not sensorFault \delImp_{T_NF4a} (\forall v : motion=v \delCopy_{T_2} motionValue=v)) ) NL : Whenever the motion detector does work correctly, the motion detector value used by the system is equal to the motion detector value returned by the sensor. References : PD-Sec3.1.3/NF4 Comment : Times ? Copied and adapted from NF1 -> Pattern ? -> DelayedCopy as in NF1a NF4b: Formal : \always ( (sensorFault \delImp_{T_NF4b} motionValue='occupied' ) ) NL : Whenever the motion sensor does not work correctly for at least T_NF4b time units, the motion value used by the system is 'occupied' and this remains so at least as long as the precondition is true. PatternInst : DelayedImplication (sensorFault, motionValue='occupied', T_NF4b) References : PD-Sec3.1.3/NF4 # End ReqSpec "Room" % ----------------------------------------------------------------------------- % ----------------------------------------------------------------------------- # The requirement specification for offices ReqSpec Office Declaration: Predicates : Domains : LS : the possible light scenes U12 Functions : appliedLightScene : LS the light scene applied by the system U12 chosenLightScene : LS the light scene last selected at the control panel U12 cpTaskLight : the task light switch in the control panel is "on" U14i taskLight : the task light is on U14i cpCeilingLight : the stste of the ceiling light switch in the control panel U14ii ceilingLight : the state of the ceiling light (on/off/ambient) U14ii cpLightLevel : the ambient light level set by the control panel U14iii lightLevel : the ceiling light level U14iii Constants : T_U12 : the time delay between choosing and applying a certain light scene U12 T_U14 : the time delay between setting and applying a certain light level U14i T_U14 : the time delay between setting and applying a certain light level U14ii T_U14 : the time delay between setting and applying a certain light level U14iii % ----------------------------------------------------------------------------- Formalization: U12: Formal : \always ( \forall l chosenLightScene=l \delImp_{T} appliedLightScene=l ) NL : Whenever the chosen light scene is l for at least time T_{U12}, the applied light scene is l within time T_{U12} and remains l as long as the precondition is true. References : PD-Sec3.1.1/U12 CustomerReq : Is this depending on the occupation of the office? See U2. U13: NonFormal : The control panel should be installed moveably like a telephone in the offices. References : PD-Sec3.1.1/U13 U14i: Formal : \always ( cpTaskLight \delEquiv_{T_{U14}} taskLight ) NL : Whenever the task light switch in the control panel is on (off), the task light will be on (off) within T_U14 time units and stays on (off) as long as the precondition is true. NonFormal : The task light switch is contained in the control panel. References : PD-Sec3.1.1/U14(i) PatternInst : DelayedEquivalence (cpTaskLight, taskLight, T_U14) Comment : This could lead to potential conflicts with other requirements that also try to control taskLight. Should be replaced by a formulation that allows other source predicates to have influence on the target predicate. Last access or higher priority wins? -> New pattern definition! U14ii: Formal : \always ( \forall l: cpCeilingLight=l \delEquiv_{T_{U14}} ceilingLight=l ) NL : Whenever the ceiling light switch in the control panel is on (off), the ceiling light will be on (off) within T_U14 time units and stays on (off) as long as the precondition is true. NonFormal : The ceiling light switch is contained in the control panel. References : PD-Sec3.1.1/U14(ii) PatternInst : DelayedEquivalence (cpTaskLight, taskLight, T_U14) CustomerReq : What does ceilingLight="ambient" mean ? U14iii: Formal : \always ( cpLightLevel \delEquiv_{T_{U14}} lightLevel ) NL : Whenever the light level in the control panel is set to "l" the light level will be "l" within T_U14 time units and stays "l" as long as the precondition is true. NonFormal : The ambient light level setting is contained in the control panel. References : PD-Sec3.1.1/U14(ii) PatternInst : DelayedEquivalence (cpLightLevel, lightLevel, T_U14) % End ReqSpec "Office" % ----------------------------------------------------------------------------- % ----------------------------------------------------------------------------- # The requirement specification for hallway sections ReqSpec Hallway (nearHallwayDoor, outDoorSensorFault) Declaration: Predicates : nearHallwayDoor : a person is near a hallway door to this hallway U18 outDoorSensorFault : the outdoor light sensor does not work correctly NF3 hallwayOccupied1 : there is a person near hallway section door 1 hallwayOccupied2 : there is a person near hallway section door 2 hallwayOccupied : the hallway is occupied by a person U17, FM2, NF3 safeLight : the hallway light is sufficient to move safely U17 lightOn : the light in the hallway is on NF3, NF5, U19i, U19ii, U18 lightOff : The light in the hallway is off U19i, U19ii, FM2 switchPushed : the wall switch is pushed down U19i, U19ii uncontrollableLight : the lights are neither controllable automatically nor manually NF5 Constants : T_U17 : the time delay between a hallway occupation and the safe light status U17 T_U18 : the time delay between a sufficiently long occupation of an adjacent hallway and switching on the lights U18 TU19 : The maximal time between pushing the switch and switching off the light. U19i, U19ii T2 : the time delay between a sufficiently long occupation of the hallway and switching off the light FM2 T_NF5: the time delay between the loss of ligth control and switching on the lights. NF5 % ----------------------------------------------------------------------------- Formalization : U17: Formal : \always ( hallwayOccupied \delImp_{T_U17} safeLight ) NL : Whenever the hallway is occupied for at least time T_{U17}, the light is sufficient to move safely within time T_{U17} and remains sufficient to move safely as long as the precondition is true. References : PD-Sec3.1.1/U17 Comment : Analogous to U1 -> pattern definition or "derivation" from a common requirement type? U18: Formal : \always ( nearHallwayDoor \delImp_{T_{U18}} lightOn ) NL : Whenever a person is continuously in the near of a door to the hallway for at least T_U18 time units, then the light in the hallway will be on within this time span, and remains on at least as long as the person is near the hallway. References : PD-Sec3.1.1/U18 PatternInst : DelayedImplication (nearHallwayDoor, lightOn) Comment : "before" is here interpreted geographically and not temporally. The time T_U18 should be set to value reasonable for typical pedestrian speeds. U19i: Formal : \always ( [switchPushed] \and lightOn \imp \eventually_{\leq TU19} lightOff ) NL : Whenever the switch becomes pushed and the light is on, the light is off within TU19 time units. References : PD-Sec.3.1.1/U19(i) U19ii: Formal : \always ( [switchPushed] \and \not lightOn \imp \eventually_{\leq TU19} lightOn ) NL : Whenever the switch becomes pushed and the light is not on, the light is on within TU19 time units. References : PD-Sec.3.1.1/U19(ii) FM2: Formal : \always ( \not hallwayOccupied \delImp_{T2 min} lightOff ) NL : Whenever the hallway is continuously not occupied for at least T2 minutes, then the light is off within this time span and remains off at least as long as the hallway is not occupied. References : PD-Sec3.1.2/FM2 PatternInst : DelayedImplication (hallwayOccupied, lightOff, T2) FM4: NonFormal : The value T2 can be set for each hallway section separatly. References : PD-Sec3.1.2/FM4 Comment : Is this achieved by instantiating T2 for each hallway section? NF3: Formal : \always ( sensorFault \and hallwayOccupied \delImp_{T_NF3} lightOn ) NL : Whenever the outdoor light sensor does not work correctly and the hallway is occupied for at least T_NF3 time units, then eventually within this time span, the light in the hallway is on and remains on at least as long as the outdoor light sensor does not work correctly and the hallway is occupied. References : PD-Sec3.1.3/NF3 PatternInst : DelayedImplication (sensorFault \and hallwayOccupied, lightOn, T_NF3) NF5: Formal : \always ( uncontrollableLight \delImp_{T_NF5} lightOn ) NL : Whenever the lights are neither controllable automatically nor manually for at least T_NF5 time units, then eventually within this time span, the light in the hallway is on and remains so at least as long as the lights are neither controllable automatically nor manually. PatternInst : DelayedImplication (uncontrollableLight, lightOn, T_NF5) References : PD-Sec3.1.3/NF5 % End "ReqSpec "Hallway" % ----------------------------------------------------------------------------- % ----------------------------------------------------------------------------- ReqSpec ControlSystem Declaration: Predicates: malfunction : a malfunction occurs FM7 fmInformed : the facility manager is informed FM7 outdoorLightSensorFault : the outdoor light sensor does not work correctly staircase1.occupied : the staircase 1 is occupied HALLWAYS staircase2.occupied : the staircase 2 is occupied HALLWAYS Domains: Rooms = {Zi1, ....} Offices = { ... } Constants : T : the time delay between a malfunction and the information of the facility manager. FM7 % ----------------------------------------------------------------------------- Formalization: ROOMS: Formal : \bigand_{r \in Rooms} r.Room (outdoorLightSensorFault) NL : The "Room" requirements are satisfied for each room. PatternInst : Room (outdoorLightSensorFault) OFFICES: Formal : \bigand_{o \in Offices} o.Office (outdoorLightSensorFault) NL : The "Office" requirements are satisfied for each office. PatternInst : Office (outdoorLightSensorFault) HALLWAYS: Formal : hw1.Hallway (staircase1.occupied \or hw2.roomOccupied1, outdoorLightSensorFault) \and hw2.Hallway (hw1.roomOccupied2 \or hw3.roomOccupied1, outdoorLightSensorFault) \and hw3.Hallway (hw2.roomOccupied2 \or staircase2.occupied, outdoorLightSensorFault) NL : The "Hallway" requirements are satisfied for each hallway section regarding the respective occupancy values. PatternInst : Hallway (...) FM7: Formal : \always ( malfunction \delEquiv_{T}} fmInformed ) NL : Whenever a malfunction occurs for at least time T, the f.m. is informed within time T and remains informed as long as the precondition is true. And conversely, whenever no malfunction occurs for at least time T, the f.m. is no longer informed within time T and is not informed as long as this precondition is true. References : PD-Sec3.1.2/FM7 PatternInst : DelayedEquivalence (malfunction, fmInformed, T) CustomerReq : What is a "malfunction"? What means 'the facility manager has to be informed'? Comments : (copied from U11) FM8: NonFormal : If a malfunction occurs, the control system supports the facility manager by finding the reason. Comment : I suppose that "finding the reason" means locating the fault in the future control system architecture. But architecture is something unknown to this specification level. References : PD-Sec3.1.2/FM8 FM9: NonFormal : The system provides reports on current and past energy consumption. References : PD-Sec3.1.2/FM9 FM10: NonFormal : All malfunctions and unusual conditions are stored and reported on request References : PD-Sec3.1.2/FM10 FM11: NonFormal : Malfunctions that the system cannot detect can be entered manually. References : PD-Sec3.1.2/FM11 NF6: NonFormal : All hardware connections have to be made according to DIN standards. References : PD-Sec3.1.3/NF6 NF7: NonFormal : No hazardous condition for persons, inventory or building are allowed. References : PD-Sec3.1.3/NF7 Comment : Formalize? NF8: NonFormal : The control panel should be easy and intuitive to use. References : PD-Sec3.1.3/NF8 NF9: NonFormal : The system warns about unreasonable inputs. References : PD-Sec3.1.3/NF9 Comment : Formalize? % End ReqSpec "ControlSystem" % ----------------------------------------------------------------------------- % -----------------------------------------------------------------------------