Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

PLACIDUS: Engineering Product Lines of Rigorous Assurance Cases

Logan Murphy, Torin Viger, Alessio Di Sandro, Marsha Chechik

TL;DR

The paper tackles the challenge of producing rigorous assurance cases for software product lines (SPLs) where building product-specific ACs is infeasible. It introduces PLACIDUS, a lifted, formal-methods–driven methodology that integrates SPLE with formal verification by formalizing variability-aware AC semantics in Lean and providing Eclipse-based tooling for lifted development. Key contributions include a formal theory of variational ACs, lifting templates and analyses to SPLs, and a demonstrative partial PL AC for a medical-device product line. The approach enables scalable, provably correct assurance across entire product families, offering reusable proofs and evidence that reflect variability points in SPL design.

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.

PLACIDUS: Engineering Product Lines of Rigorous Assurance Cases

TL;DR

The paper tackles the challenge of producing rigorous assurance cases for software product lines (SPLs) where building product-specific ACs is infeasible. It introduces PLACIDUS, a lifted, formal-methods–driven methodology that integrates SPLE with formal verification by formalizing variability-aware AC semantics in Lean and providing Eclipse-based tooling for lifted development. Key contributions include a formal theory of variational ACs, lifting templates and analyses to SPLs, and a demonstrative partial PL AC for a medical-device product line. The approach enables scalable, provably correct assurance across entire product families, offering reusable proofs and evidence that reflect variability points in SPL design.

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.
Paper Structure (6 sections, 4 figures)

This paper contains 6 sections, 4 figures.

Table of Contents

  1. Introduction
  2. Background & Related Work
  3. Assurance Cases and GSN
  4. Software Product Lines
  5. Building Product Lines of Assurance Cases with PLACIDUS
  6. Formal Foundations of Lifted Assurance Case Development

Figures (4)

  • Figure 1: Brute-force vs. lifted development of rigorous ACs for product lines.
  • Figure 2: An AC fragment (in GSN) for a hypothetical system. This AC is obtained by instantiating a generic model checking template with model ${\tt M\_SYS}$ and CTL specification ${\tt ALARM\_SPEC}$.
  • Figure 3: A Featured Transition System (FTS) over features $\mathbb{F} = \{{\tt A}, {\tt B}\}$ and feature model $\Phi = {\tt A} ~{\tt xor}~ {\tt B}$ (adapted from beek2019static).
  • Figure 4: Three assurance engineering methodologies: traditional assurance engineering (A); proof-driven assurance engineering (B); lifted, proof-driven assurance engineering via $\mathsf{PLACIDUS}$ (C).

Theorems & Definitions (2)

  • definition thmcounterdefinition: Lifting Murphy2023ReusingYF
  • definition thmcounterdefinition: Variational Proof