Requirements engineering digest, week 38 of 2026

1. LLM-enabled Behavior Driven Development Workflow for Formally Verified Hardware Designs

   Luca Müller, Qian Liu, Rolf Drechsler

   arXiv (cs.AR) · preprint

   Introduces Formal Verification Gherkin Scenarios, a controlled natural language for writing hardware specifications that reduces ambiguity while staying interpretable and machine-checkable, and shows the resulting LLM-driven workflow outperforms established methods by 2.48x in RTL functional correctness and 2.54x in formal assertion coverage.

   Abstract

   Recently, the use of Large Language Models (LLMs) for different tasks in the Electronic Design Automation (EDA) life-cycle has been studied extensively, but an integrated view is lacking. Specifications are the foundation of this life-cycle, but they suffer from ambiguity when written in natural language, which especially affects the quality of LLM output. Formal specifications mitigate these ambiguities, but they come with their own challenges. On the other hand, Controlled Natural Language (CNL) specifications can serve as a middle-ground, reducing ambiguity while retaining interpretability. In this work, we propose an integrated view on the use of LLMs for EDA and establish an LLM-enabled behavior driven hardware development workflow. We introduce and define Formal Verification Gherkin Scenarios (FV Gherkin Scenarios), unlocking CNL specifications as the foundation for formally verified hardware designs via Formal Property Verification (FPV). Experimental evaluation shows that our workflow is able to outperform other established LLM-based methods by 2.48x in functional correctness of generated Register Transfer Level (RTL) designs and by 2.54x in formal coverage of generated assertions for FPV.

   Source: arxiv.org/abs/2609.15318

2. A11yLTLNav: Automatic Detection of Accessibility Navigation Failures

   Chenming Ge, Kewen Peng, Chengyang Shi, Ben Greenman, Yue Jiang

   arXiv (cs.HC) · preprint

   Organizes accessibility navigation failures for blind and low-vision screen-reader users into a taxonomy drawn from prior research, formalizes a browser-observable subset as executable Linear Temporal Logic properties, and pairs that with runtime monitoring to catch interaction failures that static checkers miss, confirming 274 of 309 reported failures across 31 generated websites.

   Abstract

   For blind and low-vision (BLV) screen-reader users, a website that appears accessible in a static snapshot can become difficult or impossible to navigate once interaction begins. Yet, most automated accessibility checkers miss failures involving focus, interface state, and accessible feedback across interactions. We present A11yLTLNav, a property-based approach for automatically detecting accessibility navigation failures. Through a structured review of prior research, we organize accessibility navigation failures into a failure taxonomy and formalize a browser-observable subset as executable Linear Temporal Logic properties over action-state traces. A11yLTLNav combines random keyboard exploration with runtime property monitoring to detect these failures during interactions. We evaluate A11yLTLNav on 31 generated websites based on real-world websites and tasks. It reported 309 accessibility failures, of which 274 were confirmed, achieving 88.7% precision and identifying more confirmed failures than the comparison checkers. Our results show that A11yLTLNav transforms accessibility knowledge into reusable checks of interface behavior over time.

   Source: arxiv.org/abs/2609.17959

3. Relationally Guided Use Case Modeling with LLMs

   Guangyu Wang, Bangqi Li, Ji Wu, Zhijun Shao

   arXiv (cs.SE) · preprint

   Proposes FlowGen, which extracts semantic elements from natural-language use case descriptions into a relational graph to generate basic flows, predict branch points, and construct alternative flows automatically, outperforming competitive baselines by double-digit margins across 13 public and 7 industrial datasets.

   Abstract

   Use case flows are important elements of use case modeling because they support downstream software engineering activities, including requirements analysis, architectural and detailed design, and test case generation. However, constructing them manually is costly and expertise-intensive, while existing automated approaches still struggle to preserve semantic consistency, control-flow logic, data-flow logic, and the intended system boundary, especially when identifying branch points and generating alternative flows. To address this problem, we propose FlowGen for complete use case flow construction. FlowGen uses LLM-based Semantic Information Processing (SIP) to extract semantic elements, constructs a Semantic Relational Graph (SRG) encoded by an enhanced R-GAT for basic flow generation (BFGen), and further supports branch point prediction through BPP and branch-conditioned alternative flow generation through AFGen. Evaluations on 13 public and 7 industrial datasets show that FlowGen consistently outperforms competitive baselines in all three core components. In particular, BFGen improves over the best baseline by 14% in Precision, 7-25% in Recall, 11-30% in F1, and 10-19% in AUC; BPP improves Precision by 30-110%, Recall by 33-91%, and F1 by 32-117%; AFGen improves Precision by 8-23%, F1 by 5-18%, and AUC by 0.6-2.5%. Moreover, we validate the effectiveness of the LLM-based SIP module and the attention preservation factor in BFGen, analyze the impact of requirement completeness on BFGen, and examine how different scopes of branch-related context affect AFGen.

   Source: arxiv.org/abs/2609.18291

