This Dezyne example is Pieter Cuijper’s submission for the Dezyne Challenge 2016. The goal of this example is to illustrate the modelling of an embedded system in its physical context.
The envisioned system is inspired by a robot that manipulates objects on a conveyor belt. The envisioned robot would have a placer capability, allowing it to put blocks onto slots of the conveyor belt. It would also have a pusher capability, allowing it to push blocks off the conveyor belt into a bucket. Of course, the robot would have to be able to detect whether there is a block on the current slot, and it would have to be able to signal the master controller that the conveyor belt should be moved to the next slot.
In this model, we decide to specify physical components as components. As a consequence we can use separate interfaces for separate physical variables, but have to rely on `multi-component-verification' (currently not available in Dezyne) to model-check the components completely.
An important decision when modelling physical components, is to model the progress of time as initiated by the output of a requires interface, rather than as an input of a provides interface. The reason for this, is that the system as a whole may have to provide output events that react on the progress of time. If time itself is a provided input event, enerating an output while processing the input is not possible in the requires/provides paradigm. Therefore, the progress of time must be initiated from an output on a lower requires port (and may be handed on upwards through a components provides port) rather than vice versa (i.e. time simulations trickle up, not down).
We equip the simulation of time also with an 'error' event, in order to circumvent compliance errors when model-checking a component that has illegal behaviour that cannot be captured by its interfaces.
The master component just ensures that the belt is only started after the controller gives off a proceed event… otherwise, programs are passed through from the MasterInterface. In an ultimate version, with multiple robots on a joint production line, this Master component would be an autonomous system, driving all the others. This, however, cannot be modelled as such in Dezyne, because each component that has behaviour needs to have a provides interface to make that behaviour visible on…
The controller can be programmed by the master. The master sends it commands on how to react on measurements. Subsequently, the controller measures, and acts according to the latest commands given by the master. While doing so, the controller has to take into account that placing and pushing at the same time is not allowed. Furthermore one should only measure if the production line is not moving. Whether this is successfully implemented can, at this point, not be verified using Dezyne. But maybe we can transform the Dezyne program into a model-checking language for the purpose?
The following statements form the heart of the physical model of the robot. If a motor is running, every time tick, the value of its position will change. Because we have a very simplistic model here, the position switches between its original position and 'not its original position', but this could be refined if a more accurate representation of the physics is needed for some reason. That, however, is outside the scope of Dezyne, since it involves handling data rather than control information.
The production line on which the robot of this example operates, is a good example of how physical interfaces sometimes need to be connected on a higher level, and cannot always contain all information necessary for verification. The production line contains slots that may be empty or filled with a block. When the belt moves, a new slot is placed in front of the robot. Moving the belt is initiated by the master controller, while manipulating the blocks on the belt is performed by the robot. One important property to verify is that the robot should not try to manipulate blocks while the belt is moving. However, this cannot be captured in the interfaces of the belt, because the information whether it is moving or not is determined by an interface connected to the master controller, while the manipulation itself is determined by an interface connected to the robot. As a consequence, the illegality of the manipulation of a moving belt has to be captured in the production line component, and cannot be verified on the component level. As a consequence, the interfaces with the master controller and the robot remain very simple.
The responsibility of a slot on the conveyor belt, specified in the ProductionLineSlot interface, summarises to:
See what is currently on the production line
Measure whether the production line is in position (i.e. not moving)
Push anything that is on the production line belt off
Place a white block onto the production line belt
The responsibility of the conveyor belt, specified in the ProductionLineBelt interface, summarises to:
Signal that it has reached its next slot and stop moving
When I started out on this challenge, I had of course heard already that Dezyne was in principle not intended as a modelling language for physical components. That part was obvious. Still, I wanted to give it a try to see how far one would be able to get, modelling the entire robot and controller in its physical environment. I had though that the greatest part of the challenge would be the fact that Dezyne is oriented towards control, and abstracts away from all data. What I had not realised, is that the greatest challenge in fact would be to model a physical system using the requires-provides paradigm.
Lesson 1 Time
What took me longest to figure out, but is perhaps the most important lesson when considering the modelling of physical components in Dezyne, is that the requires-provides paradigm does not allow for 'spontaneous' behaviour by components. Every event is somehow triggered by another event. For physical components, this means that there must be an external 'time' event that triggers the internal physics of the component. Furthermore, after trying both options, it turned out that using a 'requires time' interface, with time as an output event gives a more natural model than using a 'provides time' interface with time as an input trigger. The reason for this, is that time will usually trigger output events on the provides interfaces of a physical component, and Dezyne prevents the generation of such output events within the scope of a provides input.
Lesson 2 Levels of abstraction
At the current state of the art, Dezyne is unable to simulate or verify combinations of components. This means that everything you need to verify must be captured in the interfaces. But in a physical component (and most likely in some software components as well) the individual physical variables have nothing worth verifying on their interface. It is only when the interaction between the physical variables is described that we see something worth investigating. For example, in our production line example, the placer motor should not put a block into a slot where there is already a block present. Such an action might break the machine. If we have separate interfaces for the motor and the slot, we have no way to model such a requirement, and can therefore not model-check it. On the other hand, if we make both motor and slot part of the same interface, we enforce that they are implemented by the same component. In this case, that would mean that we consider the robot and the production line to be the same component, while the production line is provided by a different party (the practical coordinator) than the robot (which is build by the group of students).
The conclusion is that at different levels of abstraction/interfacing different model checking questions may be answered. Having flexibility to switch between these levels of abstraction is important. Currently, this can only be done in Dezyne by providing separate models at each level of abstraction. I hope that in future versions, we get the possibility to model-check combinations of components as well. For the current challenge, I decided for reasons of time, to stick to one level only.
Also, if modelling physical components, it is sometimes useful to specify nondeterministic behaviour in a component. I used workarounds for that in my modelling, which worked quite well. But depending on how the use of Dezyne develops, I can imagine that it becomes a choice whether components have to be deterministic.
Lesson 3 Requires/Provides
I’m not sure whether it is part of the requires/provides paradigm, or just a detail that was added in Dezyne, but there is this rule that when using multiple provides interfaces, you can only trigger an output on one of them at the same time. I assume this is because the order of execution would otherwise be difficult to predict. However, for the modelling of physical behaviour of components, especially in the light of the low level of abstraction that I was modelling at, this makes things difficult. A physical component usually defines a relation between different interfaces, and a time trigger will result in events that may even occur on all outgoing ports.
Usually, if you have to think about workarounds in Dezyne, you also have to think about whether you are not making a mistake in how you built up your software in the first place. But, in the case of modelling physical components, I think the requires/provides paradigm as it is currently being used may really be the cause of the trouble. Still, despite that, I did manage to model the entire system :)
Lesson 4 Small bugs are caught before you get to the big ones
Because you are programming at a high level of abstraction in Dezyne, you capture the 'trivial bugs' (forgetting cases, initializations, and other nuisances) before they start biting you. The misleading thing is that you do not really notice this happening, because you are running into the same mistakes you feel you always make. But because you catch them in this early stage, it means they do not interfere with your debugging of the 'really difficult ones' later on. Also, it is clearer what kind of mistakes you made, because the verifier identifies them for you.
For me, now it is time to start building a real robot and playing around with the design of it before returning to Dezyne. Once I have done that, this model may need some refinements based on insights of what the actual robots should be capable of, and based on insights what the protocol for the master should become.
At some point, the code generation capabilities of Dezyne may need to be tested.
Either, I could use them to automatically generate mCRL2 or other model-checker models from Dezyne models. Or I could use them in a traditional sense to generate code for the PP2 processor, or for an Arduino processor (as we may be switching to those in the near future).
Rests me to say, that I had fun trying out Dezyne, and I will certainly suggest it for students who would like to try something new.
The verification capabilities that I would like to have for educational purposes do not seem to be there yet, but the tool is certainly developing in the right direction.
Also, I can clearly see the advantages of modelling your code in Dezyne before writing the details, as I have caught many small errors this way.
(But I am also convinced that my current control-code will still contain some errors that only come to light if we can model-check at a higher level of abstraction!)
You can download the example in a zip-file 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.