This tutorial assumes that you have developed control software in C, C++, C# and/or Java. Most likely you have worked hands-on with finite state machines in some form or other, maybe with Harel state machines or UML statecharts. You’ve seen that deeply nested if-then-else control logic leads to debugging nightmares – every fix seems to break something else. You’ve experienced unhandled events, race conditions, deadlocks and live-locks, some of which are not reproducible. You know about state machine determinism and non-overlapping guards.
The tutorial also assumes that you already generally understand the benefits Dezyne brings to developing control software – see the next paragraph – and that you now want to create something realistic with it, gaining fluency with its domain-specific language and its techniques.
Benefits summary: Dezyne enables you to methodically and efficiently divide complex control problems into verified problem-free components and interfaces that you re-compose into reliable, trustworthy systems. Verified Dezyne models have no unhandled events, problematic race conditions, deadlocks or live-locks in their core state-management and communications “skeleton” logic. Source code that Dezyne auto-generates from models will be free of these same problems. For more information about Dezyne’s benefits, see the materials on the Verum’s Dezyne website or contact Verum.
Dezyne runs on all common platforms as an Eclipse™ or Visual Studio™ plug-in, or via command line. Models are expressed in a simple, immediately familiar C/Java-like language.
The tutorial guides you step-by-small-step, with explanations, through building and verifying a model of a single-threaded burglar-alarm system, in Eclipse. 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 Eclipse or Visual Studio user interface; for information about the Eclipse plug-in user interface see the online help.
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.