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.

We give an introduction to the MARS toolchain for formal modeling and verification of hybrid systems. It consists of translators from Simulink/Stateflow models to Hybrid Communicating Sequential Processes (HCSP), and tools for simulation, code generation, and deductive verification of an HCSP model. We apply the toolchain to model the descent guidance control phase of the recently launched Tianwen I mars lander, and verify that it correctly controls the velocity of the lander.