Monitor synthesis on the basis of temporal requirements for ROS environment

OData support
Dr. Majzik István
Department of Measurement and Information Systems

The goal of the project is to give an implementation to a new method for runtime verification on the Robot Operating System (ROS) platform using minimal resources. ROS is an open source platform with the goal of making industrial automation tasks and robot development easier.

During the implementation I developed a monitor application. When the application is integrated into a working ROS system, it can monitor and verify that system, and if the system violated or fulfilled the given property (e.g.a safety requirement) it will run the appropriate commands, or even shut down the system. The application is generated dynamically from the given property. This method will guarantee that the binary only contains the necessary components for the monitoring.

The properties are given as Linear Temporal Logic (LTL) expressions to the generator. LTL is a language to describe temporal ordering of atomic events. From this constraint the generator creates the monitor application source code using various transformations and optimizations. The created source code does not contain the necessary parts for extracting and filtering atomic events. This extracting and filtering has to be written by the application developer because the generator cannot determinate where and how the data can be accessed and filtered in order to produce the atomic events. To write these methods, the application developer has to use the ROS topics. These topics use the publisher-subsciber pattern to advertise messages, so the developer has to know the right topic to filter. After acquiring the necessary events, the verification can commence with the so-called logic evaluation blocks. These blocks only evaluate the actual part of the constraint thus saving resources.

After defining the primary events, the monitor is ready for compilation. After the compilation is complete, the component is ready to be inserted into the system and start its monitoring.


Please sign in to download the files of this thesis.