PLACIDUS: Engineering Product Lines of Rigorous Assurance Cases

• URL: http://arxiv.org/abs/2407.10345v1
• Date: Sun, 14 Jul 2024 22:13:44 GMT
• Title: PLACIDUS: Engineering Product Lines of Rigorous Assurance Cases
• Abstract summary: 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.
• Score: 1.71849622776539
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: In critical software engineering, structured assurance cases (ACs) are used to demonstrate how key properties (e.g., safety, security) are supported by evidence artifacts (e.g., test results, proofs). ACs can also be studied as formal objects in themselves, such that formal methods can be used to establish their correctness. Creating rigorous ACs is particularly challenging in the context of software product lines (SPLs), wherein a family of related software products is engineered simultaneously. Since creating individual ACs for each product is infeasible, AC development must be lifted to the level of product lines. In this work, we propose PLACIDUS, a methodology for integrating formal methods and software product line engineering to develop provably correct ACs for SPLs. To provide rigorous foundations for PLACIDUS, we define a variability-aware AC language and formalize its semantics using the proof assistant Lean. We provide tool support for PLACIDUS as part of an Eclipse-based model management framework. Finally, we demonstrate the feasibility of PLACIDUS by developing an AC for a product line of medical devices.

Related papers

• ABC-Bench: Benchmarking Agentic Backend Coding in Real-World Development [72.4729759618632]
  We introduce ABC-Bench, a benchmark to evaluate agentic backend coding within a realistic, executable workflow.<n>We curated 224 practical tasks spanning 8 languages and 19 frameworks from open-source repositories.<n>Our evaluation reveals that even state-of-the-art models struggle to deliver reliable performance on these holistic tasks.
  arXiv  Detail & Related papers  (2026-01-16T08:23:52Z)
• Towards Verifiably Safe Tool Use for LLM Agents [53.55621104327779]
  Large language model (LLM)-based AI agents extend capabilities by enabling access to tools such as data sources, APIs, search engines, code sandboxes, and even other agents.<n>LLMs may invoke unintended tool interactions and introduce risks, such as leaking sensitive data or overwriting critical records.<n>Current approaches to mitigate these risks, such as model-based safeguards, enhance agents' reliability but cannot guarantee system safety.
  arXiv  Detail & Related papers  (2026-01-12T21:31:38Z)
• Aligning Security Compliance and DevOps: A Longitudinal Study [5.128220263390701]
  RefA is a prescriptive model of a security compliant DevOps lifecycle based on the IEC 62443-4-1 standard.<n>We demonstrate how RefA facilitates the transfer of security compliance knowledge to product development teams.
  arXiv  Detail & Related papers  (2025-12-16T14:43:14Z)
• Assurance Case Development for Evolving Software Product Lines: A Formal Approach [5.038351795081423]
  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.
  arXiv  Detail & Related papers  (2025-11-04T21:52:14Z)
• Knowledge-Guided Multi-Agent Framework for Application-Level Software Code Generation [47.691865459572995]
  This paper envisions a Knowledge-Guided Application-Level Code Generation framework named KGACG.<n> KGACG aims to trans- form software requirements specification and architectural design document into executable code.
  arXiv  Detail & Related papers  (2025-10-22T03:10:58Z)
• Requirements Development and Formalization for Reliable Code Generation: A Multi-Agent Vision [45.59678433715798]
  We envision the first multi-agent framework for reliable code generation based on textscrequirements textscdevelopment and textscformalization, named textscReDeFo.<n>The core of textscReDeFo is the use of formal specifications to bridge the gap between potentially ambiguous natural language requirements and precise executable code.
  arXiv  Detail & Related papers  (2025-08-26T04:45:04Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  Code generation with large language models (LLMs) is increasingly adopted in production but fails to ensure code quality.<n>We propose REAL, a reinforcement learning framework that incentivizes LLMs to generate production-quality code.
  arXiv  Detail & Related papers  (2025-05-28T17:57:47Z)
• OntoGSN: An Ontology for Dynamic Management of Assurance Cases [0.3999851878220878]
  We present OntoGSN: an ontology and supporting OWL for managing ACs in the Goalcturing Notation (GSN) standard.<n>OntoGSN offers a knowledge representation and a queryable graph that can be automatically, evaluated, and updated.<n>We demonstrate the utility of our contributions in an example involving assurance of robustness in large language models.
  arXiv  Detail & Related papers  (2025-05-20T08:15:16Z)
• APE-Bench I: Towards File-level Automated Proof Engineering of Formal Math Libraries [5.227446378450704]
  APE-Bench I is the first realistic benchmark built from real-world commit histories of Mathlib4. Eleanstic is a scalable parallel verification infrastructure optimized for proof checking across multiple versions of Mathlib.
  arXiv  Detail & Related papers  (2025-04-27T05:04:02Z)
• Using Assurance Cases to Guide Verification and Validation of Research Software [0.0]
  We illustrate how ACs can guide VnV activities via a case study of software for automatically extracting the 3D segmentation of the aorta from medical images of the chest. The case study highlights that code is not the only artifact of interest for building confidence and that making an explicit distinction between software and user responsibilities is useful.
  arXiv  Detail & Related papers  (2024-11-05T17:39:32Z)
• Designing and Implementing a Generator Framework for a SIMD Abstraction Library [53.84310825081338]
  We present TSLGen, a novel end-to-end framework for generating an SIMD abstraction library. We show that our framework is comparable to existing libraries, and we achieve the same performance results.
  arXiv  Detail & Related papers  (2024-07-26T13:25:38Z)
• 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)
• Automating SBOM Generation with Zero-Shot Semantic Similarity [2.169562514302842]
  A Software-Bill-of-Materials (SBOM) is a comprehensive inventory detailing a software application's components and dependencies. We propose an automated method for generating SBOMs to prevent disastrous supply-chain attacks. Our test results are compelling, demonstrating the model's strong performance in the zero-shot classification task.
  arXiv  Detail & Related papers  (2024-02-03T18:14:13Z)
