Statusvortrag von Dipl.-Inf. Sebastian Ebert

Abstract:

Ensuring trustworthiness, the predictability and correctness of robotic systems, is critical for a human co-worker’s safety. However, verifying these systems is complex due to their distributed nature and reliance on implementation-specific definitions rather than comprehensive system models. 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. To address this, the dissertation introduces a model-driven approach utilizing distributed and time Petri nets providing the necessary modeling depth. 

The proposed approach addresses three challenges: the rationale behind a robotic systems decision, its correctness, and its future actions. The first challenge is addressed by integrating structural, (timed) behavioral, and communicative aspects of ROS-based systems into a formal modeling language. This facilitates system verification and the automated generation of ROS nodes. To address whether the system is functioning correctly and what its future actions are, the approach employs runtime modeling and analysis of runtime and synthetic traces. Continuous monitoring and analysis against a formal specification ensures the system's correctness and predictability, by detecting inconsistencies and reduces testing efforts by focusing revalidation only on modified implementations. 

The effectiveness of the proposed approach will be demonstrated through industrial case studies involving multiple industrial robotic arms, showcasing its ability to describe, verify, and optimize the structure, (timed) behavior, and communication of ROS applications.