The tutorial guides you step-by-small-step, with explanations, through building and verifying a model of a single-threaded burglar-alarm system, in the Dezyne-IDE. The model is built with hierarchical components that communicate through events. You should already understand these concepts, and you need to be able to run the Dezyne-IDE see the Dezyne IDE Manual.
Tutorial goals in decreasing order of priority are 1) efficiency of learning, 2) rigor, and 3) completeness. You should go through the tutorial from beginning to end: later sections depend on earlier ones.
We will build the system from the bottom up, first as the simplest possible useful system, ultimately as a realistic system with complex behaviours. Along the way, we will always ensure our work-in-progress components and subsystems have no inherent logical errors in their states and communications.
Also along the way, we will automatically generate C++ source code that implements the verified logic, and at the end we’ll automatically generate audit-ready state tables, state charts, sequence diagrams and architectural system diagrams. Then we’ll look back and consider the obstacles that could arise when we need to extend or refactor the system – not many, it turns out.
|• Dezyne Hello World Turning an LED On and Off|
|• Simplest Usable Dezyne System Model|
|• Defining and Managing Component States|
|• Time and Timers Making an LED Blink|
|• Possible Events Multiplexing Sensor Inputs|
|• The Alarm System|