Distributed Petri nets ROS

被引：2

作者：

Ebert, Sebastian ^{[1
,3
]}

Mey, Johannes ^{[2
,3
]}

Schoene, Rene ^{[2
,3
]}

Goetz, Sebastian ^{[3
]}

Assmann, Uwe ^{[1
,2
,3
]}

机构：

[1] Ctr Tactile Internet Human Loop CeTI, Dresden, Germany

[2] 6G Life, Dresden, Germany

[3] Tech Univ Dresden, Chair Software Technol, Dresden, Germany

来源：

INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING | 2024年 / 20卷 / 04期

关键词：

Petri nets; Model-driven engineering; Robotic software engineering; Robot operating system;

D O I：

10.1007/s11334-024-00570-5

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Verifying industrial robotic systems is a complex task because those systems are distributed and solely defined by their implementation instead of models of the system to be verified. Some technologies mitigate parts of this problem, e.g., robotic middleware such as the Robotic Operating System (ROS) or concrete solutions such as automata-based specification of robot behavior. However, they all lack the required modeling depth to describe the structure, behavior, and communication of the system. We introduce an improved version of our previous model-driven approach based on Petri nets, integrating these three aspects of ROS-based systems. Using a formal modeling language enables verification of the described system and the generation of complete system parts in the form of ROS nodes. This reduces testing effort because the specification of component workflows and interfaces remains formally proven, while only changed implementations have to be revalidated. We extended our previous approach with novel model transformations, which considerably improved our approach's performance and memory requirements. We evaluate our approach in a case study involving multiple industrial robotic arms and show that the structure of and communication between ROS nodes can be described and verified.

引用

页码：531 / 557

页数：27

共 46 条

[21] Heinzemann C, 2018, IEEE INT C INT ROBOT, P8308, DOI 10.1109/IROS.2018.8593559
[22] Hillah L.M., 2009, Petri Net Newsletter, V76, P9
[23] Hillah L-M, 2010, 31 INT C APPL THEOR
[24] Holzmann Gerald J, 2004, The SPIN Model Checker: Primer and Reference Manual
[25] Jensen K., 1983, INFORMATIK, V66, P166, DOI [10.1007/978-3-642-69028-012, DOI 10.1007/978-3-642-69028-012]
[26] Jensen K., 1992, ANAL METHODS PRACTIC, V1, DOI [DOI 10.1007/978-3-662-03241-1, 10.1007/978-3-662-06289-0, DOI 10.1007/978-3-662-06289-0]
[27] Kilgo Paul, 2012, Simulation, Modeling, and Programming for Autonomous Robots. Proceedings of the Third International Conference, SIMPAR 2012, P125, DOI 10.1007/978-3-642-34327-8_14
[28] Formal Verification of ROS Based Systems Using a Linear Logic Theorem Prover
Kortik, Sitar
Shastha, Tejas Kumar
[J]. 2021 IEEE INTERNATIONAL CONFERENCE ON ROBOTICS AND AUTOMATION (ICRA 2021), 2021, : 9368 - 9374
[29] Petri net-based cooperation in multi-agent systems
Kotb, Y. T.
Beauchemin, S. S.
Barron, J. L.
[J]. FOURTH CANADIAN CONFERENCE ON COMPUTER AND ROBOT VISION, PROCEEDINGS, 2007, : 123 - +
[30] Lesire C, 2018, IEEE INT C INT ROBOT, P6952, DOI 10.1109/IROS.2018.8594328

← 1 2 3 4 5 →