• InferAligner: Inference-Time Alignment for Harmlessness through Cross-Model Guidance [56.184255657175335]
  We develop textbfInferAligner, a novel inference-time alignment method that utilizes cross-model guidance for harmlessness alignment. Experimental results show that our method can be very effectively applied to domain-specific models in finance, medicine, and mathematics. It significantly diminishes the Attack Success Rate (ASR) of both harmful instructions and jailbreak attacks, while maintaining almost unchanged performance in downstream tasks.
  arXiv  Detail & Related papers  (2024-01-20T10:41:03Z)
• Operationalizing Assurance Cases for Data Scientists: A Showcase of Concepts and Tooling in the Context of Test Data Quality for Machine Learning [1.6403311770639912]
  Assurance Cases (ACs) are an established approach in safety engineering to argue quality claims in a structured way. We propose a framework to support the operationalization of ACs for Machine Learning (ML) components based on technologies that data scientists use on a daily basis: Python and Jupyter Notebook. Results from the application of the framework, documented through notebooks, can be integrated into existing AC tools.
  arXiv  Detail & Related papers  (2023-12-08T09:34:46Z)
• Simulation-based Safety Assurance for an AVP System incorporating Learning-Enabled Components [0.6526824510982802]
  Testing, verification and validation AD/ADAS safety-critical applications remain as one the main challenges. We explain the simulation-based development platform that is designed to verify and validate safety-critical learning-enabled systems.
  arXiv  Detail & Related papers  (2023-09-28T09:00:31Z)
• OpenICL: An Open-Source Framework for In-context Learning [48.75452105457122]
  We introduce OpenICL, an open-source toolkit for In-context Learning (ICL) and large language model evaluation. OpenICL is research-friendly with a highly flexible architecture that users can easily combine different components to suit their needs. The effectiveness of OpenICL has been validated on a wide range of NLP tasks, including classification, QA, machine translation, and semantic parsing.
  arXiv  Detail & Related papers  (2023-03-06T06:20:25Z)
• Lessons from Formally Verified Deployed Software Systems (Extended version) [65.69802414600832]
  This article examines a range of projects, in various application areas, that have produced formally verified systems and deployed them for actual use. It considers the technologies used, the form of verification applied, the results obtained, and the lessons that the software industry should draw regarding its ability to benefit from formal verification techniques and tools.
  arXiv  Detail & Related papers  (2023-01-05T18:18:46Z)
• SMT-Based Safety Verification of Data-Aware Processes under Ontologies (Extended Version) [71.12474112166767]
  We introduce a variant of one of the most investigated models in this spectrum, namely simple artifact systems (SASs) This DL, enjoying suitable model-theoretic properties, allows us to define SASs to which backward reachability can still be applied, leading to decidability in PSPACE of the corresponding safety problems.
  arXiv  Detail & Related papers  (2021-08-27T15:04:11Z)
• Safe RAN control: A Symbolic Reinforcement Learning Approach [62.997667081978825]
  We present a Symbolic Reinforcement Learning (SRL) based architecture for safety control of Radio Access Network (RAN) applications. We provide a purely automated procedure in which a user can specify high-level logical safety specifications for a given cellular network topology. We introduce a user interface (UI) developed to help a user set intent specifications to the system, and inspect the difference in agent proposed actions.
  arXiv  Detail & Related papers  (2021-06-03T16:45:40Z)

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.