Dezyne is a model-driven software engineering language and accompanying set of tools that enable software engineers to design, validate, verify and generate software components, mainly targeting embedded/industrial systems. Dezyne aims to eliminate the need for testing by applying formal verification methods.

Sure, there are plenty of tools with a similar goal but Dezyne strikes a great balance between the expressiveness of its domain-specific language and the features they can offer on top of it. More powerful languages limit a lot what you can automatically do with them, especially when it comes to automatic verification. Simpler languages are much easier to deal with but may not cover the real scenarios your clients need to model. This balance is something that Verum, the company behind Dezyne, learned with their first product (ASD:Suite). In this sense, Dezyne is a second generation product built from the very start as a co-creation development with customers, with emphasis on usability and ease of adoption.

Dezyne current major version (version 2) comes with the promise of:

Dezyne is the easiest way to build verifiable correct embedded software … Model-driven software engineering with Dezyne is 3 – 5 times more efficient than coding

I asked about these metrics and confirmed they were based on real data taken from some of their customers (e.g. see this case study).

After trying it out, I can say that, for sure, Dezyne is a quick and practical way to generate correct software following a component-based approach.

Dezyne was free for non-commercial use. But recently, we got even better news on this front: The Dezyne language is now been released as free software. Dezyne FOSS is the core implementation of the Dezyne language. Verum will continue to sponsor development of Dezyne, as well as offer the commercial Dezyne-IDE integration.

 “We are sharing the Dezyne language, convinced that it will benefit many users. Not just in creating trustworthy systems affordably but also to enable the future inception of currently unimaginable applications. We believe that by releasing the Dezyne language implementation as free software is not just a commitment to its longevity, it will allow the underlying ideas to thrive and continue to mature.” – Rutger van Beusekom, Verum’s CTO

Installing Dezyne

You can directly download the Dezyne IDE.  LSP is used to to interface with commonly used IDE’s such as VS Code and Emacs so more integrations with other well-known IDEs are feasible. Previous versions were shipped as an Eclipse RCP so I guess Eclipse support is still there.

Once the installation is completed we are ready to model, verify and generate embedded software with Dezyne. To get started, I strongly recommend you to follow the tutorials. They are really well done and you’ll be up modeling and generating code in no time!

If you don’t have time to browse the tutorials, the following screenshot of Dezyne’s User Interface will allow me to give you a 1-minute overview of the tool. On the left, you’ll find the usual project explorer and tree-based view of the opened model. The central part allows you to specify the components and interfaces of your model with Dezyne’s textual DSL. From these textual definitions, a number of graphical views are immediately rendered (a system view focusing on the interactions between components, a statechart view and a couple of table-based view summarizing the states and the events). On the bottom, Dezyne displays the results of verifying the model. As we’ll see below, you can also perform a step-by-step simulation of the model and generate code from it. Let’s look at each of these three core functionalities in more detail.

Dezyne’s User Interface (click to enlarge)

Modeling embedded systems with Dezyne

Dezyne is a textual DSL. Its syntax reminds me of some other textual UML languages, but it comes with precise semantics underpinned on the mCRL2 formal specification language (this post explains the encoding of Dezyne models as mCRL2 specifications).

The full details of the Dezyne syntax are explained here, but I’m confident you can get the core details of the example model from the screenshot above. We define a “system” component that connects two components: a switch and a LED. Both components are connected via the ILedJordi interface exposing two turnon/turnoff methods. The LED component “implements” this interface, while the switch one uses it. This is how both components are connected. The LED component is defined in another model, imported in this one.

import LEDComponent.dzn;
 
component LEDSwitchSystem {
  system {
    LED led;
    Switch switch;
    switch.iLed <=> led.iLed;
   // LEDSwitchSystem system2;
  }
}
 
 
component Switch {	
  requires ILEDJordi iLed; 
}	
 
interface ILEDJordi {
  in void turnOn();
  in void turnOff();
 
  behaviour {
    on turnOn: {}
    on turnOff: {}
  }
}

The language is obviously richer than what you see here. For instance, you can attach preconditions to the events or mark some states as illegal. Do not forget to check the language reference for the full possibilities of Dezyne’s DLS!

Verifying and validating embedded software models with Dezyne

Needless to say: writing software is a challenging task. We want to make sure our software is right (Verification) and that we are building the right software (Validation).

On the verification side, Dezyne checks syntactic errors and well-formedness rules directly in the editor, highlighting problematic definitions on the spot, but it also offers a verification functionality able to detect more complex errors. For instance, if I uncomment the LEDSwitchSystem system2; line in the previous example, Dezyne will alert me of the recursive definition.

Model checking error reported by Dezyne

To validate the model, Dezyne offers a step-by-step simulation of your model. You can choose what event you would like to trigger and see how the components react to it. The tool is smart enough to show only the possible events at any time, depending on the current state of the system. For instance, the next screenshot shows a possible execution scenario for the Camera example (one of the many complete Dezyne sample projects provided to help you in your learning process).

Simulating a Dezyne model

This sequence view is also used to explain more complex errors detected during the verification phase. In short, you can regard verification as simulation to the max: all possible paths are tried out (in a clever way) such that all possible execution scenarios are examined in order to verify that the component is free from any runtime behavioural issues: deadlocks, race conditions, component adheres to all contracts (behaviour) of the interfaces of all ports, etc.

Let’s see it on a more complex example of an alarm system (also included in the tool as part of the downloadable examples). Dezyne detects that the Alarm system is illegal and can explain you why: the alarm is turned on a second time without being turned off first.

Code-generation of embedded software from component-based models

The more useful is a model the more likely is that designers will take the time to completely specify and verify that model. Modeling without code-generation feels like a missing opportunity!. That’s why Dezyne comes with code-generators for a variety of languages (depending on the version you’re in not all of them may be available at the time, check the release notes).

Translations try to be as straightforward as possible to facilitate the readability of the code, especially at the individual component level. A Denzyne runtime engine takes care of gluing the complete system. And while Dezyne does not offer round-trip engineering (in fact, Verum promises that you never have to edit the generated code so round-trip engineering is not needed), it does support the integration with external components (i.e. hardware-oriented ones) as part of the code generation and compilation process.

Do you want more?

I hope by now I’ve convinced you to give Dezyne a try . It’s definitely a great tool but I always need more so here we go with a few additional suggestions I’d love to see coming through in the future:

• Create a public repository with the models created with the free version. I think many of us would like to take a look and gather some stats on the kinds of models people try to write
• Provide some import/export functionality that helps potential customers try Dezyne reusing preexisting UML models.
• Probably many projects need to model again and again a set of typical components (LEDs, switches, …). It would be great to have some modeling libraries we could import in our projects to get for free a predefined set of useful components.
• Provide an overall view of the project, showing all components (even those not directly depending on each other).
• Consider opening some kind of “Dezyne marketplace” where other people can provide (and maybe sell?) their own extensions to Dezyne (e.g. new generators or the modeling libraries mentioned above).

Feel free to provide your own suggestions. From the exchanges I’ve had so far with Verum, I can tell you they are really open to react to your feedback.

Jordi Cabot

FNR Pearl Chair. Head of the Software Engineering RDI Unit at LIST. Affiliate Professor at University of Luxembourg.  More about me.