Improving code quality in ROS packages using a temporal extension of first-order logic

摘要

Robots are given more and more challenging tasks in domains such as transport and delivery, farming or health. Software is a key component for robots, and Robot Operating System (ROS) is a popular open-source middleware for writing robotics applications. Code quality matters a lot because a poorly written software is much more likely to contain bugs and will be harder to maintain over time. Within a code base, finding faulty patterns takes a lot of time and money. We propose a framework to search automatically user-provided faulty code patterns. This framework is based on [Formula: see text], a temporal extension of first-order logic, and Pangolin, a verification engine for C[Formula: see text] programs. We formalized with [Formula: see text] five faulty patterns related to ROS and embedded systems. We analyzed with Pangolin 25 ROS packages looking for occurrences of these patterns and found a total of 218 defects. To prevent the faulty patterns from arising in new ROS packages, we propose a design pattern, and we show how Pangolin can be used to enforce it.