MSVL建模、仿真与验证软件的扩展及其应用

论文摘要

本文主要讨论基于投影时序逻辑PTL(Projection Temporal Logic)的MSVL(Modeling, Simulation and Verification Language)建模、仿真与验证软件的实现原理,扩展及应用,MSVL是一种时序逻辑程序设计语言,它是PTL的可执行子集,我们可以采用MSVL语言描述软、硬件系统,并对系统进行建模、仿真和自动化性质验证。文中首先介绍了PTL,并给出了实现MSVL建模、仿真及验证软件的基本方法,还详细说明了该软件的功能、基本框架以及各个模块的作用,然后,本文说明了对该软件进行的面向对象扩展,包括基本理论,具体实现以及简单的例子分析,接着,文中又给出了对MSVL建模、仿真与验证软件在柱面计算方面的扩充,同样,介绍了其实现的基本理论以及具体方法,并给出一个详细的例子,最后,本文介绍了如何实现加标记的PTL统一模型检测算法,回顾了PTL统一模型检测算法的实现步骤,给出了加标记的PTL统一模型检测算法及其在该软件中的实现,并给出了加标记的PTL统一模型检测算法验证无穷区间模型的例子。

论文目录

• 摘要
• Abstract
• 第一章 绪论
• 1.1 研究背景
• 1.2 时序逻辑程序设计语言
• 1.2.1 时序逻辑
• 1.2.2 时序逻辑程序设计语言
• 1.3 本文所做的工作及内容安排
• 第二章 框架投影时序逻辑程序设计语言MSVL
• 2.1 投影时序逻辑
• 2.1.1 语法
• 2.1.2 语义
• 2.2 MSVL简介
• 2.2.1 语法
• 2.2.2 语义
• 2.3 MSVL建模、仿真与验证软件
• 2.3.1 基本原理及技术
• 2.3.2 MSVL软件流程及功能描述
• 2.3.3 MSVL软件框架
• 2.3.4 应用实例及分析
• 第三章 面向对象扩展及实现
• 3.1 逻辑基础及语法扩展
• 3.1.1 投影时序逻辑的扩展
• 3.1.2 MSVL语句的扩展
• 3.1.3 面向对象MSVL的特点
• 3.2 面向对象概念在MSVL软件中的实现
• 3.2.1 词法分析模块实现
• 3.2.2 语法分析模块实现
• 3.2.3 化简模块实现
• 3.3 实例分析
• 第四章 柱面计算引入及实现
• 4.1 基本理论
• 4.1.1 并行计算‖和投影运算prj
• 4.1.2 柱面计算
• 4.2 MSVL软件中的实现
• 4.2.1 词法分析模块实现
• 4.2.2 语法分析模块实现
• 4.2.3 化简模块实现
• 4.3 实例分析
• 第五章 加标记的PTL统一模型检测算法的实现
• 5.1 PTL统一模型检测算法回顾
• 5.1.1 算法介绍
• 5.1.2 算法存在的问题
• 5.2 加标记的PTL统一模型检测算法
• 5.2.1 算法描述
• 5.2.2 MSVL建模、仿真与验证软件中的实现
• 5.3 无穷路径的性质验证实例
• 5.3.1 简单例子
• 5.3.2 哲学家就餐问题
• 第六章 总结与展望
• 6.1 总结
• 6.2 展望
• 致谢
• 参考文献
• 附录A
• 附录B
• 附录C