唐江峻[1]2004年在《基于STGA的并发程序测试》文中进行了进一步梳理本文提出一种基于带赋值符号迁移系统STGA选取测试同步序列的方法。与传统的基于标号：迁移系统LTS的方法相比，STGA中保留了对测试同步序列的选取有重要影响的结构信息，因此有利于高效率同步序列的选取。实例研究证实了这一优越性。 在这个基础上我们还提出了若干覆盖率标准来指导同步序列的选取，实例研究也表明在发现错误的能力方面，根据这些覆盖率选取出来的同步序列要好于随机选取的同步序列。
刘剑[2]2005年在《传值进程与移动进程的模型检测方法》文中认为并发理论研究并发现象,即多个独立运行的计算主体(进程)相互间通过交换信息(通信)实现协作,以共同完成预定的任务的计算现象。自六七十年代起各种并发理论相继提出并得到广泛研究,例如,Petri Net、进程代数、模态逻辑等。本文的工作主要集中于传值进程理论和移动界程理论上。 模型检测是一种针对并发系统的自动分析与验证技术。其基本原理是用状态迁移图S表示要分析的系统,用模态/时序逻辑公式φ描述要检查的性质。系统是否具有所要求的性质就转化为S是否满足φ,对有限状态系统这个问题是可判定的。和其他验证方法(如:模拟、测试、机器证明等)相比模型检测方法具有两项突出的优点:其一,验证过程完全自动化:其二,当抽象模型不满足逻辑公式时,检测工具会自动产生一个反例来说明为什么不满足,以用于查错和修改。 本文的研究工作主要由传值系统的模型检测方法和移动系统的模型检测方法两部分组成。 在传值进程系统中,本文的工作主要包括叁方面:首先本文讨论谓词μ演算和模态图之间的语义等价问题。模态图是谓词μ演算的一种图形表示形式,它的提出是为了克服线性谓词μ演算公式复杂难懂,不利于机器处理的缺点;将谓词μ演算应用到传值进程的模型检测中。本文通过定义嵌套谓词等式系来建立两者之间的联系。提出了从文本公式到模态图的转换算法并证明了转换的正确性。其次,本文研究了传值进程模型检测中诊断信息的生成问题,引入两种有效的诊断信息表示结构:证明图和示例;提出了相应的诊断信息生成算法并予以实现。此外,为了对付模型检测的状态爆炸问题,本文研究了弱谓词μ演算和弱互模拟之间的关系。定义基于STGA的惰性迁移的概念,并证明惰性迁移的前后状态是弱互模拟的,并且在象有限的模型下,它们满足相同的弱谓词μ演算性质。在此基础上提出了传值进程模型检测的一种偏序归约方法,并将该方法集成到已实现的自动检测工具中。 在移动进程系统方面,本文的工作主要是实现了移动界程的模型检测系统。主要工作包括提出移动界程的底层de Bruijn表示;并将其应用到有限控制移动界程的范式表示上,提出了移动界程的有效的底层表示方法。在此基础上实现了带不动点算子的界程逻辑的模型检测算法。该工具是首个能检测带递归性质的移动界程模型检测系统。
吴鹏[3]2005年在《并发系统的模型检测与测试》文中指出随着网络、分布式系统及移动计算的迅速发展,并发理论成为计算机科学前沿的研究热点。本文围绕这一前沿领域,研究并发软件的分析、验证和测试。主要结果有: 1.提出基于带赋值符号迁移图的网络协议建模框架。该建模框架从网络协议的构成要素(包括服务原语、协议数据单元等)出发,把协议实体表示为其各任务分量的并发复合,进而把网络协议表示为其各协议实体的并发复合。这种组合建模方法支持传值通信机制,通过引入变量和参数避免了对协议实体状态的直接穷举,有效地反映了网络协议的组成结构和消息传递特性。 2.无死锁是网络协议的重要性质之一,但直接验证网络协议无死锁需要遍历整个状态空间,易导致状态空间爆炸。本文提出网络协议无死锁的充分条件——互连性,即对于满足互连性的网络协议,如果其各并发分量无死锁,则网络协议也不会死锁。而且,互连性判定可以在符号迁移图上直接执行,而不必展开网络协议的全局状态。这样,只须验证网络协议各并发分量无死锁,即可证明网络协议无死锁,而不必直接对网络协议进行验证,从而使模型验证工具能够处理更复杂的并发系统。 3.基于上述网络协议建模方法,本文详细阐述了关于移动IPv4和IPv6移动性的实例研究。其结果表明这种建模方法和思路支持动态网络拓扑结构,能够有效地对移动网络协议进行分析和验证,而不必引入显式的移动符号或移动迁移。特别是在验证移动IPv6的路由特性时,发现在移动节点漫游切换过程中会发生数据丢失,即若家乡代理在确认移动节点的绑定更新请求之后更新其本地的绑定表,则这期间家乡代理截获的发往移动节点家乡地址的数据包将会被转发到失效的地址上;而另一方面,若家乡代理在更新其本地的绑定表之后确认移动节点的绑定更新请求,则这期间移动节点在收到其家乡代理的绑定确认之前就可能收到数据包,对此IPv6协议规范未明确定义移动节点的行为。 4.提出一阶事件约束逻辑FOSCL以描述并发软件测试过程中输入/输出事件之间的时序关系及事件参数之间的数据相关性,进而提出基于FOSCL的符号测试用例生成方法并开发了相应的测试用例自动生成工具。实验结果表明基于FOSCL生成的符号测试用例集有效地避免了由于对输入参数实例化引起的状态爆炸问题,能够达到比较理想的迁移覆
薄莉莉, 姜淑娟, 张艳梅, 王兴亚, 于巧[4]2019年在《并发缺陷检测技术研究进展》文中研究说明多核时代的到来使得并发程序的设计备受人们关注。然而,并发程序的并发性和不确定性容易引发并发缺陷。因此,快速且有效地检测出这些并发缺陷尤为重要。首先,将目前常见的并发缺陷分为五大类(并发类型状态缺陷、死锁、数据竞争、原子性违背和顺序违背);随后,从软件运行的角度,将现有的并发缺陷检测技术分为静态分析、动态分析和动静结合分析,并对每一类进行详细的分析、比较和总结;接着,对并发缺陷检测技术的通用性进行分析和总结;最后,从通用准确的并发缺陷检测、软硬件相结合的并发缺陷检测、并发缺陷检测修复一体化、适用于松散内存模型的并发缺陷检测、安卓等其他应用平台的并发缺陷检测和分布式系统非确定性并发缺陷研究等方面,对并发缺陷检测技术的未来研究进行了探讨。
参考文献：
[1]. 基于STGA的并发程序测试[D]. 唐江峻. 中国科学院研究生院（软件研究所）. 2004
[2]. 传值进程与移动进程的模型检测方法[D]. 刘剑. 中国科学院研究生院（软件研究所）. 2005
[3]. 并发系统的模型检测与测试[D]. 吴鹏. 中国科学院研究生院（软件研究所）. 2005
[4]. 并发缺陷检测技术研究进展[J]. 薄莉莉, 姜淑娟, 张艳梅, 王兴亚, 于巧. 计算机科学. 2019
标签：计算机软件及计算机应用论文; 程序测试论文; 测试模型论文; 并发测试论文;