Status report of the MODES3 project
We are now at the finish!
The distributed logic developed in Yakindu is nearly finished. We are now also finishing the MQTT based communication between the components. Valudation and verification helped us to find design errors in the developed protocol! IncQuery and VIATRA really helped our work. The integration testing of the distributed protocol will be conducted tomorrow, stay tuned!
The hardware system is also under design. Many of the components have already produced and integrated, most of the BeagleBone devices are built into the system. Now, we have som problem caused by a short circuit, but hopefully we will solve also these problems in the next few days!
Computer vision can recognize the movement of the trains and also the EMF metamodell is developed to feed the VIATRA-CEP engine with complex events. Our contribution to the open-soruce complex event processing engine is on the way, we have used some cool formal stuff to enhance the language and also the execution. New timing extensions can be used in the language and the semantics were also changed. Our improvements will probably be presented at the 1st Workshop on Monitoring and Testing of Cyber-Physical Systems , we have sent an abstract there. So hopefully we can meet at the CPS Week in Vienna!
We have some problems with the real-time chip of the BeagleBone, so we now plan to use a real-time operating system in the BBB-s and we will use the runtime monitors on the application processor.
Our Lego robot used to help the transportation is also under development. Computer vision was tested and the controller is also finished. However, we are now debugging the MQTT communication between the components.
OpenModelica models are used to simulate the movement of the robot. We can predict not only the movement of the robot, but also the validate the commands we plan to send!
After this hard working weekend, we plan to integrate the components together! Follow our work in this blog, and watch the pictures and videos here!
Introducing our Model-based Demonstrator for Smart and Safe Systems
Hi everyone! Let me start by introducing our project called MoDeS3, which stands for Model-based Demonstrator for Smart and Safe Systems. The main goal of our IoT challenge application is to demonstrate the many cool and innovative ways in which open source modeling tools can be used for systems development in the age of Internet-of-Things.
Our case study is a railway system: users can control trains arbitrarily as long as it is not dangerous. Accidents and dangerous situations are detected using sensors embedded into the track: they sense the trespass of the trains and send this information to the controllers. It is important to note that this is just local information, so we have to ensure that it will be shared between the components. We employ six BeagleBone Black (BBB) embedded computers to run the safety logic, configured as a distributed system, where each BBB is responsible for some track sections.
As you can imagine, the real software engineering challenge is how to develop the distributed safety logic. We use the open source Yakindu Statecharts tool to design the software components. It is much easier than manual programming, as it provides a code generator to produce C or Java code.
In order to supercharge the expressive power of Yakindu models, we have developed custom validation and verification rules. For this purpose, we used the open source EMF-IncQuery engine. Our IncQueries can be used to analyse the well-formedness of the models, for example to check if the state chart is deterministic and complete. This turned-out to be a useful feature as many design time errors were found, well before deployment and debugging even began!
In addition to the validators, we have also developed model transformations to generate formal models from the state chart models. These formal models, together with associated model checking tools such as UPPAAL, are used to check the deadlock freedom and reachability of the states in the model. In the future, we plan to work more in this direction, in order to automatically analyse other properties such as fault-tolerance properties. We developed the model transformations using the VIATRA framework.
To make distributed systems work in practice, we need communication channels. For this project, we are going to use MQTT for its simplicity, reliability and flexibility. The open source Eclipse Paho framework helps us in establishing and maintaining the communication between the components.
In order to provide system-wide safety guarantees, we plan to build an additional layer on top of reliable communication channels, to facilitate runtime monitors. These smart components will evaluate the behaviour of the local components, and run locally on the PRU 32-bit microcontrollers of the BBBs. They will analyse if the communication works correctly and there is no problem within the controller itself.
To augment local monitors, the overall system status will be monitored using computer vision techniques. For this purpose, we attached a camera to a stage above the tracks that will observe the movement of the trains. The video stream is processed by OpenCV, a state-of-the-art open source computer vision library. We have implemented train recognition algorithms to detect the position of the trains.
The combination of local monitoring data and computer vision data will be aggregated on the system level and processed using complex event processing (CEP). The role of this high-level monitoring technique is to integrate multiple monitoring data sources and make sure that if the distributed safety logic does not work correctly, this additional level of logic can still bring the system to a safe state. Our system-level safety framework will be built using an open source complex event processing engine called VIATRA-CEP.