The goal of this Dezyne modelling example is to illustrate how main cruise control functionality can be modelled in Dezyne.

The context


The cruise control has a user interface with a mechanical on/off switch and 2 monostable switches. These are pairwise overloaded to

  • Set (SET) the target speed and start the cruising mode or decrease (COAST) the target speed.

  • Resume (RES) cruising with a target speed set before or increase (ACC) the target speed

Invisible to the user also the status of the brake and gas pedals are monitored and taken into account in the controller. As output of the system the throttle is controlled.

The system modelled in Dezyne

The problem is split into 2 parts:

  • The top level is a discrete system keeping track of the overall state of the system.

  • The bottom level is a continuous control loop to keep the actual speed as close as possible to the target speed.

In the Dezyne model this distinction is reflected in the following component decomposition:


These are the external interfaces:

  • ISwitch – the on/off switch of the cruise controller

  • ISetpoint – reflects the two monostable switches

  • IBrake – the sensor measuring whether the brake pedal was activated

  • IGas – the sensor measuring whether the gas pedal was activated

  • IThrottle – the actuator controlling the throttle

  • ISpeedSensor – the sensor measuring the actual speed of the car

Most of these UI components are mapped on interfaces connected at bottom of the hierarchy. In principle Dezyne allows interfaces both at the top of the system and at the bottom so technically it does not matter. The reasoning here is that in many graphical programming environments the trigger of a button is implemented as a callback function. This is also what happens if a UI component is connected to the bottom of the hierarchy.

Another reason is the fact that as callback we can make use of another interesting semantic feature in Dezyne: We can specify whether the event will always happen or whether it just might happen using the keywords inevitable and optional. This is important information for the verifier. Suppose such an event is the only escape from a potential deadlock situation. In the case of inevitable the event will always happen so the verifier will conclude that there will always be an escape possible and there is no deadlock. In the case of optional there is a potential deadlock and the verifier will indicate that.

In the modelled cruise control the Gas press and release are considered inevitable, they will always happen[1]. However, the Brake press and release are optional: It would be a bad design if one of these Brake events were essential to a correct functioning of the cruise control system[2].

The ISwitch interface is an exception here. This is connected to the top since in Dezyne it is obligatory to have at least one “provides” interface for a component. In a way it is logical then to have the main on/off switch of the system connected at the root of the hierarchy.

The SpeedController (sub)system

This is the continuous control loop. The SpeedController is further decomposed into the following:


A part of the functionality deals with a timer and data processing and hence cannot be implemented in Dezyne. Therefore a hand written component (SpeedHW) is included in the hierarchy but fully enclosed in Dezyne interfaces. In this way the calculations are fully encapsulated and appropriate control signals are exchanged over the interfaces. This also means that the overall control logic can be verified in Dezyne. In the diagram the hand written component is displayed with a colour different from the regular components.

On the other hand looking at the complexity of this solution there might a be natural split between which part of the problem is best expressed in Dezyne and which part might better be done for example in Matlab or on a PLC. A continuous control loop is relatively easy in Matlab or a PLC. So the whole SpeedController subsystem might be better implemented in one of those. For the discrete part Dezyne is the obvious choice. In this document we will review the whole system as an interesting exercise how to model this in Dezyne.

The handwritten component SpeedHW is responsible for:

  • Storage of target speed

  • Retrieval of actual speed

  • Calculation of the difference between target speed and actual speed

  • Generation of the timer event that triggers the continuous control loop

No code for this component is included in this example but from the description it is obvious that this is not very complex. The Dezyne verifier only needs the interface specifications. For details on the syntax of the hand written code and how to integrate that with auto-generated code see other examples.

The interface ISpeedControl always allows setting of the targetspeed. On the other hand speedup and speeddown are only allowed in the active state. The client of ISpeedControl is the Cruise Control component and ensures that these preconditions are met. Since the user can always activate all switches the Cruise Control must ignore these events in the situations where they are not permitted by ISpeedControl.

The Cruise Control component

