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

职业：用于移动机器人系统开发的稳健且轻量级的形式化方法

• 批准号: 2338706
• 负责人: John-Paul Ore
• 金额: $ 59.47万
• 依托单位: North Carolina State University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2024
• 资助国家: 美国
• 起止时间: 2024-07-01 至 2029-06-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2338706&HistoricalAwards=false
• 关键词: CAREER; Robust; Lightweight; Formal; Methods

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.

移动机器人有可能扩大人们的能力，并减少人们目前在一系列人类努力中手工做的沉闷，肮脏或危险工作的数量，尤其是在医疗保健，国防，建筑和农业方面。但是，构建移动机器人具有挑战性且昂贵，因为机器人系统开发人员难以成本效率地构建，测试和维护可靠的软件。我们对机器人系统开发过程的了解存在差距，该过程阻碍了构建软件工具以支持该过程。借助当前的工具和技术，尤其很难构建一个可以升级到安全，可靠且可靠的移动机器人而无需从头开始的原型机器人。该项目旨在创建轻巧的技术和软件工具，以帮助机器人系统开发人员建立更安全，更有能力的机器人，同时保持经济可行。这项工作利用了视频游戏开发工具的进步，使得更容易测试移动机器人应该做的事情也不应该做什么。建造移动机器人需要在包括电气，机械和软件工程在内的多个领域的专业知识，并且在这些领域之间进行协调可能会具有挑战性。除了建立特殊的软件工具外，该项目还将研究和教学融合在一起，以使工程的最新进展（称为基于模型的工程工程）可以使学生成为可以建立，操作和维护更可靠的移动移动机器人的跨学科的未来劳动力的一部分。该项目利用行为树的模型检查的模型检查，并确保自动化的类型的型号和某些系统的绘制类型，并建议使用某些类型的系统。自动化程序分析和测试是现代软件连续集成和部署（CI/CD）的基本部分，但是机器人开发人员很难自动化，跟踪和评估系统测试工作。当前的技术未达到软件/硬件系统的异质共同发展的需求，尤其是当系统在现场验证时。该项目旨在开发从机器人系统开发人员已经使用的现有工件中推断机器人系统测试案例的技术。此外，该项目旨在创建用于推断和比较通常一起使用的物理单元组的技术，这些技术通常一起使用，以更好地理解程序，并在机器人系统实现中使用物理单元的使用方式进行新的模式。该项目的预期结果包括创建一个软件工具，可帮助开发人员检测和跟踪在其软件中共同发生的物理单元，创建一种工具，以帮助机器人系统开发人员衡量其系统已行使的行为树的数量，并开发测试案例的优先测试策略，以实地测试移动机器人系统的现场测试。这项研究应用了从软件工程到机器人自主权的基于模型的测试覆盖范围的概念，该研究领域的目的是降低将正式方法应用于机器人软件系统的障碍。该奖项反映了NSF的法定任务，并被认为是值得通过基金会的知识分子和更广泛影响的审查审查的审查标准来通过评估来通过评估来支持的。