Bug finding through consistency checking for robotic systems

<p dir="ltr">Robotic systems have rapidly growing applications in our daily lives. Engineering such systems becomes increasingly important. Due to the unique characteristics of such systems, e.g., the need to model the physical world and satisfy real-time and resource constraints, robotic system engineering poses new challenges to developers. First, developers should follow certain dimensional rules, e.g., a length value cannot be added to a velocity value while performing operations on program variables representing the physical dimensions such as distance, velocity, and acceleration. Since such variables have physical units (e.g., meter) that are not explicitly declared unlike their datatypes (e.g., float), a compiler does not complain in case of incorrect manipulation of physical units. It can be hard for developers to get these physical units correct all the time. Therefore, inferring an abstract physical unit type for variables and checking their physical unit type consistency is of particular importance for validating the correctness of such systems. Existing solutions have various limitations such as requiring developers to annotate variables with physical units and only handling variables that are directly or transitively used in popular robotic libraries with known physical unit information. To address these limitations, we propose an approach that can tap into new sources of information such as variable names and expression forms to make probabilistic inference of physical units for a larger portion of the variable space, facilitating the detection of more inconsistencies. Second, developers should make proper use of physical frames of reference. Specifically, the operation of a robotic system involves moving individual body parts and interacting with the external world. It entails precisely measuring the positions and orientations of body parts and external objects. All these measurements are represented with respect to a set of coordinate systems (also called frames of reference or frames in short). Various computations require the measurements in one frame to be translated to another frame. There exist popular libraries such as ROS that provide functions to facilitate translation between frames, however, it is the responsibility of developers to determine the frames of program variables and the places where the translation is needed, and to implement the concrete translations correctly. Therefore, the use of frames is error-prone. ROS provides mostly runtime tools to help developers debug frame-related problems. However, a static tool that can detect these problems before running the system is highly desirable. We introduce type inference and checking technique for frames in ROS-based software and implement a fully automated static tool to detect frame inconsistencies and convention violations. Third, robotic systems implemented using a popular library, ROS, perform a majority of operations in callbacks. Callbacks in robotic programs are the functions that are invoked as a result of internal or external events. ROS provides various elements to initialize callbacks and to setup their execution. It is a developer's responsibility to program the composition of those elements and hence can lead to errors. The recent works have studied timing aspects such as response time and latency, and alternate algorithms for callback execution for ROS-based systems. Unlike them, we focus on how the improper composition of callback setup elements can lead to problems. For that, we define a class of inconsistencies related to the callback execution setup and propose a lightweight static approach for detecting such inconsistencies by constructing a graphical view of the setup. Further, we briefly discuss another challenge faced by developers while engineering robotic systems, namely, developers should correctly configure and integrate components of modular robotic software with various input parameters, string identifiers, and timing parameters.</p>