This Dezyne example is submitted by Floris Rouwen. The example is part of the Lunar Zebro project, which, as well as the ZEs-Benige RObot (Zebro), is a TU Delft project [1].

These projects are supported by different companies throughout the Netherlands. This specific part of the Lunar Zebro project was greatly supported by Verum [2].

The current workhorse of the ZEs-Benige RObot (Zebro) Project, is a Zebro called DeciZebro [3]. It is roughly the size of an A4 sheet of paper. The TU Delft has started this project as it is determined to bring the Zebro concept to the surface of our moon. Lunar Zebro builds on the legacy of DeciZebro.

To maximise the probability of a mission success, this project uses Dezyne to develop the Locomotion Sub-System (LSS) software of Lunar Zebro. The LSS software is designed, verified, simulated and integrated into native code, all with the help of Dezyne.


The Moon is a very harsh environment to be in. There are many mechanical challenges regarding temperature, vacuum and Lunar Regolith. But software also faces many challenges. This is due to different kinds of radiation that are present in space. Our Earth has a magnetic shield that protects us from most of this radiation, but the Moon does not.

The effects of radiation are seen in software in roughly two ways. First there are Single Event Effects (SEE). These are, for example, noticeable as bitflips [4] or false readings from sensors. Next to SEE there are Total Ionising Dose (TID) effects. These effects are degradation or even complete destruction of components. Degradation of components can influence sensor measurements over time.

In short, a lot of unpredictable behaviour will occur in the system, while we expect the system to function predictable. Dezyne adds to this predictability as all events that trigger state machine changes are checked. Additionally, the system will never end up in an undefined state as Dezyne does not allow this.


The Locomotion Sub-System (LSS) of Lunar Zebro consists of a Locomotion Controller (LC) and six leg modules. The leg modules consist of a Brushless Direct Current (BLDC) motor and smart motor driver. This motor driver controls the motion of each motor and monitors current consumption and temperature. The motor drivers are developed by hand. The LC is developed with Dezyne. The result is shown below.



The LocomotionController_t component accepts commands from a high-level controller on its provides port (OBC Interface) and communicates with six leg modules on six of its requires ports (Motor Driver Interface). Additionally, the LC talks to six handwritten components. The four timers are similar to the timer example provided by Verum. The Locomotion Algorithm is based on the work done in the Zebro Project using Max-Plus Algebra by [5]. The handwritten component functions as a framework in which this research can be implemented. Next, the Data Manager stores data retrieved from all motor drivers. Currently, it does not log data over time. Lastly, the StatusArmour_t and Status_t blocks are currently unused.


The high-level controller is the On-Board Computer (OBC) of the system. The LC offers the following functionality on its provides interface:

  1. Receive Messages from the OBC (asynchronous)

    • Start Motor Control

    • Stop Motor Control

    • Stand Up

    • Lay Down

    • Walk (direction, heading, speed)

    • Request data (data requested / heartbeat)

    • Emergency Stop

  2. Send Messages to the OBC (synchronous)

    • Reply requested data (requested data / heartbeat)

This functionality on the provides interface results in the following events on the six motor driver interfaces that are requires interfaces:

  1. Receive Messages from the LC (asynchronous)

    • Start Motor Control

    • Stop Motor Control

    • Rotate Motor Forward (position, delta time)

    • Rotate Motor Backward (position, delta time)

    • Request data (data requested / heartbeat)

    • Emergency Stop

  2. Send Messages to the LC (synchronous)

    • Reply requested data (requested data / heartbeat)

The other interfaces and components can be found in the attached documentation.



The LSS software provides functionality that is best described by looking at the OBC interface. Essentially, it makes Lunar Zebro walk and talk. But inside the LC, a little bit more is going on.

First, there is a system of ‘heartbeats’ between all devices. Timers are reset when communication happened or should happen. This way, the LC knows which devices are operational at all times. Currently, when any device becomes unresponsive, the system enters a fatal error state. An example of this is shown in Figure 1, where the LC detects the OBC becoming unresponsive. It is assumed that blocks within Dezyne can not become unresponsive as long as they are not handwritten. Additionally, it is assumed that communication over Dezyne interfaces always arrives at components. Therefore, all interfaces that do not leave the system may be synchronous and do not require a heartbeat. However, one can question these assumptions when realising that a bitflip might cause a Dezyne block to malfunction. For now, we assume a watchdog timer will catch this and reset the device.

