PLACIDUS：面向严格保障案例的工程化产品线
软件工程
2024-07-16 v1
摘要
在关键软件工程中，使用结构化保障案例(AC)来展示关键属性(如安全、安全)如何由证据构件(如测试结果、证明)所支持。AC也可作为自身的形式化对象，以便使用形式化方法来确立其正确性。在软件产品线(SPL)背景下构建严格的AC尤为具有挑战性，因为需要同时工程化一族相关软件产品。由于为每个产品构建单独的AC是不可行的，AC开发必须提升到产品线层面。本文提出了PLACIDUS，一种将形式化方法与软件产品线工程集成以开发SPLs可证明正确AC的方法。为了为PLACIDUS提供严格基础，我们定义了一种具备可变性的AC语言，并使用证明助手Lean形式化其语义。我们提供了作为Eclipse基于模型管理框架的一部分的工具支持。最后，我们通过为一款医疗设备产品线开发AC来展示PLACIDUS的可行性。
引用
@article{arxiv.2407.10345,
title = {PLACIDUS: Engineering Product Lines of Rigorous Assurance Cases},
author = {Logan Murphy and Torin Viger and Alessio Di Sandro and Marsha Chechik},
journal= {arXiv preprint arXiv:2407.10345},
year = {2024}
}