E-CSPE约束的一致性判定

分布式程序目前被大量使用．由于并发的存在，测试分布式程序需要采用事件约束来判定运行事件序列的正确性，事件约束之间需要判定一致性．初始的事件约束可以通过规约来定义，作者提出E-CSPE约束的描述规则来推导新约束，并提出约束之间的一致性判定机制．该算法具有多项式复杂度．     

基于事件约束的分布式程序正确性测试

由于并发的存在和不确定性,在以规约为基础来测试分布式程序的正确性时,必须考虑程序 执行时的内部状态.这些内部状态通过端口显示为事件序列,程序规约需要对序列中各事件间 的依赖关系作约定,即定义事件约束集.该文提出了E-CSPE(extended-constraints on suc ceeding and preceding events),以形式化描述这类事件约束,它由3个基本描述规则组成, 分别对应于3种不同类型的事件约束.通过判断程序执行时所产生的事件序 列集同这些事件约束集的一致性以及对约束集覆盖程     

基于EE-CSPE约束的并发程序测试

由于执行的不确定性,并发程序的测试需要验证程序执行的事件序列.定义事件之间的约束是验证事件序列合法性的前提.本文提出了一种事件约束的形式化描述方法,扩充了E-CSPE（extended constraints on succeeding and preceding events）对事件排斥约束和后决约束的定义,更全面地描述了前后事件的依赖关系,并给出了基于此方法的确定性测试和非确定性测试规则.     

面向Java的分布式程序测试系统

由于程序的分布运行,测试分布式程序必须同时考虑并发特性和运行环境.介绍了一个面向Java语言的分布式程序测试系统JDPT(Java-oriented distributed program testing system).JDPT基于运行环境定义事件,通过事件序列记录分布式程序的运行过程,并定义事件约束检测可行事件序列集的有效性.通过该技术,JDPT可以有效地判断程序在运行环境中并发执行的正确性,适用于跨平台的Java程序测试.     

GC-MCR:有向图约束指导的并发缺陷检测方法

约束求解应用到程序分析的多个领域,在并发程序分析方面也得到了深入的应用.并发程序随着多核处理器的快速发展而得到广泛使用,然而并发缺陷对并发程序的安全性和可靠性造成了严重的影响,因此,针对并发缺陷的检测尤为重要.并发程序线程运行的不确定性导致的线程交织爆炸问题,给并发缺陷的检测带来了一定挑战.已有并发缺陷检测算法通过约减无效线程交织,以降低在并发程序状态空间内的探索开销.比如,最大因果模型算法把并发程序状态空间的探索问题转换成约束求解问题.然而,其在约束构建过程中会产生大量冗余和冲突的约束,大幅度增加了约束求解的时间以及约束求解器的调用次数,降低了并发程序状态空间的探索效率.针对上述问题,提出了一种有向图约束指导的并发缺陷检测方法 GC-MCR (directed graph constraint-guided maximal causalityreduction).该方法旨在通过使用有向图对约束进行过滤和约减,从而提高约束求解速度,并进一步提高并发程序状态空间的探索效率.实验结果表明:GC-MCR方法构建的有向图可以有效优化约束的表达式,从而提高约束求解器的求解速度并减少求解器的调用次...     

基于事件约束的软件过程验证

软件过程是以人为中心的系统,其特点是动态性和不断演化.既定过程模型在实际执行时往往有所偏差.基于E-CSPE(extended constraints on succeeding and proceeding events)约束实现过程验证和偏差测量.事件约束根据过程模型定义.过程实例执行被记录为事件序列.通过分析事件序列对事件约束的覆盖和违反结果,可以计算EPD(event constraint based process difference metric)和EAD(event constraint based activity deviation metric)指标.EPD指标可以反映过程执行与过程模型的偏差,EAD指标则为过程演化提供依据.     

SSACC:一种基于软件科学法的Ada并发复杂性度量

本文致力于将软件科学法应用于Ada程序的并发复杂性度量,描述其方法和基于这种方法的相应工具SSACC。文中为Ada并发程序提出了一个面向度量的操作元-操作符模型,将任务和入口作为操作元,将程序中的并发动作作为对任务施加的操作。SSACC是Ada并发复杂性度量工具MACC的一部分。     

基于Petri网的并发程序测试用例产生方法

并发程序的测试路径具有不可预测性,而Pctri网在描述并发方面具有其它系统模型无法比拟的优势。因此通过Petri网来产生并发程序的测试路径:对有并发程序的源代码构造的Petri网模型进行图形矩阵转换;按照一定的规则得出相应的独立段组;合并独立段组得出网的独立段群,此独立段群即为该并发程序的测试路径。实验证明,将Petri网用于并发程序测试用的例生成降低了测试难度,提高了测试效率。     

基于约束依赖图的并发程序模型检测工具

