arXiv subjects

Siao Wang

Publications and source records attributed to Siao Wang.

3 recordsLinked to original sources

arXiv2025

RouthSearch: Inferring PID Parameter Specification for Flight Control Program by Coordinate Search

Flight control programs use PID control modules with user-configurable Proportional (P), Integral (I), and Derivative (D) parameters to manage UAV flying behaviors. Users can adjust these PID parameters during flight. However, flight control programs lack sufficient safety checks on user-provided PID parameters, leading to a severe UAV vulnerability - the input validation bug. This occurs when a user misconfigures PID parameters, causing dangerous states like deviation from the expected path, loss of control, or crash. Prior works use random testing like fuzzing, but these are not effective in the three-dimensional search space of PID parameters. The expensive dynamic execution of UAV tests further hinders random testing performance. We address PID parameter misconfiguration by combining the Routh-Hurwitz stability criterion with coordinate search, introducing RouthSearch. Instead of ad-hoc identification, RouthSearch principledly determines valid ranges for three-dimensional PID parameters. We first leverage the Routh-Hurwitz Criterion to identify a theoretical PID parameter boundary, then refine it using efficient coordinate search. The determined valid range can filter misconfigured PID parameters from users during flight and help discover logical bugs in flight control programs. We evaluated RouthSearch across eight flight modes in PX4 and Ardupilot. Results show RouthSearch determines valid ranges with 92.0% accuracy compared to ground truth. RouthSearch discovers 3,853 PID misconfigurations within 48 hours, while the STOA work PGFuzz discovers only 449 sets, significantly outperforming prior works by 8.58 times. Our method also helped detect three bugs in ArduPilot and PX4.

cs.SE↗

arXiv2025

Extracting Formal Specifications from Documents Using LLMs for Automated Testing

Automated testing plays a crucial role in ensuring software security. It heavily relies on formal specifications to validate the correctness of the system behavior. However, the main approach to defining these formal specifications is through manual analysis of software documents, which requires a significant amount of engineering effort from experienced researchers and engineers. Meanwhile, system update further increases the human labor cost to maintain a corresponding formal specification, making the manual analysis approach a time-consuming and error-prone task. Recent advances in Large Language Models (LLMs) have demonstrated promising capabilities in natural language understanding. Yet, the feasibility of using LLMs to automate the extraction of formal specifications from software documents remains unexplored. We conduct an empirical study by constructing a comprehensive dataset comprising 603 specifications from 37 documents across three representative open-source software. We then evaluate the most recent LLMs' capabilities in extracting formal specifications from documents in an end-to-end fashion, including GPT-4o, Claude, and Llama. Our study demonstrates the application of LLMs in formal specification extraction tasks while identifying two major limitations: specification oversimplification and specification fabrication. We attribute these deficiencies to the LLMs' inherent limitations in processing and expressive capabilities, as well as their tendency to fabricate fictional information. Inspired by human cognitive processes, we propose a two-stage method, annotation-then-conversion, to address these challenges. Our method demonstrates significant improvements over the end-to-end method, with a 29.2% increase in the number of correctly extracted specifications and a 14.0% improvement in average accuracy. In particular, our best-performing LLM achieves an accuracy of 71.6%.

cs.SE↗

arXiv2023

EnvGuard: Guaranteeing Environment-Centric Safety and Security Properties in Web of Things

Web of Things (WoT) technology facilitates the standardized integration of IoT devices ubiquitously deployed in daily environments, promoting diverse WoT applications to automatically sense and regulate the environment. In WoT environment, heterogeneous applications, user activities, and environment changes collectively influence device behaviors, posing risks of unexpected violations of safety and security properties. Existing work on violation identification primarily focuses on the analysis of automated applications, lacking consideration of the intricate interactions in the environment. Moreover, users' intention for violation resolving strategy is much less investigated. To address these limitations, we introduce EnvGuard, an environment-centric approach for property customizing, violation identification and resolution execution in WoT environment. We evaluated EnvGuard in two typical WoT environments. By conducting user studies and analyzing collected real-world environment data, we assess the performance of EnvGuard, and construct a dataset from the collected data to support environment-level violation identification. The results demonstrate the superiority of EnvGuard compared to previous state-of-the-art work, and confirm its usability, feasibility and runtime efficiency.

cs.SE↗