Fully automated verification of large-scale software and hardware systems is arguably the holy grail of formal methods. Large language models (LLMs) have recently demonstrated their potential for enhancing the degree of automation in formal verification by, e.g., generating formal specifications as essential to deductive verification, yet exhibit poor scalability due to long-context reasoning limitations and, more importantly, the difficulty of inferring complex, interprocedural specifications. This paper presents Preguss – a modular, finegrained framework for automating the generation and refinement of formal specifications. Preguss synergizes between static analysis and deductive verification by steering two components in a divide-and-conquer fashion: (i) potential runtime error-guided construction and prioritization of verification units, and (ii) LLM-aided synthesis of interprocedural specifications at the unit level. We show that Preguss substantially outperforms state-of-the-art LLM-based approaches and, in particular, it enables highly automated RTE-freeness verification for real-world programs with over a thousand LoC, with a reduction of 80.6%~88.9% human verification effort.

Time series anomaly detection (TSAD) is essential for ensuring the safety and reliability of aerospace software systems. Although large language models (LLMs) provide a promising training-free alternative to unsupervised approaches, their effectiveness in aerospace settings remains under-examined because of complex telemetry, misaligned evaluation metrics, and the absence of domain knowledge. To address this gap, we introduce ATSADBench, the first benchmark for aerospace TSAD. ATSADBench comprises nine tasks that combine three pattern-wise anomaly types, univariate and multivariate signals, and both in-loop and out-of-loop feedback scenarios, yielding 108,000 data points. Using this benchmark, we systematically evaluate state-of-the-art open-source LLMs under two paradigms: Direct, which labels anomalies within sliding windows, and Prediction-Based, which detects anomalies from prediction errors. To reflect operational needs, we reformulate evaluation at the window level and propose three user-oriented metrics: Alarm Accuracy (AA), Alarm Latency (AL), and Alarm Contiguity (AC), which quantify alarm correctness, timeliness, and credibility. We further examine two enhancement strategies, few-shot learning and retrieval-augmented generation (RAG), to inject domain knowledge. The evaluation results show that (1) LLMs perform well on univariate tasks but struggle with multivariate telemetry, (2) their AA and AC on multivariate tasks approach random guessing, (3) few-shot learning provides modest gains whereas RAG offers no significant improvement, and (4) in practice LLMs can detect true anomaly onsets yet sometimes raise false alarms, which few-shot prompting mitigates but RAG exacerbates. These findings offer guidance for future LLM-based TSAD in aerospace software.

Requirements classification, which organizes software requirements into structured categories, is crucial in safety-critical domains such as aerospace. However, practical implementation is challenging due to the absence of unified, domain-specific taxonomies, as different developers often adopt divergent classification schemes. Moreover, safety-critical requirements frequently intertwine functional and reliability constraints, creating complex multi-label classification challenges. Existing supervised learning approaches depend on large annotated datasets, which are rarely feasible in specialized industries, while current LLM-based methods face difficulties handling hierarchical, multi-label scenarios effectively. To address these issues, we propose TRClass, a novel taxonomy-guided classification approach. The key idea behind TRClass is to integrate domain knowledge into the classification process by first constructing a unified taxonomy semi-automatically, extracting structure from existing documents, and refining it with expert validation. TRClass then guides an LLM to classify requirements by reasoning step-by-step through the taxonomy hierarchy, using few-shot retrieval and confidence-based exploration to achieve accurate multi-label decisions. We validate TRClass using aerospace software requirements as a representative case study for safety-critical industries. Results show that TRClass consistently outperforms baselines, with all components contributing to its overall effectiveness, and remains robust across different LLM configurations. A user study further confirms its practical usability in real-world industrial scenarios.

The reuse of requirements artifacts is essential for software development, particularly in aerospace systems where high reliability and efficiency are paramount. However, current methods for managing these artifacts are predominantly manual and costly, as the artifacts are dispersed across multiple documents and exist in heterogeneous formats. Leveraging recent advances in large language models (LLMs) offers a promising opportunity for automating and scaling requirements reuse. Nonetheless, this approach faces two critical challenges: (1) encapsulating scattered, diverse requirement artifacts into coherent and reusable components, and (2) organizing these components into a structured, easily retrievable library. To address these challenges, we introduce AeroR, a novel format for encapsulating aerospace requirements artifacts, and propose AERORM, an LLM-based method for automated requirements artifact management. AERORM operates in two phases: first, it consolidates requirements from disparate sources into reusable components (i.e., AeroRs); then, it organizes these AeroRs into a hierarchical library to enable efficient retrieval. We validate AERORM on artifacts from six aerospace projects, successfully encapsulating 1,624 AeroRs. A user study with senior engineers shows that 67% of sampled AeroRs are high-quality, and a comparative retrieval study across 12 configurations achieves a best-case Recall@10 exceeding 80%. These results demonstrate the potential of AERORM to automate requirements reuse at scale, offering a practical solution for safety-critical domains.