4. Code-as-Auditor: Executable Compliance Reasoning via Regulation-to-Code

   Jisoo Kim, Taeyoon Kwack, Jinwoo Jang, Woo Kyung Kim, Honguk Woo

   arXiv (cs.SE) · preprint

   Translates regulatory text into formalized checklists and executable decision trees, then dynamically expands each checklist item into factual and counterfactual questions grounded in case evidence, improving the accuracy and traceability of automated privacy and data-protection compliance assessments over ungrounded LLM reasoning.

   Abstract

   Large Language Models (LLMs) are increasingly adopted for compliance and legal reasoning tasks, yet their outputs often lack explicit grounding in legal logic and evidence. We present Code-as-Auditor, an LLM-based framework that extends the model's reasoning capability toward structured and evidence-grounded compliance assessment. The framework translates regulatory information into (1) formalized checklists and executable decision trees, encoding regulations and conditions as interpretable code structures. During inference, each checklist item is (2) dynamically expanded into factual and counterfactual questions, guiding the model to reason over case-specific evidence and potential violations. This process establishes a reasoning pipeline that proceeds from evidence identification, through rule application, to final decision-making, while a self-verification loop improves the logical consistency of the generated code and the traceability of outcomes. Experiments on privacy and data protection scenarios demonstrate that Code-as-Auditor delivers more accurate and evidence-backed evaluations, enabling automated compliance regulation checking grounded in explicit regulatory criteria.

   Source: arxiv.org/abs/2609.19199

5. Mind the Gap: How SBOM Specification Ambiguities Lead to Divergent Software Bills of Materials. An Empirical Tool Study

   Alan Prado, Olivier Zendra, Philippe Boinot, Olivier Barais

   arXiv (cs.CR) · preprint

   An empirical study of three widely used SBOM generators across more than 3,000 JavaScript and Rust projects finding that most divergence between their outputs is systematic rather than accidental, tracing back to underspecified dependency scope, naming, and provenance rules in the SBOM specifications themselves, just as the EU Cyber Resilience Act is about to make SBOMs a legal compliance requirement.

   Abstract

   Software Bill of Materials (SBOMs) will become mandatory starting in December 2027 under the European Cyber Resilience Act (CRA) [8]. Although previous studies have highlighted significant differences among SBOM generators, the reasons for these discrepancies remain unknown, as does whether they stem from implementation errors or deliberate design choices. In this paper, we evaluate three widely used SBOM generators across more than 3,000 JavaScript and Rust projects, using a groundtruth baseline derived from dependency lockfiles. Our results show that these tools diverge in terms of both dependency coverage and SBOM completeness. Importantly, most of these discrepancies are systematic rather than accidental: they arise from differing assumptions regarding dependency scope, naming, provenance, and representation, while others reflect inconsistent support for fields defined in SBOM specifications. These findings demonstrate that many of the observed discrepancies cannot simply be ''fixed'': they require clearer standardization. As SBOM generation becomes a legal compliance requirement, the choice of tool itself can influence the resulting SBOM, potentially becoming a source of undetected non-compliance. We argue that future SBOM standards should define canonical rules regarding dependency scope, provenance, and representation to improve interoperability and compliance.

   Source: arxiv.org/abs/2609.19920

6. SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs?

   George Ma, Benjamin Mikek, Haoyu Li, Ferhat Erata, Yuhao Zhang, Zeren Shui, Behrooz Omidvar Tehrani, Jun Huan, Murali Krishna Ramanathan, Somayeh Sojoudi, Hao Zhou, Anoop Deoras

   arXiv (cs.LG) · preprint

   A pipeline that turns a real GitHub issue and its accepted patch into a formal specification and machine-checked proof obligation, finding that a correct formal specification lifts issue-resolution rates well above test-based checking, but that models writing their own specifications gain nothing over an unaided baseline because most fail an audit for faithfully constraining the required behavior.

   Abstract

   Ensuring the correctness of LLM-generated code is a core challenge for modern software engineering. Benchmarks for agentic code generation check correctness with held-out test suites, which are inherently incomplete and increasingly susceptible to memorization. Formal verification avoids both problems, but existing work covers only standalone tasks whose specifications are given as input, not real issues, which touch large repositories and state intent in vague natural language. We present Benchproofer, a pipeline that turns a coding task with a known correct patch into a formally verified one: it writes a specification for the new code, summarizes the existing functions that code calls with axioms, and admits an instance only after mechanical and adversarial gates agree. Applying it to SWE-bench Verified yields SWE-Proof, 500 real issues whose correctness is formally verified rather than tested, and it extends to SWE-bench Pro. Across two frontier models, verification catches what tests miss: a quarter to a half of test-passing patches admit counterexamples, which a structured natural-language specification does not fix, while a correct formal one lifts resolution from 85% to 95% for Opus 4.8. Writing that specification is the hard part: models that must write their own gain nothing over an unaided baseline, and only 62% of their specifications pass our audit. The usual failure is faithfulness, a specification that constrains part of the required behavior and leaves the rest free. Specification quality still tracks the outcome, failing on 89% of unresolved instances against 47% of resolved ones, making faithful specification synthesis a concrete open problem.

   Source: arxiv.org/abs/2609.21190

7. Code generation for legal metadata extraction: a decomposition-based in-context learning approach

   Anmol Singhal, Travis Breaux

   Requirements Engineering Journal · published

   A decomposition-based in-context learning method that turns legal regulatory text into executable Python code capturing structural and semantic legal metadata and their interrelationships, reaching 90.5% semantic accuracy at extracting legal requirements from US data-breach notification laws and generalizing to the unseen federal COPPA statute.

   Abstract

   Software systems must comply with legal regulations, which is a resource-intensive task, particularly for small organizations and startups lacking dedicated legal expertise. Extracting metadata from regulations to elicit legal requirements for software is a critical step to ensure compliance. However, it is a cumbersome task due to the length and complex nature of legal text. Although prior work has pursued automated methods for extracting structural and semantic metadata from legal text, they do not consider the interplay and interrelationships among attributes associated with these metadata types, and they rely on manual labeling or heuristic-driven machine learning, which does not always generalize to new documents. In this paper, we introduce a decomposition-based in-context learning method for automatically generating a canonical representation of legal text encoded as executable Python code. Our representation is instantiated from a manually designed Python class structure that serves as a domain-specific metamodel, capturing both structural and semantic legal metadata and their interrelationships. Our corpus contains 13 US state data breach notification laws (332 paragraphs), of which six unseen laws (182 paragraphs) form the held-out test set. On this test set, our proposed method using GPT−5.1 achieves 90.5% semantic test accuracy with a precision of 79.4% and a recall of 81.9%. We also assess the generalizability of the method to the Children’s Online Privacy Protection Act (COPPA), a US federal law. The results demonstrate that, once a domain metamodel and expert-authored examples are available, few-shot code generation can extract legal metadata relationships without training a task-specific supervised model and can be adapted to unseen legislation.

   Source: doi.org/10.1007/s00766-026-00468-7 · doi:10.1007/s00766-026-00468-7

8. Requirements-Based Test Generation: A Comprehensive Survey

   Zhenzhen Yang, Rubing Huang, Chenhui Cui, Nan Niu, Dave Towey

   ACM Transactions on Software Engineering and Methodology · published

   A comprehensive survey of three decades of requirements-based test generation research, categorizing requirements types, generation approaches, resulting test-case types, and available tools, and summarizing industrial applications and open research challenges.

   Abstract

   As an important way of assuring software quality, software testing generates and executes test cases to identify software failures. Many strategies have been proposed to guide test-case generation, such as source code-based approaches and methods based on bug reports. Requirements-based test generation (RBTG) constructs test cases based on specified requirements, aligning with user needs and expectations, without requiring access to the source code. Since its introduction in 1994, there have been many contributions to the development of RBTG, including various approaches, implementations, tools, assessment and evaluation methods, and applications. This article provides a comprehensive survey on RBTG, categorizing requirements types, classifying approaches, investigating types of test cases, summarizing available tools, and analyzing experimental evaluations. This article also summarizes the domains and industrial applications of RBTG and discusses some open research challenges and potential future work.

   The source publishes this abstract as raw markup. Macros have been replaced by the text the publisher's own rendering shows for them, and the rest of the markup removed. The authors' wording is unchanged.

   Source: doi.org/10.1145/3771727 · doi:10.1145/3771727

