Assurance Case Development for Evolving Software Product Lines: A Formal Approach

• URL: http://arxiv.org/abs/2511.03026v1
• Date: Tue, 04 Nov 2025 21:52:14 GMT
• Title: Assurance Case Development for Evolving Software Product Lines: A Formal Approach
• Abstract summary: In critical software engineering, structured assurance cases (ACs) are used to demonstrate how key system properties are supported by evidence.<n>This article describes a formal approach to lifted AC development and regression analysis.<n>We formalize a language of variability-aware ACs for SPLs and study the lifting of template-based AC development.
• Score: 5.038351795081423
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: In critical software engineering, structured assurance cases (ACs) are used to demonstrate how key system properties are supported by evidence (e.g., test results, proofs). Creating rigorous ACs is particularly challenging in the context of software product lines (SPLs), i.e, sets of software products with overlapping but distinct features and behaviours. Since SPLs can encompass very large numbers of products, developing a rigorous AC for each product individually is infeasible. Moreover, if the SPL evolves, e.g., by the modification or introduction of features, it can be infeasible to assess the impact of this change. Instead, the development and maintenance of ACs ought to be lifted such that a single AC can be developed for the entire SPL simultaneously, and be analyzed for regression in a variability-aware fashion. In this article, we describe a formal approach to lifted AC development and regression analysis. We formalize a language of variability-aware ACs for SPLs and study the lifting of template-based AC development. We also define a regression analysis to determine the effects of SPL evolutions on variability-aware ACs. We describe a model-based assurance management tool which implements these techniques, and illustrate our contributions by developing an AC for a product line of medical devices.

Related papers

• LLMs in Digital EDA: A perspective on shifting roles from Generation to Orchestration [0.0]
  Large language models (LLMs) enable direct translation from design intent to hardware implementations.<n>This Perspective defines three hierarchical roles that reveal how capability accumulates.<n>This reveals a syntax trap in which models are trained to produce plausible code rather than physically correct hardware.
  arXiv  Detail & Related papers  (2026-08-27T14:29:35Z)
• How Do Developers Maintain and Evolve Their Agents' Instructions? An Empirical Study [9.708580060106414]
  Agent Context Files (ACFs) have emerged as a practical mechanism to guide agents through structured instructions.<n>This paper plans to investigate the evolution of ACFs and their role in agent-driven development.
  arXiv  Detail & Related papers  (2026-06-24T00:32:18Z)
• AI Harness Engineering: A Runtime Substrate for Foundation-Model Software Agents [1.4323566945483497]
  Foundation models have transformed automated code generation, yet autonomous software-engineering agents remain unreliable in realistic development settings.<n>We propose a model-harness-environment system in which a runtime substrate mediates how a foundation-model agent observes a project, acts on it, receives feedback, and establishes that a change is complete.<n>The framework reframes the central question of autonomous software engineering from whether a foundation model can produce a patch to whether the model-harness-environment system can produce a verifiably correct, attributed, and maintainable change.
  arXiv  Detail & Related papers  (2026-05-13T11:14:59Z)
• Qwen-Scope: Turning Sparse Features into Development Tools for Large Language Models [80.45129499188461]
  We introduce Qwen-Scope, an open-source suite of sparse autoencoders (SAEs) built on the Qwen model family.<n>We show that SAEs can go beyond post-hoc analysis to serve as practical interfaces for model development along four directions.
  arXiv  Detail & Related papers  (2026-05-12T10:01:06Z)
• Environment-Aware Code Generation: How far are We? [52.69113158357018]
  It is unclear whether large language models (LLMs) can reliably generate executable code tailored to a user's specific environment.<n>We present the first systematic study of Environment-Aware Code Generation (EACG), where generated code must be functionally correct and directly executable under arbitrary software configurations.<n>Our results show that current LLMs struggle with environment-specific code generation, while our adaptations improve environment compatibility and executability.
  arXiv  Detail & Related papers  (2026-01-18T04:58:15Z)
• A Causal Perspective on Measuring, Explaining and Mitigating Smells in LLM-Generated Code [49.09545217453401]
  Propensity Smelly Score (PSC) is a metric that estimates the likelihood of generating particular smell types.<n>We identify how generation strategy, model size, model architecture and prompt formulation shape the structural properties of generated code.<n> PSC helps developers interpret model behavior and assess code quality, providing evidence that smell propensity signals can support human judgement.
  arXiv  Detail & Related papers  (2025-11-19T19:18:28Z)
