We’re here to help you

Menu

The Alarm System

Requirements

Our next alarm system has a pincode keypad, a multi-color LED, a siren, and sensors. The keypad silently discards invalid pincodes. The system has two basic sequences of events: On power up the system is unarmed, the LED is green, and sensors are disabled.

  1. Green: unarmed.

  2. Yellow: Valid pincode entry arms the system, turns the LED yellow and enables sensors.

  3. Red: A sensor trigger disables the sensors and turns the LED red.

  4. Either Yellow: Valid pincode entry soon enough cancels the timer and returns the system to the armed state with yellow LED and enabled sensors.

  5. Or Red with siren: Timer timeout turns on the siren.

  6. Yellow: Valid pincode entry turns off the siren and returns to armed state.

Alternate sequence with no sensor trigger event:

  1. Green: Unarmed

  2. Yellow: Valid pincode entry arms the system, turns the LED yellow, and enables sensors.

  3. Green: Valid pincode entry disarms the system, turns the LED green, and disables sensors.

One might white-board the initial conceptual system like this:

image

After power-up, a valid pincode event can arrive any time at the Controller, whether appropriate or not. Once the Controller enables the sensors, they can trigger events at any moment but possibly never. The LED is configured to be a solid-color green on power-up, yellow when armed, and red whenever there is a sensor-generated alarm active. The Controller starts the timer when a sensor triggers and starts the siren upon timeout. A user must enter a valid pincode to exit the alarm state and to silence the siren if it has begun sounding.

The Controller

Usually we start designing by sketching interfaces, since we can always reasonably assume that a “hand-written” component will correctly implement any given interface. The below interface captures the two main kinds of incoming events for the controller: user-entered pincodes, and sensor trigger events. Timer timeout events are different since the controller has to initiate them.

interface IController {
  in void validPincode();
  in void sensorTriggered();

  behaviour {
    on validPincode: {}
    on sensorTriggered: {}
  }
}

The above minimal interface declares implicitly that any and every incoming event is “legal”, i.e. the caller does not have to track the controller’s state and avoid inappropriate calls. Said another way, the implemented interface will not hit an assertion via an illegal event. A minimal Controller component would start up Unarmed; go from there to Armed upon a valid pincode; go from Armed to Alarming upon getting a sensorTriggered event; return to Armed state upon valid pincode; and return to Unarmed after another valid pincode.

Exercise: Build the minimal controller yourself before reading the below code.

component Controller {
  provides IController iController;

  behaviour {
    enum State { Unarmed, Armed, Alarming };
    State state = State.Unarmed;

    [state.Unarmed] {
      on iController.validPincode(): state = State.Armed;
      on iController.sensorTriggered(): {}
    }
    [state.Armed] {
      on iController.validPincode(): state = State.Unarmed;
      on iController.sensorTriggered(): state = State.Alarming;
    }
    [state.Alarming] {
      on iController.validPincode(): state = State.Armed;
      on iController.sensorTriggered(): {}
    }
  }
}

The above honors its interface contract by always silently accepting and ignoring a sensorTriggered event when it is not in the Armed state.

Adding the LED

Next we add simple control for an LED.

interface ILED {
  // assumes green automatically on power-up
  in void setGreen();
  in void setYellow();
  in void setRed();

  behaviour {
    on setGreen, setYellow, setRed: {}
  }
}
component LED {provides ILED iLed;}

Exercise: Integrate the LED.

Note that the below integrated code imports the LED interface as opposed to declaring it.

import LED.dzn;

interface IController {
  in void validPincode();
  in void sensorTriggered();

  behaviour {
    on validPincode: {}
    on sensorTriggered: {}
 }
}

component Controller {
  provides IController iController;
  requires ILED iLed;

  behaviour {
    enum State { Unarmed, Armed, Alarming };
    State state = State.Unarmed;

    [state.Unarmed] {
      on iController.validPincode(): {
        state = State.Armed;
        iLed.setYellow();
      }
      on iController.sensorTriggered(): {}
    }
    [state.Armed] {
      on iController.validPincode(): {
        state = State.Unarmed;
        iLed.setGreen();
      }
      on iController.sensorTriggered(): {
        state = State.Alarming;
        iLed.setRed();
      }
    }
    [state.Alarming] {
      on iController.validPincode(): {
        state = State.Armed;
        iLed.setYelow();
      }
      on iController.sensorTriggered(): {}
    }
  }
}

Adding the Sensors

Now we add sensors, removing the sensorTriggered event from the Controller and importing the sensor we constructed earlier.

import LED.dzn;
import Sensor.dzn;
interface IController {
  in void validPincode();

  behaviour { on validPincode: {} }
}

component Controller {
 provides IController iController;
 requires ILED iLed;
 requires ISensor iSensor;

 behaviour {
  enum State { Unarmed, Armed, Alarming };
  State state = State.Unarmed;

  [state.Unarmed] {
    on iController.validPincode(): {
      ISensor.turnOn();
      state = State.Armed;
      iLed.setYellow();
    }
    on iSensor.triggered(): {}
  }
  [state.Armed] {
    on iController.validPincode(): {
      iSensor.turnOff();
      state = State.Unarmed;
      iLed.setGreen();
    }
    on iSensor.triggered(): {
      iSensor.turnOff();
      state = State.Alarming;
      iLed.setRed();
    }
  }
  [state.Alarming] {
    on iController.validPincode(): {
       iSensor.turnOn();
       state = State.Armed;
       iLed.setYelow();
    }
    on iSensor.triggered(): illegal;
  }
 }
}

