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.
翻译:安全临界软件系统在许多情况下是作为产品系列设计和实施的,通常称为软件产品系列(SPL),SPL内的产品在包括哪些特点方面各不相同。将现有分析技术应用到SPL及其安全案例通常具有挑战性,因为与支持特性数量有关的产品数量可能指数化。在本文件中,我们为现有单一产品安全分析向产品系列提供经认证的方法和基础设施。为了保证我们基础设施的认证安全,我们用互动的理论验证来实施,包括正式定义、脂质、正确性标准标定标语和证明。我们运用这一基础设施来正式确定和取消变化影响评估算法。我们提出了取消算法的正式定义,概述了其正确性证明(在网上提供经机器检查的完整证据),并讨论了其在模式管理框架内的执行情况。