• Verifying Correctness of PLC Software during System Evolution using Model Containment Approach [22.261628532402067]
  We propose a verification-based approach to ensure the correctness of the upgraded version of a PLC software.<n>We have developed a home-grown Petri net-based containment checker.<n>We have compared our approach with verifAPS, a popular tool used for software upgradation, and observed nearly 4x performance improvement.
  arXiv  Detail & Related papers  (2025-09-06T04:45:17Z)
• LASA: Enhancing SoC Security Verification with LLM-Aided Property Generation [7.52190283487474]
  Formal property verification (FPV) provides the capability to model and validate design behaviors.<n>Current practices require significant manual efforts to create such properties, making them time-consuming, costly, and error-prone.<n>This paper presents LASA, a novel framework that leverages LLMs and retrieval-augmented generation (RAG) to produce non-vacuous security properties.
  arXiv  Detail & Related papers  (2025-06-22T01:21:03Z)
• Self-Refinement Strategies for LLM-based Product Attribute Value Extraction [51.45146101802871]
  This paper investigates applying two self-refinement techniques to the product attribute value extraction task.<n>The experiments show that both self-refinement techniques fail to significantly improve the extraction performance while substantially increasing processing costs.<n>For scenarios with development data, fine-tuning yields the highest performance, while the ramp-up costs of fine-tuning are balanced out as the amount of product descriptions increases.
  arXiv  Detail & Related papers  (2025-01-02T12:55:27Z)
• KaPQA: Knowledge-Augmented Product Question-Answering [59.096607961704656]
  We introduce two product question-answering (QA) datasets focused on Adobe Acrobat and Photoshop products. We also propose a novel knowledge-driven RAG-QA framework to enhance the performance of the models in the product QA task.
  arXiv  Detail & Related papers  (2024-07-22T22:14:56Z)
• PLACIDUS: Engineering Product Lines of Rigorous Assurance Cases [1.71849622776539]
  In critical software engineering, structured assurance cases (ACs) are used to demonstrate how key properties are supported by evidence artifacts. We propose PLACIDUS, a methodology for integrating formal methods and software product line engineering to develop provably correct ACs for SPLs.
  arXiv  Detail & Related papers  (2024-07-14T22:13:44Z)
• Integrated Modeling, Verification, and Code Generation for Unmanned Aerial Systems [10.292890852621346]
  Unmanned Aerial Systems (UAS) are widely used in safety-critical fields such as industrial production, military operations, and disaster relief. This paper aims to investigate an integrated approach to modeling, verification, and code generation for UAS.
  arXiv  Detail & Related papers  (2024-06-13T14:53:40Z)
• Transformers as Statisticians: Provable In-Context Learning with In-Context Algorithm Selection [88.23337313766353]
  This work first provides a comprehensive statistical theory for transformers to perform ICL. We show that transformers can implement a broad class of standard machine learning algorithms in context. A emphsingle transformer can adaptively select different base ICL algorithms.
  arXiv  Detail & Related papers  (2023-06-07T17:59:31Z)
• Progressive Open-Domain Response Generation with Multiple Controllable Attributes [13.599621571488033]
  We propose a Progressively trained Hierarchical Vari-Decoder (PHED) to tackle this task. PHED deploys Conditional AutoEncoder (CVAE) on Transformer to include one aspect of attributes at one stage. PHED significantly outperforms the state-of-the-art neural generation models and produces more diverse responses as expected.
  arXiv  Detail & Related papers  (2021-06-07T08:48:39Z)
• DirectDebug: Automated Testing and Debugging of Feature Models [55.41644538483948]
  Variability models (e.g., feature models) are a common way for the representation of variabilities and commonalities of software artifacts. Complex and often large-scale feature models can become faulty, i.e., do not represent the expected variability properties of the underlying software artifact.
  arXiv  Detail & Related papers  (2021-02-11T11:22:20Z)
• Hierarchical Variational Autoencoder for Visual Counterfactuals [79.86967775454316]
  Conditional Variational Autos (VAE) are gathering significant attention as an Explainable Artificial Intelligence (XAI) tool. In this paper we show how relaxing the effect of the posterior leads to successful counterfactuals. We introduce VAEX an Hierarchical VAE designed for this approach that can visually audit a classifier in applications.
  arXiv  Detail & Related papers  (2021-02-01T14:07:11Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.