Robotics systems are complex component-based systems that can consist of many interacting components. When composing and evolving complex component-based systems, the resulting behavior of component interactions sometimes differs from the developers' expectations. This can, for example, manifest itself in components indefinitely waiting for a required message that no other component sends, components reaching a deadlock state, or messages getting ignored due to systems being in an incorrect state. These bugs, which we call behavioral architecture composition bugs, are often hard to find because the fault locations are spread throughout many different locations in the system.

Model-based analysis is a common technique to identify incorrect behavioral composition of complex, safety-critical systems, such as robotics systems. However, in practice, robotics companies usually do not have any formal models, as models for hundreds of software components is a very costly and often labor-intensive and error-prone process. Behavioral models, which would need to be updated whenever the behavior of the component changes, are especially expensive to create.

In this dissertation, I present an approach to automatically infer behavioral models for components of systems based on the Robot Operating System (ROS), the most popular framework for robotics systems, using a combination of static and dynamic analysis by exploiting assumptions about the usage of the ROS framework Application Programming Interface (API) and behavioral idioms. Static analysis looks for architecturally-relevant API calls that implement message sending, handling received messages, sleeping for a periodic interval, and behavioral idioms that implement state-dependent behavior and state transitions. Based on this information, static analysis infers state machine models of architecturally-relevant component behavior. Due to limitations of static analysis, the resulting models are often partial. To complement statically inferred models, I present an approach to instrument the source locations of known unknowns and dynamically observe their values. Then, resulting models will be translated into the common language TLA+/PlusCal used for model-checking. Furthermore, I present a model-based analysis technique to find architecture-misconfiguration bugs in the resulting TLA+ models. Then, I present a technique that automatically generates visual diagrams from the inferred models. Our human study with practicing roboticists and graduate students finds that these diagrams support the understanding of architecturally-relevant component behavior without slowing down participants. This work is a contribution towards making well-proven and powerful but infrequently used methods of model-based analysis more accessible and economical in practice to make robotics systems more reliable and safe.

126 pages

Thesis Committee:
Claire Le Goues (Co-chair)
David Garlan (Co-chair)
Christopher Stgeven Timperley
Ivano Malavolta (Vrije Universiteit Amsterdam)

Nicolas Christin, Head, Software and Societal Systems Department
Martial Hebert, Dean, School of Computer Science

Creative Commons License: CC-BY-NC (Attribution-Non-Commerical)

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu