Towards Certified Analysis of Software Product Line Safety Cases

TL;DR

This paper introduces a formal, certified methodology for extending safety analysis techniques from individual software products to entire software product lines using theorem proving, ensuring safety guarantees across all variants.

Contribution

It presents a novel infrastructure for certified lifting of safety analyses to SPLs, formalized and verified within an interactive theorem prover.

Findings

Formal definition of lifted Change Impact Assessment algorithm

Machine-checked correctness proof of the lifting process

Implementation within a model management framework

Abstract

Safety-critical software systems are in many cases designed and implemented as families of products, usually referred to as Software Product Lines (SPLs). Products within an SPL vary from each other in terms of which features they include. Applying existing analysis techniques to SPLs and their safety cases is usually challenging because of the potentially exponential number of products with respect to the number of supported features. In this paper, we present a methodology and infrastructure for certified \emph{lifting} of existing single-product safety analyses to product lines. To ensure certified safety of our infrastructure, we implement it in an interactive theorem prover, including formal definitions, lemmas, correctness criteria theorems, and proofs. We apply this infrastructure to formalize and lift a Change Impact Assessment (CIA) algorithm. We present a formal definition of the lifted algorithm, outline its correctness proof (with the full machine-checked proof available online), and discuss its implementation within a model management framework.