TeSSLa/ROS Bridge

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.


Step-By-Step Example

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.

Basic setup

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.

The counter node

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.

The TeSSLa specification

(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.

Building the monitor with ROS integration

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:

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.

Starting the TeSSLa/ROS node

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.