基于全测试器的实时时序逻辑RTCTL*符号模型检测器的研究与开发

发布时间：2020-12-25 03:09

　　进入21世纪以来,信息技术已逐渐成为推动经济发展和提升生产效率的强大动力,软件技术的普及度越来越高,软件行业呈现出高速发展的趋势。随着计算机系统规模日益增加、问题域不断加大,其系统设计的复杂度也在不断飆升。系统复杂度的增加意味着出现错误的可能性也就更大,其安全性不容忽视;如何保障程序的安全性和提高程序的可靠性一直以来是软件技术发展的核心问题之一。以穷举状态为基础的模型检测因其自动化程度高,并能在系统不满足性质时提供反例等优点受到普遍关注和应用,成为解决该问题的有效途径之一。由于现有模型检测工具的形式化规范语言,如计算树逻辑（computation tree logic,简称CTL）和线性时序逻辑（linear temporal logic,简称LTL）等,存在规范描述能力不足,无法验证实时时序逻辑（real-time temporal logic,简称RTCTL*）的问题,本文基于全时序测试器（简称测试器）优化了 RTCTL*算法并证明了关键测试器的正确性和完备性,提出了一种RTCTL*符号模型检测工具——RTSMC（RTCTL*symbolic model checker）,该工具基... 

【文章来源】：华侨大学福建省

【文章页数】：67 页

【学位级别】：硕士

【文章目录】：
摘要
Abstract
第1章 引言
    1.1 研究背景与意义
    1.2 国内外研究现状
    1.3 论文的主要工作
    1.4 论文结构
    1.5 本章小结
第2章 相关技术
    2.1 形式化验证
    2.2 ROBDD
    2.3 JAVABDD
    2.4 符号化模型检测
    2.5 规范
    2.6 模型检测工具
    2.7 本章小结
第3章 基于全测试器的符号模型检测算法
    3.1 基础模型
        3.1.1 公平性离散系统JDS
        3.1.2 JDS的同步并行组合
        3.1.3 RTCTL* 语法语义及等价关系
        3.1.4 测试器——“全时序测试器”的简称
    3.2 RTCTL* 算法与证明
        3.2.1 RTCTL* 的测试器
        3.2.2 ?f的测试器
        3.2.3 f ∧ g的测试器
        3.2.4 Ef的测试器
        3.2.5 Xf的测试器及证明
        3.2.6 fUg的测试器及证明
        3.2.7 fU[a,b]g的测试器及证明
    3.3 本章小结
第4章 基于JTLV实现RTSMC
    4.1 系统原型框架
    4.2 RTSMC验证流程
    4.3 词法语法解析
    4.4 RTSMC核心模块的实现
        4.4.1 RTCTL* 接口
        4.4.2 Env扩展
        4.4.3 RTCTL* 构造器
        4.4.4 RTCTL* 解析器
    4.5 本章小结
第5章 实验结果与分析
    5.1 实验环境
    5.2 实验结果展示与分析
        5.2.1 功能 & 边界测试
        5.2.2 对比Nu SMV验证实时时序逻辑
        5.2.3 对比nu XMV验证实时时序逻辑
    5.3 本章小结
第6章 总结与展望
    6.1 本文的主要成果
    6.2 本文的创新点
    6.3 本文的不足
    6.4 后续工作展望
参考文献
致谢



本文编号：2936839