RVSPEC: Cyber-Physical Interplay Graphs for Formal Specification of Robotic Vehicle Control Software

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 cyberphysical 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 interplay– 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.