9. Requirements-Driven Automated Software Testing: A Systematic Review

   Fanyu Wang, Chetan Arora, Chakkrit Tantithamthavorn, Kaicheng Huang, Aldeida Aleti

   ACM Transactions on Software Engineering and Methodology · published

   A systematic literature review of 156 studies, filtered from an initial 27,333, on requirements-driven automated software testing, finding that rule-based transformation techniques dominate over machine-learning approaches and that full automation from requirements to test artifacts remains rare.

   Abstract

   Automated software testing has significant potential to enhance efficiency and reliability within software development processes. However, its broader adoption faces considerable challenges, particularly concerning alignment between test generation methodologies and software requirements. Requirements-Driven Automated Software Testing (REDAST) addresses this gap by systematically leveraging requirements as the foundation for automated test artifact generation. This systematic literature review (SLR) critically examines the REDAST landscape, analyzing the current state of requirements input formats, transformation techniques, generated test artifacts, evaluation methods, and prevailing limitations. We conducted a thorough analysis of 156 relevant studies selected through a rigorous multi-stage filtering process from an initial collection of 27,333 papers sourced from six major research databases. Our findings highlight the predominance of functional requirements, model-based specifications, and natural language formats. Rule-based techniques are extensively utilized, while machine learning-based approaches remain relatively underexplored. Furthermore, most existing frameworks are sequential and dependent on singular intermediate representations, and while test cases, structured textual formats, and requirements coverage are common, full automation remains rare. We identify significant gaps related to automation completeness, and dependency on input quality. This comprehensive synthesis provides a detailed overview of REDAST research and limitations, offering clear, evidence-based recommendations to guide future advancements in automated software testing.

   The source publishes this abstract as raw markup. Macros have been replaced by the text the publisher's own rendering shows for them, and the rest of the markup removed. The authors' wording is unchanged.

   Source: doi.org/10.1145/3767739 · doi:10.1145/3767739

10. Character-level Perturbations in Software Requirements: Evaluating Transformer Models Robustness Across Learning Paradigms and Classification Tasks

    Wejdan Alqahtani, Waad Alhoshan

    International Journal of Computational Intelligence Systems · published

    An empirical study of four transformer models across three requirements classification tasks finding that fine-tuned classifiers lose up to 41.5% accuracy under small amounts of character-level text noise while zero-shot models stay robust, with practical guidance for choosing configurations that hold up on noisy, real-world requirements text.

    Abstract

    Transformer models have shown promising results in software requirements classification. However, their robustness to real-world textual noise remains underexplored. In practice, requirements are frequently affected by typographical errors, transmission artifacts, and optical character recognition mistakes, which can degrade model reliability. This study investigates the robustness of transformer models for requirements classification under character-level adversarial perturbations from two complementary analytical perspectives: transfer learning paradigm and task type. We conduct an empirical evaluation of four models (BERT, RoBERTa, All-MiniLM, and BART) across three transfer learning paradigms (zero-shot, few-shot, and fine-tuning) and three classification tasks of increasing complexity (functional binary, security binary, and NFR multi-class). Experiments are performed on benchmark software requirement datasets perturbed at three character-level noise intensities, where 5%, 10%, and 15% of the characters in each requirement statement are modified. Our results indicate a performance–robustness trade-off across learning paradigms. Zero-shot learning shows notable robustness, with no statistically significant performance degradation, whereas fine-tuning, despite achieving the highest baseline performance, exhibits considerable vulnerability, with degradation of up to 41.5%. With respect to task complexity, security classification shows relatively high robustness (15.2% degradation), while functional and NFR classification are more affected, with degradation rates of 35.4% and 38.2%, respectively. Furthermore, no single transformer model performs consistently well across all settings. These findings offer practical guidance for selecting robust transformer-based configurations for processing software requirements from noisy and imperfect sources.

    Source: doi.org/10.1007/s44196-026-01589-1 · doi:10.1007/s44196-026-01589-1