RVSPEC: Cyber-Physical Interplay Graphs for Formal Specification of Robotic Vehicle Control Software
Chaoqi Zhang, Minhyun Cho, Inseok Hwang, Hyungsub Kim
AI summary
Problem
Manually creating formal specifications for robotic vehicle control software is time-consuming and error-prone, while existing automated methods ignore the critical cyber-physical interplay between internal hardware/software properties and external environmental factors that dictate real-world physical behavior.
Approach
RVSPEC quantifies how internal and external factors influence physical states by constructing a cyber-physical interplay graph from simulation or real-world test data, then uses this graph to guide multi-agent large language models in generating context-aware formal specifications.
Key results
- Introduces the first cyber-physical interplay graph to quantify internal and external factor impacts on physical states
- Develops a multi-agent LLM framework that leverages graph data to generate accurate formal specifications
- Achieves 80.7% specification accuracy across four robotic vehicle control software packages, outperforming the 51.6% baseline
- Reduces fuzzing false positives by 79.9% while preserving bug-finding capability
Why it matters
Enables developers and researchers to efficiently detect logic bugs in critical robotic systems without wasting resources on physically plausible false alarms.
Abstract
Robotic vehicles (RVs) have increasingly deployed in critical missions. Yet, RV control software is prone to logic bugs that cause unexpected physical behaviors, deviating from the developers’ intentions. For instance, Hakuto-R Mission 1 lunar lander physically crashed on the lunar surface due to a misinterpretation of sensor data. To discover such bugs, developers leverage bug-finding tools, from formal methods to fuzzing. To use these tools, human experts first need to manually create formal specifications (e.g., temporal logic) as bug oracles. Yet, such manual efforts are time-consuming and error-prone. Previous efforts to automatically generate such specifications merely translate natural-language documentation into formal specifications. In turn, they overlook the cyber-physical interplay inherent in RVs, which is often absent from the documentation, e.g., altitude changes caused by air pressure and servo lag. To tackle this limitation, we introduce RVSPEC, an automatic specification generation framework. It first constructs a cyber- physical interplay graph (CPG). It captures the quantification about how much internal (control software-dependent and hardware-specific properties intrinsic to an RV) and external factors (environmental conditions) influence the RV’s physical states. Then, RVSPEC uses the CPG to guide large language model agents, enabling the generation of cyber-physical inter- play–aware formal specifications. We evaluated RVSPEC on four popular RV control software packages, including ArduPilot and PX4 for aerial vehicles, openpilot for autonomous vehicles, and cFS for spacecrafts. The evaluation showed that specifications created by RVSPEC achieved an accuracy of 80.7%, whereas the baseline’s ones attained 51.6%. When applying the specifications for fuzzing, those generated by RVSPEC reduced the number of false positives from 4,790 (baseline) to 964 (79.9% reduction) while preserving the bug-finding capability. The code is available at https://github.com/KimHyungSub/RVSpec.