Chaoqi Zhang and Hyungsub Kim, Indiana University Bloomington
Generating accurate metric temporal logic (MTL) formulas, as formal specifications, for robotic vehicle (RV) control software is essential for bug finding and fixing. However, generating these formulas is a labor-intensive and error-prone task, posing a challenge to the scalable creation of such formal specifications. To tackle this challenge, we propose AUTOSPEC, a multi-agent framework guiding large language models (LLMs) to automate MTL generation from documentation written in natural language. AUTOSPEC consists of three LLM agents, specialized for extracting logic policies, identifying physical context, and generating MTL formulas. Each agent operates with customized prompt engineering and few-shot examples. We evaluate AUTOSPEC on two popular RV control software packages (ArduPilot and PX4). Demonstrating a substantial improvement, AUTOSPEC achieves 87% accuracy, while the baselines only show 18% accuracy.
Open Access Media
USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.