Autonomous Unmanned Systems (AUSs) emerge to replace human operators for better efficiency and effectiveness, especially in harsh and dangerous environments which frequently imply uncertainty. Safety has become one of the top concerns for AUS designs. To address AUS safety concerns systematically, we aim to establish a comprehensive taxonomy of AUS safety and provide a safety-by-design framework for architecting safer AUSs. We conduct a systematic literature review on 65 primary studies and analyze them from three perspectives: system and environment features, safety threats, and countermeasures. We adopt feature models to organize the survey results and establish a taxonomy for AUSs safety issues. Based on the taxonomy, we figure out a reference architecture that integrates three control loops dealing with the uncertainty of operating environments, external threats and system deviations, respectively. Our survey reveals that AUS safety is still a formative field and presents a taxonomy for AUSs safety issues and a safe-by-design framework for architecting safer AUSs.

Autonomous Driving Systems (ADSs) are complex systems that must satisfy multiple safety requirements. In particular cases, all the requirements cannot be satisfied at the same time, and the control software of the ADS must make trade-offs among their satisfaction. Usually, the trading-offs in the decision-making process are configurable; different configuration options can affect driving behaviors, satisfying or violating requirements at different degrees. Therefore, it is highly important to know whether a configuration can guarantee a safe drive or not, i.e., whether it leads to requirement violations that exceed the allowable range or not. However, there is currently no approach to systematically assess the safety of ADS configurations from the perspective of requirements violations. To bridge this gap, this paper proposes a “Hierarchical Safety Assessment” approach (HSA) that is able to quantitatively analyze the violation severity of safety requirements and distinguish safer ADS configurations based on the requirements violations comparison done in a hierarchical way by following requirements importance. We apply HSA to an industrial ADS under six traffic situations. Evaluation results show that HSA is effective in distinguishing safer configurations and provides useful feedback to ADS engineers to reconfigure the ADS in a better way.

Autonomous Driving Systems (ADSs) are complex systems that must satisfy multiple requirements such as safety, compliance to traffic rules, and comfortableness. However, satisfying all these requirements may not always be possible due to emerging environmental conditions. Therefore, the ADSs may have to make trade-offs among multiple requirements during the ongoing operation, resulting in one or more requirements violations. For ADS engineers, it is highly important to know which combinations of requirements violations may occur, as different combinations can expose different types of failures. However, there is currently no testing approach that can generate scenarios to expose different combinations of requirements violations. To address this issue, in this paper, we introduce the notion of requirements violation pattern to characterize a specific combination of requirements violations. Based on this notion, we propose a testing approach named EMOOD that can effectively generate test scenarios to expose as many requirements violation patterns as possible. EMOOD uses a prioritization technique to sort all possible patterns to search for, from the most to the least critical ones. Then, EMOOD iteratively includes an evolutionary many-objective optimization algorithm to find different combinations of requirements violations. In each iteration, the targeted pattern is determined by a dynamic prioritization technique to give preferences to those patterns with higher criticality and higher likelihood to occur. We apply EMOOD to an industrial ADS under two common traffic situations. Evaluation results show that EMOOD outperforms three baseline approaches in generating test scenarios by discovering more requirements violation patterns.

During flights, an unmanned aerial vehicle (UAV) may not be allowed to move across certain areas due to soft constraints such as privacy restrictions. Current methods on self-adaption focus mostly on motion planning such that the trajectory does not trespass predetermined restricted areas. When the environment is cluttered with uncertain obstacles, however, these motion planning algorithms are not flexible enough to find a trajectory that satisfies additional privacy-preserving requirements within a tight time budget during the flights. In this paper, we propose a privacy risk aware motion planning method through the reconfiguration of privacy-sensitive sensors. It minimises environmental impact by re-configuring the sensor during flight, while still guaranteeing the safety and energy hard constraints such as collision avoidance and timeliness. First, we formulate a model for assessing privacy risks of dynamically detected restricted areas. In case the UAV cannot find a feasible solution to satisfy both hard and soft constraints from the current configuration, our decision making method can then produce an optimal reconfiguration of the privacy-sensitive sensor with a more efficient trajectory. We evaluate the proposal through various simulations with different settings in a virtual environment and also validate the approach through real test flights on DJI Matrice 100 UAV.

Autonomous unmanned systems (AUS) emerge to take place of human operators in harsh or dangerous environments. However, such environments are typically dynamic and uncertain, causing unanticipated accidents when autonomous behaviours are no longer safe. Even though safe autonomy has been considered in the literature, little has been done to address the environmental safety requirements of AUS systematically. In this paper, we conduct a systematical literature review and set up a taxonomy of environment-centric safety requirements for AUS. We then analyse the neglected issues to suggest several new research directions towards the vision of environmental-centric safe autonomy.