Running Example

Violation Details of the Motivating Example

This case study corresponds to the motivating example presented in Section 2.3 of the paper, showcasing HAFuzz's input requirements and a counterexample trace generated through fuzzing. The visualized outputs below utilize two distinct annotation schemes:
1. Red markers denote critical system states associated with the LTL violation.
2. Orange markers identify transitions triggered by IFTTT rule interactions.
At timestamp 8, the air conditioner was turned off, and the window was opened. However, at timestamp 9, the air conditioner was activated again (heating mode), and the window remained open at timestamp 10. This sequence violates the LTL specification.

It can be observed that we conducted a high-precision simulation, where the temperature change between the two states can take any double value in the range of [-2, 2]. This is one of the reasons why it is challenging to trigger violation scenarios under this specification.

Input:

IFTTT Rules:

1) IF Temperature Sensor.temperature < 20.5 THEN Air Conditioner.heat & Window.close

2) IF Temperature Sensor.temperature > 20.5 THEN Window.open

3) IF Clock.time > 9 & Motion Detector.motion = inactive THEN Window.close

4) IF Air Quality Monitor.carbonDioxide > 15 & Motion Detector.motion = active THEN Window.close & Air Purifier.on

LTL Spec:

G ! ( Clock.time < 8
&& X ( Window.WindowState = open && Air Conditioner.HvacMode = off )
&& XX Air Conditioner.HvacMode = heat
&& XXX ( Window.WindowState = open U Clock.time = 11 ) )

Device Json:

{"Name": "Temperature Sensor","InternalVariables": [{"Name": "temperature","LowerBound": 0,"UpperBound": 100,"NaturalChangeRate": "[-2, 2]"}],}

{"Name": "Clock", .... }

....

HAFuzz will output a counterexample trace:

StateNode 0 Device Air Conditioner WorkingState: off Window WorkingState: closed Air Purifier WorkingState: on Dynamics carbonDioxide VariableVal: 9.050062853674333 ChangeRate: 0 motion VariableVal: inactive temperature VariableVal: 21.711909410269104 ChangeRate: 0 time VariableVal: 6 ChangeRate: 1

StateNode 1 Device Air Conditioner WorkingState: off Window WorkingState: open Air Purifier WorkingState: on Dynamics carbonDioxide VariableVal: 9.050062853674333 ChangeRate: -0.3463560258914127 motion VariableVal: active temperature VariableVal: 21.711909410269104 ChangeRate: -1.4034988498435275 time VariableVal: 7 ChangeRate: 1

StateNode 2 Device Air Conditioner WorkingState: off Window WorkingState: open Air Purifier WorkingState: on Dynamics carbonDioxide VariableVal: 8.70370682778292 ChangeRate: 0.009673042695883982 motion VariableVal: active temperature VariableVal: 20.30841056042558 ChangeRate: 1.2464190539940487 time VariableVal: 8 ChangeRate: 1

StateNode 3Device Air Conditioner WorkingState: heat Window WorkingState: closed Air Purifier1 WorkingState: on Dynamics carbonDioxide VariableVal: 8.713379870478803 ChangeRate: 0.6641892560345373 motion VariableVal: inactive temperature VariableVal: 21.554829614419628 ChangeRate: 1.194259665528031 time VariableVal: 9 ChangeRate: 1

StateNode 4 Device Air Conditioner WorkingState: heat Window WorkingState: open Air Purifier WorkingState: on Dynamics carbonDioxide VariableVal: 9.377569126513341 ChangeRate: 0.34195911404532 motion VariableVal: inactive temperature VariableVal: 22.749089279947658 ChangeRate: 0.30341484386190265 time VariableVal: 10 ChangeRate: 1

StateNode 5 Device Air Conditioner WorkingState: heat Window WorkingState: closed Air Purifier WorkingState: on Dynamics carbonDioxide VariableVal: 9.719528240558661 ChangeRate: 0.7099356812202182 motion VariableVal: inactive temperature VariableVal: 23.05250412380956 ChangeRate: 0.0 time VariableVal: 11 ChangeRate: 1

Note 1: Distinct IFTTT rules may have varying impacts on the same device (e.g., the state of the window). HAFuzz sequentially evaluates these rules according to the input order to determine the device's final state at the next timestamp.
Note 2: Motion is an environmental variable.