并发系统的模型检测与测试

论文题目: 并发系统的模型检测与测试

论文类型: 博士论文

论文专业: 计算机软件与理论

作者: 吴鹏

导师: 林惠民

关键词: 并发系统,模型检测,网络协议,移动,基于模型的测试,符号测试用例,一阶事件约束

文献来源: 中国科学院研究生院（软件研究所）

发表年度: 2005

论文摘要: 随着网络、分布式系统及移动计算的迅速发展,并发理论成为计算机科学前沿的研究热点。本文围绕这一前沿领域,研究并发软件的分析、验证和测试。主要结果有: 1.提出基于带赋值符号迁移图的网络协议建模框架。该建模框架从网络协议的构成要素(包括服务原语、协议数据单元等)出发,把协议实体表示为其各任务分量的并发复合,进而把网络协议表示为其各协议实体的并发复合。这种组合建模方法支持传值通信机制,通过引入变量和参数避免了对协议实体状态的直接穷举,有效地反映了网络协议的组成结构和消息传递特性。 2.无死锁是网络协议的重要性质之一,但直接验证网络协议无死锁需要遍历整个状态空间,易导致状态空间爆炸。本文提出网络协议无死锁的充分条件——互连性,即对于满足互连性的网络协议,如果其各并发分量无死锁,则网络协议也不会死锁。而且,互连性判定可以在符号迁移图上直接执行,而不必展开网络协议的全局状态。这样,只须验证网络协议各并发分量无死锁,即可证明网络协议无死锁,而不必直接对网络协议进行验证,从而使模型验证工具能够处理更复杂的并发系统。 3.基于上述网络协议建模方法,本文详细阐述了关于移动IPv4和IPv6移动性的实例研究。其结果表明这种建模方法和思路支持动态网络拓扑结构,能够有效地对移动网络协议进行分析和验证,而不必引入显式的移动符号或移动迁移。特别是在验证移动IPv6的路由特性时,发现在移动节点漫游切换过程中会发生数据丢失,即若家乡代理在确认移动节点的绑定更新请求之后更新其本地的绑定表,则这期间家乡代理截获的发往移动节点家乡地址的数据包将会被转发到失效的地址上;而另一方面,若家乡代理在更新其本地的绑定表之后确认移动节点的绑定更新请求,则这期间移动节点在收到其家乡代理的绑定确认之前就可能收到数据包,对此IPv6协议规范未明确定义移动节点的行为。 4.提出一阶事件约束逻辑FOSCL以描述并发软件测试过程中输入/输出事件之间的时序关系及事件参数之间的数据相关性,进而提出基于FOSCL的符号测试用例生成方法并开发了相应的测试用例自动生成工具。实验结果表明基于FOSCL生成的符号测试用例集有效地避免了由于对输入参数实例化引起的状态爆炸问题,能够达到比较理想的迁移覆

论文目录:

摘要

Abstract

第一章引言

1.1 模型检测

1.1.1 概述

1.1.2 工具

1.2 并发软件测试

1.2.1 基于有限状态机的测试

1.2.2 基于标号迁移系统的测试

1.2.3 工具

1.3 本文的目标、贡献和组成

第二章并发系统的模型检测

2.1 传值并发进程

2.2 带赋值符号迁移图

2.3 CTL

2.4 一阶μ演算

第三章网络协议分析与验证

3.1 协议实现结构分析

3.2 网络协议建模框架

3.3 无死锁分析

第四章移动IP实例研究

4.1 移动IPv4

4.1.1 协议建模

4.1.2 模型检测

4.2 IPv6的移动性

4.2.1 协议建模

4.2.2 模型检测

第五章一阶事件约束逻辑

5.1 语法

5.2 语义

5.3 表达能力

5.3.1 CTL

5.3.2 CSPE

5.4 一阶μ演算定义

第六章并发软件测试

6.1 模型确定化

6.1.1 Τ

6.1.2 不可辨识的输入／输出动作

6.2 模型切片

6.2.1 符号路径

6.2.2 切片算法

6.3 测试用例生成

6.4 实例研究

第七章结束语

7.1 结论

7.2 下一步的工作

附录A 英文缩写对照

参考文献

发表文章目录

致谢

发布时间: 2005-07-08

参考文献

[1].并发系统综合的PN行为理论及其应用[D]. 蒋昌俊.中国科学院研究生院（计算技术研究所）1998
[2].并发系统的动作细化理论[D]. 郑光.兰州大学2008
[3].扩展π演算的建模、验证与测试[D]. 罗玲.西安电子科技大学2015
[4].并发系统的建模与验证一体化方法的研究[D]. 夏默.清华大学2015
[5].面向逻辑标记转换系统的进程演算CLL_R的研究[D]. 张严.南京航空航天大学2015

并发系统的模型检测与测试

猜你喜欢