plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/SSR_fi/SSR.uml - chess/chess - Git at Google

 <?xml version="1.0" encoding="UTF-8"?>
 <xmi:XMI xmi:version="20131001" xmlns:xmi="http://www.omg.org/spec/XMI/20131001" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:Blocks="http://www.eclipse.org/papyrus/0.7.0/SysML/Blocks" xmlns:CHESSContract="http:///CHESSContract.ecore" xmlns:CHESSViews="http://CHESS/Core/Views" xmlns:Core="http://CHESS/Core" xmlns:DataTypes="http://www.eclipse.org/papyrus/DataTypes/1" xmlns:DependableComponent="http://CHESS/Dependability/DependableComponent" xmlns:PortAndFlows="http://www.eclipse.org/papyrus/0.7.0/SysML/PortAndFlows" xmlns:ThreatsPropagation="http://CHESS/Dependability/ThreatsPropagation" xmlns:ecore="http://www.eclipse.org/emf/2002/Ecore" xmlns:uml="http://www.eclipse.org/uml2/5.0.0/UML" xsi:schemaLocation="http://www.eclipse.org/papyrus/0.7.0/SysML/Blocks http://www.eclipse.org/papyrus/0.7.0/SysML#//blocks http://CHESS/Core/Views http://CHESS#//Core/CHESSViews http://CHESS/Core http://CHESS#//Core http://www.eclipse.org/papyrus/DataTypes/1 http://www.eclipse.org/papyrus/MARTE/1#//VSL/DataTypes http://CHESS/Dependability/DependableComponent http://CHESS#//DependableComponent http://www.eclipse.org/papyrus/0.7.0/SysML/PortAndFlows http://www.eclipse.org/papyrus/0.7.0/SysML#//portandflows http://CHESS/Dependability/ThreatsPropagation http://CHESS#//ThreatsPropagation">
   <uml:Model xmi:id="_3PIH0MktEee0hNePRc2zdw" name="RootElement">
     <packagedElement xmi:type="uml:Package" xmi:id="_xRZHYMnYEeejHePP_Hzkeg" name="modelRequirementView"/>
     <packagedElement xmi:type="uml:Package" xmi:id="_1irWYMnYEeejHePP_Hzkeg" name="modelSystemView">
       <packagedElement xmi:type="uml:Package" xmi:id="_DHQ8wMnZEeejHePP_Hzkeg" name="PhisicalArchitecture" visibility="package">
         <packagedElement xmi:type="uml:Class" xmi:id="_NzOwMMnZEeejHePP_Hzkeg" name="System" visibility="public">
           <ownedRule xmi:type="uml:Constraint" xmi:id="__xm5cMnhEeejHePP_Hzkeg" name="alarm_or" constrainedElement="_WXNfQMngEeejHePP_Hzkeg _0Y_qIMnbEeejHePP_Hzkeg">
             <specification xmi:type="uml:OpaqueExpression" xmi:id="_74KIwNZwEeeO6aCjdQZPkg">
               <language>OCRA</language>
               <body>selector.switch_current_use:= monitor1.absence_alarm or monitor2.absence_alarm</body>
             </specification>
           </ownedRule>
           <ownedRule xmi:type="uml:Constraint" xmi:id="_qR-5sMniEeejHePP_Hzkeg" name="monitor1_enabled" constrainedElement="_atZR0MnfEeejHePP_Hzkeg _r2tVcMnaEeejHePP_Hzkeg">
             <specification xmi:type="uml:OpaqueExpression" xmi:id="_DuZFMNZxEeeO6aCjdQZPkg">
               <language>OCRA</language>
               <body>monitor1.enabled:=(selector.current_use=1)</body>
             </specification>
           </ownedRule>
           <ownedRule xmi:type="uml:Constraint" xmi:id="_psuJIMnlEeejHePP_Hzkeg" name="monitor2_enabled" constrainedElement="_atZR0MnfEeejHePP_Hzkeg _r2tVcMnaEeejHePP_Hzkeg">
             <specification xmi:type="uml:OpaqueExpression" xmi:id="_IEF6INZxEeeO6aCjdQZPkg">
               <language>OCRA</language>
               <body>monitor2.enabled:=(selector.current_use=2)</body>
             </specification>
           </ownedRule>
           <ownedAttribute xmi:type="uml:Port" xmi:id="_0dXXUMncEeejHePP_Hzkeg" name="speed" aggregation="composite">
             <type xmi:type="uml:PrimitiveType" href="pathmap://UML_LIBRARIES/UMLPrimitiveTypes.library.uml#Real"/>
           </ownedAttribute>
           <ownedAttribute xmi:type="uml:Port" xmi:id="_43cV8MncEeejHePP_Hzkeg" name="sensed_speed" aggregation="composite">
             <type xmi:type="uml:PrimitiveType" href="pathmap://UML_LIBRARIES/UMLPrimitiveTypes.library.uml#Real"/>
           </ownedAttribute>
           <ownedAttribute xmi:type="uml:Port" xmi:id="_7Hr6QMncEeejHePP_Hzkeg" name="sensed_speed_is_present" aggregation="composite">
             <type xmi:type="uml:PrimitiveType" href="pathmap://UML_LIBRARIES/UMLPrimitiveTypes.library.uml#Boolean"/>
           </ownedAttribute>
           <ownedAttribute xmi:type="uml:Property" xmi:id="_YySFcMneEeejHePP_Hzkeg" name="sensor1" type="_rDtnsMnZEeejHePP_Hzkeg" aggregation="composite" association="_YyuKUMneEeejHePP_Hzkeg"/>
           <ownedAttribute xmi:type="uml:Property" xmi:id="_ds_r8MneEeejHePP_Hzkeg" name="sensor2" type="_rDtnsMnZEeejHePP_Hzkeg" aggregation="composite" association="_ds_r8cneEeejHePP_Hzkeg"/>
           <ownedAttribute xmi:type="uml:Property" xmi:id="_oc_DwMneEeejHePP_Hzkeg" name="selector" type="_u-CvQMnZEeejHePP_Hzkeg" aggregation="composite" association="_odINsMneEeejHePP_Hzkeg"/>
           <ownedAttribute xmi:type="uml:Property" xmi:id="_raFHAMneEeejHePP_Hzkeg" name="monitor2" type="_oK1EIMnbEeejHePP_Hzkeg" aggregation="composite" association="_raOQ8MneEeejHePP_Hzkeg">
             <qualifier xmi:type="uml:Property" xmi:id="_ezWakMnfEeejHePP_Hzkeg" name="monitor2" type="_oK1EIMnbEeejHePP_Hzkeg" aggregation="composite"/>
           </ownedAttribute>
           <ownedAttribute xmi:type="uml:Property" xmi:id="_fqL78MnfEeejHePP_Hzkeg" name="monitor1" type="_oK1EIMnbEeejHePP_Hzkeg" aggregation="composite" association="_fqVs8MnfEeejHePP_Hzkeg"/>
           <ownedAttribute xmi:type="uml:Property" xmi:id="_Zia9YMnoEeejHePP_Hzkeg" name="sense" type="_ZvFgYMnoEeejHePP_Hzkeg"/>
           <ownedAttribute xmi:type="uml:Property" xmi:id="__M-hcMuZEee9L_NsVF0R0A" name="error" visibility="public">
             <type xmi:type="uml:PrimitiveType" href="pathmap://UML_LIBRARIES/UMLPrimitiveTypes.library.uml#Integer"/>
           </ownedAttribute>
           <ownedConnector xmi:type="uml:Connector" xmi:id="_Djn54MnfEeejHePP_Hzkeg">
             <end xmi:type="uml:ConnectorEnd" xmi:id="_Djn54cnfEeejHePP_Hzkeg" role="_0dXXUMncEeejHePP_Hzkeg"/>
             <end xmi:type="uml:ConnectorEnd" xmi:id="_Djn54snfEeejHePP_Hzkeg" partWithPort="_ds_r8MneEeejHePP_Hzkeg" role="_CqGDIMnaEeejHePP_Hzkeg"/>
           </ownedConnector>
           <ownedConnector xmi:type="uml:Connector" xmi:id="_Fj69sMnfEeejHePP_Hzkeg">
             <end xmi:type="uml:ConnectorEnd" xmi:id="_Fj69scnfEeejHePP_Hzkeg" role="_0dXXUMncEeejHePP_Hzkeg"/>
             <end xmi:type="uml:ConnectorEnd" xmi:id="_Fj69ssnfEeejHePP_Hzkeg" partWithPort="_YySFcMneEeejHePP_Hzkeg" role="_CqGDIMnaEeejHePP_Hzkeg"/>
           </ownedConnector>
           <ownedConnector xmi:type="uml:Connector" xmi:id="_lEMtkMnfEeejHePP_Hzkeg">
             <end xmi:type="uml:ConnectorEnd" xmi:id="_lEMtkcnfEeejHePP_Hzkeg" partWithPort="_ds_r8MneEeejHePP_Hzkeg" role="_POAPoMnaEeejHePP_Hzkeg"/>
             <end xmi:type="uml:ConnectorEnd" xmi:id="_lEMtksnfEeejHePP_Hzkeg" partWithPort="_raFHAMneEeejHePP_Hzkeg" role="_VHTzEMnfEeejHePP_Hzkeg"/>
           </ownedConnector>
           <ownedConnector xmi:type="uml:Connector" xmi:id="_mspSEMnfEeejHePP_Hzkeg">
             <end xmi:type="uml:ConnectorEnd" xmi:id="_mspSEcnfEeejHePP_Hzkeg" partWithPort="_YySFcMneEeejHePP_Hzkeg" role="_POAPoMnaEeejHePP_Hzkeg"/>
             <end xmi:type="uml:ConnectorEnd" xmi:id="_mspSEsnfEeejHePP_Hzkeg" partWithPort="_fqL78MnfEeejHePP_Hzkeg" role="_VHTzEMnfEeejHePP_Hzkeg"/>
           </ownedConnector>
           <ownedConnector xmi:type="uml:Connector" xmi:id="_m5V00MngEeejHePP_Hzkeg">
             <end xmi:type="uml:ConnectorEnd" xmi:id="_m5V00cngEeejHePP_Hzkeg" partWithPort="_ds_r8MneEeejHePP_Hzkeg" role="_JqxQkMnaEeejHePP_Hzkeg"/>
             <end xmi:type="uml:ConnectorEnd" xmi:id="_m5V00sngEeejHePP_Hzkeg" partWithPort="_oc_DwMneEeejHePP_Hzkeg" role="_lA57QMnaEeejHePP_Hzkeg"/>
           </ownedConnector>
           <ownedConnector xmi:type="uml:Connector" xmi:id="_sJ9Z4MngEeejHePP_Hzkeg">
             <end xmi:type="uml:ConnectorEnd" xmi:id="_sJ9Z4cngEeejHePP_Hzkeg" partWithPort="_YySFcMneEeejHePP_Hzkeg" role="_JqxQkMnaEeejHePP_Hzkeg"/>
             <end xmi:type="uml:ConnectorEnd" xmi:id="_sJ9Z4sngEeejHePP_Hzkeg" partWithPort="_oc_DwMneEeejHePP_Hzkeg" role="_gDg0MMnaEeejHePP_Hzkeg"/>
           </ownedConnector>
           <ownedConnector xmi:type="uml:Connector" xmi:id="_vCu90MngEeejHePP_Hzkeg">
             <end xmi:type="uml:ConnectorEnd" xmi:id="_vCu90cngEeejHePP_Hzkeg" partWithPort="_YySFcMneEeejHePP_Hzkeg" role="_POAPoMnaEeejHePP_Hzkeg"/>
             <end xmi:type="uml:ConnectorEnd" xmi:id="_vCu90sngEeejHePP_Hzkeg" partWithPort="_oc_DwMneEeejHePP_Hzkeg" role="_imFeoMnaEeejHePP_Hzkeg"/>
           </ownedConnector>
           <ownedConnector xmi:type="uml:Connector" xmi:id="_w8xooMngEeejHePP_Hzkeg">
             <end xmi:type="uml:ConnectorEnd" xmi:id="_w8xoocngEeejHePP_Hzkeg" partWithPort="_ds_r8MneEeejHePP_Hzkeg" role="_POAPoMnaEeejHePP_Hzkeg"/>
             <end xmi:type="uml:ConnectorEnd" xmi:id="_w8xoosngEeejHePP_Hzkeg" partWithPort="_oc_DwMneEeejHePP_Hzkeg" role="_oR0SYMnaEeejHePP_Hzkeg"/>
           </ownedConnector>
           <ownedConnector xmi:type="uml:Connector" xmi:id="_KP8WAMnhEeejHePP_Hzkeg">
             <end xmi:type="uml:ConnectorEnd" xmi:id="_KQGHAMnhEeejHePP_Hzkeg" partWithPort="_oc_DwMneEeejHePP_Hzkeg" role="_uy6A0MnaEeejHePP_Hzkeg"/>
             <end xmi:type="uml:ConnectorEnd" xmi:id="_KQGHAcnhEeejHePP_Hzkeg" role="_43cV8MncEeejHePP_Hzkeg"/>
           </ownedConnector>
           <ownedConnector xmi:type="uml:Connector" xmi:id="_L9eO0MnhEeejHePP_Hzkeg">
             <end xmi:type="uml:ConnectorEnd" xmi:id="_L9eO0cnhEeejHePP_Hzkeg" partWithPort="_oc_DwMneEeejHePP_Hzkeg" role="_0oeGAMnaEeejHePP_Hzkeg"/>
             <end xmi:type="uml:ConnectorEnd" xmi:id="_L9eO0snhEeejHePP_Hzkeg" role="_7Hr6QMncEeejHePP_Hzkeg"/>
           </ownedConnector>
           <nestedClassifier xmi:type="uml:Class" xmi:id="_ZvFgYMnoEeejHePP_Hzkeg" name="Sense">
             <ownedRule xmi:type="uml:Constraint" xmi:id="_Z5NswMnoEeejHePP_Hzkeg" name="Sense_Assume">
               <specification xmi:type="uml:LiteralString" xmi:id="_Z5NswsnoEeejHePP_Hzkeg" name="Sense_Assume" value="/--assuming that: &#xD;&#xA;- at the beginning the speed is 0&#xD;&#xA;- the acceleration/deceleration is below a threshold  &#xD;&#xA;--/&#xD;&#xA;speed=0 &amp; G(&#xD;&#xA;&#x9;(next(speed) - speed)&lt;=1&#xD;&#xA;&#x9;and&#xD;&#xA;&#x9;(next(speed) - speed)>=-1&#xD;&#xA;&#x9;)"/>
             </ownedRule>
             <ownedRule xmi:type="uml:Constraint" xmi:id="_Z5NswcnoEeejHePP_Hzkeg" name="Sense_Guarantee">
               <specification xmi:type="uml:LiteralString" xmi:id="_Z5Nsw8noEeejHePP_Hzkeg" name="Sense_Guarantee" value="/--we expect that: &#xD;&#xA;- there is always a sensed speed&#xD;&#xA;- the delta between the speed and the sensed speed is &lt;= 2 &#xD;&#xA;--/&#xD;&#xA;always ((sensed_speed - speed &lt;= 4) and&#xD;&#xA;   &#x9;    (sensed_speed - speed >= - 4) and&#xD;&#xA;&#x9;    sensed_speed_is_present)"/>
             </ownedRule>
           </nestedClassifier>
           <nestedClassifier xmi:type="uml:DataType" xmi:id="_W8BEcMusEeeCqPEGjtWMTA" name="sensor1.sense"/>
           <nestedClassifier xmi:type="uml:DataType" xmi:id="_W8dwYMusEeeCqPEGjtWMTA" name="sensor2.sense"/>
           <nestedClassifier xmi:type="uml:DataType" xmi:id="_W8dwYsusEeeCqPEGjtWMTA" name="selector.select"/>
           <nestedClassifier xmi:type="uml:DataType" xmi:id="_W8dwZMusEeeCqPEGjtWMTA" name="selector.switch"/>
           <nestedClassifier xmi:type="uml:DataType" xmi:id="_W8dwZsusEeeCqPEGjtWMTA" name="monitor2.monitor"/>
           <nestedClassifier xmi:type="uml:DataType" xmi:id="_W8m6UMusEeeCqPEGjtWMTA" name="monitor1.monitor"/>
         </packagedElement>
         <packagedElement xmi:type="uml:Class" xmi:id="_rDtnsMnZEeejHePP_Hzkeg" name="SpeedSensor">
           <ownedAttribute xmi:type="uml:Port" xmi:id="_CqGDIMnaEeejHePP_Hzkeg" name="speed" visibility="public" aggregation="composite">
             <type xmi:type="uml:PrimitiveType" href="pathmap://UML_LIBRARIES/UMLPrimitiveTypes.library.uml#Real"/>
           </ownedAttribute>
           <ownedAttribute xmi:type="uml:Port" xmi:id="_JqxQkMnaEeejHePP_Hzkeg" name="sensed_speed" aggregation="composite">
             <type xmi:type="uml:PrimitiveType" href="pathmap://UML_LIBRARIES/UMLPrimitiveTypes.library.uml#Real"/>
           </ownedAttribute>
           <ownedAttribute xmi:type="uml:Port" xmi:id="_POAPoMnaEeejHePP_Hzkeg" name="sensed_speed_is_present" aggregation="composite">
             <type xmi:type="uml:PrimitiveType" href="pathmap://UML_LIBRARIES/UMLPrimitiveTypes.library.uml#Boolean"/>
           </ownedAttribute>
           <ownedAttribute xmi:type="uml:Property" xmi:id="_ThLpIMnnEeejHePP_Hzkeg" name="sense" type="_T_4XUMnnEeejHePP_Hzkeg"/>
           <ownedBehavior xmi:type="uml:StateMachine" xmi:id="_1qgJwMnlEeejHePP_Hzkeg" name="SpeedSensorSM">
             <region xmi:type="uml:Region" xmi:id="_6lXhQMnlEeejHePP_Hzkeg" name="Region1">
               <transition xmi:type="uml:Transition" xmi:id="__WixQMnlEeejHePP_Hzkeg" name="init_to_primary" guard="_etissHe_EemmJfmKAb07HA" source="_7iKgsMnlEeejHePP_Hzkeg" target="_8WKwgMnlEeejHePP_Hzkeg">
                 <ownedRule xmi:type="uml:Constraint" xmi:id="_etissHe_EemmJfmKAb07HA">
                   <specification xmi:type="uml:OpaqueExpression" xmi:id="_etissXe_EemmJfmKAb07HA">
                     <language>CleanC</language>
                     <body>true</body>
                   </specification>
                 </ownedRule>
                 <effect xmi:type="uml:OpaqueBehavior" xmi:id="_Tqn1UEpuEemoF--jg2W8cQ">
                   <language>CleanC</language>
                   <body>sensed_speed=0; sensed_speed_is_present = true;</body>
                 </effect>
               </transition>
               <transition xmi:type="uml:Transition" xmi:id="_Ab-vUMnmEeejHePP_Hzkeg" name="pr_to_pr" guard="_LGTkAMnmEeejHePP_Hzkeg" source="_8WKwgMnlEeejHePP_Hzkeg" target="_8WKwgMnlEeejHePP_Hzkeg">
                 <ownedRule xmi:type="uml:Constraint" xmi:id="_LGTkAMnmEeejHePP_Hzkeg">
                   <specification xmi:type="uml:OpaqueExpression" xmi:id="_TlKmsMnmEeejHePP_Hzkeg">
                     <language>CleanC</language>
                     <body>true</body>
                   </specification>
                 </ownedRule>
                 <effect xmi:type="uml:OpaqueBehavior" xmi:id="_aTzo8MnmEeejHePP_Hzkeg">
                   <language>CleanC</language>
                   <body>sensed_speed_is_present=true;&#xD;
 sensed_speed=speed;</body>
                 </effect>
               </transition>
               <subvertex xmi:type="uml:Pseudostate" xmi:id="_7iKgsMnlEeejHePP_Hzkeg" name="Initial1"/>
               <subvertex xmi:type="uml:State" xmi:id="_8WKwgMnlEeejHePP_Hzkeg" name="primary"/>
             </region>
           </ownedBehavior>
           <ownedBehavior xmi:type="uml:StateMachine" xmi:id="_FgpGcM3gEeeAvtXJQCAINA" name="faultSpeedSensor">
             <region xmi:type="uml:Region" xmi:id="_MMaa4M3gEeeAvtXJQCAINA" name="Region1">
               <transition xmi:type="uml:Transition" xmi:id="_omoYwM3gEeeAvtXJQCAINA" name="init_to_error" source="_kidYsM3gEeeAvtXJQCAINA" target="_li1QkM3gEeeAvtXJQCAINA"/>
               <transition xmi:type="uml:Transition" xmi:id="_twi44M3gEeeAvtXJQCAINA" name="failure" source="_li1QkM3gEeeAvtXJQCAINA" target="_qV8aQM3gEeeAvtXJQCAINA"/>
               <subvertex xmi:type="uml:Pseudostate" xmi:id="_kidYsM3gEeeAvtXJQCAINA" name="Initial1"/>
               <subvertex xmi:type="uml:State" xmi:id="_li1QkM3gEeeAvtXJQCAINA" name="nominal"/>
               <subvertex xmi:type="uml:State" xmi:id="_qV8aQM3gEeeAvtXJQCAINA" name="error"/>
             </region>
           </ownedBehavior>
           <nestedClassifier xmi:type="uml:Class" xmi:id="_T_4XUMnnEeejHePP_Hzkeg" name="Sense">
             <ownedRule xmi:type="uml:Constraint" xmi:id="_UYxYcMnnEeejHePP_Hzkeg" name="Sense_Assume">
               <specification xmi:type="uml:LiteralString" xmi:id="_UYxYcsnnEeejHePP_Hzkeg" name="Sense_Assume" value="/--assuming that: &#xD;&#xA;- at the beginning the speed is 0&#xD;&#xA;- the acceleration/deceleration is below a threshold  &#xD;&#xA;--/&#xD;&#xA;speed=0 &amp; G(&#xD;&#xA;&#x9;(next(speed) - speed)&lt;=1&#xD;&#xA;&#x9;and&#xD;&#xA;&#x9;(next(speed) - speed)>=-1&#xD;&#xA;&#x9;)"/>
             </ownedRule>
             <ownedRule xmi:type="uml:Constraint" xmi:id="_UYxYccnnEeejHePP_Hzkeg" name="Sense_Guarantee">
               <specification xmi:type="uml:LiteralString" xmi:id="_UY6iYMnnEeejHePP_Hzkeg" name="Sense_Guarantee" value="/--we expect that: &#xD;&#xA;- there is always a sensed speed&#xD;&#xA;- the delta between the speed and the sensed speed is &lt;= 1 &#xD;&#xA;--/&#xD;&#xA;always ((sensed_speed - speed &lt;= 1) and&#xD;&#xA;   &#x9;      &#x9;      (sensed_speed - speed >= - 1) and&#xD;&#xA;&#x9;&#x9;      sensed_speed_is_present)"/>
             </ownedRule>
           </nestedClassifier>
         </packagedElement>
         <packagedElement xmi:type="uml:Class" xmi:id="_u-CvQMnZEeejHePP_Hzkeg" name="Selector">
           <ownedAttribute xmi:type="uml:Port" xmi:id="_gDg0MMnaEeejHePP_Hzkeg" name="input1" aggregation="composite">
             <type xmi:type="uml:PrimitiveType" href="pathmap://UML_LIBRARIES/UMLPrimitiveTypes.library.uml#Real"/>
           </ownedAttribute>
           <ownedAttribute xmi:type="uml:Port" xmi:id="_imFeoMnaEeejHePP_Hzkeg" name="input1_is_present" aggregation="composite">
             <type xmi:type="uml:PrimitiveType" href="pathmap://UML_LIBRARIES/UMLPrimitiveTypes.library.uml#Boolean"/>
           </ownedAttribute>
           <ownedAttribute xmi:type="uml:Port" xmi:id="_lA57QMnaEeejHePP_Hzkeg" name="input2" aggregation="composite">
             <type xmi:type="uml:PrimitiveType" href="pathmap://UML_LIBRARIES/UMLPrimitiveTypes.library.uml#Real"/>
           </ownedAttribute>
           <ownedAttribute xmi:type="uml:Port" xmi:id="_oR0SYMnaEeejHePP_Hzkeg" name="input2_is_present" aggregation="composite">
             <type xmi:type="uml:PrimitiveType" href="pathmap://UML_LIBRARIES/UMLPrimitiveTypes.library.uml#Boolean"/>
           </ownedAttribute>
           <ownedAttribute xmi:type="uml:Port" xmi:id="_r2tVcMnaEeejHePP_Hzkeg" name="current_use" visibility="package" type="_GyjP8MrPEee1tdS56VBt8w" aggregation="composite"/>
           <ownedAttribute xmi:type="uml:Port" xmi:id="_uy6A0MnaEeejHePP_Hzkeg" name="output" aggregation="composite">
             <type xmi:type="uml:PrimitiveType" href="pathmap://UML_LIBRARIES/UMLPrimitiveTypes.library.uml#Real"/>
           </ownedAttribute>
           <ownedAttribute xmi:type="uml:Port" xmi:id="_0oeGAMnaEeejHePP_Hzkeg" name="output_is_present" aggregation="composite">
             <type xmi:type="uml:PrimitiveType" href="pathmap://UML_LIBRARIES/UMLPrimitiveTypes.library.uml#Boolean"/>
           </ownedAttribute>
           <ownedAttribute xmi:type="uml:Port" xmi:id="_0Y_qIMnbEeejHePP_Hzkeg" name="switch_current_use" visibility="package" aggregation="composite">
             <type xmi:type="uml:PrimitiveType" href="pathmap://UML_LIBRARIES/UMLPrimitiveTypes.library.uml#Boolean"/>
           </ownedAttribute>
           <ownedAttribute xmi:type="uml:Property" xmi:id="_3jARkMnnEeejHePP_Hzkeg" name="select" type="_3unrsMnnEeejHePP_Hzkeg"/>
           <ownedAttribute xmi:type="uml:Property" xmi:id="_Kjh8MMnoEeejHePP_Hzkeg" name="switch" type="_KwfaIMnoEeejHePP_Hzkeg"/>
           <ownedBehavior xmi:type="uml:StateMachine" xmi:id="_kqsMQODnEeesgt_aO67QgA" name="selector_SM">
             <region xmi:type="uml:Region" xmi:id="_ngMZwODnEeesgt_aO67QgA" name="Region1">
               <transition xmi:type="uml:Transition" xmi:id="_sukjIODnEeesgt_aO67QgA" name="init_to_in1" guard="_Gj2v4He_EemmJfmKAb07HA" source="_oO1BYODnEeesgt_aO67QgA" target="_o13zQODnEeesgt_aO67QgA">
                 <ownedRule xmi:type="uml:Constraint" xmi:id="_Gj2v4He_EemmJfmKAb07HA">
                   <specification xmi:type="uml:OpaqueExpression" xmi:id="_Gj2v4Xe_EemmJfmKAb07HA">
                     <language>CleanC</language>
                     <body>true</body>
                   </specification>
                 </ownedRule>
                 <effect xmi:type="uml:OpaqueBehavior" xmi:id="_3OclEEpsEemoF--jg2W8cQ">
                   <language>CleanC</language>
                   <body>current_use = 1; output=0;output_is_present=true;</body>
                 </effect>
               </transition>
               <transition xmi:type="uml:Transition" xmi:id="_uiy50ODnEeesgt_aO67QgA" name="in1_to_in1" guard="_1n8XkODnEeesgt_aO67QgA" source="_o13zQODnEeesgt_aO67QgA" target="_o13zQODnEeesgt_aO67QgA">
                 <ownedRule xmi:type="uml:Constraint" xmi:id="_1n8XkODnEeesgt_aO67QgA">
                   <specification xmi:type="uml:OpaqueExpression" xmi:id="_7fmugODnEeesgt_aO67QgA">
                     <language>CleanC</language>
                     <body>!switch_current_use</body>
                   </specification>
                 </ownedRule>
                 <effect xmi:type="uml:OpaqueBehavior" xmi:id="_DfTwAODoEeesgt_aO67QgA">
                   <language>CleanC</language>
                   <body>output=input1 ; output_is_present=input1_is_present;</body>
                 </effect>
               </transition>
               <transition xmi:type="uml:Transition" xmi:id="_FRv-AODoEeesgt_aO67QgA" name="in1_to_in2" guard="_H77FQODoEeesgt_aO67QgA" source="_o13zQODnEeesgt_aO67QgA" target="_qxZr0ODnEeesgt_aO67QgA">
                 <ownedRule xmi:type="uml:Constraint" xmi:id="_H77FQODoEeesgt_aO67QgA">
                   <specification xmi:type="uml:OpaqueExpression" xmi:id="_K56gYODoEeesgt_aO67QgA">
                     <language>CleanC</language>
                     <body>switch_current_use</body>
                   </specification>
                 </ownedRule>
                 <effect xmi:type="uml:OpaqueBehavior" xmi:id="_OegBcODoEeesgt_aO67QgA">
                   <language>CleanC</language>
                   <body>current_use=2;output=input2; output_is_present=input2_is_present;</body>
                 </effect>
               </transition>
               <transition xmi:type="uml:Transition" xmi:id="_PZNWMODoEeesgt_aO67QgA" name="in2_to_in1" guard="_TM1_4ODoEeesgt_aO67QgA" source="_qxZr0ODnEeesgt_aO67QgA" target="_o13zQODnEeesgt_aO67QgA">
                 <ownedRule xmi:type="uml:Constraint" xmi:id="_TM1_4ODoEeesgt_aO67QgA">
                   <specification xmi:type="uml:OpaqueExpression" xmi:id="_YA_rYODoEeesgt_aO67QgA">
                     <language>CleanC</language>
                     <body>switch_current_use</body>
                   </specification>
                 </ownedRule>
                 <effect xmi:type="uml:OpaqueBehavior" xmi:id="_bAVKUODoEeesgt_aO67QgA">
                   <language>CleanC</language>
                   <body>current_use=1;output=input1 ; output_is_present=input1_is_present;</body>
                 </effect>
               </transition>
               <transition xmi:type="uml:Transition" xmi:id="_gnJo4ODoEeesgt_aO67QgA" name="in2_to_in2" guard="_rMG1YODoEeesgt_aO67QgA" source="_qxZr0ODnEeesgt_aO67QgA" target="_qxZr0ODnEeesgt_aO67QgA">
                 <ownedRule xmi:type="uml:Constraint" xmi:id="_rMG1YODoEeesgt_aO67QgA">
                   <specification xmi:type="uml:OpaqueExpression" xmi:id="_w7INsODoEeesgt_aO67QgA">
                     <language>CleanC</language>
                     <body>!switch_current_use</body>
                   </specification>
                 </ownedRule>
                 <effect xmi:type="uml:OpaqueBehavior" xmi:id="_6yCocODoEeesgt_aO67QgA">
                   <language>CleanC</language>
                   <body>output=input2; output_is_present=input2_is_present;</body>
                 </effect>
               </transition>
               <subvertex xmi:type="uml:Pseudostate" xmi:id="_oO1BYODnEeesgt_aO67QgA" name="Initial1"/>
               <subvertex xmi:type="uml:State" xmi:id="_o13zQODnEeesgt_aO67QgA" name="input_1"/>
               <subvertex xmi:type="uml:State" xmi:id="_qxZr0ODnEeesgt_aO67QgA" name="input_2"/>
             </region>
           </ownedBehavior>
           <nestedClassifier xmi:type="uml:Class" xmi:id="_3unrsMnnEeejHePP_Hzkeg" name="Select">
             <ownedRule xmi:type="uml:Constraint" xmi:id="_37u6oMnnEeejHePP_Hzkeg" name="Select_Assume">
               <specification xmi:type="uml:LiteralString" xmi:id="_37u6osnnEeejHePP_Hzkeg" name="Select_Assume" value="true"/>
             </ownedRule>
             <ownedRule xmi:type="uml:Constraint" xmi:id="_37u6ocnnEeejHePP_Hzkeg" name="Select_Guarantee">
               <specification xmi:type="uml:LiteralString" xmi:id="_37u6o8nnEeejHePP_Hzkeg" name="Select_Guarantee" value="/-- we expect that:&#xD;&#xA;- at the beginning the sensed speed is 0&#xD;&#xA;- the sensed speed will be measured by the current sensor &#xD;&#xA;--/&#xD;&#xA;(output=0 and output_is_present = TRUE) and always ((next(current_use=1) implies &#xD;&#xA;    &#x9;     (next(output)=input1 and next(output_is_present)=input1_is_present)) and &#xD;&#xA;   &#x9;    (next(current_use=2) implies &#xD;&#xA;&#x9;     (next(output)=input2 and next(output_is_present)=input2_is_present)))"/>
             </ownedRule>
           </nestedClassifier>
           <nestedClassifier xmi:type="uml:Class" xmi:id="_KwfaIMnoEeejHePP_Hzkeg" name="Switch">
             <ownedRule xmi:type="uml:Constraint" xmi:id="_K8RMUMnoEeejHePP_Hzkeg" name="Switch_Assume">
               <specification xmi:type="uml:LiteralString" xmi:id="_K8RMUsnoEeejHePP_Hzkeg" name="Switch_Assume" value="true&#x9;"/>
             </ownedRule>
             <ownedRule xmi:type="uml:Constraint" xmi:id="_K8RMUcnoEeejHePP_Hzkeg" name="Switch_Guarantee">
               <specification xmi:type="uml:LiteralString" xmi:id="_K8RMU8noEeejHePP_Hzkeg" name="Switch_Guarantee" value="/--we expect that :&#xD;&#xA;- the switch of the sensor depends only on the input boolean port 'switch_current_use'&#xD;&#xA;--/&#xD;&#xA;always (&#xD;&#xA;    ((current_use=1 and switch_current_use) implies next(current_use)=2) and&#xD;&#xA;    ((current_use=2 and switch_current_use) implies next(current_use)=1) and&#xD;&#xA;    ((not switch_current_use) implies not change(current_use)))"/>
             </ownedRule>
           </nestedClassifier>
           <nestedClassifier xmi:type="uml:Signal" xmi:id="_kVfHYODeEeesgt_aO67QgA" name="switch_signal"/>
         </packagedElement>
         <packagedElement xmi:type="uml:Class" xmi:id="_oK1EIMnbEeejHePP_Hzkeg" name="MonitorPresence">
           <ownedAttribute xmi:type="uml:Port" xmi:id="_VHTzEMnfEeejHePP_Hzkeg" name="input_is_present" aggregation="composite">
             <type xmi:type="uml:PrimitiveType" href="pathmap://UML_LIBRARIES/UMLPrimitiveTypes.library.uml#Boolean"/>
           </ownedAttribute>
           <ownedAttribute xmi:type="uml:Port" xmi:id="_atZR0MnfEeejHePP_Hzkeg" name="enabled" aggregation="composite">
             <type xmi:type="uml:PrimitiveType" href="pathmap://UML_LIBRARIES/UMLPrimitiveTypes.library.uml#Boolean"/>
           </ownedAttribute>
           <ownedAttribute xmi:type="uml:Port" xmi:id="_WXNfQMngEeejHePP_Hzkeg" name="absence_alarm" visibility="package" aggregation="composite">
             <type xmi:type="uml:PrimitiveType" href="pathmap://UML_LIBRARIES/UMLPrimitiveTypes.library.uml#Boolean"/>
           </ownedAttribute>
           <ownedAttribute xmi:type="uml:Property" xmi:id="_u2hCkMnnEeejHePP_Hzkeg" name="monitor" type="_vDWksMnnEeejHePP_Hzkeg"/>
           <ownedBehavior xmi:type="uml:StateMachine" xmi:id="_XGR_UMreEee1tdS56VBt8w" name="monitorSM">
             <region xmi:type="uml:Region" xmi:id="_XGR_UcreEee1tdS56VBt8w" name="Region1">
               <transition xmi:type="uml:Transition" xmi:id="_8eE8MMreEee1tdS56VBt8w" name="init_to_pr" guard="_0cS4IHe_EemmJfmKAb07HA" source="_7DoXcMreEee1tdS56VBt8w" target="_7yuSEMreEee1tdS56VBt8w">
                 <ownedRule xmi:type="uml:Constraint" xmi:id="_0cS4IHe_EemmJfmKAb07HA">
                   <specification xmi:type="uml:OpaqueExpression" xmi:id="_0cS4IXe_EemmJfmKAb07HA">
                     <language>CleanC</language>
                     <body>true</body>
                   </specification>
                 </ownedRule>
                 <effect xmi:type="uml:OpaqueBehavior" xmi:id="_rmQkgEptEemoF--jg2W8cQ">
                   <language>CleanC</language>
                   <body>absence_alarm=false;</body>
                 </effect>
               </transition>
               <transition xmi:type="uml:Transition" xmi:id="_9PjccMreEee1tdS56VBt8w" name="pr_to_pr" guard="_AwHZIMrfEee1tdS56VBt8w" source="_7yuSEMreEee1tdS56VBt8w" target="_7yuSEMreEee1tdS56VBt8w">
                 <ownedRule xmi:type="uml:Constraint" xmi:id="_AwHZIMrfEee1tdS56VBt8w">
                   <specification xmi:type="uml:OpaqueExpression" xmi:id="_fBRDcMrfEee1tdS56VBt8w">
                     <language>CleanC</language>
                     <body>true</body>
                   </specification>
                 </ownedRule>
                 <effect xmi:type="uml:OpaqueBehavior" xmi:id="_n_aqMMrfEee1tdS56VBt8w">
                   <language>CleanC</language>
                   <body>absence_alarm=(!(input_is_present) &amp;&amp; (enabled));</body>
                 </effect>
               </transition>
               <subvertex xmi:type="uml:Pseudostate" xmi:id="_7DoXcMreEee1tdS56VBt8w" name="Initial1"/>
               <subvertex xmi:type="uml:State" xmi:id="_7yuSEMreEee1tdS56VBt8w" name="primary"/>
             </region>
           </ownedBehavior>
           <nestedClassifier xmi:type="uml:Class" xmi:id="_vDWksMnnEeejHePP_Hzkeg" name="Monitor">
             <ownedRule xmi:type="uml:Constraint" xmi:id="_vUrlQMnnEeejHePP_Hzkeg" name="Monitor_Assume">
               <specification xmi:type="uml:LiteralString" xmi:id="_vUrlQsnnEeejHePP_Hzkeg" name="Monitor_Assume" value="/-- assuming that:&#xD;&#xA;- at the beginning the sensor associated to this monitor is working&#xD;&#xA;--/&#xD;&#xA;input_is_present=TRUE"/>
             </ownedRule>
             <ownedRule xmi:type="uml:Constraint" xmi:id="_vUrlQcnnEeejHePP_Hzkeg" name="Monitor_Guarantee">
               <specification xmi:type="uml:LiteralString" xmi:id="_vUrlQ8nnEeejHePP_Hzkeg" name="Monitor_Guarantee" value="/-- we expect that:&#xD;&#xA;- an alarm is triggered whenever the monitor is enabled and the input is not present (is absent)&#xD;&#xA;--/&#xD;&#xA;always ((absence_alarm) iff (enabled and not(input_is_present)))"/>
             </ownedRule>
           </nestedClassifier>
           <nestedClassifier xmi:type="uml:Signal" xmi:id="_HInIEODfEeesgt_aO67QgA" name="absence_alarm_event"/>
         </packagedElement>
         <packagedElement xmi:type="uml:Association" xmi:id="_YyuKUMneEeejHePP_Hzkeg" name="Association4" memberEnd="_YySFcMneEeejHePP_Hzkeg _YyuKU8neEeejHePP_Hzkeg">
           <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_YyuKUcneEeejHePP_Hzkeg" source="org.eclipse.papyrus">
             <details xmi:type="ecore:EStringToStringMapEntry" xmi:id="_YyuKUsneEeejHePP_Hzkeg" key="nature" value="SysML_Nature"/>
           </eAnnotations>
           <ownedEnd xmi:type="uml:Property" xmi:id="_YyuKU8neEeejHePP_Hzkeg" name="system" type="_NzOwMMnZEeejHePP_Hzkeg" association="_YyuKUMneEeejHePP_Hzkeg"/>
         </packagedElement>
         <packagedElement xmi:type="uml:Association" xmi:id="_ds_r8cneEeejHePP_Hzkeg" name="Association5" memberEnd="_ds_r8MneEeejHePP_Hzkeg _ds_r9MneEeejHePP_Hzkeg">
           <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_ds_r8sneEeejHePP_Hzkeg" source="org.eclipse.papyrus">
             <details xmi:type="ecore:EStringToStringMapEntry" xmi:id="_ds_r88neEeejHePP_Hzkeg" key="nature" value="SysML_Nature"/>
           </eAnnotations>
           <ownedEnd xmi:type="uml:Property" xmi:id="_ds_r9MneEeejHePP_Hzkeg" name="system" type="_NzOwMMnZEeejHePP_Hzkeg" association="_ds_r8cneEeejHePP_Hzkeg"/>
         </packagedElement>
         <packagedElement xmi:type="uml:Association" xmi:id="_odINsMneEeejHePP_Hzkeg" name="Association6" memberEnd="_oc_DwMneEeejHePP_Hzkeg _odINs8neEeejHePP_Hzkeg">
           <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_odINscneEeejHePP_Hzkeg" source="org.eclipse.papyrus">
             <details xmi:type="ecore:EStringToStringMapEntry" xmi:id="_odINssneEeejHePP_Hzkeg" key="nature" value="SysML_Nature"/>
           </eAnnotations>
           <ownedEnd xmi:type="uml:Property" xmi:id="_odINs8neEeejHePP_Hzkeg" name="system" type="_NzOwMMnZEeejHePP_Hzkeg" association="_odINsMneEeejHePP_Hzkeg"/>
         </packagedElement>
         <packagedElement xmi:type="uml:Association" xmi:id="_raOQ8MneEeejHePP_Hzkeg" name="Association8" memberEnd="_raFHAMneEeejHePP_Hzkeg _raOQ88neEeejHePP_Hzkeg">
           <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_raOQ8cneEeejHePP_Hzkeg" source="org.eclipse.papyrus">
             <details xmi:type="ecore:EStringToStringMapEntry" xmi:id="_raOQ8sneEeejHePP_Hzkeg" key="nature" value="SysML_Nature"/>
           </eAnnotations>
           <ownedEnd xmi:type="uml:Property" xmi:id="_raOQ88neEeejHePP_Hzkeg" name="system" type="_NzOwMMnZEeejHePP_Hzkeg" association="_raOQ8MneEeejHePP_Hzkeg"/>
         </packagedElement>
         <packagedElement xmi:type="uml:Association" xmi:id="_fqVs8MnfEeejHePP_Hzkeg" name="Association8" memberEnd="_fqVs88nfEeejHePP_Hzkeg _fqL78MnfEeejHePP_Hzkeg">
           <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_fqVs8cnfEeejHePP_Hzkeg" source="org.eclipse.papyrus">
             <details xmi:type="ecore:EStringToStringMapEntry" xmi:id="_fqVs8snfEeejHePP_Hzkeg" key="nature" value="SysML_Nature"/>
           </eAnnotations>
           <ownedEnd xmi:type="uml:Property" xmi:id="_fqVs88nfEeejHePP_Hzkeg" name="system" type="_NzOwMMnZEeejHePP_Hzkeg" association="_fqVs8MnfEeejHePP_Hzkeg"/>
         </packagedElement>
       </packagedElement>
       <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_9i2i4MnhEeejHePP_Hzkeg">
         <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_9i2i4cnhEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML">
           <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#/"/>
         </eAnnotations>
         <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_TZ_nULU5EduiKqCzJMWbGw"/>
       </profileApplication>
       <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_9i2i4snhEeejHePP_Hzkeg">
         <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_9i2i48nhEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML">
           <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//modelelements"/>
         </eAnnotations>
         <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_Gx8MgLX7EduFmqQsrNB9lw"/>
       </profileApplication>
       <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_9i2i5MnhEeejHePP_Hzkeg">
         <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_9i2i5cnhEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML">
           <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//blocks"/>
         </eAnnotations>
         <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_fSw28LX7EduFmqQsrNB9lw"/>
       </profileApplication>
       <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_9jTO0MnhEeejHePP_Hzkeg">
         <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_9jTO0cnhEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML">
           <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//portandflows"/>
         </eAnnotations>
         <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_rpx28LX7EduFmqQsrNB9lw"/>
       </profileApplication>
       <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_9m4HQMnhEeejHePP_Hzkeg">
         <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_9m4HQcnhEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML">
           <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//constraints"/>
         </eAnnotations>
         <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_5WYJ0LX7EduFmqQsrNB9lw"/>
       </profileApplication>
       <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_9m4HQsnhEeejHePP_Hzkeg">
         <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_9m4HQ8nhEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML">
           <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//activities"/>
         </eAnnotations>
         <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_C2zXMLX8EduFmqQsrNB9lw"/>
       </profileApplication>
       <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_9m4HRMnhEeejHePP_Hzkeg">
         <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_9m4HRcnhEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML">
           <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//allocations"/>
         </eAnnotations>
         <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_NxdG4LX8EduFmqQsrNB9lw"/>
       </profileApplication>
       <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_9oEaEMnhEeejHePP_Hzkeg">
         <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_9oEaEcnhEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML">
           <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//requirements"/>
         </eAnnotations>
         <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_OOJC4LX8EduFmqQsrNB9lw"/>
       </profileApplication>
       <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_9pG74MnhEeejHePP_Hzkeg">
         <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_9pG74cnhEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML">
           <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//interactions"/>
         </eAnnotations>
         <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_meOioLX8EduFmqQsrNB9lw"/>
       </profileApplication>
       <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_9pG74snhEeejHePP_Hzkeg">
         <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_9pG748nhEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML">
           <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//statemachines"/>
         </eAnnotations>
         <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_nAF5kLX8EduFmqQsrNB9lw"/>
       </profileApplication>
       <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_9pG75MnhEeejHePP_Hzkeg">
         <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_9pG75cnhEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML">
           <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//usecases"/>
         </eAnnotations>
         <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_neZmMLX8EduFmqQsrNB9lw"/>
       </profileApplication>
       <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_iBhF8M3gEeeAvtXJQCAINA">
         <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_iBhF8c3gEeeAvtXJQCAINA" source="http://www.eclipse.org/uml2/2.0.0/UML">
           <references xmi:type="ecore:EPackage" href="http://CHESS#//FailurePropagation"/>
         </eAnnotations>
         <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_hdOrwLwzEd-CDNLmLgazUQ"/>
       </profileApplication>
       <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_iBqP4M3gEeeAvtXJQCAINA">
         <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_iBqP4c3gEeeAvtXJQCAINA" source="http://www.eclipse.org/uml2/2.0.0/UML">
           <references xmi:type="ecore:EPackage" href="http://CHESS#//ThreatsPropagation"/>
         </eAnnotations>
         <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_5g4wEDQ3EeC0ueejuetpgA"/>
       </profileApplication>
     </packagedElement>
     <packagedElement xmi:type="uml:Package" xmi:id="_otw4kMrMEee1tdS56VBt8w" name="modelComponentView">
       <packagedElement xmi:type="uml:DataType" xmi:id="_24b0MMugEeemE4e81vDbeA" name="Double" visibility="protected"/>
       <packagedElement xmi:type="uml:DataType" xmi:id="_GyjP8MrPEee1tdS56VBt8w" name="Interval1_2"/>
       <packagedElement xmi:type="uml:SignalEvent" xmi:id="_E0Z5QOFtEeedP_hzDpiVAg" name="switch_signal_event" signal="_kVfHYODeEeesgt_aO67QgA"/>
       <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_OeWI4MrNEee1tdS56VBt8w">
         <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_OeWI4crNEee1tdS56VBt8w" source="http://www.eclipse.org/uml2/2.0.0/UML">
           <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/MARTE/1#//GRM"/>
         </eAnnotations>
         <appliedProfile xmi:type="uml:Profile" href="pathmap://Papyrus_PROFILES/MARTE.profile.uml#_XVWGUAPMEdyuUt-4qHuVvQ"/>
       </profileApplication>
       <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_OeddoMrNEee1tdS56VBt8w">
         <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_OeddocrNEee1tdS56VBt8w" source="http://www.eclipse.org/uml2/2.0.0/UML">
           <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/MARTE/1#//Alloc"/>
         </eAnnotations>
         <appliedProfile xmi:type="uml:Profile" href="pathmap://Papyrus_PROFILES/MARTE.profile.uml#_ar8OsAPMEdyuUt-4qHuVvQ"/>
       </profileApplication>
       <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_fxwU8MrOEee1tdS56VBt8w">
         <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_fxwU8crOEee1tdS56VBt8w" source="http://www.eclipse.org/uml2/2.0.0/UML">
           <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/MARTE/1#//VSL/DataTypes"/>
         </eAnnotations>
         <appliedProfile xmi:type="uml:Profile" href="pathmap://Papyrus_PROFILES/MARTE.profile.uml#_9FdqwA-MEdyLh7muGbCqMw"/>
       </profileApplication>
       <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_f3JC0MugEeemE4e81vDbeA">
         <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_f3JC0cugEeemE4e81vDbeA" source="http://www.eclipse.org/uml2/2.0.0/UML">
           <references xmi:type="ecore:EPackage" href="http://CHESS#//ComponentModel"/>
         </eAnnotations>
         <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_MftccDQ2EeC0ueejuetpgA"/>
       </profileApplication>
     </packagedElement>
     <packagedElement xmi:type="uml:Package" xmi:id="_JjGU4MrjEee1tdS56VBt8w" name="modeDeploymentView"/>
     <packagedElement xmi:type="uml:Package" xmi:id="_CDbeUMrjEee1tdS56VBt8w" name="modelAnalysisView">
       <packagedElement xmi:type="uml:Package" xmi:id="_dNgC8MrjEee1tdS56VBt8w" name="modelDependabilityAnalysisView" URI="">
         <packagedElement xmi:type="uml:Package" xmi:id="_sDdU4E-yEemU0aMen8TVXg" name="modelSystemView_PhisicalArchitecture">
           <packagedElement xmi:type="uml:Component" xmi:id="_6WxCcE-yEemU0aMen8TVXg" name="FTA"/>
           <packagedElement xmi:type="uml:Component" xmi:id="_e8vg0E-zEemU0aMen8TVXg" name="FTA"/>
           <packagedElement xmi:type="uml:Component" xmi:id="_rDf3QE-zEemU0aMen8TVXg" name="CONTRACT_REF"/>
           <packagedElement xmi:type="uml:Component" xmi:id="_8v_zsHe_EemmJfmKAb07HA" name="CONTRACT_COMPOSITE_IMPLEMENTATION_ANALYSIS_1"/>
           <packagedElement xmi:type="uml:Component" xmi:id="_oEn0AHfDEemmJfmKAb07HA" name="FTA_ANALYSIS_1"/>
           <packagedElement xmi:type="uml:Component" xmi:id="_dw9usHfKEemiWaxj_3Hy5w" name="FTA_ANALYSIS_2"/>
           <packagedElement xmi:type="uml:Component" xmi:id="_8Khx4NnlEempZePwVoyTHA" name="CONTRACT_FTA"/>
           <packagedElement xmi:type="uml:Component" xmi:id="_qnqwYNnrEempZePwVoyTHA" name="CONTRACT_IMPL"/>
           <packagedElement xmi:type="uml:Component" xmi:id="_utBcMNnrEempZePwVoyTHA" name="PROP_VAL"/>
           <packagedElement xmi:type="uml:Component" xmi:id="_yCJk8NnrEempZePwVoyTHA" name="CONT_PROP_VAL"/>
           <packagedElement xmi:type="uml:Component" xmi:id="_0yqkwNnrEempZePwVoyTHA" name="MODEL_CHECK"/>
           <packagedElement xmi:type="uml:Component" xmi:id="_4J37sNnsEempZePwVoyTHA" name="MODEL_CHECK"/>
           <packagedElement xmi:type="uml:Component" xmi:id="_KrA8wMK6Eeqrbc3PZZCA9Q" name="CONTRACT_BASED_FTA_ANALYSIS_1"/>
         </packagedElement>
         <packagedElement xmi:type="uml:Class" xmi:id="_2Y9ZAMuXEee9L_NsVF0R0A" name="analisys_context"/>
         <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_NZrioMuYEee9L_NsVF0R0A">
           <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_NZ4-AMuYEee9L_NsVF0R0A" source="http://www.eclipse.org/uml2/2.0.0/UML">
             <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/MARTE/1#//GQAM"/>
           </eAnnotations>
           <appliedProfile xmi:type="uml:Profile" href="pathmap://Papyrus_PROFILES/MARTE.profile.uml#_4bV20APMEdyuUt-4qHuVvQ"/>
         </profileApplication>
       </packagedElement>
     </packagedElement>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_3uHw8MktEee0hNePRc2zdw">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_3uSJAMktEee0hNePRc2zdw" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#/"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_TZ_nULU5EduiKqCzJMWbGw"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_4W8rgMktEee0hNePRc2zdw">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_4W8rgcktEee0hNePRc2zdw" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//modelelements"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_Gx8MgLX7EduFmqQsrNB9lw"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_4XGcgMktEee0hNePRc2zdw">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_4XGcgcktEee0hNePRc2zdw" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//blocks"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_fSw28LX7EduFmqQsrNB9lw"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_4XGcgsktEee0hNePRc2zdw">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_4XGcg8ktEee0hNePRc2zdw" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//portandflows"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_rpx28LX7EduFmqQsrNB9lw"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_4XGchMktEee0hNePRc2zdw">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_4XGchcktEee0hNePRc2zdw" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//constraints"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_5WYJ0LX7EduFmqQsrNB9lw"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_4XQNgMktEee0hNePRc2zdw">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_4XQNgcktEee0hNePRc2zdw" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//activities"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_C2zXMLX8EduFmqQsrNB9lw"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_4XQNgsktEee0hNePRc2zdw">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_4XQNg8ktEee0hNePRc2zdw" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//allocations"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_NxdG4LX8EduFmqQsrNB9lw"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_4XQNhMktEee0hNePRc2zdw">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_4XQNhcktEee0hNePRc2zdw" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//requirements"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_OOJC4LX8EduFmqQsrNB9lw"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_4XQNhsktEee0hNePRc2zdw">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_4XalkMktEee0hNePRc2zdw" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//interactions"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_meOioLX8EduFmqQsrNB9lw"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_4XalkcktEee0hNePRc2zdw">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_4XalksktEee0hNePRc2zdw" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//statemachines"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_nAF5kLX8EduFmqQsrNB9lw"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_4Xalk8ktEee0hNePRc2zdw">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_4XallMktEee0hNePRc2zdw" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//usecases"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_neZmMLX8EduFmqQsrNB9lw"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_uI994MnYEeejHePP_Hzkeg">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_uJHu4MnYEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://CHESS#//Core"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_ad4owDgVEd-68Z_bhNRGsA"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_uJRf4MnYEeejHePP_Hzkeg">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_uJtkwMnYEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://CHESS#//Core/CHESSViews"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_FttqgMJDEd-0jpzjleFnug"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_bQEv0MnZEeejHePP_Hzkeg">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_bQEv0cnZEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http:///CHESSContract.ecore#/"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSContract/CHESSContract.profile.uml#_Hmdm0NDVEeG5E52m3d5H1g"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_x0SGQMrOEee1tdS56VBt8w">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_x0bQMMrOEee1tdS56VBt8w" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/MARTE/1#//VSL/DataTypes"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://Papyrus_PROFILES/MARTE.profile.uml#_9FdqwA-MEdyLh7muGbCqMw"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_2nBfsMrSEee1tdS56VBt8w">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_2nLQsMrSEee1tdS56VBt8w" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://CHESS#//Safety"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_f-f6oMvrEeSajLw6mg2A8Q"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KFJm4E-zEemU0aMen8TVXg">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KFLcEE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://CHESS#/"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_EA6IcDcwEd-mWLzcI61s7Q"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KGRBME-zEemU0aMen8TVXg">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KGRoQE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://CHESS#//FailurePropagation"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_hdOrwLwzEd-CDNLmLgazUQ"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KGVSoE-zEemU0aMen8TVXg">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KGYV8E-zEemU0aMen8TVXg" source="PapyrusVersion">
         <details xmi:type="ecore:EStringToStringMapEntry" xmi:id="_KGYV8U-zEemU0aMen8TVXg" key="Version" value="0.1.8"/>
         <details xmi:type="ecore:EStringToStringMapEntry" xmi:id="_KGYV8k-zEemU0aMen8TVXg" key="Comment" value=""/>
         <details xmi:type="ecore:EStringToStringMapEntry" xmi:id="_KGYV80-zEemU0aMen8TVXg" key="Copyright" value=""/>
         <details xmi:type="ecore:EStringToStringMapEntry" xmi:id="_KGYV9E-zEemU0aMen8TVXg" key="Date" value="2010-09-24"/>
         <details xmi:type="ecore:EStringToStringMapEntry" xmi:id="_KGYV9U-zEemU0aMen8TVXg" key="Author" value=""/>
       </eAnnotations>
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KGVSoU-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_QgRZcMe6Ed-7etIj5eTw0Q"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_cE_bwLwzEd-CDNLmLgazUQ"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KGZkEE-zEemU0aMen8TVXg">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KGaLIE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://CHESS#//StateBasedComponents"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_d50lQL86Ed-TL8tpOyViyA"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KGfDoE-zEemU0aMen8TVXg">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KGfDoU-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://CHESS#//FaultTolerance"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_mbqqgL86Ed-TL8tpOyViyA"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KGiG8E-zEemU0aMen8TVXg">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KGiuAE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://CHESS#//MaintenanceMonitoring"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_oUVxcL88Ed-TL8tpOyViyA"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KGmYYE-zEemU0aMen8TVXg">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KGm_cE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://CHESS#//StateBasedAnalysis"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_Wgxh0L8_Ed-TL8tpOyViyA"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KGpbsE-zEemU0aMen8TVXg">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KGqCwE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://CHESS#//DependableComponent"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_uNKOgDQ2EeC0ueejuetpgA"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KGuUME-zEemU0aMen8TVXg">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KGviUE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://CHESS#//ThreatsPropagation"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_5g4wEDQ3EeC0ueejuetpgA"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KG89sE-zEemU0aMen8TVXg">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KG9kwE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://CHESS#//MitigationMeans"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_kJICMFiIEeGbwa2cK55fPQ"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KHABAE-zEemU0aMen8TVXg">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KHEScE-zEemU0aMen8TVXg" source="PapyrusVersion">
         <details xmi:type="ecore:EStringToStringMapEntry" xmi:id="_KHEScU-zEemU0aMen8TVXg" key="Version" value="0.1.8"/>
         <details xmi:type="ecore:EStringToStringMapEntry" xmi:id="_KHESck-zEemU0aMen8TVXg" key="Comment" value=""/>
         <details xmi:type="ecore:EStringToStringMapEntry" xmi:id="_KHESc0-zEemU0aMen8TVXg" key="Copyright" value=""/>
         <details xmi:type="ecore:EStringToStringMapEntry" xmi:id="_KHESdE-zEemU0aMen8TVXg" key="Date" value="2010-09-24"/>
         <details xmi:type="ecore:EStringToStringMapEntry" xmi:id="_KHESdU-zEemU0aMen8TVXg" key="Author" value=""/>
       </eAnnotations>
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KHAoEE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_S2Uq0ce6Ed-7etIj5eTw0Q"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_nyQ7MLwzEd-CDNLmLgazUQ"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KHE5gE-zEemU0aMen8TVXg">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KHFgkE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://CHESS#//HardwareBaseline"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_1TsX8MCpEd-RT45s8cwWMg"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KHH80E-zEemU0aMen8TVXg">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KHH80U-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://CHESS#//RTComponentModel"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_WgatoDgVEd-68Z_bhNRGsA"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KHM1UE-zEemU0aMen8TVXg">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KHNcYE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://CHESS#//ARINCComponentModel"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_GMlQEGwuEeWvYIaEJT1qow"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KHQfsE-zEemU0aMen8TVXg">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KHRGwE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://CHESS#//ComponentModel"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_MftccDQ2EeC0ueejuetpgA"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KHXNYE-zEemU0aMen8TVXg">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KHX0cE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://CHESS#//STS"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_-aQIUKbREeSHP5PnCeTneg"/>
     </profileApplication>
     <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_ZLiWoILiEeqxuOOz6y6Ozw">
       <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_ZLjkwILiEeqxuOOz6y6Ozw" source="http://www.eclipse.org/uml2/2.0.0/UML">
         <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/MARTE/1#//GQAM"/>
       </eAnnotations>
       <appliedProfile xmi:type="uml:Profile" href="pathmap://Papyrus_PROFILES/MARTE.profile.uml#_4bV20APMEdyuUt-4qHuVvQ"/>
     </profileApplication>
   </uml:Model>
   <Core:CHESS xmi:id="_vGqVMMnYEeejHePP_Hzkeg" base_Model="_3PIH0MktEee0hNePRc2zdw"/>
   <CHESSViews:RequirementView xmi:id="_66csUMnYEeejHePP_Hzkeg" base_Package="_xRZHYMnYEeejHePP_Hzkeg"/>
   <CHESSViews:SystemView xmi:id="_-r16UMnYEeejHePP_Hzkeg" base_Package="_1irWYMnYEeejHePP_Hzkeg"/>
   <Blocks:Block xmi:id="_NzdZsMnZEeejHePP_Hzkeg" base_Class="_NzOwMMnZEeejHePP_Hzkeg"/>
   <CHESSContract:System xmi:id="_dI6gwMnZEeejHePP_Hzkeg" base_Class="_NzOwMMnZEeejHePP_Hzkeg"/>
   <Core:CHGaResourcePlatform xmi:id="_h1ngcMnZEeejHePP_Hzkeg" base_Classifier="_NzOwMMnZEeejHePP_Hzkeg"/>
   <Blocks:Block xmi:id="_rD2xoMnZEeejHePP_Hzkeg" base_Class="_rDtnsMnZEeejHePP_Hzkeg"/>
   <Blocks:Block xmi:id="_u-CvQcnZEeejHePP_Hzkeg" base_Class="_u-CvQMnZEeejHePP_Hzkeg"/>
   <PortAndFlows:FlowPort xmi:id="_Cq1C8MnaEeejHePP_Hzkeg" base_Port="_CqGDIMnaEeejHePP_Hzkeg" direction="in"/>
   <PortAndFlows:FlowPort xmi:id="_Jq6agMnaEeejHePP_Hzkeg" base_Port="_JqxQkMnaEeejHePP_Hzkeg" direction="out"/>
   <PortAndFlows:FlowPort xmi:id="_POKAoMnaEeejHePP_Hzkeg" base_Port="_POAPoMnaEeejHePP_Hzkeg" direction="out"/>
   <PortAndFlows:FlowPort xmi:id="_gDqlMMnaEeejHePP_Hzkeg" base_Port="_gDg0MMnaEeejHePP_Hzkeg" direction="in"/>
   <PortAndFlows:FlowPort xmi:id="_imPPoMnaEeejHePP_Hzkeg" base_Port="_imFeoMnaEeejHePP_Hzkeg" direction="in"/>
   <PortAndFlows:FlowPort xmi:id="_lBDsQMnaEeejHePP_Hzkeg" base_Port="_lA57QMnaEeejHePP_Hzkeg" direction="in"/>
   <PortAndFlows:FlowPort xmi:id="_oR9cUMnaEeejHePP_Hzkeg" base_Port="_oR0SYMnaEeejHePP_Hzkeg" direction="in"/>
   <PortAndFlows:FlowPort xmi:id="_r2_pUMnaEeejHePP_Hzkeg" base_Port="_r2tVcMnaEeejHePP_Hzkeg" direction="out"/>
   <PortAndFlows:FlowPort xmi:id="_uzDKwMnaEeejHePP_Hzkeg" base_Port="_uy6A0MnaEeejHePP_Hzkeg" direction="out"/>
   <PortAndFlows:FlowPort xmi:id="_0oxA8MnaEeejHePP_Hzkeg" base_Port="_0oeGAMnaEeejHePP_Hzkeg" direction="out"/>
   <Blocks:Block xmi:id="_oK-1IMnbEeejHePP_Hzkeg" base_Class="_oK1EIMnbEeejHePP_Hzkeg"/>
   <PortAndFlows:FlowPort xmi:id="_0ZTMIMnbEeejHePP_Hzkeg" base_Port="_0Y_qIMnbEeejHePP_Hzkeg" direction="in"/>
   <PortAndFlows:FlowPort xmi:id="_0dqSQMncEeejHePP_Hzkeg" base_Port="_0dXXUMncEeejHePP_Hzkeg" direction="in"/>
   <PortAndFlows:FlowPort xmi:id="_43lf4MncEeejHePP_Hzkeg" base_Port="_43cV8MncEeejHePP_Hzkeg" direction="out"/>
   <PortAndFlows:FlowPort xmi:id="_7H1EMMncEeejHePP_Hzkeg" base_Port="_7Hr6QMncEeejHePP_Hzkeg" direction="out"/>
   <PortAndFlows:FlowPort xmi:id="_VHTzEcnfEeejHePP_Hzkeg" base_Port="_VHTzEMnfEeejHePP_Hzkeg" direction="in"/>
   <PortAndFlows:FlowPort xmi:id="_atibwMnfEeejHePP_Hzkeg" base_Port="_atZR0MnfEeejHePP_Hzkeg" direction="in"/>
   <PortAndFlows:FlowPort xmi:id="_WXXQQMngEeejHePP_Hzkeg" base_Port="_WXNfQMngEeejHePP_Hzkeg" direction="out"/>
   <CHESSContract:ContractProperty xmi:id="_ThVaIMnnEeejHePP_Hzkeg" base_Property="_ThLpIMnnEeejHePP_Hzkeg"/>
   <CHESSContract:Contract xmi:id="_UABhQMnnEeejHePP_Hzkeg" base_Class="_T_4XUMnnEeejHePP_Hzkeg" Assume="_UY6iYcnnEeejHePP_Hzkeg" Guarantee="_UY6iYsnnEeejHePP_Hzkeg"/>
   <CHESSContract:FormalProperty xmi:id="_UY6iYcnnEeejHePP_Hzkeg" base_Constraint="_UYxYcMnnEeejHePP_Hzkeg"/>
   <CHESSContract:FormalProperty xmi:id="_UY6iYsnnEeejHePP_Hzkeg" base_Constraint="_UYxYccnnEeejHePP_Hzkeg"/>
   <CHESSContract:ContractProperty xmi:id="_u2ks8MnnEeejHePP_Hzkeg" base_Property="_u2hCkMnnEeejHePP_Hzkeg"/>
   <CHESSContract:Contract xmi:id="_vDd5cMnnEeejHePP_Hzkeg" base_Class="_vDWksMnnEeejHePP_Hzkeg" Assume="_vUrlRMnnEeejHePP_Hzkeg" Guarantee="_vUrlRcnnEeejHePP_Hzkeg"/>
   <CHESSContract:FormalProperty xmi:id="_vUrlRMnnEeejHePP_Hzkeg" base_Constraint="_vUrlQMnnEeejHePP_Hzkeg"/>
   <CHESSContract:FormalProperty xmi:id="_vUrlRcnnEeejHePP_Hzkeg" base_Constraint="_vUrlQcnnEeejHePP_Hzkeg"/>
   <CHESSContract:ContractProperty xmi:id="_3jARkcnnEeejHePP_Hzkeg" base_Property="_3jARkMnnEeejHePP_Hzkeg"/>
   <CHESSContract:Contract xmi:id="_3unrscnnEeejHePP_Hzkeg" base_Class="_3unrsMnnEeejHePP_Hzkeg" Assume="_37u6pMnnEeejHePP_Hzkeg" Guarantee="_37u6pcnnEeejHePP_Hzkeg"/>
   <CHESSContract:FormalProperty xmi:id="_37u6pMnnEeejHePP_Hzkeg" base_Constraint="_37u6oMnnEeejHePP_Hzkeg"/>
   <CHESSContract:FormalProperty xmi:id="_37u6pcnnEeejHePP_Hzkeg" base_Constraint="_37u6ocnnEeejHePP_Hzkeg"/>
   <CHESSContract:ContractProperty xmi:id="_KjrtMMnoEeejHePP_Hzkeg" base_Property="_Kjh8MMnoEeejHePP_Hzkeg"/>
   <CHESSContract:Contract xmi:id="_KwpLIMnoEeejHePP_Hzkeg" base_Class="_KwfaIMnoEeejHePP_Hzkeg" Assume="_K8RMVMnoEeejHePP_Hzkeg" Guarantee="_K8RMVcnoEeejHePP_Hzkeg"/>
   <CHESSContract:FormalProperty xmi:id="_K8RMVMnoEeejHePP_Hzkeg" base_Constraint="_K8RMUMnoEeejHePP_Hzkeg"/>
   <CHESSContract:FormalProperty xmi:id="_K8RMVcnoEeejHePP_Hzkeg" base_Constraint="_K8RMUcnoEeejHePP_Hzkeg"/>
   <CHESSContract:ContractProperty xmi:id="_Zia9YcnoEeejHePP_Hzkeg" base_Property="_Zia9YMnoEeejHePP_Hzkeg" RefinedBy="_W8T_YMusEeeCqPEGjtWMTA _W8dwYcusEeeCqPEGjtWMTA _W8dwY8usEeeCqPEGjtWMTA _W8dwZcusEeeCqPEGjtWMTA _W8dwZ8usEeeCqPEGjtWMTA _W8m6UcusEeeCqPEGjtWMTA"/>
   <CHESSContract:Contract xmi:id="_ZvFgYcnoEeejHePP_Hzkeg" base_Class="_ZvFgYMnoEeejHePP_Hzkeg" Assume="_Z5XdwMnoEeejHePP_Hzkeg" Guarantee="_Z5XdwcnoEeejHePP_Hzkeg"/>
   <CHESSContract:FormalProperty xmi:id="_Z5XdwMnoEeejHePP_Hzkeg" base_Constraint="_Z5NswMnoEeejHePP_Hzkeg"/>
   <CHESSContract:FormalProperty xmi:id="_Z5XdwcnoEeejHePP_Hzkeg" base_Constraint="_Z5NswcnoEeejHePP_Hzkeg"/>
   <CHESSViews:ComponentView xmi:id="_vnH9EMrMEee1tdS56VBt8w" base_Package="_otw4kMrMEee1tdS56VBt8w"/>
   <CHESSViews:DeploymentView xmi:id="_P-N-MMrjEee1tdS56VBt8w" base_Package="_JjGU4MrjEee1tdS56VBt8w"/>
   <CHESSViews:AnalysisView xmi:id="_RhnDkMrjEee1tdS56VBt8w" base_Package="_CDbeUMrjEee1tdS56VBt8w"/>
   <CHESSContract:ContractRefinement xmi:id="_W8T_YMusEeeCqPEGjtWMTA" base_DataType="_W8BEcMusEeeCqPEGjtWMTA" Instance="_YySFcMneEeejHePP_Hzkeg" Contract="_ThVaIMnnEeejHePP_Hzkeg"/>
   <CHESSContract:ContractRefinement xmi:id="_W8dwYcusEeeCqPEGjtWMTA" base_DataType="_W8dwYMusEeeCqPEGjtWMTA" Instance="_ds_r8MneEeejHePP_Hzkeg" Contract="_ThVaIMnnEeejHePP_Hzkeg"/>
   <CHESSContract:ContractRefinement xmi:id="_W8dwY8usEeeCqPEGjtWMTA" base_DataType="_W8dwYsusEeeCqPEGjtWMTA" Instance="_oc_DwMneEeejHePP_Hzkeg" Contract="_3jARkcnnEeejHePP_Hzkeg"/>
   <CHESSContract:ContractRefinement xmi:id="_W8dwZcusEeeCqPEGjtWMTA" base_DataType="_W8dwZMusEeeCqPEGjtWMTA" Instance="_oc_DwMneEeejHePP_Hzkeg" Contract="_KjrtMMnoEeejHePP_Hzkeg"/>
   <CHESSContract:ContractRefinement xmi:id="_W8dwZ8usEeeCqPEGjtWMTA" base_DataType="_W8dwZsusEeeCqPEGjtWMTA" Instance="_raFHAMneEeejHePP_Hzkeg" Contract="_u2ks8MnnEeejHePP_Hzkeg"/>
   <CHESSContract:ContractRefinement xmi:id="_W8m6UcusEeeCqPEGjtWMTA" base_DataType="_W8m6UMusEeeCqPEGjtWMTA" Instance="_fqL78MnfEeejHePP_Hzkeg" Contract="_u2ks8MnnEeejHePP_Hzkeg"/>
   <ThreatsPropagation:ErrorModel xmi:id="_jlW3QM3gEeeAvtXJQCAINA" base_StateMachine="_FgpGcM3gEeeAvtXJQCAINA"/>
   <ThreatsPropagation:InternalFault xmi:id="_wT2jIM3gEeeAvtXJQCAINA" occurrence="0.05" base_Transition="_twi44M3gEeeAvtXJQCAINA"/>
   <ThreatsPropagation:ErrorState xmi:id="_yHV6AM3gEeeAvtXJQCAINA" base_State="_qV8aQM3gEeeAvtXJQCAINA" probability="0.05"/>
   <ThreatsPropagation:StuckAt xmi:id="_yJufoM3gEeeAvtXJQCAINA" property="_POAPoMnaEeejHePP_Hzkeg" value="FALSE" base_State="_qV8aQM3gEeeAvtXJQCAINA"/>
   <CHESSContract:DelegationConstraint xmi:id="_NWlO0NZuEeeO6aCjdQZPkg" base_Constraint="__xm5cMnhEeejHePP_Hzkeg"/>
   <CHESSContract:DelegationConstraint xmi:id="_OtA2QNZuEeeO6aCjdQZPkg" base_Constraint="_qR-5sMniEeejHePP_Hzkeg"/>
   <CHESSContract:DelegationConstraint xmi:id="_P2nioNZuEeeO6aCjdQZPkg" base_Constraint="_psuJIMnlEeejHePP_Hzkeg"/>
   <CHESSViews:DependabilityAnalysisView xmi:id="_oOsCwE-yEemU0aMen8TVXg" base_Package="_dNgC8MrjEee1tdS56VBt8w"/>
   <DependableComponent:AnalysisContextElement xmi:id="_8wZcUHe_EemmJfmKAb07HA" type="CONTRACT_COMPOSITE_IMPLEMENTATION_ANALYSIS" date="Fri Jul 10 17:08:46 CEST 2020" valid="true" result="&lt;?xml version=&quot;1.0&quot; encoding=&quot;UTF-8&quot;?>&#xD;&#xA;&lt;ns:OcraOutput xmlns:xsi=&quot;http://www.w3.org/2001/XMLSchema-instance&quot; xsi:schemaLocation=&quot;OcraOutput.xsd&quot; xmlns:ns=&quot;https://es.fbk.eu/tools/ocra/xml/OcraOutput&quot;>&#xD;&#xA; &lt;OcraResult checkType=&quot;ocra_check_refinement&quot; timestamp=&quot;&quot;>&#xD;&#xA;  &lt;Component type=&quot;System&quot;>&#xD;&#xA;   &lt;Contract name=&quot;Sense&quot;>&#xD;&#xA;    &lt;CheckResult proofType=&quot;implementation&quot; contractName=&quot;Sense&quot;>&#xD;&#xA;     &lt;Value value=&quot;OK&quot;/>&#xD;&#xA;    &lt;/CheckResult>&#xD;&#xA;    &lt;CheckResult proofType=&quot;environment&quot; contractName=&quot;sensor1.Sense&quot;>&#xD;&#xA;     &lt;Value value=&quot;OK&quot;/>&#xD;&#xA;    &lt;/CheckResult>&#xD;&#xA;    &lt;CheckResult proofType=&quot;environment&quot; contractName=&quot;sensor2.Sense&quot;>&#xD;&#xA;     &lt;Value value=&quot;OK&quot;/>&#xD;&#xA;    &lt;/CheckResult>&#xD;&#xA;    &lt;CheckResult proofType=&quot;environment&quot; contractName=&quot;selector.Select&quot;>&#xD;&#xA;     &lt;Value value=&quot;OK&quot;/>&#xD;&#xA;    &lt;/CheckResult>&#xD;&#xA;    &lt;CheckResult proofType=&quot;environment&quot; contractName=&quot;selector.Switch&quot;>&#xD;&#xA;     &lt;Value value=&quot;OK&quot;/>&#xD;&#xA;    &lt;/CheckResult>&#xD;&#xA;    &lt;CheckResult proofType=&quot;environment&quot; contractName=&quot;monitor2.Monitor&quot;>&#xD;&#xA;     &lt;Value value=&quot;OK&quot;/>&#xD;&#xA;    &lt;/CheckResult>&#xD;&#xA;    &lt;CheckResult proofType=&quot;environment&quot; contractName=&quot;monitor1.Monitor&quot;>&#xD;&#xA;     &lt;Value value=&quot;OK&quot;/>&#xD;&#xA;    &lt;/CheckResult>&#xD;&#xA;   &lt;/Contract>&#xD;&#xA;  &lt;/Component>&#xD;&#xA; &lt;/OcraResult>&#xD;&#xA; &lt;OcraResult checkType=&quot;ocra_check_implementation&quot; timestamp=&quot;&quot;>&#xD;&#xA;  &lt;Component type=&quot;Selector&quot;>&#xD;&#xA;   &lt;Contract name=&quot;Switch&quot;>&#xD;&#xA;    &lt;CheckResult>     &lt;Value value=&quot;OK&quot;/>&#xD;&#xA;    &lt;/CheckResult>&#xD;&#xA;   &lt;/Contract>&#xD;&#xA;   &lt;Contract name=&quot;Select&quot;>&#xD;&#xA;    &lt;CheckResult>     &lt;Value value=&quot;OK&quot;/>&#xD;&#xA;    &lt;/CheckResult>&#xD;&#xA;   &lt;/Contract>&#xD;&#xA;  &lt;/Component>&#xD;&#xA; &lt;/OcraResult>&#xD;&#xA; &lt;OcraResult checkType=&quot;ocra_check_implementation&quot; timestamp=&quot;&quot;>&#xD;&#xA;  &lt;Component type=&quot;SpeedSensor&quot;>&#xD;&#xA;   &lt;Contract name=&quot;Sense&quot;>&#xD;&#xA;    &lt;CheckResult>     &lt;Value value=&quot;OK&quot;/>&#xD;&#xA;    &lt;/CheckResult>&#xD;&#xA;   &lt;/Contract>&#xD;&#xA;  &lt;/Component>&#xD;&#xA; &lt;/OcraResult>&#xD;&#xA; &lt;OcraResult checkType=&quot;ocra_check_implementation&quot; timestamp=&quot;&quot;>&#xD;&#xA;  &lt;Component type=&quot;MonitorPresence&quot;>&#xD;&#xA;   &lt;Contract name=&quot;Monitor&quot;>&#xD;&#xA;    &lt;CheckResult>&lt;counter-example type=&quot;0&quot; id=&quot;1&quot; desc=&quot;IC3 smt counterexample&quot; >&#xD;&#xA;&#x9;&lt;node>&#xD;&#xA;&#x9;&#x9;&lt;state id=&quot;1&quot;>&#xD;&#xA;&#x9;&#x9;&#x9;&lt;value variable=&quot;State&quot;>primary&lt;/value>&#xD;&#xA;&#x9;&#x9;&#x9;&lt;value variable=&quot;absence_alarm&quot;>FALSE&lt;/value>&#xD;&#xA;&#x9;&#x9;&#x9;&lt;value variable=&quot;input_is_present&quot;>TRUE&lt;/value>&#xD;&#xA;&#x9;&#x9;&#x9;&lt;value variable=&quot;enabled&quot;>FALSE&lt;/value>&#xD;&#xA;&#x9;&#x9;&lt;/state>&#xD;&#xA;&#x9;&lt;/node>&#xD;&#xA;&#x9;&lt;node>&#xD;&#xA;&#x9;&#x9;&lt;state id=&quot;2&quot;>&#xD;&#xA;&#x9;&#x9;&#x9;&lt;value variable=&quot;State&quot;>primary&lt;/value>&#xD;&#xA;&#x9;&#x9;&#x9;&lt;value variable=&quot;absence_alarm&quot;>FALSE&lt;/value>&#xD;&#xA;&#x9;&#x9;&#x9;&lt;value variable=&quot;input_is_present&quot;>FALSE&lt;/value>&#xD;&#xA;&#x9;&#x9;&#x9;&lt;value variable=&quot;enabled&quot;>TRUE&lt;/value>&#xD;&#xA;&#x9;&#x9;&lt;/state>&#xD;&#xA;&#x9;&lt;/node>&#xD;&#xA;&#x9;&lt;node>&#xD;&#xA;&#x9;&#x9;&lt;state id=&quot;3&quot;>&#xD;&#xA;&#x9;&#x9;&#x9;&lt;value variable=&quot;State&quot;>primary&lt;/value>&#xD;&#xA;&#x9;&#x9;&#x9;&lt;value variable=&quot;absence_alarm&quot;>TRUE&lt;/value>&#xD;&#xA;&#x9;&#x9;&#x9;&lt;value variable=&quot;input_is_present&quot;>FALSE&lt;/value>&#xD;&#xA;&#x9;&#x9;&#x9;&lt;value variable=&quot;enabled&quot;>TRUE&lt;/value>&#xD;&#xA;&#x9;&#x9;&lt;/state>&#xD;&#xA;&#x9;&lt;/node>&#xD;&#xA;&#x9;&lt;node>&#xD;&#xA;&#x9;&#x9;&lt;state id=&quot;4&quot;>&#xD;&#xA;&#x9;&#x9;&#x9;&lt;value variable=&quot;State&quot;>primary&lt;/value>&#xD;&#xA;&#x9;&#x9;&#x9;&lt;value variable=&quot;absence_alarm&quot;>TRUE&lt;/value>&#xD;&#xA;&#x9;&#x9;&#x9;&lt;value variable=&quot;input_is_present&quot;>FALSE&lt;/value>&#xD;&#xA;&#x9;&#x9;&#x9;&lt;value variable=&quot;enabled&quot;>TRUE&lt;/value>&#xD;&#xA;&#x9;&#x9;&lt;/state>&#xD;&#xA;&#x9;&lt;/node>&#xD;&#xA;&#x9;&lt;node>&#xD;&#xA;&#x9;&#x9;&lt;state id=&quot;5&quot;>&#xD;&#xA;&#x9;&#x9;&#x9;&lt;value variable=&quot;State&quot;>primary&lt;/value>&#xD;&#xA;&#x9;&#x9;&#x9;&lt;value variable=&quot;absence_alarm&quot;>TRUE&lt;/value>&#xD;&#xA;&#x9;&#x9;&#x9;&lt;value variable=&quot;input_is_present&quot;>FALSE&lt;/value>&#xD;&#xA;&#x9;&#x9;&#x9;&lt;value variable=&quot;enabled&quot;>TRUE&lt;/value>&#xD;&#xA;&#x9;&#x9;&lt;/state>&#xD;&#xA;&#x9;&lt;/node>&#xD;&#xA;&#x9;&lt;loops> 3 &lt;/loops>&#xD;&#xA;&lt;/counter-example>&#xD;&#xA;     &lt;Value value=&quot;NOT_OK&quot;/>&#xD;&#xA;    &lt;/CheckResult>&#xD;&#xA;   &lt;/Contract>&#xD;&#xA;  &lt;/Component>&#xD;&#xA; &lt;/OcraResult>&#xD;&#xA;&lt;/ns:OcraOutput>&#xD;&#xA;" root="_NzOwMMnZEeejHePP_Hzkeg" base_Component="_8v_zsHe_EemmJfmKAb07HA"/>
   <DependableComponent:AnalysisContextElement xmi:id="_oEvIwHfDEemmJfmKAb07HA" type="FTA_ANALYSIS" date="Tue Sep 08 14:05:30 CEST 2020" valid="true" result="C:\Users\Alberto\Google Drive\AMASS Project\ARTA_p1\eclipse\git_home\CHESS_FBK\plugins\contracts\org.polarsys.chess.contracts.verificationService.test.runtime\resources\SSR_fi\VerificationResults\extended_RootElement_System_FTA_ANALYSIS_c1_2020-09-08-14-05-30.xml" root="_NzOwMMnZEeejHePP_Hzkeg" base_Component="_oEn0AHfDEemmJfmKAb07HA">
     <conditions>property::sensor1.sensed_speed_is_present=TRUE</conditions>
   </DependableComponent:AnalysisContextElement>
   <DependableComponent:AnalysisContextElement xmi:id="_dxkLoHfKEemiWaxj_3Hy5w" type="FTA_ANALYSIS" date="Thu May 16 13:05:07 CEST 2019" valid="true" result="C:\Users\Alberto\git\CHESS_SystemArchitectureProjects_last\SSR_fi\VerificationResults\extended_RootElement_System_FTA_ANALYSIS_c1_2019-05-16-13-05-07.xml" root="_NzOwMMnZEeejHePP_Hzkeg" base_Component="_dw9usHfKEemiWaxj_3Hy5w">
     <conditions>property::sensor1.sensed_speed_is_present=FALSE</conditions>
   </DependableComponent:AnalysisContextElement>
   <DataTypes:BoundedSubtype xmi:id="_s4Ip0ILyEeqxuOOz6y6Ozw" minValue="1" maxValue="2" base_DataType="_GyjP8MrPEee1tdS56VBt8w"/>
   <DependableComponent:AnalysisContextElement xmi:id="_KrRbcMK6Eeqrbc3PZZCA9Q" type="CONTRACT_BASED_FTA_ANALYSIS" date="Fri Jul 10 16:35:13 CEST 2020" valid="true" result="C:\Users\Alberto\Google Drive\AMASS Project\ARTA_p1\eclipse\git_home\CHESS_FBK\plugins\contracts\org.polarsys.chess.contracts.verificationService.test.runtime\resources\SSR_fi\VerificationResults\RootElement_modelSystemView_PhisicalArchitecture_System_CONTRACT_BASED_FTA_ANALYSIS_2020-07-10-16-35-09.xml" root="_NzOwMMnZEeejHePP_Hzkeg" base_Component="_KrA8wMK6Eeqrbc3PZZCA9Q"/>
 </xmi:XMI>