文摘
英文文摘
致谢
第一章引言
1.1课题背景和意义
1.2国内外研究现状
1.3存在的问题
1.4本文工作及贡献
1.5本文的组织
第二章时态逻辑概述
2.1 时态逻辑的起源与发展
2.1.1模态逻辑简介
2.1.2时态逻辑的极小系统
2.1.3时态逻辑的扩充系统
2.2计算机科学中的时态逻辑
2.2.1线性时态逻辑(linear Temporal Logic)
2.2.2分支时态逻辑(Branching Temporal Logic)
2.2.3区间时态逻辑(Interval Temporal Logic)
2.3本文采用的时态逻辑—命题线性时态逻辑PLTL
2.3.1 PLTL语法
2.3.2 PLTL语义
2.3.3 PLTL演绎系统
2.4小结
第三章并发系统计算模型及其分析
3.1并发系统与计算模型
3.2状态机模型与分析
3.3佩特里(Petri)网模型与分析
3.4 进程代数模型
3.5基于转换系统的一种计算模型：FTS模型
3.5.1(基本)转换系统BTS
3.5.2公平转换系统FTS
3.5.3 FTS模型的时态语义
3.6关于FTS模型可信性的一种粒度分析方法
3.6.1一种简单程序设计语言（SPL）
3.6.2 SPL与FTS的计算行为比较
3.6.3一种粒度求精方法
3.6.4一种限制临界引用条件（LCR）
3.7小结
第四章并发系统性质形式化描述与分类
4.1程序的形式化描述
4.1.1程序的形式化描述与程序性质
4.1.2几种常见的形式化描述方法
4.2并发程序性质的PLTL描述
4.2.1安全性
4.2.2 活性
4.2.3终止的程序性质
4.3并发程序性质的进一步讨论
4.3.1程序性质的形式化定义
4.3.2程序性质的进一步分类
4.4基于PLTL的网络通信协议形式化描述
4.4.1协议及其形式化描述
4.4.2基于PLTL的AB协议形式化描述
4.5小结
第五章并发系统演绎证明与自动验证
5.1程序的正确性证明
5.1.1 Floyd方法
5.1.2 Hoare公理化方法
5.1.3 Dijkstra最弱前置条件方法
5.1.4其它验证方法
5.2基于扩充ω-自动机的一种演绎证明方法
5.2.1 Manna-Pnueli演绎规则方法
5.2.2 Manna-Pnueli(时态)验证图方法
5.2.3基于扩充ω-自动机的一种图验证方法
5.2.4一个应用实例
5.3基于PLTL的一种模型检验算法
5.3.1模型检验概述
5.3.2一种PLTL模型检验算法
5.3.3一个应用实例：Peterson互斥算法的模型检验
5.3.4符号模型检验
5.4小结
第六章实时系统形式开发方法初步研究
6.1实时系统概述
6.2实时系统的几个重要模型
6.2.1时间自动机(TFSA)
6.2.2 时间Petri网
6.2.3时间进程代数
6.3基于转换系统的实时系统的一种建模方法
6.3.1时间转换系统TTS
6.3.2实时转换模型RTM：一种改进的TTS
6.3.3一个例子
6.4实时系统的一种定量时态逻辑描述方法
6.4.1定量时态逻辑
6.4.2实时性质描述的几个简单例子
6.4.3实例分析——监视器计时网（WTN）的描述
6.5小结
第七章混合系统形式开发方法初步研究
7.1混合系统概述
7.2混合系统的几个重要模型
7.2.1混合自动机(HFSA)
7.2.2混合Petri网(HPN)
7.2.3时段演算及其扩充
7.2.4混合CSP
7.3基于FTS的混合系统的一种建模方法
7.3.1混合系统的时间模型
7.3.2混合转换系统HTS
7.3.3一个例子
7.4混合系统描述的一种扩充时态逻辑
7.4.1语法
7.4.2语义
7.4.3实例分析——煤气燃烧器的安全性描述
7.5小结
第八章与相关工作比较
8.1交替并发模型的可信性
8.2并发程序形式化定义与分类
8.3网络协议活性描述和逐步求精
8.4并发系统图形验证与模型检验
8.5实时及混合系统的描述与建模
第九章结束语
参考文献
攻读博士学位期间科研和学术论文情况
