CAREER: Robust and Lightweight Formal Methods for Mobile Robot System Development

Mobile robots have the potential to amplify people's capabilities and reduce the amount of dull, dirty, or dangerous work that people currently do by hand across a broad set of human endeavors, especially in health care, national defense, construction, and agriculture. However, building a mobile robot is challenging and expensive because robot system developers struggle to cost-effectively build, test, and maintain reliable software. There is a gap in our knowledge of the robotic system development process that hinders building software tooling to support that process. With current tools and techniques, it is especially hard to build a prototype robot that can be upgraded into a safe, reliable, and dependable mobile robot without having to start from scratch. This project aims to create lightweight techniques and software tools that help robot system developers build safer and more capable robots while remaining economically feasible. This work leverages advances in video game development tools to make it easier to test what a mobile robot should and should not do. Building mobile robots requires expertise in several areas, including electrical, mechanical, and software engineering, and coordinating information across these areas can be challenging. In addition to building special software tools, this project puts research and teaching together so that recent advances in engineering, called model-based engineering, can prepare students to be part of an interdisciplinary future workforce that can build, operate, and maintain more reliable mobile robots.This project utilizes model checking of behavior trees and abstract type inference of physical units to automatically suggest system tests and to help ensure the absence of certain classes of software defects. Automated program analysis and testing are fundamental parts of modern software's continuous integration and deployment (CI/CD), but robot developers struggle to automate, track, and assess system testing efforts. Current techniques fall short of the demands of heterogeneous co-evolution of software/hardware systems, especially when systems are validated in the field. The project aims to develop techniques for inferring robotic system test cases from existing artifacts that robot system developers are already using. Additionally, this project seeks to create techniques for inferring and comparing groups of physical units that are commonly used together to better understand programs and discover novel patterns in how physical units are used in robotic system implementations. The expected outcomes of this project include creating a software tool that helps developers detect and track the physical units that co-occur in their software, creating a tool that helps robot system developers measure how much of a behavior tree their system has exercised, and developing test case prioritization strategies for field testing of mobile robotic systems. This research applies notions of model-based test coverage from software engineering to robot autonomy, and a goal of this research area is to lower the barriers to applying formal methods to robotic software systems.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.