%============================================================================== Requirements Specification 2.2 : %============================================================================== %============================================================================== %============================================================================== %============================================================================== Organizational Aspects: ProjectName : Light_32_4 Authors : Kronenburg, Peper Status : after "formal review" Referenced Document : InAr : team3_inst_arch.v1.fm Referenced Document : PD : team3-problemdescription % This document contains the formalization of several needs for a new light % control system for the fourth floor of building 32 of the University of % Kaiserslautern. The needs are given in the document Problemdescription. Needs % which could up to now not be formalized are presented in their natural % language version. A more informal description of the environment in which the % control system should be embedded is given in the document % team3_inst_arch.v[n].fm. A more informal explanation of the terms and % entities used in this requirements are given in the document dictionary. The % formal definitions of the terms used in this document are given in the % document domain knowledge. % % The main motivation for the development of a new light control system are the % disadvantages of the currently existing system. Since all lights are % controlled manually, electrical energy is wasted by lighting rooms which are % not occupied and by little possibilities to adjust light sources relative to % need and daylight. % % Additionally this document contains a formalization of the environment. %============================================================================== %============================================================================== %============================================================================== %============================================================================== % eingebaute Typen: % BOOLEAN : {true, false} % INTEGER : ganze Zahlen % NATURAL : natürliche Zahlen % BINARY : {0,1} \subset NATURAL % PERCENT : {0, ..., 100} \subset NATURAL % TIME : corresponding time domain, currently NATURAL with unit % milliseconds %============================================================================== %============================================================================== % F A C I L I T Y M A N A G E R %============================================================================== %============================================================================== Description Class FacMan (Domain R) %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Signature %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Timed Predicate: lightOff (R) NL : facility manager light off Intention : the facility manager has turned all lights off in a certain room Scope : eh References : PD/FM6 %------------------------------------------------------------------------------ Timed Predicate: informed NL : facility manager informed Intention : facility manager is informed Scope : eh References : FM7 Used By : FM7 %------------------------------------------------------------------------------ %============================================================================== %============================================================================== % C O N T R O L P A N E L %============================================================================== %============================================================================== Description Class CtrlPanel %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Signature %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Domain CL_SWITCH_STATUS = { 100, 0, ambient } Intention : set of possible values that can be set for the ceiling lights by using the control panel NL : values of the window ceiling light switch of the control panel References : PD/U14, PD/U16 Used By : used at all ??? CustomerReq : For the sake of simplicity on is replaced by 100 and off by 0. Is this ok? CustomerResp : ok, ist aber eine Einschraenkung, koennte auch sinnvoll sein, on nicht gleich 100 zu setzen => Energie sparen Comment : keine Einschraenkung! Kunde ueberzeugt. %------------------------------------------------------------------------------ Domain AMB_LIGHT_LEV = { 0, 10, ..., 100 } Intention : set of possible values that can be chosen for the ambient light level by using the control panel NL : values of the setting of the ambient light level of the control panel References : PD/U14, PD/U16 CustomerReq : What are the possible values? CustomerResp : Kontrolliert den Dimmer: 0, 10-100 Comment : ok %------------------------------------------------------------------------------ Timed Function chosenLightScene () --> LIGHT_SCENES Intention : light scene set by using the control panel NL : control panel light scene Scope : ev References : PD/U6 Used By : U2, U3, U6 %------------------------------------------------------------------------------ Timed Function ambLightLev () --> AMB_LIGHT_LEV Intention : the value defined for the ambient light level by using the control panel NL : ambient light level of the control panel Scope : ev References : PD/3.1.1:U14, PD/3.1.1:U16 /U7 ("The ambient light level setting is contained in the control panel.") Used By : U14iii %------------------------------------------------------------------------------ Timed Function winCeilLightSwitch () --> CL_SWITCH_STATUS Intention : the value defined for the window ceiling light by using the control panel NL : window ceiling light switch of the control panel Scope : ev References : PD-Sec3.1.1/U14(ii), PD-Sec3.1.1/U16(i) ("The window ceiling light switch is contained in the control panel.") Used By : U14ii %------------------------------------------------------------------------------ Timed Function wallCeilLightSwitch () -> CL_SWITCH_STATUS Intention : the value defined for the wall ceiling light by using the control panel NL : wall ceiling light switch of the control panel Scope : ev References : PD-Sec3.1.1/U14(ii), PD-Sec3.1.1/U16(i) ("The wall ceiling light switch is contained in the control panel.") Used By : U14ii %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ ReqSpec %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Property P_1 NonFormal : The control panel should be easy and intuitive to use. References : PD-Sec3.2.3/NF8 %============================================================================== %============================================================================== % O F F I C E C O N T R O L P A N E L %============================================================================== %============================================================================== Description Class OfficeCtrlPanel derived from CtrlPanel %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Signature %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Domain TL_SWITCH_STATUS = { 1, 0 } Intention : set of possible values that can be set for the task light by using the control panel NL : values of the task light switch of the control panel References : CustomerReq : For the sake of simplicity on is replaced by 1 and off by 0. Is this ok? CustomerResp : ok! %------------------------------------------------------------------------------ Timed Function taskLightSwitch () --> TL_SWITCH_STATUS NL : task light switch of the control panel Intention : the value defined for the task light by using the control panel Scope : ev References : PD/3.1.1:U14 ("The task light switch is contained in the control panel.") Used By : U14i %------------------------------------------------------------------------------ %============================================================================== %============================================================================== % L I G H T %============================================================================== %============================================================================== Description Class Light %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Signature %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Timed Function : status () --> Binary Intention : the status of a light (voltage is considered) NL : status=1 : light on status=0 : light off status=* : status of the light Scope : eh References : InAr/4.1 Used By : U14i %------------------------------------------------------------------------------ %============================================================================== %============================================================================== % C E I L I N G L I G H T %============================================================================== %============================================================================== Description Class CeilingLight : Derived from Light %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Signature %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ TimeConstant T_1 NL : dimmer reaction time Intention : duration between changing the dimmer and the corresponding reaction of the light References : InAr/6 %------------------------------------------------------------------------------ Timed Function : dim () --> Percent Intention : status of the dimmer for controlling a ceiling light NL : dimmer Scope : sv References : InAr/4.1 %------------------------------------------------------------------------------ Timed Function : pulse () --> Binary Intention : status of a pulse that can be sent by the control system to control the impulse relais NL : pulse status Scope : sv References : InAr/7 Used By : Used at all ??? CustomerReq : Is the declaration correct? Nothing is said in InAr. CustomerResp : Was wollt Ihr denn zurueckliefern - Status des Pulses? CustomerReq : Where is the problem? %------------------------------------------------------------------------------ Timed Function : impRel () --> Binary Intention : status of an imulse relais for controlling a ceiling light NL : impulse relais Scope : eh References : InAr/7 CustomerReq : Is the declaration correct? In InAr 0,100 % is given. CustomerResp : Wozu ist das gut, dafuer gibt es doch die status line? CustomerReq : Where is the problem? %------------------------------------------------------------------------------ Timed Function : statLine () --> Binary NL : task light status line Intention : the status of a status line showing the status of the light Scope : ev References : InAr/4.1, InAr/5 %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ DomKnow %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Property D_1 Formal : \always ( statLine = 1 <--> impRel = 1 ) NL : The status line of the ceiling light is 1 if and only if the impulse relais is 1. References : InAr/7 PatternInst : Comment : %------------------------------------------------------------------------------ Property D_2: Formal : \allways( \forall p \in PERCENT: dim = p /\ impRel = 1 \delCopy_{\le T_1} status = p ) NL : The illumination level of the ceiling light always corresponds to the value of the dimmer with a maximal delay given by the reaction time of the dimmer if the impulse relais is on. References : InAr/7 PatternInst: Comment : %------------------------------------------------------------------------------ Property D_3 Formal : \allways ( statLine = 1 <--> status = 1 ) NL : The value of the status line of the light is 1 if and only if the value of the light is 1. References : PatternInst : CustomerResp : Der Wert v. sll ist 1 gdw Spannung an der Lampe ist. Comment : %------------------------------------------------------------------------------ %============================================================================== %============================================================================== % P U S H B U T T O N %============================================================================== %============================================================================== Description Class PushButton %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Signature %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Timed Function : status () --> BINARY NL : push button Intention : push button = 1 iff the button is pushed Scope : eh References : InAr/4.2, InAr/5 %------------------------------------------------------------------------------ %============================================================================== %============================================================================== % L I G H T - B U T T O N S E T %============================================================================== %============================================================================== Description Class LightButtonSet (Nat numButtons) Intention : Combines a number of push buttons with a light %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Signature %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Object light : Light Object button : PushButton [numButtons] %------------------------------------------------------------------------------ TimeConstant T_1 NL : push button reaction time Intention : duration between pushing a push button and the corresponding reaction of the light References : InAr/6 %------------------------------------------------------------------------------ Timed Predicate: pushBut NL : any button is pushed Intention : pushBut represents if any button is pushed Scope : eh References : PD/FM6 % ----------------------------------------------------------------------------- TimeConstant T_2 Intention : The maximal time between pushing the switch and switching off the light. NL : immediately Used By : U19i, U19ii %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ DomKnow %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Property D_1 Formal : pushBut <--> \exists i \in {1, ... , numButtons} (button[i].status = 1) NL : pushBut is true iff any button is pushed References : PatternInst : Comment : %------------------------------------------------------------------------------ Property D_2 Formal : \always( light.status = 0 /\ [pushBut] --> \eventually_{\le T_1} light.status = 1 ) NL : The status of the light always changes from on to off within the reaction time of the push buttons if any pushbutton is pushed. References : PatternInst : Comment : CustomerResp: Warum auch hier nicht 0/1? Nicht immer! Kommt auf das Relais an. Gilt DKH2 nicht auch im Office? Comment : 1) Better comprehensibility 2) Sorry? 3) Of course! This is actually instantiated in offices! %------------------------------------------------------------------------------ Property D_3 Formal : \always( light.status = 1 /\ [pushBut] --> \eventually_{\le T_1} light.status = 0 ) NL : The status of the light always changes from off to on within the reaction time of the push buttons if any pushbutton is pushed. References : PatternInst : Comment : %------------------------------------------------------------------------------ %============================================================================== %============================================================================== % C E I L I N G - L I G H T - B U T T O N S E T %============================================================================== %============================================================================== Description Class CeilingLightButtonSet derived from LightButtonSet Intention : Extends the LightButtonSet for CeilingLight %------------------------------------------------------------------------------ Object LightButtonSet::light : CeilingLight %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ DomKnow %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Property D_1 Formal : \always( \forall d: light.impRel = 0 /\ [pushBut] /\ light.dim = d \impl \eventually_{\le LightButtonSet::T_1} light.status = d ) NL : Whenever the impulse relais is off and any push button is pushed the ceiling light is dimmed within the reaction time of the push button to the value given by the dimmer. References : InAr/7 PatternInst : Comment : %------------------------------------------------------------------------------ Property D_2 Formal : \always( light.impRel = 1 /\ [pushBut] \eventually_{\le LightButtonSet::T_1} light.status = 0 ) NL : Whenever the impulse relais is on and the push button is pushed the ceiling light is off within the reaction time of the push button. References : InAr/7 PatternInst : Comment : %------------------------------------------------------------------------------ %============================================================================== %============================================================================== % M O T I O N D E T E C T O R %============================================================================== %============================================================================== Description Class MotDet %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Signature %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Timed Predicate fault Intention : fault is true iff the motion detector does not work correctly NL : motion detector fault Scope : eh References : PD/NF4a, PD/NF4b Used By : NF4a, NF4b %------------------------------------------------------------------------------ Timed Function status () --> Binary Intention : status of the sensor that reports whether a motion in a room is detected or not NL : room motion detector value Scope : ev References : InAr/4.1 Used By : NF4a %------------------------------------------------------------------------------ Timed Function assStatus () --> Binary Intention : value assumed by the system concerning the occupancy of a room NL : assumed room motion detector value Scope : sh References : PD/3.2.1:NF4 Used By : NF4a, NF4b %------------------------------------------------------------------------------ TimeConstant T_1 Intention : The time delay between a motion detection of the sensor and the occupancy recognition by the system. Used By : NF4a %------------------------------------------------------------------------------ TimeConstant T_2 Intention : The time delay between a correct operation of the motion detector and the corresponding system behaviour Used By : NF4a %------------------------------------------------------------------------------ TimeConstant T_3 Intention : The time delay between a malfunction of the motion detector and the corresponding system behaviour Used By : NF4b %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ ReqSpec %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Property P_1 Formal : \always ( (\not fault \delImp_{\leq T_2} (\forall v : status=v \delCopy_{T_1} assStatus=v))) NL : Whenever the motion detector is working correctly for at least T_2 time units, then eventually within this time span, the motion detector value used by the system is equal to the value returned by the motion detector with a maximum delay of T_1. References : PD-Sec3.2.1/NF4 Comment : Times ? Copied and adapted from NF1 -> Pattern ? -> DelayedCopy as in NF1a %------------------------------------------------------------------------------ Property P_2 Formal : \always ( (fault \delImp_{\leq T_3} assStatus = 1 )) NL : Whenever the motion detector is not working correctly for at least T_3 time units, then eventually within this time span, the motion detector value used by the system is 'occupied' with a maximum delay of T_1 and remains so at least as long as the precondition is true. PatternInst : DelayedImplication (fault, assStatus = 1, T_3) References : PD-Sec3.2.1/NF4 %------------------------------------------------------------------------------ %============================================================================== %============================================================================== % D O O R %============================================================================== %============================================================================== Description Class Door %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Signature %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Timed Function : closedContact () --> Binary NL : closedContact=* : status of the door closed contact closedContact=1 : the door is completely closed closedContact=0 : the door is not completely closed Intention : represents whether the door is closed or not Scope : ev References : InAr/4.1, InAr/5 CustomerReq : Meaning of values 0=? 1=? CustomerResp : laut InstArch: 1, wenn die Tuer vollst. geschlossen ist, 0 sonst %------------------------------------------------------------------------------ %============================================================================== %============================================================================== % A R E A %============================================================================== %============================================================================== Description Class Area Intention : Some general considerations on areas with light; possible areas are currently rooms and hallways. %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Signature %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Timed Predicate: occupied Intention : the area is occupied by a person NL : area occupied Scope : eh References : PD/U1, PD/U2, PD/U3, PD/U4, PD/FM3, PD/FM6 Used By : U1, U2, U3, U4, FM3, FM6 CustomerResp : tatsaechlich, oder gemessen? Comment : tatsaechlich. %------------------------------------------------------------------------------ Timed Predicate: allLightsOff Intention : all ceiling lights in an area are off NL : all ceiling lights off Scope : eh References : PD/FM1, PD/FM3, PD/FM6 UsedBy : FM1, FM3, FM6 CustomerResp : tatsaechlich, oder angefordert? Comment : tatsaechlich. %------------------------------------------------------------------------------ Timed Predicate: safeLight Intention : light is sufficient to move safely NL : safe light Scope : eh References : PD/U17 %------------------------------------------------------------------------------ TimeConstant T_1 Intention : The time delay between occupation of an area and the establishment of safe light. Used By : U1 CustomerReq : Is it possible to identify several of the time constants? Is it possible to establish relations between different time constants, e.g. <, >, ...? Is it possible to restrict the domain of some time constants, e.g. have a specific reaction time to be under/over a specific value? CustomerResp : Belegt -| Sensor misst Belegtheit | Kontrollsystem reagiert | Licht geht an Comment : Gesamtzeit von "Belegt" bis "Licht geht an". %------------------------------------------------------------------------------ Timed Function T_2 () -> Time Intention : The time delay between a sufficiently long non-occupation of an area and switching off the light Used By : FM3 Comment : %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ ReqSpec %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Property P_1 Formal : \always ( occupied \delImp_{\leq T_1} safeLight ) NL : Whenever the area is occupied for at least time T_1, 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. References : PD-Sec3.1.1/U1,U17 PatternInst : DelayedImplication (occupied, safeLight, T_1) CustomerReq : We suppose that it is not desired to allow a light scene "Very Dark" to be applicable to any occupied area, thus suppressing the safe light condition! o.k. ? CustomerResp : ok! sonst kann man das Licht nicht ausschalten, ohne sich zu gefaehrden. NL unklar! %------------------------------------------------------------------------------ Property P_2 NonFormal : Use daylight to achieve the desired light whenever possible. References : PD-Sec3.1.2/FM1 Comment : Formalization waits for a refined version. %------------------------------------------------------------------------------ Property P_3 Formal : \always ( \not occupied \delImp_{\leq T_2 min} allLightsOff ) NL : Whenever the area is continuously not occupied for at least T_2 minutes, then all lights are off within this time span and remain off at least as long as the area is not occupied. References : PD-Sec3.1.2/FM3,FM2,FM6 PatternInst : DelayedImplication (occupied, allLightsOff, T_2) CustomerReq : This could lead to potential conflicts with requirement U18. Is there any priority? CustomerResp : 1) Tischlampe? 2) unklar retroperspektiv! Comment : 1) Gibt es hier nicht. 2) ? %------------------------------------------------------------------------------ Property P_4 NonFormal : The value T_2 can be set by the facility manager for each area separately. References : PD-Sec3.1.2/FM5,FM4 Comment : Is this achieved by instantiating T_2 for each area? CustomerReq : Who sets T_2? CustomerResp : Der Hausmeister, ist ja auch in dessen Interesse. T_3 erweckt den Anschein, dass es sich um T_4 handelt Belegt --| | | T_3 | T_4 | Licht --------------| | | | ^ suff. long. non-occup. Zeitkonstanten: T_1 : vorherige Rueckkehr : light scene spaeter : standard LS keine Aussage ueber die Reaktionszeit des Lichtes! T_2,T_3 : Nach diesen Zeiten wird das Licht ausgeschaltet, wieder keine Aussage ueber die Reaktionszeit. Es gilt: T_2, T_3 < T_1 %------------------------------------------------------------------------------ %============================================================================== %============================================================================== % R O O M %============================================================================== %============================================================================== Description Class Room derived from Area Intention : Contains the specification of environment and requirements common to any kind of room. %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Signature %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Object cp : CtrlPanel Object win,wall : CeilingLightButtonSet (numButtons = 1) Object md : MotDet %------------------------------------------------------------------------------ Value ambient Intention : a value that can be set by the control panel for ceiling lights meaning that the actually set ambient light level should be maintained NL : ambient References : PD/3.1.1:U14 CustomerResp : unklar %------------------------------------------------------------------------------ Domain LIGHT_SCENES = CtrlPanel::TL_SWITCH_STATUS x (PERCENT \cup {ambient}) x (PERCENT \cup {ambient}) x CtrlPanel::AMB_LIGHT_LEV Intention : set of possible values that can be chosen for light scenes. The first component determines the value of the task light, the second component the value of the window ceiling light, the third component the value of the wall ceiling light, and the fourth component the ambient light level. In a room that is not an office the first component is not relevant. NL : values of light scenes References : CustomerReq : Is this the intended definition of a light scene? Used By : U2, U3, U4, U6 CustomerResp : Aha. Gem. Dictionary eigentl. nicht. ambientlightlevel x deskill x lightlist Comment : Subject to possible future changes. %------------------------------------------------------------------------------ Timed Predicate userInformed Intention : the user is informed in a specific way NL : user is informed Scope : eh References : PD/U11 Used By : U11 %------------------------------------------------------------------------------ Timed Function curStandLightScene () --> LIGHT_SCENES Intention : the standard light scene that is currently valid NL : current standard light scene Scope : sh References : PD/NF2 Used By : NF2 %------------------------------------------------------------------------------ Timed Function faultStandLightScene () --> LIGHT_SCENES Intention : the light scene that has to become standard light scene in the case of a malfunction of the outdoor light sensors NL : fault standard light scene Scope : sh References : PD/NF2 Used By : NF2 %------------------------------------------------------------------------------ Timed Function noFaultStandLightScene () --> LIGHT_SCENES Intention : the light scene that has to become standard light scene in the case of no malfunctions NL : no fault standard light scene Scope : sh References : PD/U4 CustomerResp : Unterschied zur curStandLightScene ? stdLS =^ DefaultLS =^ ErrLS Comment : Die curStandLightScene enthaelt auch den Fehlerfall. %------------------------------------------------------------------------------ Timed Function applLightScene () --> LIGHT_SCENES Intention : light scene applied by the control system NL : applied light scene Scope : sh References : Used By : U2, U3, U4, U6 %------------------------------------------------------------------------------ Timed Function ambLightLev () --> AMB_LIGHT_LEV Intention : the ambient light level in a room NL : ambient light level Scope : eh References : PD-Sec3.1.1/U14(iii), PD-Sec3.1.1/U16(ii) Used By : U14iii %------------------------------------------------------------------------------ TimeConstant T_3 Intention : The time delay between occupation of a room, when a light scene is chosen, and the establishment of the chosen light scene Used By : U2 %------------------------------------------------------------------------------ TimeConstant T_4 Intention : The time delay during which the reoccupation of a room leads to reestablishing the previous light scene and the time delay between a sufficiently often occupation and the application of the chosen light scene Used By : U3, U4 (former T_U4a) %------------------------------------------------------------------------------ TimeConstant T_5 Intention : The time delay between a sufficiently long non-occupation and the application of the standard light scene. NL : immediately Used By : U4 %------------------------------------------------------------------------------ TimeConstant T_6 Intention : The time delay between setting and applying a certain light level Used By : U14i, U14ii, U14iii %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ ReqSpec %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Property P_1 Formal : \always ( curStandLightScene = (0,100,100,\undef) ) NL : The standard light scene in the case of a malfunction of the outdoor light sensors is that all ceiling lights are on and the task light is off (in the case of offices). References : PD-Sec3.2.1/NF2 CustomerReq : Do standard and default light scene refer to the same light scene? What is the standard light scene if there is no malfunction? CustomerResp : see Decl. of defaultLightScene %------------------------------------------------------------------------------ Property P_2 Formal : \always ( \forall l \in LIGHT_SCENES (occupied /\ cp.chosenLightScene=l) \delImp_{\leq T_3} applLightScene=l) NL : Whenever the room is occupied and light scene l is chosen for at least time T_3, 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,U1,U6,U12 PatternInst : ConditionalContinuity (occupied, cp.chosenLightScene) CustomerReq : Is the light scene set by the control panel always the "actual chosen Light scene" or are there any other possibilities to set a light scene? CustomerResp : Nein. ActualLS wird ueber deas Panel eingestellt. Comment : P_2 hat Prioritaet gegenueber Area::P_1 %------------------------------------------------------------------------------ Property P_3 Formal : \always ( ( [occupied] \and \sometimesInThePast_{(0, T_4]} occupied \and cp.chosenLightScene=l) \imp \eventually_{T_5} applLightScene=l) NL : Whenever the room becomes occupied now and was occupied sometimes within the last T_4 minutes and the light scene l was last chosen, the light scene l is applied immediately. 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? %------------------------------------------------------------------------------ Property P_4 Formal : \always ( [occupied] \and \alwaysInThePast_{(0,T_4]} \not occupied) \imp \eventually_{T_5} applLightScene = curStandLightScene) NL : Whenever the room becomes occupied now and has not been occupied during the last T_4 minutes, the current standard light scene is applied immediately. References : PD-Sec.3.1.1/U4 %------------------------------------------------------------------------------ Property P_5 NonFormal : The light scenes can be chosen by using the control panel. References : PD-Sec.3.1.1/U6 CustomerReq : Is the control panel the only possibility to enter a light scene? In U2 there is additionally occupancy required. What is the relevant requirement? %------------------------------------------------------------------------------ Property P_6 NonFormal : For each room a default light scene can be chosen (not by using the control panel). References : PD-Sec3.1.1/U8 CustomerReq : Who sets the default light scene? CustomerResp : FM %------------------------------------------------------------------------------ Property P_7 NonFormal : For each room a default ambient light level can be set (not by using the control panel). References : PD-Sec3.1.1/U9 CustomerReq : What is the precise intention/definition of the term ambient light level? Who sets the light level? CustomerResp : Wurde in die LightScene aufgenommen Comment : to be further discussed %------------------------------------------------------------------------------ Property P_8 NonFormal : The value T_4 can be set for each room separately (not by using the control panel). References : PD-Sec3.1.1/U10 CustomerReq : Who sets the T1? CustomerResp : FM %------------------------------------------------------------------------------ Property P_9 Formal : \always ( \forall ll: (cp.winCeilLightSwitch=0 \/ cp.winCeilLightSwitch=100) /\ ll = cp.winCeilLightSwitch ) \delImp_{\leq T_6} win.light.status=ll ) NL : Whenever the window ceiling light switch in the control panel is on (off) for at least T_6 time units, the window ceiling light will be on (off) within this time span and remains on (off) as long as the precondition is true. References : PD-Sec3.1.1/U14(ii), PD-Sec3.1.1/U16(i) CustomerReq : This is an extended interpretation of need U14. Does it correspond with the customer's intention? CustomerResp : Jo %------------------------------------------------------------------------------ Property P_10 Formal : \always ( \forall l: (cp.wallCeilLightSwitch=0 \/ cp.wallCeilLightSwitch=100) /\ l = cp.wallCeilLightSwitch ) \delImp_{\leq T_6} wall.light.status=l ) NL : Whenever the wall ceiling light switch in the control panel is on (off) for at least T_6 time units, the wall ceiling light will be on (off) within this time span and remains on (off) as long as the precondition is true. References : PD-Sec3.1.1/U14(ii), PD-Sec3.1.1/U16(i) CustomerReq : This is an extended interpretation of need U14. Does it correspond with the customer's intention? %------------------------------------------------------------------------------ Property P_11 Formal : \always ( cp.winCeilLightSwitch = ambient \delImp_{\leq T_6} win.light.status=\undef ) NL : Whenever the window ceiling light switch in the control panel is ambient for at least T_6 time units, the window ceiling light will be \undef within this time span and remains \undef as long as the precondition is true. References : PD-Sec3.1.1/U14(ii), PD-Sec3.1.1/U16(i) CustomerReq : In which way has the window ceiling light to behave if ambient is selected at the control panel? CustomerResp : s.u. Comment : discuss %------------------------------------------------------------------------------ Property P_12 Formal : \always ( cp.wallCeilLightSwitch = ambient \delImp_{\leq T_6} wall.light.status=\undef ) NL : Whenever the wall ceiling light switch in the control panel is ambient for at least T_6 time units, the wall ceiling light will be \undef within this time span and remains \undef as long as the precondition is true. References : PD-Sec3.1.1/U14(ii), PD-Sec3.1.1/U16(i) CustomerReq : In which way has the window ceiling light to behave if ambient is selected at the control panel? %------------------------------------------------------------------------------ Property P_13 Formal : \always ( \forall ll: cp.ambLightLev=ll \delImp_{\leq T_6} ambLightLev=ll ) NL : Whenever the ambient light level in the control panel is "ll" for at least T_6 time units, the ambient light level will be "ll" within this time span and remains "ll" as long as the precondition is true. References : PD-Sec3.1.1/U14(iii), PD-Sec3.1.1/U16(ii) CustomerReq : This is an extended interpretation of need U14. Does it correspond with the customer's intention? %------------------------------------------------------------------------------ Property P_14 Formal : \always( cp.chosenLightScene = ( 0, cp.winCeilLightSwitch, cp.wallCeilLightSwitch, cp.ambLightLev )) NL : The light scene chosen by the control panel corresponds with the settings of the switches of the control panel. References : PatternInst : Comment : CustomerReq : Is this correct? CustomerResp : Eigentlich schon Lichtszenerie: grosses Problem ! :-( Wir wollten: schoene Lichtszenerien, keine beeintraechtigung der derzeitigen Funktionalitaet im Fehlerfall, Standardeinstellungen Was kann nun mit dieser techn. Realisierung alles erfuellt werden? Wie wird das bestehnde Verhalten integriert? - Ueber den in InitArch beschriebenen Dimmer kann die geforderte Entkopplung recht gut realisiert werden. - Da das KS die Lichtszenen aendert, muss das Panel auch von diesem angepasst werden. - U5 macht so eigentlich keinen Sinn, da man nicht wieder in die zuvor eingestellte Lichtszene zurueckkehren kann. Commment : discuss %------------------------------------------------------------------------------ %============================================================================== %============================================================================== % O F F I C E %============================================================================== %============================================================================== Description Class Office : Derived from Room Intention : Additional requirements for rooms that are offices %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Signature %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Object tl : LightButtonSet (numButtons = 1) Intention : The task light with its push button Object Room::cp : OfficeCtrlPanel %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ DomKnow %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Property D_1 Formal : \allways (allLightsOff <--> win.light.status = 0 /\ wall.light.status = 0 /\ tl.status = 0) NL : All lights are off if and only if both ceiling lights and the task light are off. Used By : FM1, FM3, FM6 %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ ReqSpec %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Property P_1 NonFormal : The control panel should be installed moveably like a telephone in the offices. References : PD-Sec3.1.1/U13 %------------------------------------------------------------------------------ Property P_2 Formal : \always ( \forall b: cp.taskLightSwitch = b \delImp_{\leq Room::T_6} tl.status = b ) NL : Whenever the task light switch in the control panel is on (off) for at least Room::T_6 time units, the task light will be on (off) within this time span and remains on (off) as long as the precondition is true. References : PD-Sec3.1.1/U14(i) Comment : This could lead to potential conflicts with other requirements that also try to control the task light. 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! This is an extended interpretation of need U14. Does it correspond with the customer's intention? %----------------------------------------------------------------------------- %============================================================================== %============================================================================== % N O O F F I C E %============================================================================== %============================================================================== Description Class NoOffice : Derived from Room % additional requirements for rooms that are no offices %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ DomKnow %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Property D_1 Formal : \always (allLightsOff <--> win.light.status = 0 /\ wall.light.status = 0) NL : All lights are off if and only if both ceiling lights are off. %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ ReqSpec %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Property P_1 NonFormal : The control panel should be installed near a door to the hallway. References : PD-Sec3.1.1/U15 %------------------------------------------------------------------------------ %============================================================================== %============================================================================== % H A L L W A Y S E C T I O N %============================================================================== %============================================================================== % The requirement specification for hallway sections Description Class HallwaySection derived from Area %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Signature %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Object eastMd, westMd, middleMd : MotDet Object light : CeilingLightButtonSet (\undef) CustomerReq : How many push buttons? CustomerResp : Bitte zaehlen :-) %------------------------------------------------------------------------------ Timed Predicate: nearHallwayDoor NL : near a hallway door Intention : a person is near a hallway door to this hallway section Scope : eh References : PD/U18 Used By : U18 %------------------------------------------------------------------------------ Timed Predicate: hwLightUncontroll NL : hallway light uncontrollable Intention : the light is neither controllable automatically nor manually Scope : eh References : PD/NF5 Used By : NF5 CustomerReq : How should this be determined? -> Definition? CustomerResp : Das waere, wenn ueberhaupt, was fuer die HW. %------------------------------------------------------------------------------ TimeConstant T_3 Intention : The time delay between a sufficiently long occupation of an adjacent hallway section and switching on the lights Used By : U18 % ----------------------------------------------------------------------------- TimeConstant T_4 Intention : The time delay between the loss of ligth control and switching on the lights. Used By : NF5 %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ DomKnow %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Property D_1 Formal : \allways (allLightsOff <--> light.status=0) NL : All lights are off if and only if the hallway light is off. %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ ReqSpec %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Property P_1 Formal : \always ( nearHallwayDoor \delImp_{\leq T_3} light.status = 1 ) NL : Whenever a person is continuously in the near of a hallway door of the hallway section for at least T_3 time units, then the light in the hallway section will be on within this time span, and remains on at least as long as the person is near the hallway section. References : PD-Sec3.1.1/U18 PatternInst : DelayedImplication (nearHallwayDoor, light.status = 1) Comment : "before" is here interpreted geographically and not temporally. The time T_3 should be set to value reasonable for typical pedestrian speeds. CustomerReq : Need U18 given in the problem description cannot be satisfied, since it is not possible to look in the future. Is the given interpretation where "before" is interpreted geographically and not temporally satisfactory? CustomerResp : Jo: Wie, was? Das kann man feststellen: Der Bewegungsmelder teilt immer mit, ob jemand eintreten will oder nicht. Nicht schlimm, wenn mal unnoetig das Licht eingeschaltet wird. Ich wuerde sagen, dass jemand eintreten will, bzw. das Licht einzuschalten ist, wenn - Tuer zu, Bewegung registriet, Tuer auf - Tuer auf, Bewegung registriert Falls die Detektoren geschickt angebracht sind, dann ist eine bessere Entscheidung, bei offener Tuer: ------------------------------- Det. A | Det. B ..........\++++++++++++ Ueberwachte Bereiche: . + ..........+.\++++++++++++ ........+.|.+.+++++++++++ ------------------------------- %------------------------------------------------------------------------------ Property P_2 Formal : \always ( hwLightUncontroll \delImp_{\leq T_4} light.status = 1) NL : Whenever the lights are neither controllable automatically nor manually for at least T_4 time units, then eventually within this time span, the light in the hallway section is on and remains so at least as long as the lights are neither controllable automatically nor manually. PatternInst : DelayedImplication (hwLightUncontroll, light.status = 1, T_4) References : PD-Sec3.2.1/NF5 CustomerResp : This property is not realizable using the pre-installation. %------------------------------------------------------------------------------ %============================================================================== %============================================================================== % O U T D O O R L I G H T S E N S O R %============================================================================== %============================================================================== Description Class OutDoorLightSensor %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Signature %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Domain OUT_LIGHT_VALUES = { 1, ..., 10000 } NL : outdoor light values Intention : set of possible values reported by the outdoor light sensor References : Used By : NF1a, NF1b %------------------------------------------------------------------------------ Timed Predicate: outLightSensorFault NL : outdoor light sensor fault Intention : the outdoor light sensors do not work correctly Scope : eh References : PD/U11, PD/NF1a, PD/NF1b, PD/NF2 Used By : NF3 %------------------------------------------------------------------------------ Timed Function : outLight () --> OUT_LIGHT_VALUES NL : outdoor light Intention : value returned by a sensor attached perpendicularly to the facade for measuring the outdoor illuminance Scope : ev References : InAr/5 Used By : NF1a %------------------------------------------------------------------------------ Timed Function : assOutLight () --> OUT_LIGHT_VALUES NL : assumed outdoor light Intention : value assumed by the system concerning the outdoor illuminance Scope : sh References : PD/3.3.1:NF1 Used By : NF1a, NF1b Comment : DomKnow ??? %------------------------------------------------------------------------------ Timed Function : lastCorrectOutLight () --> OUT_LIGHT_VALUES NL : last correctly measured outdoor light Intention : last corectly measured value of the outdoor illuminance Scope : eh References : PD/3.2.1:NF1 Used By : NF1b %------------------------------------------------------------------------------ %============================================================================== %============================================================================== % S T A I R C A S E %============================================================================== %============================================================================== Description Class StairCase %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Signature %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Object md : MotDet Intention : sensor placed in front of the adjacent hallway door for detecting motions %------------------------------------------------------------------------------ %============================================================================== %============================================================================== % F L O O R %============================================================================== %============================================================================== Main Description Floor %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Signature %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Object o435 : Office NL : office 435 Intention : the office in floor 32/4 with No 435 References : InAr/2.1 % entsprechend für alle Räume aus Figure 1 von InAr: Object o433, o432, o429, o425, o423, o421, o419, o417, o415, o424 o416, o414, o412 : Office Object m427, cl411, cl426, cl422, cl418, cl411 : NoOffice Domain ROOMS = {o435, o433, o432, o429, o425, o423, o421, o419, o417, o415, o424, o416, o414, o412, m427, cl411, cl426, cl422, cl418, cl411} %------------------------------------------------------------------------------ Object fm : FacMan (ROOMS) %------------------------------------------------------------------------------ Object d_421_423 : Door Object d_423_425 : Door Object d_431_433 : Door Object d_433_435 : Door Object d_414_416 : Door Object d_416_418 : Door Object d_418_420 : Door Object d_420_422 : Door Object d_o435, d_o433, d_o432, d_o429, d_o425, d_o423, d_o421, d_o419, d_o417, d_o415, d_o424, d_o416, d_o414, d_o412, d_m427, d_cl411, d_cl426, d_cl422, d_cl418, d_cl411 : Door %------------------------------------------------------------------------------ Object h1 : HallwaySection NL : hallway 1 Intention : hallway in the east of floor 32/4 References : InAr/2.1 Object h2 : HallwaySection NL : hallway 2 Intention : hallway in the middle of floor 32/4 References : InAr/2.1 Object h3 : HallwaySection NL : hallway 3 Intention : hallway in the west of floor 32/4 References : InAr/2.1 %------------------------------------------------------------------------------ Object ols1 : OutdoorLightSensor NL : outdoor light sensor 1 Intention : outdoor light sensor in the north-east direction References : InAr/2.1 (ols1) Object ols2 : OutdoorLightSensor NL : outdoor light sensor 2 Intention : outdoor light sensor in the south-west direction References : InAr/2.1 (ols2) Object ols3 : OutdoorLightSensor NL : outdoor light sensor 3 Intention : outdoor light sensor in the north-west direction References : InAr/2.1 (ols3) Object ols4 : OutdoorLightSensor NL : outdoor light sensor 4 Intention : outdoor light sensor in the south-east direction References : InAr/2.1 (ols4) Object ols5 : OutdoorLightSensor NL : outdoor light sensor 5 Intention : outdoor light sensor in the north direction References : InAr/2.1 (ols5) Object ols6 : OutdoorLightSensor NL : outdoor light sensor 6 Intention : outdoor light sensor in the south direction References : InAr/2.1 (ols6) %------------------------------------------------------------------------------ Object scw : StairCase NL : western staircase Intention : staircase in the west of floor 32/4 References : InAr/2.1 Object sce : StairCase NL : eastern staircase Intention : staircase in the east of floor 32/4 References : InAr/2.1 %------------------------------------------------------------------------------ TimeConstant T_1 Intention : The time delay between the outdoor light value returned by the sensor and the outdoor light value used by the system. Used By : NF1a %------------------------------------------------------------------------------ TimeConstant T_2 Intention : The time delay between a malfunction and the information of the facility manager Used By : FM7 %------------------------------------------------------------------------------ TimeConstant T_3 Intention : The time delay between a malfunction of the outdoor light sensor and the time a user is informed about this malfunction Used By : U11 %------------------------------------------------------------------------------ TimeConstant T_4 Intention : The time delay between a correct sensor operation (sensor fault) and the corresponding system behaviour. Used By : NF1a,NF1b %------------------------------------------------------------------------------ TimeConstant T_5 Intention : The time delay between a malfunction of the outdoor light sensor and the corresponding system behaviour Used By : NF2 %------------------------------------------------------------------------------ TimeConstant T_6 Intention : The time delay between a malfunction of the outdoor light sensor and switching on the lights if the hallway is occupied. Used By : NF3 % ----------------------------------------------------------------------------- Timed Predicate: malfunction NL : malfunction Intention : a malfunction occurs Scope : eh References : FM7 Used By : FM7 %------------------------------------------------------------------------------ Timed Predicate: safeLight NL : safe light Intention : light is sufficient to move safely Scope : eh References : PD/U17 Used By : U1 %------------------------------------------------------------------------------ Timed Predicate outLightSensorFault NL : The fault of some outdoor light sensor Scope : eh %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ ReqSpec %------------------------------------------------------------------------------ %------------------------------------------------------------------------------ Property P_1 Formal : \always ( outLightSensorFault \equiv ols1.outLightSensorFault \or ... \or ols6.outLightSensorFault) NL : Some outdoor light sensor has a malfunction. %------------------------------------------------------------------------------ Property P_2 Formal : \always ( \forall r \in ROOMS : outLightSensorFault \delEquiv_{\leq T_3} r.userInformed ) NL : Whenever some outdoor light sensors are not working correctly for at least time T_3, the user is informed within time T_3 and remains informed as long as the precondition is true. And conversely, whenever the outdoor light sensor works correctly for at least time T_3, the user is not informed within time T_3 and is not informed as long as this precondition is true. References : PD-Sec3.1.1/U11 PatternInst : DelayedEquivalence (outLightSensorFault, r.userInformed, T_3) CustomerReq : What is the meaning of 'the user is informed'? CustomerResp : Blinklicht und Sirene :-) %------------------------------------------------------------------------------ Property P_3 Formal : \always ( malfunction \delEquiv_{\leq T_2} fm.informed ) NL : Whenever a malfunction occurs for at least T_2 time units, the f.m. is informed within time T_2 and remains informed as long as the precondition is true. And conversely, whenever no malfunction occurs for at least time T_2, the f.m. is no longer informed within time T_2 and is not informed as long as this precondition is true. References : PD-Sec3.1.2/FM7 PatternInst : DelayedEquivalence (malfunction, fm.informed, T_2) CustomerReq : What is a "malfunction"? What means 'the facility manager has to be informed'? Comment : (copied from U11) CustomerResp : Defekte Sensoren/Aktuatoren - ist eigentlich nicht genau FM7. %------------------------------------------------------------------------------ Property P_4 NonFormal : If a malfunction occurs, the control system supports the facility manager by finding the reason. Comment : We 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 %------------------------------------------------------------------------------ Property P_5 NonFormal : The system provides reports on current and past energy consumption. References : PD-Sec3.1.2/FM9 %------------------------------------------------------------------------------ Property P_6 NonFormal : All malfunctions and unusual conditions are stored and reported on request References : PD-Sec3.1.2/FM10 %------------------------------------------------------------------------------ Property P_7 NonFormal : Malfunctions that the system cannot detect can be entered manually. References : PD-Sec3.1.2/FM11 %------------------------------------------------------------------------------ Property P_8 Formal : \always ( (\not outLightSensorFault \delImp_{\leq T_4} (\forall s \forall v: assOutLight(s)=v \delCopy_{T_1} outLight(s)=v))) NL : Whenever some outdoor light sensors are not working correctly for at least T_4 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_1 time units. References : PD-Sec3.2.1/NF1 Comment : Additional requirement covering the "normal case". New operator is currently developed. CustomerReq : Has a fault of the outdoor light sensors to be considered for each sensor separately or as it is currently for all together? CustomerResp : Fuer jeden Raum getrennt :-) %------------------------------------------------------------------------------ Property P_9 Formal : \always ( (outLightSensorFault \delImp_{\leq T_4} (\forall s: assOutLight(s) = lastCorrectOutLight(s) )) NL : Whenever some outdoor light sensors are not working correctly for at least T_4 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.2.1/NF1 CustomerReq : Is the standard light scene in this case to be applied? "No" is supposed. PD-Sec.3.2.1/NF1 is not a fail safe assumption! Fail safe would be that there is no outdoor light. This can always be overruled manually. Should the requirement be modified in this way? CustomerResp : Nein. Die Lichtverhaelt. aendern sich nicht so schnell. Einfach den LightLevel ... (Anm.d.Red.: kann ich nich' lesen) %------------------------------------------------------------------------------ Property P_10 Formal : \always ( \forall r \in ROOMS : outLightSensorFault \delImp_{\leq T_5} r.curStandLightScene = r.faultStandLightScene) NL : Whenever some outdoor light sensors are not working correctly for at least T_5 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.2.1/NF2 PatternInst : DelayedImplication (outLightSensorFault, curStandLightScene = faultStandLightScene, T_5) CustomerReq : Is the standard light scene in this case to be applied? "No" is supposed. Do standard and default light scene refer to the same light scene? CustomerResp : 1) Nein. 2) Ja. %------------------------------------------------------------------------------ Property P_11 Formal : \always ( \forall h in HALLWAYS : outLightSensorFault \and h.occupied \delImp_{\leq T_6} h.light.status = 1 ) NL : Whenever some outdoor light sensor are not working correctly and the hallway is occupied for at least T_6 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. References : PD-Sec3.2.1/NF3 PatternInst : DelayedImplication (outLightSensorFault \and occupied, light.status = 1, T_6) Comment : Aehnlichkeit zu NF2ii: evtl. Area::Timed Predicate faultLight und verfeinern als Room::curStandLightScene = faultStandLightScene, bzw. HallwaySection::light.status = 1 %------------------------------------------------------------------------------ Property P_12 NonFormal : All hardware connections have to be made according to DIN standards. References : PD-Sec3.2.2/NF6 %------------------------------------------------------------------------------ Property P_13 NonFormal : No hazardous condition for persons, inventory or building are allowed. References : PD-Sec3.2.2/NF7 Comment : Formalize? %------------------------------------------------------------------------------ Property P_14 NonFormal : The system warns about unreasonable inputs. References : PD-Sec3.2.3/NF9 Comment : Formalize? %------------------------------------------------------------------------------