Formal Modeling and Verification of Publisher-Subscriber Paradigm in ROS 2

要約

ロボット オペレーティング システム (ROS) は、ロボット アプリケーションを開発するための最も人気のあるミドルウェアの 1 つですが、安全性が重要な環境でリアルタイム ロボット システムに適用すると、大きな欠点が発生します。
このため、オリジナルの ROS の最も優れた側面をサポートしながら、分散ロボット システムにリアルタイム機能を実装するために、ROS 2 が 2017 年にリリースされました。
ROS プログラムの正式な保証と正確性を提供するために行われた作業はまだあまり多くありません。
この論文では、ロボット システムの正しい動作を保証するというこの困難な問題に対処するためのフレームワークを提案します。
我々は、ROS 2 プログラムの正式なモデリングを提案し、また、時限オートマトンのネットワークを使用してプログラムを記述します。
次に、モデル内と時限オートマトンのネットワーク内での ROS プログラムの実行セットが同じであることを証明します。
したがって、ROS 2 プログラムのパブリッシャーとサブスクライバーのシナリオを分析するために、私たちのアルゴリズムはまずプログラムをモデルに変換し、次に時限オートマトンのネットワークに変換します。
我々のアプローチの適用性と妥当性は、簡略化されたシステムと実際のロボットシステムでいくつかの実験を行うことによって検証され、結果と限界が議論されます。

要約(オリジナル)

The Robot Operating System (ROS) is one of the most popular middleware for developing robot applications, but it is subject to major shortcomings when applied to real-time robotic systems in safety-critical environments. For this reason, ROS 2 was released in 2017 for implementing real-time capabilities in distributed robotic systems while supporting the most prominent aspects of the original ROS. There is still not much work done to provide formal guarantees and correctness of a ROS program. In this paper, we propose a framework to address this challenging problem of guaranteeing the correct behaviour of robotic systems. We propose a formal modelling of a ROS 2 program, and also describe the program using a network of timed automata. We then prove that the sets of executions of a ROS program in the model and in the network of timed automata are the same. Thus to analyze a publisher-subscriber scenario of ROS 2 program, our algorithm first converts the program into the model, and then into the network of timed automata. The applicability and validity of our approach are verified by conducting several experiments on a simplified system and an actual robotic system, and the results and limitations are discussed.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google