TeSSLa-ROS-Bridge - Runtime Verification of Robotic Systems
Title | TeSSLa-ROS-Bridge - Runtime Verification of Robotic Systems |
Publication Type | Conference Paper |
Year of Publication | 2023 |
Authors | Begemann, MJohannes, Kallwies, H, Leucker, M, Schmitz, M |
Conference Name | 20th International Colloquium on Theoretical Aspects of Computing (ICTAC) |
Date Published | 11/2023 |
Publisher | Springer, Cham |
Conference Location | Lima, Peru |
Keywords | Robotic Systems, ROS, Runtime verification |
Abstract | Runtime Verification is a formal method to check a run of a system against a specification. To this end, a monitor is generated from the specification checking the system under scrutiny. Typically, runtime verification is used for checking executions of programs. However, it may equally be well suited for runs of robotic systems, most of which are built and controlled on top of the Robot Operating System (ROS). In stream runtime verification the specifications are given as stream transformations and this approach has become popular recently with several stream runtime verification systems starting from LOLA having emerged. This paper introduces the TeSSLa-ROS-Bridge, which allows to interact with ROS-based robotic systems via the temporal stream-based specification language TeSSLa. |
URL | https://link.springer.com/chapter/10.1007/978-3-031-47963-2_23 |
DOI | 10.1007/978-3-031-47963-2_23 |
@inproceedings {1439, title = {TeSSLa-ROS-Bridge - Runtime Verification of Robotic Systems}, booktitle = {20th International Colloquium on Theoretical Aspects of Computing (ICTAC)}, year = {2023}, month = {11/2023}, publisher = {Springer, Cham}, organization = {Springer, Cham}, address = {Lima, Peru}, abstract = {<p>Runtime Verification is a formal method to check a run of a system against a specification. To this end, a monitor is generated from the specification checking the system under scrutiny. Typically, runtime verification is used for checking executions of programs. However, it may equally be well suited for runs of robotic systems, most of which are built and controlled on top of the Robot Operating System (ROS). In stream runtime verification the specifications are given as stream transformations and this approach has become popular recently with several stream runtime verification systems starting from LOLA having emerged. This paper introduces the TeSSLa-ROS-Bridge, which allows to interact with ROS-based robotic systems via the temporal stream-based specification language TeSSLa.</p> }, keywords = {Robotic Systems, ROS, Runtime verification}, doi = {10.1007/978-3-031-47963-2_23}, url = {https://link.springer.com/chapter/10.1007/978-3-031-47963-2_23}, author = {Marian Johannes Begemann and Hannes Kallwies and Martin Leucker and Malte Schmitz} }
- News
- Research
- Teaching
- Staff
- Martin Leucker
- Diedrich Wolter
- Ulrike Schräger-Ahrens
- Aliyu Ali
- Mahmoud Abdelrehim
- Phillip Bende
- Juljan Bouchagiar
- Marc Bätje
- Tobias Braun
- Gerhard Buntrock
- Anja Grotrian
- Hannes Hesse
- Raik Hipler
- Elaheh Hosseinkhani
- Hannes Kallwies
- Frauke Kerlin
- Karam Kharraz
- Mohammad Khodaygani
- Ludwig Pechmann
- Waqas Rehan
- Martin Sachenbacher
- Andreas Schuldei
- Annette Stümpel
- Gesina Schwalbe
- Tobias Schwartz
- Daniel Thoma
- Lars Vosteen
- Open Positions
- Contact