The Robot Operating System (ROS) is a widely used operating system for robots. TeSSLa provides a ROS integration that allows the easy connection of TeSSLa monitors with ROS nodes.
TeSSLa/ROS Bridge allows an easy application of Runtime Verification to robot systems by executing monitors to verify basic safety properties on a ROS system.
include "TesslaROSBridge.tessla"
@RosSubscription("/reduced_scan_to_tessla", "int64", "10")
in scan: Events[Int]
# Stop if there are short rays detected
def stop = scan < 20
@RosPublisher("/result_from_tessla_to_ros", "bool", "10")
out stop
Thus, with the help of TeSSLa/ROS Bridge a specification like the one above can be used to bring a robot system with a distance sensor to a stop when it approaches an obstacle too closely in order to prevent a collision, as shown here in the video.
This article shall give a quick introduction to the functionality and usage of the TeSSLa/ROS Bridge.
Further information about the project can be found in the corresponding README.
The TeSSLa/ROS Bridge is a ROS node, which is executed together with the other nodes on the robot system and executes a monitor, automatically generated from a TeSSLa specification.
The monitor can easily be connected to topics of other ROS nodes by annotations in the TeSSLa specification.
The monitor can either be solely used for monitoring and writing the outputs to a log file. However it can also be used for controlling purposes and output streams can again be attached to ROS topics.
In this example we will explain the TeSSLa/ROS integration by means of a simple counter example.
Therefore we provide a ROS node which increments a counter and resets it, when a reset signal is received. A TeSSLa monitor observes this node and when the counter has reached number 10 it triggers the reset signal of the counter node.
The example is the default example contained in the TeSSLa/ROS Bridge project on the TeSSLa GitLab.
The first step for using TeSSLa/ROS Bridge is to clone the TeSSLa/ROS Bridge repository from the TeSSLa Gitlab
git clone https://git.tessla.io/ros/tesslarosbridge.git
cd tesslarosbridge
(Alternatively the directory can be downloaded as zip File via this link)
Next, ROS2 Dashing, Java, Rust/Cargo etc. have to be installed. More detailed information about this can be found in the TeSSLa/ROS Bridge README.
Finally the TeSSLa/ROS Bridge node has to be pre-built, which is done by the following commands:
colcon build --symlink-install
Now the TeSSLa/ROS Bridge is ready to run. It can now be configured with the corresponding TeSSLa specification and executed.
However, before we proceed to the monitor, we first take a look at the counter node which will later be observed and controlled by the monitor.
The counter node is written in Python and located in src/tesslabridge/tesslabridge/examples/counter_with_reset.py
We do not address the details here as this node is only used for a quick example and not part of the TeSSLa/ROS Bridge itself. However in the python file there are the methods timer_callback and reset_callback defined.
The first one timer_callback increments the global variable counter by 1 and builds an Int64 message with the value which is then logged and published via counter_publisher (see below).
The second one reset_callback resets the global counter variable if the argument msg contains the data value true.
In the __init__ function a ROS publisher (counter_publisher) is created and attached to topic /counter and method reset_callback is connected to topic /reset_counter. Furthermore a timer is set to call timer_callback with configurable time counter_timer_period.
To sum up, this ROS node periodically increments a counter and notifies connected ROS nodes via the topic /counter and resets the counting process when a message with value true is received on topic /reset_counter.
(For more information see also the TeSSLa introduction and the TeSSLa tutorial)
The specification of the TeSSLa monitor can be found in config_tessla/counter_with_reset.tessla:
include "TesslaROSBridge.tessla"
@RosSubscription("/counter", "int64", "10")
in x: Events[Int]
def reset = x > 10
@RosPublisher("/reset_counter", "bool", "10")
out reset
From TeSSLa compiler version 2.1.0 on the include in the first line can be replaced by include lib "ros_bridge:1.0.0". In this case the library is downloaded automatically and included if it is not yet present in the working directory.
This TeSSLa specification has one input stream x and an output stream reset. The reset stream is a boolean stream which has an event, always when x has one. The value of this event is true if the corresponding event on stream x is greater than 10 and false otherwise:
stream x: bubbles
stream reset: bubbles
---
1: x = 8
1: reset = false
2: x = 9
2: reset = false
3: x = 10
3: reset = false
4: x = 11
4: reset = true
5: x = 0
5: reset = false
The input stream x also contains the annotation @RosSubscription (defined in the included TeSSLaROSBridge.tessla) which connects the stream x to the ROS topic /counter. The second parameter of the annotation provides information about the type of the topic (which has to be compatible with the type of the TeSSLa stream) and the QoS profile. Likewise the output of stream reset is connected to the ROS topic /reset_counter.
Note that these topic names are the ones from the Python counter example in the section above.
After the specification has been adjusted the TeSSLa/ROS bridge has to be built.
Before the build process some configurations have to be adjusted for this purpose:
The variable tessla_specifiaction_file in scripts/build_project.sh has to be adjusted by the name of the TeSSLa specification which shall be monitored (without the .tessla ending). In our case counter_with_reset which already is default.
The configuration of the ROS project src/tesslabridge/config/tessla_bridge.yaml has to be adjusted:
Switch use_trace can be set to true or false depending on whether one wants to create a log file with the outputs of the TeSSLa monitor.
trace_path has to contain the full path of the log file to be generated.
When the configuration is finished, the TeSSLa/ROS node can be built by running scripts/build_project.sh.
The script translates the specification into a Rust monitor and attaches it to a ROS node which is then automatically connected to other nodes according to the information given by the annotations.
In general the TeSSLa/ROS bridge node can be started with
source ./../install/setup.bash
ros2 launch tesslabridge tessla_bridge.launch.py
(see scripts/start_TeSSLaBridge_standalone.sh)
To launch the full example (i.e. TeSSLa/ROS bridge and the counter node from above) just run scripts/start_example_counter_with_reset.sh.
The output of the TeSSLa/ROS node can be seen on screen and in the log file configured above.