This Dezyne modelling example is Terry Dennemans’s submission for the Dezyne Challenge 2018.
The IOT Home Automation system contains two sub systems:
The control part that automates lighting and water sprinkler installation.
The monitoring system that keeps track of gas, water and electricity usage and production, and more detailed usage information coming from a ZWAVE system build up with power nodes.
The following list of requirements/features is available for the control system:
Curtain lighting, outside door and outside port lighting are controlled automatically and switched on/off when a related switch is triggered and current time is such that sun is down.
A start delay can be set for the lights for becoming active.
Duration of active door and port lights can be set, and start of duration starts at door/port opening, or when door/port is closed again.
Water sprinkler system is controlled by time intervals as specified by user.
An offsite database is used to keep track of the control settings.
An offsite website is used that allows for setting up the control settings (not part of this project).
Current time, sunset and sun rise time are retrieved from an internet service.
The following list of requirements/features is available for monitoring system:
The electricity and gas meter are read via a serial connection; the electricity meter also keeps track of the solar electricity production that was delivered back to the electricity net.
The water meter is connected with a hall sensor that generates pulses. So it needs to count the pulses that come by as an indication how much water is used.
The ZWAVE system is a mesh network of power nodes. These power nodes will report their current and total electricity usage.
At the moment, the control and monitoring systems are running on a Raspberry Pi and an Arduino board. The current implementation is far from finished and could use some clean up and refactoring. It is also not working reliable and once in a while suffers from crashes, that require a restart of the boards. One reason of the crashes is that the Arduino board has too little resources to fulfill its task; It is expected that running everything on a Raspberry Pi should suffice. Maybe we need two because of physical location and existing wiring for the devices being controlled.
To make things more reliable I wanted to use this Dezyne project; I made a start of cleaning up and refactoring the current implementation. For the Dezyne challenge, the idea was to run everything on one Raspberry Pi, but because of running out of time, the actual implementation on the Raspberry Pi has not been completed.
Figure below shows the Home utility monitoring system that currently consists of three sub systems (will have to become four to also deal with the solar panel installation). The bottom connectors show what the system needs from the outside (model) world.
The next figure shows the contents of the home control systems. Two outputs at the bottom are used for the internet time service and for the database connection used to get the settings of the control system. Further you see a Relay output module with 8 outputs. This is used to switch the power lines (both line and phase for safety reasons) for the lights and water valve used in this system. There are three switches used for the Door, Port and Curtains, which serves as trigger to see if an action needs to be taken for the lights. The OutputAction Systems are used for the switch-triggered actions. The TimedAction System is used for the actions that are based on set times and durations, which in this system is used for the water sprinkler system. The control system has a simple display showing current time and state of the system. Further it has an RTC (Real Time Controller) that gets synchronized every day (in current model).
Home Utility Monitoring
The monitoring system is designed around the timing mechanism implemented in the Electricity and Gas system. The gas and electricity meter will output a new status overview every few seconds.
When the system starts, it will initialize the several subsystems (ZwaveController, WaterCounter and ElecGasCounter). To initialize the water counter, the last acquired and saved monitoring data needs to be loaded from the database. Since the water counter is just a pulse counter, it needs to know the status of the counter when saved the last time.
Once all systems are initialized, the subsystems are asked for its current state and the combination of collected data will be persisted to the database. Since the Gas and Electricity system gives a new output every few seconds, the data collection will wait until new Gas and Electricity data has been received (See the blocking WaitForNextGasElecData call). While waiting for the new package, all subsystems are collecting their data. When the Gas and Electricity ystem outputs a new package, also the other packages are asked for their current data. All monitoring data is uploaded to the database. Once uploading is finished the whole data collection starts again for waiting for a new GasElec package to arrive.
The water counter gets initialized with the previous counter state in the StartCounting call. Every time the WaterCounter receives a pulse, the counter data is updated. The current counter data is polled using the GetCurrentCounter call.
The home control system is used to (de)activate devices connected to relay outputs. The outputs are triggered by time and or events because of switches being opened or closed when doors (or curtain) opens or close.
An OutputAction takes care of (de)activation a single output. Such output action can be configured using the SetActionSetting call. Configuration is the duration of an active action, but also the start delay after a received trigger and whether the duration is counted when the trigger is removed again or immediately after the start delay, can be configured.
The simulation above starts with the configuration. Then the SwitchActiveWhileSunDown is called which starts a timer to implement the start delay. When timer elapses, the output switch is activated. In this example the duration is counted after the trigger becomes inactive. This happens in the SwitchInActive call. This creates another timer for the duration, and on its timeout the output switch is deactivated. Another simulation could be done where the duration timer immediately starts after the output switch has been activated. This is left as an exercise for the reader.
A TimedAction takes care of activating an output switch based on current time and configured times for activating an output.
In above simulation first the action is configured using the SetActionSetting call. Next the SetCurrentTime is called to update the model with a new time. The isTimedActionPlanned helper function is used to determine whether the output switch should be active or not.
In above simulation the curtain switch is activated indicating that the curtains are closed and curtain lights should switch on when sun is down. The HomeControl system determines whether sun is up or down and triggers the curtainAction that curtain switch has become active; The sun is up, so output switch will not be activated. On next checkpoint the time changes, but unfortunately the model is not good. Since time has changed it could be that in the meantime the sun went down. When this happens, the curtain light should get activated (because the curtains are still closed).
This means the HomeControl system needs to be modified to deal with this missing feature. This is an example of where the model checker verifies everything is ok, but the model is not doing what it should do. The simulation feature in Dezyne is a very handy tool to try actual real life scenarios and make sure it covers all use cases that the system was meant to implement. You currently have to take care yourself that you play all use-cases that you want to have covered.
Modifying the model to deal with this error is put on the TODO list.
This is not the first time I have been using Dezyne; last time was with the previous Dezyne challenge. In the meantime things improved because of feedback given earlier. There are still things that can be improved and optimized even more, to get a better user experience. Several issues have been entered (some still left from last year).
What I like a lot when using Dezyne is that creating and verifying the models gives you different views on the actual problem that you want to solve. You immediately get pointed to situations that you didn’t think of, or those that you normally would skip in the beginning. Thinking these extreme cases will normally not happen. Often when you avoid these extreme cases in the beginning, the chance is high that you will not implement them later on in the project; maybe because of time reasons or you could have forgotten about it. Because of this, you see crashes or hang-ups once in a while. While using Dezyne, you are forced to think about these cases and have to make sure your models can deal with this. E.g. in case you get a communication error, what should you do with it and how do you want to continue with your application; This I ran into several times during this project, and forced me to think about solutions for which in my earlier implementation I was just not taking care of (one of the reason I currently have crashes once in a while I guess…)
Another nice tool that I use a lot within Dezyne is the simulator. You can simulate the input stimuli for your models. The tool nicely gives the possible stimuli for each step, which you can choose from. This I use to run my use cases and check whether the models are doing what the actual use case should do; Model verifications can be perfectly ok, but it doesn’t mean the model does what it should do. It would be very powerful if you could write some kind of unit tests and/or specify some conditions that would specify the use case that you want to implement. The tool would automatically check your models for these conditions and other specs. For now, I mainly used the simulator to validate the models against the use-cases it should cover. By running the simulation, I did find situations where the model did not implement the actual use case that I wanted. Some of the models I already adjusted, but some I had to park for after the challenge.
I would recommend everyone to try out Dezyne and see what you can get from it. Although you think you can manage without, you probably will be surprised of the things you will get back from it.
This document does not describe all details of the models. I would recommend to open Dezyne and check out the different models available. Hopefully it gives you some ideas for your own models. For my project I still have some work to do to make it useable and feel comfortable to replace my current implementation.
Because of mCRL2 introduction, some of the models that were working before are not working anymore.
Some of the issues have been resolved in the meantime.
I did not notice any performance issues when using the development version of Dezyne to check the mCRL2 checker.
It is very unfortunate, but it seems that the blocking feature is not part of mCRL2 anymore. I hope this is only temporary because it is a very powerful feature when having to deal with asynchronous models that need to become synchronous at some level. I hope that this project and document showed the reason why I used it. To get it working in mCRL2 without blocking, I probably have to write some additional external code or make a more complex model.
Again, I enjoyed the Dezyne Challenge and working with Dezyne. But also again there is more time required to finish such a project, that has been available.
You can download the example in a zip-file 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.