The discrete cruise controller is a state machine with 4 states:

  • Off – the whole state machine is off. This is a 1:1 mapping of the Switch in the Off position

  • Waiting – the main Switch is On so the cruise controller is active but there is no target speed setting yet or the speed setting is temporarily disabled (e.g. by a press on the brake). The difference between these 2 situations is administrated in a local state variable speed_defined.

  • Cruising – in this state the speed control loop is active and the speed is continuously adjusted to match the target speed.

  • Override – this the situation where the driver presses the gas pedal while cruising hence effectively overruling the speed control. As soon as the pedal is released we fall back to regular cruising mode

Some of the UI interfaces only serve to send individual events to the cruise controller system and hence do not have an internal state. For some of the UI interfaces we model explicitly that the events come in a specific order and hence need an internal state. The ISwitch represents a mechanical On/Off switch so also for this one we model explicitly that the state toggles.

The Brake pedal is a special case because we need to be able to check the status of the Brake in the Waiting state. In a first implementation of the cruise controller a problem was detected by the verifier: "If the brake is pressed before a target speed is set and then the brake is released we hit an illegal".

This is obviously a situation we would like to avoid. In fact this indicates there is a more fundamental problem in this first design: By setting the target speed we move to the Cruising state so we could have a situation where the brake is pressed and the speed control loop is actively controlling the speed at the same time! It is nice to see that carefully specifying these illegals helps in letting the verifier detect fundamentally wrong behaviour.

To solve this we build in an extra test to only go to Cruising state if the brake is not in pressed state.

on isetpoint.setpoint_up_resume():
  bool bp = ibrake.brakepressed();
  if (!bp) {state = CC.Cruising; isc.activate();}

For the Gas pedal we also keep an internal state to guard that press and release must always occur in an alternating fashion[3]. This allows us to define some events in the CruiseControl component as illegal so we can leave them out of the code and rely on the default behaviour of Dezyne.

For example, if we would remove the alternating behaviour in IGas the verifier will find problems in our design, e.g.:


The problem is caused by 2 IGas pressed events in a row. Since we can only enter the Override state upon a Gas press event (and will leave the Override state upon a Gas release event) it would not be logical to handle a Gas press event in the Override state. So it is better to explicitly specify in the IGas interface that the Gas press and release events must be alternating.

Being strict in the usage of illegal in general helps in finding design errors. For example, in one iteration of the design the verifier found a problem in the scenario depicted below:


The problem reported is that a SpeedController activate event happens 2 times in a row. Analyzing this situation showed that the second call to activate was in fact a wrong function call and setspeed should have been called. The code in the Override state was:

on isetpoint.setpoint_down_set(): { isc.activate();}

where it should be:

on isetpoint.setpoint_down_set(): { isc.setspeed();}

If the activate event would not have had this protection against being called twice the problem would have passed by unnoticed and probably only have been discovered during testing much later in the process.

Ideas for extensions

A useful additional feature would be a timeout on the Override state. If the user forgets that in the background in this state, cruise control is still active he might be surprised that if he releases the gas pedal the car keeps on maintaining its speed. To support this, a timer needs to be implemented in hand written code which can send a timeout event to the CruiseControl component where it would lead to a state transition to e.g. the Waiting state.


The Eclipse project with the Dezyne model file where the interfaces and the components are defined can be downloaded from here.

Note that all of the diagrams included in this document have been produced in and exported from Dezyne. The System View and State Charts are part of the Dezyne editor. The Sequence Trace has been produced using the Dezyne simulation engine.

1. We ignore the scenario where the user never touches the gas pedal but immediately starts the cruise control after powering the car and only accelerates / decelerates using the cruise control switches.
2. In theory we could test for a deadlock situation in this way. However, in this model of the cruise controller there are no evident deadlock situations.
3. The logic model of the gas pedal is a simplified view of reality. In a real system the event gaspress would represent the situation that the pedal position is pressed deeper than the value the throttle represents and vice versa for the gasrelease event. This could be modelled by adding extra interface functions to hand written code.