欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
软件产品线保持产品个性化的同时提高了公共部分的复用。但软件产品线中包含的不确定信息，给产品带来了潜在风险。形式化验证技术逐步应用于软件产品线验证。但是传统的布尔逻辑模型不能很好地描述软件产品线的不确定性和不一致性。本文结合多值模型检测器χChek，通过基于动作的模型描述方法，对软件产品线进行描述，然后转换成为χChek规定的模型格式，同时提供多值逻辑描述。最后采用计算树逻辑描述产品线属性，使用χChek进行验证。
英文摘要：
Software Product Line（ SPL） keeps the flexibility of products and improves the reuse of the common base at the same time. But SPL includes much uncertain and inconsistent information,thus there will be some potential risks for software product.Formal validation technology has been used for validating the SPL. But the traditional model based on boolean logic can＇t well describe the nondeterminacy and inconsistency of SPL. Therefore combined with a muti-valued logic model checker,an actionbased for specifying SPL was proposed. Then the new model was converted into the model which can be checked by χChek and a lattice of multi-valued logic was generated. At last,Computation Tree Logic（ CTL） was used to describe temporal properties of the SPL and χChek can validate those properties.
同期刊论文项目
同项目期刊论文
期刊信息
位置：