投影时序逻辑的完备公理系统与形式验证

发布时间：2021-07-18 20:56

　　投影时序逻辑（Projection Temporal Logic, PTL）是一阶区间时序逻辑（Interval Temporal Logic, ITL）的扩展,引入了全新的投影操作符prj,并且同时支持有穷和无穷模型,具备了完全正则表达式的表达能力,能够方便的描述顺序、选择、循环、并行、信号量等程序结构,可在同一PTL逻辑框架内完成对待验证系统的建模和性质描述,适用于各类软硬件系统的验证.为采用定理证明的方法对并发及交互式系统验证,本文在有穷论域的前提下为PTL建立了一个完备公理系统,提出了PTL的范式（Normal Form, NF）、范式图（Normal Form Graph, NFG）、标记范式（Labeled Normal Form, LNF）和标记范式图（Labeled Normal Form Graph, LNFG）技术,利用NFG和LNFG可描述PTL公式模型的特性分别解决了有穷和无穷时间PTL的判定问题,并证明了有穷时间和无穷时间PTL公理系统的完备性,同时探讨了PTL的表达能力和基于PTL的系统建模方法,为使用PTL进行形式化验证打下了坚实的理论基础。本文的主要贡献... 

【文章来源】：西安电子科技大学陕西省 211工程院校 教育部直属院校

【文章页数】：161 页

【学位级别】：博士

【文章目录】：
摘要
Abstract
第一章 绪论
    1.1 研究背景与意义
    1.2 形式化方法
        1.2.1 模型检测
        1.2.2 定理证明
    1.3 时序逻辑
    1.4 相关研究工作
    1.5 论文的主要工作与组织结构
第二章 投影时序逻辑
    2.1 语法
    2.2 语义
    2.3 PTL操作符特点分析
    2.4 一些特殊形式的PTL公式
    2.5 小结
第三章 PTL的公理系统
    3.1 PTL的公理系统
    3.2 公理系统的可靠性
    3.3 常用定理
    3.4 小结
第四章 有穷时间PTL公理系统的完备性
    4.1 PTL的范式
        4.1.1 范式的定义
        4.1.2 范式的存在性
        4.1.3 范式的计算算法
    4.2 范式图
        4.2.1 范式图的定义
        4.2.2 范式图的构造算法
        4.2.3 范式图的一些性质
        4.2.4 范式图的局限性
    4.3 有穷时间PTL的判定算法
    4.4 有穷时间公理系统的完备性证明
    4.5 小结
第五章 无穷时间PTL公理系统的完备性
    5.1 标记范式与标记范式图的引入
    5.2 标记范式
        5.2.1 标记范式的定义
        5.2.2 标记范式的计算算法
    5.3 标记范式图
    5.4 QFPTL公式的判定算法
        5.4.1 QFPTL公式LNFG的特殊性质
        5.4.2 LNFG的化简
        5.4.3 QFPTL的判定算法
        5.4.4 QFPTL的判定实例
    5.5 PTL公式的判定算法
        5.5.1 从QPTL到QFPTL的转换
        5.5.2 PTL的判定算法
    5.6 PTL公理系统的完备性证明
    5.7 小结
第六章 基于PTL的形式化验证
    6.1 PTL与完全正则语言
        6.1.1 完全正则语言
        6.1.2 从FRE到PTL公式
        6.1.3 从PTL公式到FRE
    6.2 使用PTL进行系统建模
        6.2.1 MSVL
        6.2.2 扩展Kripke结构
    6.3 验证实例
        6.3.1 问题描述
        6.3.2 系统建模
        6.3.3 系统验证
    6.4 小结
第七章 总结与展望
    7.1 论文总结
    7.2 进一步的研究展望
致谢
参考文献
攻读博士学位期间的研究成果


【参考文献】：
期刊论文
[1]面向命题投影时序逻辑的安全协议模型检测[J]. 杨琛,段振华,王小兵.  西安交通大学学报. 2010(08)
[2]利用投影时序逻辑的多内核进程调度建模与验证[J]. 舒新峰,段振华.  西安交通大学学报. 2010(03)
[3]投影时序逻辑的公理系统与形式验证[J]. 舒新峰,段振华.  西安电子科技大学学报. 2009(04)
[4]面向投影时序逻辑的Web服务模型检测[J]. 王小兵,段振华.  西安交通大学学报. 2009(04)
[5]混合投影时序逻辑与混合系统的形式化验证[J]. 张海宾,段振华.  计算机科学. 2007(11)
[6]基于扩展投影时序逻辑的组合Web服务描述与验证[J]. 雷丽晖,段振华.  西安交通大学学报. 2007(10)
[7]使用扩展区间时序逻辑为并发工作流建模[J]. 雷丽晖,段振华.  西安电子科技大学学报. 2007(04)



本文编号：3290350