%---------------------------------------------------------------------------- Requirements Specification ??? 1.0 : %---------------------------------------------------------------------------- Organizational Aspects: ProjectName : Light_32_4 Authors : Peper Status : ??? Declarations: Formalized Requirements: % ----------------------------------------------------------------------------- U1 : Predicates : roomOccupied : the room is occupied by a person safeLight : light is sufficient to move safely lightScene : a light scene is chosen Formal : \always ( roomOccupied \and \not lightScene \imp safeLight ) NL : Whenever the room is occupied and no light scene is chosen, the light is sufficient to move safely. References : PD-Sec3.1.1/U1 PatternInst : Comment : Is it desired that a light scene "Dark" is applicable to an occupied room, thus suppressing the safe light condition? U2 : Predicates : roomOccupied : the room is occupied by a person lightScene : a light scene is chosen Formal : \always ( (roomOccupied and lightScene) \imp (lightScene \waitsfor \not roomOccupied) ) NL : Whenever the room is occupied by a person and a light scene is chosen, the light scene remains chosen until the room is not occupied. References : PD-Sec3.1.1/U2 PatternInst : ConditionalContinuity (roomOccupied, lightScene) Comment : 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? U3: Predicates : roomOccupied : the room is occupied by a person chosenLightScene = l : the light scene "l" is chosen appliedLightScene = l : the light scene "l" is applied Formal : \always ( ( roomOccupied \and \sometimesInThePast_{\leq T1} roomOccupied \and chosenLightScene=l) \imp appliedLightScene=l) NL : Whenever the room is occupied now and was occupied sometimes within the last T1 minutes and the light scene l was last chosen, the light scene l is applied. References : PD-Sec.3.1.1/U3 Comment : Or is the last APPLIED light scene to be reestablished? U4: Predicates : roomOccupied : the room is occupied by a person appliedLightScene = "standard" : the standard light scene is applied Formal : \always ( roomOccupied \and \alwaysInThePast \not roomOccupied) \imp appliedLightScene="standard" NL : Whenever the room is occupied now ans was not occupied during the last T1 minutes, the light scene 'standard' is applied. References : PD-Sec.3.1.1/U4 U5: Comment : Sorry - incomprehensible! Which lights are considered? References : PD-Sec.3.1.1/U5 U6: Predicates : chosenLightScene = l : the light scene "l" is chosen ctrlPanelLightScene = l : the light scene "l" was last selected at the control panel Formal : \always ( ctrlPanelLightScene = l \imp chosenLightScene = l ) NL : Whenever the light scene "l" was last selected at the control panel, the light scene "l" is chosen. References : PD-Sec.3.1.1/U6 Comment : This is in fact the "DelayedImplication", but generelized for a set of corresponding predicates. U7a: Predicates : chosenLightLevel = l : the light level "l" is chosen ctrlPanelLightLevel = l : the ambient light level "l" was last selected at the control panel Formal : \always ( ctrlPanelLightLevel = l \imp chosenLightLevel = l ) NL : Whenever the light level "l" was last selected at the control panel, the light level "l" is chosen. References : PD-Sec.3.1.1/U7 U7b: Predicates : chosenLightLevel = l : the light level "l" is chosen appliedLightLevel = l : the ambient light level "l" is set Formal : \always ( chosenLightLevel = l \imp_{\leq T_U7} chosenLightLevel = l ) NL : Whenever the light level "l" was last selected at the control panel, the light level "l" is chosen. References : PD-Sec.3.1.1/U7 Comment : This is in fact the "DelayedImplication", but generelized for a set of corresponding predicates. U8: Predicates : defaultLightScene : the default light scene is set References : PD-Sec3.1.1/U8 NonFormal : the default light scene can not be set by the control panel U9: Predicates : defaultLightLevel : the default ambient light level is set References : PD-Sec3.1.1/U9 U10: Formal : true Comment : This is formally represented by the fact, that T1 can be arbitrarily set for each instantiation of specification type "room" or does this mean "can be set dynamically during system life time" ? U11: Predicates : outdoorLightSensorFault : the outdoor light sensor does not work correctly userInformed : the user is informed 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) U12: Predicates : ceilingLight(l) : the status of the ceiling light depending on the applied light scene taskLight (l) : the status of the task light dep ... appliedLightScene = l : the light scene "l" is applied by the control system References : PD-Sec3.1.1/U12 U13: NonFormal : The control panel should be installed moveably like a telephone in the offices. References : PD-Sec3.1.1/U13 U14_i Predicates : cpTaskLight : the task light switch in the control panel is "on" taskLight : the task light is on 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. 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! U14_ii Predicates : cpCeilingLight = l: the ceiling light switch in the control panel is "l" ceilingLight = l : the ceiling light is "l" (on/off/ambient) Formal : \always ( cpCeilingLight \delEquiv_{T_{U14}} ceilingLight ) 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. References : PD-Sec3.1.1/U14(ii) PatternInst : DelayedEquivalence (cpTaskLight, taskLight, T_U14) Comment : What does ceilingLight="ambient" mean ? The DelayedEquivalence pattern must be extended to more than binary source and target sizes! U14_iii Predicates : cpLightLevel =l : the ambient light level set by the control panel is "l" lightLevel =l : the ceiling light level "l" 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. References : PD-Sec3.1.1/U14(ii) PatternInst : DelayedEquivalence (cpLightLevel, lightLevel, T_U14) U15: NonFormal : In all other rooms the control panel should be installed near a door to the hallway. References : PD-Sec3.1.1/U15 U16: as U14i and U14ii U17: Predicates : hallwayOccupied : the hallway is occupied by a person safeLight : the hallway light is sufficient to move safely Formal : \always ( hallwayOccupied \and \not lightScene \imp safeLight ) NL : Whenever the hallway is occupied, the light is sufficient to move safely. References : PD-Sec3.1.1/U17 Comment : Analogous to U1 -> pattern definition or "derivation" from a common requirement type? U18: Predicates : nearNextHallway(i,i+1) : a person is in hallway i near the door to hallway i+1 lightOn(i+1) : the light in hallway i+1 is on Formal : \always ( nearNextHallway (i,i+1) \delImp_{T_{U18}} lightOn(i+1) ) NL : Whenever a person is continuously in hallway i near the door to hallway i+1 for at least T_U18 time units, then the light in hallway i+1 will be on within this time span, and remains on at least as long as the person is near the next hallway. References : PD-Sec3.1.1/U18 PatternInst : DelayedImplication (nearNextHallway(i,i+1), lightOn(i+1)) Comment : "before" is here interpreted geographically than temporally. The time T_U18 should be set to value reasonable for typical pedestrian speeds. U19: Non-Formal : see Prob.Desc. References : PD-Sec3.1.1/U19 Comment : Cannot understand as in U5! % ----------------------------------------------------------------------------- FM1: Predicates : lightOff : the light is off Formal : \always ( lightOff ) NL : the light is always off References : PD-Sec3.1.2/FM1 Comment : Waiting for conflicts ... FM2: Predicates : hallwayOccupied : the hallway is occupied by a person lightOff : the light is off Formal : \always ( \not hallwayOccupied \delImp_{T2 min} lightOff ) NL : Whenever the hallway is continously 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) FM3: Predicates : roomOccupied : the room is occupied by a person lightOff : the light is off Formal : \always ( \not roomOccupied \delImp_{T2 min} lightOff ) NL : Whenever the room is continously 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 room is not occupied. References : PD-Sec3.1.2/FM2 PatternINst : DelayedImplication (roomOccupied, lightOff, T2) FM4: NonFormal : The value T2 can be set for each hallway section separatly. References : PD-Sec3.1.2/FM4 Comment : See U10 ! FM5: NonFormal : The value T3 can be set for each room separatly. References : PD-Sec3.1.2/FM5 Comment : See U10 ! FM6: Predicates : fmLightOff : the facility manager has turned the light off occupied : the room or hallway is occupied lightOff : the light is off Formal : \always ( fmLightOff \and \not occupied \and \not lightOff \imp \eventually_{\leq T_{FM6}} lightOff \or \not fmLightOff \or occupied) NL : Whenever the facility manager has turned the light off and the ??? is not occupied, the light is off within T_FM6 or the facility manager no longer turns the light off or the ??? is occupied. References : PD-Sec3.1.2/FM6 PatternInst : ConditionalBoundedResponse (fmLightOff \and \not occupied, lightOff, T_FM6) FM7: Predicates: malfunction : a malfunction occurs fmInformed : the facility manager is informed Formal : \always ( malfunction \delEquiv_{T_{U11}} fmInformed ) NL : Whenever a malfunction occurs for at least time T_{U11}, the f.m. is informed within time T_{U11} and remains informed as long as the precondition is true. And conversely, whenever no malfunction occurs for at least time T_{U11}, the f.m. is no longer informed within time T_{U11} and is not informed as long as this precondition is true. References : PD-Sec3.1.2/FM7 PatternInst : DelayedEquivalence (malfunction, fmInformed, T_U11) Comment : What is a "malfunction"? (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 % ----------------------------------------------------------------------------- NF1a: Predicates : sensorFault : the outdoor light sensor does not work correctly outdoorLight : the outdoor light value returned by the sensor outdoorLightValue: the outdoor light value used by the system Formal : \always ( (\not sensorFault \imp (outdoorLightValue=outdoorLight)) ) NL : Whenever the outdoor light sensor does work correctly, the outdoor light value used by the system is equal to the outdoor light value returned by the sensor. References : PD-Sec3.1.3/NF1 Comment : Times ? NF1b: Predicates : sensorFault : the outdoor light sensor does not work correctly outdoorLight : the outdoor light value returned by the sensor outdoorLightValue: the outdoor light value used by the system Formal : \always ( (sensorFault \imp \not [outdoorLightValue] ) ) NL : Whenever the outdoor light sensor does work not correctly, the outdoor light value used by the system does not change. References : PD-Sec3.1.3/NF1 Comment : Times ? NF2: Predicates : sensorFault : the outdoor light sensor does not work correctly standardLightScene = "all ceiling lights on" : Formal : \always ( sensorFault \delImp_{T_NF2} standardLightScene = "all ceiling lights on" ) 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 (sensorFault, standardLightScene = "all ceiling lights on", T_NF2) Comment : Is the standard light scene in this case to be applied? NF3: Predicates : sensorFault : the outdoor light sensor does not work correctly hallwayOccupied (i) : hallway i is occupied hallwayLightsOn (i) : the light in hallway i is on Formal : \always ( sensorFault \and hallwayOccupied(i) \delImp_{T_NF3} hallwayLightsOn (i) ) NL : Whenever the outdoor light sensor does not work correctly and hallway i is occupied for at least T_NF3 time units, then eventually within this time span, the light in hallway i is on and remains on at least as long as the outdoor light sensor does not work correctly and hallway i is occupied. References : PD-Sec3.1.3/NF3 PatternInst : DelayedImplication (sensorFault \and hallwayOccupied (i), hallwayLightsOn (i), T_NF3) NF4a: Predicates : sensorFault : the motion detector does not work correctly motion : the motion detector value returned by the sensor motionValue : the motion detector value used by the system Formal : \always ( (\not sensorFault \imp (motionValue=motion)) ) 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 ? NF4b: Predicates : sensorFault : the motion detector does not work correctly motion : the motion detector value returned by the sensor motionValue : the motion detector value used by the system Formal : \always ( (sensorFault \imp \not [motionValue] ) ) NL : Whenever the motion detector does work not correctly, the motion detector value used by the system does not change. References : PD-Sec3.1.3/NF4 Comment : Times ? NF5: Predicates : uncontrollableLight: the lights are neither controllable automatically nor manually lightOn : the light is on Formal : \always ( uncontrollableLight \imp lightOn ) NL : Whenever the lights are neither controllable automatically, the light is on. References : PD-Sec3.1.3/NF5 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?