基于时序逻辑的双向一致性检测

发布时间：2021-10-20 13:27

　　软件形式化是当前构建安全可信软件系统的重要方法之一。由形式化模型驱动软件开发过程中,开发人员需要首先建立一个形式化的模型并验证其正确性,然后基于该模型开发系统的代码实现。由于技术所限,目前模型自动转换技术还不足以帮助技术人员完全自动化地完成代码转换工作,转换过程仍然需要涉及大量的人为工作。因此,保证模型与代码的一致性的任务必须贯穿整个开发流程。在理想的情况下,模型是经过验证被认为相对正确的,故只需要使用基于模型的测试方法检测软件代码针对软件模型的一致性。然而,随着当今软件系统规模的不断增大,需求变动越来越频繁,对应的软件开发流程也变得越来越灵活,代码有时会先于模型被修改。例如,反向工程或项目重构的需要；在需求的临时变更导致代码亟需修改；对关键代码反向抽取模型进行形式化验证的情况等。传统的基于模型的测试方法只能检测代码之于模型的一致性而不能反作用于模型层面,模型的修改者只能人为地评估修改的正确性,大大降低了模型修改效率并增加了系统的潜在隐患。为此,本文对传统基于模型的测试方法的一致性检测进行了扩展,提出了一个可以双向检测模型与代码一致性的框架。该框架通过基于模型的测试从测试结果中抽取表达... 

【文章来源】：华东师范大学上海市 211工程院校 985工程院校 教育部直属院校

【文章页数】：52 页

【学位级别】：硕士

【文章目录】：
摘要
ABSTRACT
第一章 绪论
    1.1 研究背景
    1.2 国内外研究现状
    1.3 关键问题与技术路线
    1.4 本文的主要贡献
    1.5 本文的组织结构
第二章 相关概念介绍
    2.1 形式化建模
    2.2 模型检测
    2.3 时序逻辑
    2.4 基于模型的测试
    2.5 本章小结
第三章 一个热水壶系统实例
    3.1 模型概述
    3.2 系统行为详述
    3.3 可能出现的不一致情况
    3.4 本章小结
第四章 双向一致性检测
    4.1 基本流程
    4.2 基于模型的测试及其扩展
        4.2.1 测试用例生成
        4.2.2 测试用例扩展
        4.2.3 测试用例执行
    4.3 时序逻辑公式抽取
        4.3.1 测试结果比对与不一致分类
        4.3.2 时序逻辑公式转译
        4.3.3 时序逻辑公式优化
        4.3.4 生成时序逻辑示例
    4.4 与模型检测工具结合
    4.5 本章小结
第五章 双向一致性检测框架：ProMiner
    5.1 技术选型与架构
    5.2 组件介绍
    5.3 本章小节
第六章 实验分析
    6.1 实验方法与内容
        6.1.1 多功能智能卡系统
        6.1.2 热水壶系统和电梯系统
    6.2 实验数据
    6.3 结论与分析
    6.4 本章小结
第七章 总结与展望
    7.1 全文总结
    7.2 后续工作展望
致谢
参考文献
附录 攻读学位期间发表的学术论文


【参考文献】：
期刊论文
[1]基于Event-B方法的多应用智能卡的建模与开发[J]. 章玥,郭建,朱晓冉,王文君,朱晶洋,汤家华,陈峻念.  计算机工程与科学. 2014(10)
[2]基于模型的开发方法在多应用智能卡中的应用[J]. 章玥,郭建,朱晓冉.  信息网络安全. 2013(12)
[3]元建模技术研究进展[J]. 刘辉,麻志毅,邵维忠.  软件学报. 2008(06)
[4]面向模型检验的UML状态机语义[J]. 周颖,郑国梁,李宣东.  电子学报. 2003(S1)
[5]基于UML状态图的类测试用例自动生成方法[J]. 张毅坤,施凤鸣,姚全珠,刘军,付长龙.  计算机工程. 2003(21)
[6]模型检测:理论、方法与应用[J]. 林惠民,张文辉.  电子学报. 2002(S1)

硕士论文
[1]模型和代码的一致性检测方法的研究[D]. 王翠钦.重庆大学 2014



本文编号：3446984