Modeling, verifying and generating embedded software with Dezyne

Tweet about this on TwitterShare on FacebookBuffer this pageShare on RedditShare on LinkedInShare on Google+Email this to someone

Dezyne is a model-driven software engineering tool that enables software engineers to design, validate, verify and generate software components, mainly targetting embedded/industrial systems.

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, learnt 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.

The current major release (v.2) came out last year 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 is free for non-commercial use. However, note that under this free license agreement any models you build or code you generate is treated as Open Source and Verum reserves the right to freely publish them. You can request a free evaluation for commercial use where you get to use the tool for free for a limited period of time and the models you create during the evaluation are NOT disclosed.

Installing Dezyne

After registering on their website you’ll get a link to download Dezyne. By default, Dezyne is packaged as an Eclipse RCP so its interface will look immediately familiar to many of you. Nevertheless, it can also be installed as a separate plugin or just be used from the command line.

In fact, Dezyne is mostly cloud-based software, meaning that everything you do (like visualizing the diagrams, simulating/generating the code,…) is done on Verum’s servers so it should be possible to integrate Dezyne also in other environments. Maybe they could even implement at some point a LSP (Language server protocol)-based version to open even more the client-side part of the tool

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.

Bonus! Win a Drone

If you need an extra push to start using Dezyne, take a look at the Dezyne Challenge 2017 . All you need to do is come up with a great example of the use of Dezyne. Focus on concurrency issues and/or IoT for extra points. You could win a DJI Spark Drone!

Tweet about this on TwitterShare on FacebookBuffer this pageShare on RedditShare on LinkedInShare on Google+Email this to someone


Your email address will not be published. Required fields are marked *