框架时序逻辑程序设计解释器及模型检测工具

论文摘要

本文主要讨论一个框架时序逻辑程序设计语言FTLL （Framed Temporal Logic Programming Language）的解释器及一个基于命题投影时序逻辑PPTL （Proposition Projection Temporal Logic）进行性质描述的模型检测工具的实现。文中首先介绍了实现解释器的基于范式的基本方法,然后给出了解释器的基本框架并详细说明了各个模块的功用。此外还对FTLL中几个重要的结构的实现做了详细说明,包括框架、等待、投影、指针等操作。作为该解释器应用,它可以作为由OWL-S描述的抽象模型的模拟器,文中给出了一个详细的例子。随后,本文介绍了用FTLL为系统建模,PPTL进行性质描述,然后分别将系统和性质的非转换为各自的范式,接着对范式求交,并找它们的模型,看能否找到反例,从而进行模型检测的方法。并介绍了一个以此实现的模型检测工具,并给出了算法和一个例子。文章最后回顾了现有的模型检测工具。

论文目录

• 摘要
• Abstract
• 第一章 绪论
• 1.1 研究背景
• 1.2 形式化验证
• 1.2.1 模型检验
• 1.2.2 定理证明器
• 1.2.3 形式化综合
• 1.3 时序逻辑
• 1.4 时序逻辑程序语言
• 1.5 模型检测
• 1.6 本文所做的工作及内容安排
• 第二章 投影时序逻辑及框架时序逻辑程序设计语言
• 2.1 语法
• 2.1.1 命题投影区间时序逻辑
• 2.1.2 一阶投影区间时序逻辑（PITL）
• 2.2 语义
• 2.3 框架技术
• 2.4 一些导出公式
• 2.5 框架时序逻辑程序设计语言
• 第三章 解释器的设计与实现
• 3.1 基本方法
• 3.2 解释器框架
• 3.3 部分重要操作的实现
• 3.3.1 投影操作
• 3.3.2 Framing 操作
• 3.3.3 指针
• 3.4 应用实例
• 3.4.1 Web 服务模拟
• 3.4.2 电路仿真
• 第四章 系统性质验证
• 4.1 基本理论
• 4.2 模型查找及性质验证
• 4.2.1 模型查找
• 4.2.2 验证算法
• 4.3 实例描述
• 第五章 模型检测工具
• 总结与展望
• 致谢
• 参考文献
• 研究成果
• 附录 A
• 附录 B