Figure 1: Simulation Trace showing starting the motors and receiving a timeout from the OBC timer. The result is an emergency stop of the system.


Secondly, the locomotion algorithm must be able to drive the motors. This is shown in Figure 2. The Locomotion Algorithm works in a feed forward way at the moment. Provisions have been built in to allow a feedback loop to be closed. In Figure 2, the Locomotion Algorithm is started and generates a command to rotate motor 1.

Lastly, the data manager stores all variables of all devices. The Dezyne functions pass around strings to indicate which data from which device is requested. The handwritten functions translate these strings to actual references. The strings were the best option to allow all data being grouped in classes and reference these.

Figure 2: Simulation Trace showing the Locomotion Algorithm generating commands for the motor drivers.


Project Results

Except for the components concerning the status of the LC, the entire system is operational. Additionally, the locomotion algorithm is integrated and allows Lunar Zebro to walk and make smooth turns, which is an accomplishment for the Zebro Project.

There is still a lot of work to be done to improve on this initial design, but the core of the systems seems to be good. The first To-Do on the list is to add logging functionality to the Data Manager. This also includes retrieving the information that should be logged from the different devices. To do this, the status components will be used.

Another high priority task is error solving. The LC must be able to solve many different error scenarios like different numbers of legs failing. However, error solving must be done within a general framework. Only defining error solving strategies for specific errors will be too error-prone. We are trying to solve errors we didn’t know would occur!


Lessons learned

By far the most time-consuming part of the development with Dezyne is Code integration. This step has a very steep learning curve, especially when one has no prior knowledge of C++. So be prepared to invest some time.The integration process could be documented better by Verum and more examples would help. Unfortunately, this project cannot provide an example as the project is still ongoing and handwritten code may not be disclosed.

It was found that Dezyne is not suitable for designing the software of the leg modules. The leg modules are meant to contain little state machining and make use of interrupts that can trigger events without the CPU knowing. Dezyne is much more suitable for devices that contain more state machining and are meant to work on a Run-To-Completion basis. That is why the LC, for which this is the case, was a very suitable component to develop using Dezyne.

Remarkably, the handwritten code for the motor drivers improved a lot because of the use of Dezyne for the development of the LC. The clear interface definition between the motor drivers and LC simplified the design of the motor driver. Thus, regardless of whether Dezyne is used to verify the model and generate code, it is a proper design tool that really aids in the design phase.

Tips and guidelines for others

First and foremost: Dezyne is not perfect yet, but that should not stop you from trying it. And especially with the great support that Verum delivers, you can come a long way. Don’t hesitate to contact them with your questions at!

RTFM! Although documentation may not always be complete or easy to find, there is a lot available. And when you think you have the concepts of async, blocking, thread-safe-shell, extern, external etc. under control, maybe think again. It is vital to understand what you are doing. Some keywords concern the model checking part of Dezyne, while other are more related to code generation. When in doubt, ask!

Please consider using armour components when dealing with asynchronous communication. All armour in this project is located inside the LocomotionController_t component, while this could have been moved to separate blocks on the different communication lines. This prevents spaghetti-code. The StatusArmour is a start in that direction.


Because the project is still ongoing and handwritten code may not be disclosed, only the .dzn files are included in a .zip file here.


1. Lunar Zebro - The Mission. [Online]. Available: [Accessed 11 February 2019].
2. Verum Software Tools BV, 2018. [Online]. Available: [Accessed 9 September 2018].
3. TU Delft Zebro Project, 2018. [Online]. Available: [Accessed 20 September 2018].
4. D. Falguere, D. Boscher, T. Nuns, S. Duzellier, S. Bourdarie, R. Ecoffet, S. Barde, J. Cueto, C. Alonzo and C. Hoffman, “In-Flight Observations of the Radiation Environment and its Effects on Devices in,” IEEE Transactions on Nuclear Science, vol. 49(6), no. 0018-9499, pp. 2782-2787, December 2002.
5. L. Kinkelaar, “Adaptive Gait Switching Control Structure using Max Plus in Legged Locomotion,” Delft, 2018.