Distributed Petri nets for model-driven verifiable robotic applications in ROS

Publikation: Beitrag in FachzeitschriftForschungsartikelBeigetragenBegutachtung

Abstract

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.

Details

OriginalspracheEnglisch
Seitenumfang27
FachzeitschriftInnovations in Systems and Software Engineering
Jahrgang(2024)
PublikationsstatusVeröffentlicht - 25 Juni 2024
Peer-Review-StatusJa

Externe IDs

Scopus 85196869041
ORCID /0000-0002-3247-0264/work/168207230
ORCID /0000-0003-1537-7815/work/168720070
ORCID /0000-0002-3513-6448/work/168720205

Schlagworte