产品线变型需求的逻辑验证
Logic Verification of Product-Line Variant Requirements
摘要：
变体需求的形式化验证在软件产品线（SPL）领域引起了广泛的兴趣。特征图被广泛用于对产品线变体进行建模。然而，缺乏精确定义的正式符号表示和验证这样的模型。本文提出了一种使用一阶逻辑对SPL变体特征图进行建模和验证的方法。它提供了一个精确和严格的形式化的解释的功能图。逻辑表达式可以通过使用命题连接词对变量及其依赖关系进行建模来构建。然后，这些表达式可以通过任何合适的验证工具进行验证。一个计算机辅助调度（CAD）系统的变异特征模型的案例研究来说明验证过程。
英文摘要：
Formal verification of variant requirements has gained much interest in the software product line (SPL) community. Feature diagrams are widely used to model product line variants. However, there is a lack of precisely defined formal notation for representing and verifying such models. This paper presents an approach to modeling and verifying SPL variant feature diagrams using first-order logic. It provides a precise and rigorous formal interpretation of the feature diagrams. Logical expressions can be built by modeling variants and their dependencies by using propositional connectives. These expressions can then be validated by any suitable verification tool. A case study of a Computer Aided Dispatch (CAD) system variant feature model is presented to illustrate the verification process.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
