{title}Open/Close and Theft Flashing{/title}
{author}jp{/author}
{default}crash_flashing.html{/default}
{text}

<h2 style="font-size:140%">Open/Close and Theft Flashing</h2> 

<p>
  This test generation creates a user-defined test illustrating the <b>Open/Close and Theft Flashing</b> 
  as modeled by interacting state machines  
  
  <ul>
  <li>SystemUnderTest.OpenCloseFlashing.LockUnlockCmdGeneration
  <li>SystemUnderTest.OpenCloseFlashing.OpenCloseFlashCmdGeneration
  <li>SystemUnderTest.TheftFlashing.TheftFlashing
  </ul>
   
	 in the 
  <a href="http://www.informatik.uni-bremen.de/agbs/testingbenchmarks/turn_indicator/model_html.1.3/index.html">
turn indicator model</a>: the theft alarm sensor input (in_TheftAlarm) is only acknowledged if 
the doors are closed. Therefore the first test goal is to reach such a state where alarms from the sensor are
handled. Instead of elaborating the detailed input sequence required for this, we specify the goal
<p>
<code>
  TC-turn_indication-THEFT_ALARM-0001;
[ IMR.SystemUnderTest.TheftFlashing.TheftFlashing.THEFT_ALARM_ACTIVE.ALARM_OFF && ! IMR.in_TheftAlarm ]
Until
[ _timeTick >= 2000 && IMR.in_TheftAlarm ]
;
</code>
</p>
which expresses the test objective
<ol>
<li> <em>Find a model state where the alarm function is enabled, but no alarm has been triggered yet.</em>
(This state is characterized by basic control state  
SystemUnderTest.TheftFlashing.TheftFlashing.THEFT_ALARM_ACTIVE.ALARM_OFF and the fact that the alarm sensor
in_TheftAlarm is still passive)

<li> <em>Stay in model states satisfying this condition until 2000ms have passed since start of test 
and the alarm sensor is switched on.
</em>
</ol>

Recall that all test cases defined in LTL carry  an implicit FINALLY operator, so 
(f Until g) stands for Finally (f Until g).

By stimulating the system under test (SUT) with inputs leading to a computation finally 
fulfilling this test objective, first the close-flashing reaction (3 left and right flashing periods with
340ms ON and 320ms OFF duration), and then 
the theft alarm reaction  (left and right flashing with a 
230ms ON and 430ms OFF period) is triggered at the SUT. 

<p>
Our next objective is to switch off theft flashing by opening the door using the remote key control.
This is achieved by symbolic test case
<p>
<code>
 TC-turn_indication-THEFT_ALARM-0002;
[ IMR.SystemUnderTest.TheftFlashing.TheftFlashing.THEFT_ALARM_ACTIVE.ALARM_ON && IMR.in_TheftAlarm ]
Until
[ _timeTick >= 4000 && IMR.in_TheftAlarm && IMR.SystemUnderTest.oc_CentralLockingStatus == 1 ]
;
</code>
</p>
which requires the solver to find inputs resulting in a system state 
where
<ul>
<li> the theft alarm remains active until 4000ms since start of test have passed and the internal
model variable   oc_CentralLockingStatus has value 1 which denotes <em>"doors are unlocked"</em>
</ul>
The associated inputs calculated by the SMT solver trigger the following reactions from the SUT:
<ol>
<li> Alarm flashing is interrupted by a single doors-open flash period (340ms ON duration)
<li> After the doors-open flash period all indications are switched off - alarm flashing has been terminated,
regardless the current state of the in_TheftAlarm sensor.


</ol>