在關(guān)鍵軟件工程中，結(jié)構(gòu)化保證案例（ACs）用于展示關(guān)鍵系統(tǒng)屬性是如何通過證據(jù)（例如測試結(jié)果、證明）得到支持的。在軟件產(chǎn)品線（SPLs）的背景下創(chuàng)建嚴(yán)謹(jǐn)?shù)?ACs 尤具挑戰(zhàn)性，因?yàn)檐浖a(chǎn)品線包含具有重疊但不同特性和行為的軟件產(chǎn)品。由于軟件產(chǎn)品線可能包含大量產(chǎn)品，為每個產(chǎn)品單獨(dú)開發(fā)嚴(yán)謹(jǐn)?shù)?ACs 是不可行的。此外，如果軟件產(chǎn)品線發(fā)生變化（例如通過修改或引入新特性），評估這種變化的影響也可能變得不可行。因此，應(yīng)該提升ACs 的開發(fā)和維護(hù)方式，以便能夠?yàn)檎麄�軟件產(chǎn)品線同時開發(fā)一個統(tǒng)一的 AC，并以考慮變異性的方式進(jìn)行分析。在本文中，我們描述了一種用于提升 AC 開發(fā)和回歸分析的形式化方法。我們?yōu)檐浖a(chǎn)品線定義了一種考慮變異性的 AC 語言，并研究了基于模板的 AC 開發(fā)的提升機(jī)制。我們還定義了一種回歸分析方法，用于確定軟件產(chǎn)品線變化對考慮變異性的 ACs 的影響。我們描述了一個基于模型的保證管理工具，該工具實(shí)現(xiàn)了這些技術(shù)，并通過為一系列醫(yī)療設(shè)備開發(fā) AC 來說明我們的貢獻(xiàn)。
