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.
@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")
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
(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
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
__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
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
The specification of the TeSSLa monitor can be found in config_tessla/counter_with_reset.tessla:
@RosSubscription("/counter", "int64", "10")
in x: Events[Int]
def reset = x > 10
@RosPublisher("/reset_counter", "bool", "10")
This TeSSLa specification has one input stream
x and an output stream
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
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
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:
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:
use_trace can be set to
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
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
ros2 launch tesslabridge tessla_bridge.launch.py
To launch the full example (i.e. TeSSLa/ROS bridge and the counter node from above) just run
The output of the TeSSLa/ROS node can be seen on screen and in the log file configured above.