论文题目: 传值进程与移动进程的模型检测方法
论文类型: 博士论文
论文专业: 计算机软件与理论
作者: 刘剑
导师: 林惠民
关键词: 传值系统,移动计算,进程代数,模型检测,传值,移动界程,状态爆炸
文献来源: 中国科学院研究生院（软件研究所）
发表年度: 2005
论文摘要: 并发理论研究并发现象,即多个独立运行的计算主体(进程)相互间通过交换信息(通信)实现协作,以共同完成预定的任务的计算现象。自六七十年代起各种并发理论相继提出并得到广泛研究,例如,Petri Net、进程代数、模态逻辑等。本文的工作主要集中于传值进程理论和移动界程理论上。 模型检测是一种针对并发系统的自动分析与验证技术。其基本原理是用状态迁移图S表示要分析的系统,用模态/时序逻辑公式φ描述要检查的性质。系统是否具有所要求的性质就转化为S是否满足φ,对有限状态系统这个问题是可判定的。和其他验证方法(如:模拟、测试、机器证明等)相比模型检测方法具有两项突出的优点:其一,验证过程完全自动化:其二,当抽象模型不满足逻辑公式时,检测工具会自动产生一个反例来说明为什么不满足,以用于查错和修改。 本文的研究工作主要由传值系统的模型检测方法和移动系统的模型检测方法两部分组成。 在传值进程系统中,本文的工作主要包括三方面:首先本文讨论谓词μ演算和模态图之间的语义等价问题。模态图是谓词μ演算的一种图形表示形式,它的提出是为了克服线性谓词μ演算公式复杂难懂,不利于机器处理的缺点;将谓词μ演算应用到传值进程的模型检测中。本文通过定义嵌套谓词等式系来建立两者之间的联系。提出了从文本公式到模态图的转换算法并证明了转换的正确性。其次,本文研究了传值进程模型检测中诊断信息的生成问题,引入两种有效的诊断信息表示结构:证明图和示例;提出了相应的诊断信息生成算法并予以实现。此外,为了对付模型检测的状态爆炸问题,本文研究了弱谓词μ演算和弱互模拟之间的关系。定义基于STGA的惰性迁移的概念,并证明惰性迁移的前后状态是弱互模拟的,并且在象有限的模型下,它们满足相同的弱谓词μ演算性质。在此基础上提出了传值进程模型检测的一种偏序归约方法,并将该方法集成到已实现的自动检测工具中。 在移动进程系统方面,本文的工作主要是实现了移动界程的模型检测系统。主要工作包括提出移动界程的底层de Bruijn表示;并将其应用到有限控制移动界程的范式表示上,提出了移动界程的有效的底层表示方法。在此基础上实现了带不动点算子的界程逻辑的模型检测算法。该工具是首个能检测带递归性质的移动界程模型检测系统。
论文目录:
摘要
Abstract
第一章 引言
1.1 并发系统
1.2 形式化验证方法
1.3 模型检测
1.3.1 状态爆炸问题
1.3.2 模型检测工具及应用
1.4 本文的工作和论文的结构
第二章 模型检测的基础
2.1 CCS
2.1.1 基本定义
2.1.2 标号迁移系统
2.1.3 互模拟和弱互模拟
2.2 模态逻辑
2.2.1 模态算了
2.2.2 Hennessy-Milner逻辑
2.3 时序逻辑
2.3.1 格和不动点
2.3.2 命题模态μ演算
2.3.3 命题μ演算的模型检测方法
2.3.3.1 全局模型检测算法
2.3.3.2 局部的模型检测算法
第三章 传值进程模型和谓词μ演算
3.1 传值CCS及其操作语义
3.1.1 传值CCS语言
3.1.2 带赋值的符号迁移图
3.1.3 STGA的互模拟和弱互模拟
3.2 谓词μ演算
3.2.1 谓词μ演算的语法
3.2.2 谓词μ演算的语义
3.3 模态图
3.3.1 模态图的语法
3.3.2 模态图的语义
3.4 嵌套谓词等式系
3.4.1 嵌套谓词等式系的语法语义
3.4.2 嵌套谓词等式系的语义刻划
3.5 谓词μ演算公式和模态图的对应关系
3.5.1 谓词μ演算公式到嵌套谓词等式系的转换算法
3.5.2 转换算法的正确性证明
3.5.3 嵌套谓词等式系的模态图表示
3.6 一个谓词μ演算公式的等式系和模态图表示
3.7 互模拟和谓词μ演算的关系
3.7.1 弱谓词μ演算
3.7.1.1 弱谓词μ演算的语法
3.7.1.2 弱谓词μ演算的语义
3.7.1.3 弱谓词μ演算和谓词μ演算之间的关系
3.7.2 互模拟和谓词μ演算的关系
第四章 传值进程模型检测及诊断信息生成
4.1 传值进程模型检测算法
4.2 模型检测算法的分析
4.3 诊断信息的生成
4.3.1 证明图
4.3.2 示例
4.4 实例分析
第五章 传值进程模型检测的偏序归约方法
5.1 直观的思想
5.2 惰性迁移
5.3 偏序归约模型检测算法
第六章 移动界程的模型检测
6.1 有限控制界程演算
6.2 带不动点的界程逻辑
6.2.1 界程逻辑的语法
6.2.2 界程逻辑的语义
6.3 移动界程的模型检测算法
第七章 移动界程模型检测工具
7.1 界程演算的de Bruijn表示
7.1.1 de Bruijn变换
7.1.2 维护函数
7.2 有限控制界程演算的范式表示
7.3 de Bruijn表示下的范式和迁移规则
7.4 模型检测算法的实现
7.5 系统的实现和测试
7.5.1 系统的结构
7.5.2 状态空间存取
7.5.3 实例分析
第八章 结论
8.1 总结及相关工作的讨论
8.1.1 命题μ演算和谓词μ演算的相关工作
8.1.2 诊断信息生成方面的相关工作
8.1.3 在偏序归约方法方面
8.1.4 在移动界程的模型检测工具方面
8.2 进一步的工作
参考文献
附录A ABP的输入检测文本
附录B FireWall的输入检测文本
个人简历、在学期间的研究成果及发表的论文
致谢及声明
发布时间: 2005-07-08
参考文献
- [1].基于投影时序逻辑的Petri网模型检测[D]. 师亚.西安电子科技大学2017
- [2].模糊系统验证的形式化方法研究[D]. 范艳焕.陕西师范大学2018
- [3].On-the-Fly和动态的软件模型检测方法研究[D]. 赵璐.哈尔滨工程大学2014
- [4].程序恶意行为识别及其恶意性判定研究[D]. 张一弛.解放军信息工程大学2012
- [5].基于模型检测的二进制代码恶意行为识别技术研究[D]. 奚琪.解放军信息工程大学2014
- [6].基于模型检测的时空性能分析若干问题研究[D]. 黄镇谨.合肥工业大学2016
- [7].复杂信息系统模型的形式化验证方法研究[D]. 张涛.哈尔滨工程大学2012
- [8].基于符号化模型检测的软件演化过程模型验证[D]. 刘金卓.云南大学2013
- [9].基于模型检测的安全操作系统验证方法研究[D]. 程亮.中国科学技术大学2009
- [10].基于懒惰切片的模型检测技术研究[D]. 黄宏涛.哈尔滨工程大学2012
相关论文
- [1].界程演算模型检测[D]. 江华.贵州大学2008
- [2].基于π演算的软件体系结构形式化研究[D]. 任洪敏.复旦大学2003
- [3].软件体系结构形式描述研究[D]. 朱雪阳.中国科学院研究生院（软件研究所）2005
- [4].并行最优化算法与软件设计及数值软件移植[D]. 王建.中国科学院研究生院（软件研究所）2005
- [5].基于形式语义的构件组装与演化研究[D]. 龚洪泉.复旦大学2005
- [6].超协调时序逻辑及其模型检测方法[D]. 陈冬火.中国科学院研究生院（成都计算机应用研究所）2006
- [7].电子商务协议形式化方法及模型检测技术的研究与应用[D]. 文静华.贵州大学2006
- [8].多智能体系统的符号模型检测[D]. 骆翔宇.中山大学2006