基于多值逻辑的软件产品线模型检测

发布时间：2021-04-07 21:02

　　软件产品线工程通过管理软件产品的可变性和共性特征,提高软件开发效率,节约开发成本。模型检测是一种自动形式化验证技术。随着软件产品线在安全关键领域的广泛应用,对软件产品线的模型检测已成为软件验证领域的一个重要研究方向。在软件产品线开发的早期阶段,由于特征的复杂性,系统设计中往往存在不确定信息。然而,现有的软件产品线模型检测对这种情况下的建模和验证支持不足。为此,本文提出一种基于多值逻辑对软件产品线的不完备设计进行建模和验证的方法,可以描述软件产品线设计初期存在的不确定信息,将模型检测提前到系统开发的早期阶段进行,及时发现错误,降低后期的修复成本。本文的具体工作包括以下几个方面。首先,本文以世界双格作为理论基础,提出一种多值模型——基于双格的特征迁移系统,实现对包含不确定信息的软件产品线进行建模,并通过投影和精化关系定义特定软件产品的不完备模型和具体模型。然后,采用动作计算树逻辑描述系统的时序属性,定义动作计算树逻辑在基于双格的特征迁移系统上的语义,提出基于双格的多值模型检测。进一步,为实现基于双格的多值模型检测,一方面,提出从基于双格的特征迁移系统到多值Kripke结构的等价转换方法,开... 

【文章来源】：南京航空航天大学江苏省 211工程院校

【文章页数】：71 页

【学位级别】：硕士

【文章目录】：
摘要
ABSTRACT
注释表
第一章 绪论
    1.1 研究背景
        1.1.1 软件产品线
        1.1.2 模型检测
        1.1.3 软件产品线的模型检测
    1.2 研究现状
    1.3 本文研究内容
        1.3.1 软件产品线的不完备建模
        1.3.2 软件产品线的多值模型检测
    1.4 本文组织结构
第二章 预备知识
    2.1 软件产品线的可变性建模
        2.1.1 特征与特征图
        2.1.2 迁移系统与特征迁移系统
    2.2 多值模型检测
        2.2.1 双格与世界双格
        2.2.2 多值Kripke结构与CTL逻辑
    2.3 本章小结
第三章 软件产品线的不完备建模
    3.1 基于双格的特征迁移系统
    3.2 产品的不完备模型
    3.3 产品的具体模型
    3.4 本章小结
第四章 软件产品线的多值模型检测
    4.1 基于BFTS的多值模型检测
    4.2 多值模型检测问题的实现
        4.2.1 基于模型转换的多值模型检测
        4.2.2 基于模型分解的多值模型检测
    4.3 本章小结
第五章实验设计与分析
    5.1 χ Chek简介
    5.2 BPMCA工具设计
        5.2.1 BPMCA工具的架构设计与实现
        5.2.2 转换模型与代数格生成算法
        5.2.3 BPMCA工具的使用
    5.3 实例分析
    5.4 本章小结
第六章 总结及展望
    6.1 论文总结
    6.2 未来工作展望
参考文献
致谢
在学期间的研究成果及发表的学术论文


【参考文献】：
期刊论文
[1]软件产品线可变性建模技术系统综述[J]. 聂坤明,张莉,樊志强.  软件学报. 2013(09)
[2]面向软件产品家族的变化性建模方法[J]. 邹盛享,张伟,赵海燕,梅宏.  软件学报. 2005(01)



本文编号：3124190