模型检测是一种基于状态空间搜索的自动化验证方法,可以有效地提升程序的质量.然而,由于并发程序中线程调度的不确定性以及数据同步的复杂性,对该类程序验证时存在更为严重的状态空间爆炸问题.目前,大多采用基于独立性分析的偏序约简技术缩小并发程序探索空间.针对粗糙的独立性分析会显著增加需探索的等价类路径问题,开发了一款可细化线程迁移依赖性分析的并发程序模型检测工具CDG4CPV.首先,构造了待验证可达性性质对应的规约自动机;随后,根据线程迁移边的类型和共享变量访问信息构建约束依赖图;最后,利用约束依赖图剪裁控制流图在展开过程中的独立可执行分支.在SV-COMP 2022竞赛的并发程序数据集上进行了对比实验,并对工具的效率进行比较分析.实验结果表明,该工具可以有效地提升并发程序模型检测的效率.特别是,与基于BDD的程序分析算法相比,该工具可使探索状态数目平均减少91.38%,使时间和空间开销分别平均降低86.25%和69.80%.     

C程序并发行为控制方法及其测试工具支持

针对由于并发程序的行为不可控而导致难以对其进行测试的问题,提出了一种控制C程序中并发行为的方法。该方法以多线程同步为基础,使用测试序列和测试单位完成对并发行为的控制。在此基础上,实现了对C程序测试活动中并发行为控制的工具支持,以生产者-消费者为例说明了使用此工具进行测试活动,并讨论了其效率。     

Algebraic specifications and sequencing: A defect detection method

One class of program defects results from illegal sequences of otherwise legal operations in software implementations. Explicit statement of sequencing constraints, however, is not a common activity when specifying software even when using formal specification methods. This paper shows that constraints on program execution sequences can be derived directly from algebraic specifications. Results include heuristic methods for generating sequencing constraints and a generalization of these methods into automatable rules. The heuristics can be integrated into a specification methodology such as Larch. Engineers can use the generated sequencing constraints to detect sequencing defects in software even before dynamic testing begins. The method can be used to increase the reliability of software that is specified using algebraic methods.     

Use of sequencing constraints for specification-based testing ofconcurrent programs

This paper presents and evaluates a specification-based methodology for testing concurrent programs. This methodology requires sequencing constraints, which specify restrictions on the allowed sequences of synchronization events. Sequencing constraints for a concurrent program can be derived from the program's formal or informal specification. Details of the proposed testing methodology based on the use of Constraints on Succeeding and Preceding Events (CSPE) are given. How to achieve coverage and detect violations of CSPE constraints for a concurrent program, according to deterministic and nondeterministic testing of this program, are described. A coverage criterion for CSPE-based testing is defined and analyzed. The results of empirical studies of CSPE-based testing for four concurrent problems are reported. These results indicate that the use of sequencing constraints for specification-based testing of concurrent programs is a promising approach     

基于约束的软件失效域识别与特征分析

随机测试是实践中广泛采用的一种黑盒测试方法.近年来提出的适应性随机测试方法改进了随机测试的不足,仿真实验结果表明,改进效果取决于软件失效域的特征.提出以测试约束刻画软件失效域在输入域上的分布,探讨了基于现有的程序分析技术构造测试约束的过程,讨论了基于测试约束的软件失效域的特征分析方法.以一个实例软件验证所提出的测试约束构造过程及其软件失效域特征分析方法.测试约束揭示了软件故障的触发与传播的内在机制,基于测试约束的软件失效域的特征分析方法有助于改进测试用例的设计质量以及评价适应性随机测试方法的适用性.     

Variable strength combinatorial testing of concurrent programs

Reachability testing is an important approach to testing concurrent programs. It generates and exercises synchronization sequences automatically and on-the-fly without saving any test history. Existing reachability testing can be classified into exhaustive and t-way testing. Exhaustive testing is impractical in many cases while t-way testing may decrease the capability of fault detection in some cases. In this paper, we present a variable strength reachability testing strategy, which adopts the dynamic framework of reachability testing and uses a variable strength combinatorial strategy. Different parameter groups are provided with different covering strength. Variable strength testing covers no t-way combinations but the necessary combinations of parameters having mutual interactions in a concurrent program. It is more reasonable than t-way testing because uniform interactions between parameters do not often exist in concurrent systems. We propose a merging algorithmthat implements the variable strength combinatorial testing strategy and conduct our experiment on several concurrent programs. The experimental results indicate that our variable strength reachability testing reaches a good tradeoff between the effectiveness and efficiency. It can keep the same capability of fault detection as exhaustive reachability testing while substantially reducing the number of synchronization sequences and decreasing the execution time in most cases.     

A combinatorial testing strategy for concurrent programs

One approach to testing concurrent programs is called reachability testing, which derives test sequences automatically and on‐the‐fly, without constructing a static model. Existing reachability testing algorithms are exhaustive in that they are intended to exercise all possible synchronization sequences of a concurrent program with a given input. In this paper, we present a new testing strategy, called t‐way reachability testing, that adopts the dynamic framework of reachability testing but selectively exercises a subset of synchronization sequences. The selection of the synchronization sequences is based on a combinatorial testing strategy called t‐way testing. We present an algorithm that implements t‐way reachability testing, and report the results of several case studies that were conducted to evaluate its effectiveness. The results indicate that t‐way reachability testing can substantially reduce the number of synchronization sequences exercised during reachability testing while still effectively detecting faults. Copyright © 2007 John Wiley & Sons, Ltd.