Adding the Siren and Timer

Next we add a siren to be sounded only when a user takes too long to enter the pincode after a sensor trigger makes the LED go red. The siren interface and component are simple:

interface ISiren {
  in void turnOn();
  in void turnOff();

  behaviour {
    on turnOn, turnOff: {}
  }
}
component Siren { provides ISiren iSiren;}

We’ll put the siren in its own file Siren.dzn and include that file in the Controller. In the next step we turn on the siren whenever Alarming, and turn it off whenever returning to the Armed state.

import LED.dzn;
import Sensor.dzn;
import Siren.dzn;

interface IController {
  in void validPincode();

  behaviour { on validPincode: {} }
}

component Controller {
  provides IController iController;
  requires ILED iLed;
  requires ISensor iSensor;
  requires ISiren iSiren;

  behaviour {
    enum State { Unarmed, Armed, Alarming };
    State state = State.Unarmed;

    [state.Unarmed] {
      on iController.validPincode(): {
        ISensor.turnOn();
        state = State.Armed;
        iLed.setYellow();
      }
      on iSensor.triggered(): {}
    }
    [state.Armed] {
      on iController.validPincode(): {
        iSensor.turnOff();
        state = State.Unarmed;
        iLed.setGreen();
      }
      on iSensor.triggered(): {
        iSensor.turnOff();
        state = State.Alarming;
        iLed.setRed();
        iSiren.turnOn();
      }
    }
    [state.Alarming] {
       on iController.validPincode(): {
         iSensor.turnOn();
         state = State.Armed;
         iLed.setYelow();
         iSiren.turnOff();
       }
       on iSensor.triggered(): illegal;
    }
  }
}

Exercise: Modify the above model to turn on the siren only on a 30-second timeout after the system has been triggered into the Alarming state.

You will need to import the Timer component we created earlier and configure it correctly. The fragment of model code below shows only the key changes needed to the Controller event handling; if you copy and paste this partial solution into Dezyne you will still have to debug and finish it.

on iSensor.triggered(): {
  iSensor.turnOff();
  state = State.Alarming;
  iLed.setRed();
  iTimer.start($30000$);
  }
  on iTimer.timeout(); illegal;
}
[state.Alarming] {
  on iTimer.setRed(): {
    iSiren.turnOn();
  }
  on iController.validPincode(): {
    iTimer.cancel();
    iSensor.turnOn();
    state = State.Armed;
    iLed.setYelow();
    iSiren.turnOff();
  }

The Completed Alarm System

Below is the Dezyne-generated sequence diagram, and event trace listing, from simulating a complete round-trip exercise of the Controller component. Events included sounding the siren when the user did not enter a valid pincode soon enough after an alarm was triggered, and returning at the end to the disarmed state. (Screen shots were edited for better readability.)

image

We finish the alarm system by creating a top-level system component that shows how the other components interconnect through interfaces. This system component presents the iController interface to the yet larger software system into which it might be integrated. For this tutorial, the system component’s purpose is only to auto-generate the diagram shown below the code.

component AlarmSystem {
  provides IController iController;
  system {
    Controller controller;
    LED led;
    Sensor sensor;
    Siren siren;
    Timer timer;

    iController<=>controller.iController;
    controller.iLed<=>led.iLed;
    controller.iSensor<=>sensor.iSensor;
    controller.iSiren<=>siren.iSiren;
    controller.iTimer<=>timer.iTimer;
  }
}

image

Refactoring and Extending Dezyne Models

Dezyne models capture fundamental logical behaviour in perhaps a quarter of the lines it takes to write the same logic in compilable and usable C++. The five Dezyne models in the alarm system all have tens of lines of code each. Because Dezyne model representations are compact, easily edited and complete/compliant, that make refactoring and extending as easy as it could possibly be. Further, because Dezyne quickly verifies any change or addition to an existing model, the pace of refactoring and extending is as fast as it could possibly be.

Comparing using Dezyne to developing “by hand”

Think about having to develop this system “in the other direction”. You’d likely start with sketched sequence diagrams, which are tedious and difficult to draw manually and modify. From there you would specify and write the C++ source code, and built and test it. Along the way you would almost certainly rebuild the sequence diagram by hand more than once.

Eventually a test/verification person would have to manually generate event sequences to exercise paths through the system. That person could take week or months to do what Dezyne did in a few seconds; trace out every possible execution path through the system and ensure there are no race conditions, deadlocks, non-deterministic overlaps among guards, or other problems.

In fact, for anything but the smallest system, your test/verification staff will probably NEVER accomplish what Dezyne had done in seconds or minutes, which is attain 100% path coverage for the heart of the system, its core states-and-communications logic. This is the power of Dezyne.

If you have questions that weren’t answered by this Guide,
let our support team help you out.

Enjoy this article? Don't forget to share.