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