基于变更模型的元数据在构件回归测试中的应用研究

本文针对Orso元数据方法的不足,对构件可能的变更进行了充分分析和分类,并按照分类情况对相关的构件变更处理方法进行了详尽的形式化描述,构造了构件变更模型,描述了每个变更的具体表现形式,论述了方法变更到构件接口变更的映射机制和算法,给出了算法实现的框架,并将这些理论模型应用到自主开发的构件RegisterStuGrade中,与没有元数据情况下的回归测试用例生成技术以及Orso方法进行回归测试用例数和回归测试运行时间两方面的分析和对比,给出了比较结果.     

面向测试的多视图构件模型

构件模型不仅是构件使用者理解、使用构件的重要依据,也是构件开发者和构件使用者测试构件的基础。目前已有的构件模型主要从分析设计以及使用的角度描述构件,对构件测试中的测试要素的描述并不充分。在分析已有构件模型和构件测试要素的基础上,提出了扩展UML2．0描述的面向测试的多视图构件模型,并给出了实例。     

Internet环境下一种基于数据流的构件组装模型

随着Internet上提供在线复用的构件增多，用这种构件服务组装软件系统就成为可能．本文首先针对Internet环境构件组装系统分析了现有相关技术的不足，讨论了组装技术应用上的关键问题．为此将构件与传统的数据流计算模型相结合，设计并实现了支持广域构件组装的DFCM组装框架；给出了DFCM的总体结构，描述了其中的关键技术；经过对原型系统的模拟表明该模型框架是有效的，能够充分利用Internet固有的并行性，具有扩展性．     

基于模型检验的构件验证技术研究进展

模型检验以其自动化程度和完备性高、与构件技术互补性强等特点,在软件构件可信性质的分析和验证中发挥着日益重要的作用.将基于模型检验的构件验证方法分为基于系统规约模型的验证和基于源代码的验证,分别对其研究现状和发展动态进行了详细的综合评述.首先对模型检验与构件可信性质验证的关系进行了探讨,接着对基于SOFA,Fractal,CORBA及各种特定构件模型的验证方法和基于转化思想的源码验证、面向源码的直接验证及面向可执行代码的动态验证方法分别进行了评述.最后,指出了基于模型检验的构件验证技术所面临的主要挑战和未来的发展方向.     

用模型检验产生约简测试集

基于模型检验的自动化测试技术已经得到普遍应用,由于测试用例自动化生成过程中会产生巨大的资源消耗,优化问题越来越受到软件测试行业的广泛关注。提出一种基于节点权重的性质覆盖度计算方法,在模型检验器自动化生成测试用例之前对测试目标排序,能够更有效地检测到冗余性质,从而减少模型检验器被调用执行次数并且避免大规模的测试用例生成。     

基于耦合测试信息元数据模型的构件集成测试

文中提出一个方法,由构件开发方提供有关构件内接口变量定义和使用的信息,以提高构件的可测试性和可理解性.形式化地定义了构件耦合测试准则,定义-使用属性和观察点值.在此基础上,引入包含上述两项属性的定义-使用表(DU表),给出基于该表的构件框架.最后将上述方法应用于自主开发的构件中,并生成了相应的测试用例.将文中提出的方法与Orso方法和Kan方法进行了相关的比较,结果表明文中方法无论在测试用例生成,还是在变异发现上都更有效.     

基于构件的数据流软件可靠性模型

基于构件的数据流软件由输入数据激活的构件确定程序执行路径,其可靠性受输入数据分布特性的影响,难以采用基于状态或基于路径等传统模型进行评测。提出一个结合构件执行频度和操作剖面的可靠性模型,其从分析数据流程序结构入手,通过定义组合节点,将程序表示成多级层次结构的形式。根据构件间数据流和控制流关系,确定实际激活的构件,计算其执行频度,并将操作剖面沿着数据流向本层和下层构件传递。利用基于深度优先的递归算法思想,按照相反顺序,逐层估算各级组合节点的可靠性,最后获得整个软件的实际可靠性。应用实例表明,模型能有效地佑算基于构件数据流软件的实际可靠性,反映输入接口有效数据就绪状态及分布特性。     

接口变异在构件测试中的应用研究

对于构件使用者来说,源代码的不可得性决定了测试构件需要从构件的接口层面上进行。文章首先介绍了变异测试和遗传算法的概念;接着将遗传算法运用到构件接口变异上,通过变异测试过程获取有效而充分的测试用例,进而对构件进行测试;最后通过一个实例验证这种测试策略。     

构件功能行为测试的研究

由于构件的内部信息屏蔽和演变速度快等特点,使用者在验证构件所提供的功能与其需求是否真正一致时往往比较困难.我们用接口自动机为构件的行为建模,研究构件功能行为的测试问题.首先提出基于简单运行的测试准则,然后介绍了从构件模型中生成简单运行序列并获得功能行为的算法,最后用一个实例对所提出的方法进行了说明并与相关方法进行了对比.文中介绍的方法在系统级别对构件整体行为进行测试,可自动生成测试序列,有利于构件的验证和测试.     

面向测试的构件系统模型及测试用例生成方法

随着面向构件的软件开发方法的广泛应用,构件系统的描述和测试成为保证软件质量的关键所在。由于构件系统的复杂性和开发方法的特殊性,用传统方法对构件系统进行集成测试往往面对很多困难。提出了一种改进的面向测试的构件描述模型,称为TCSM,它着重对构件系统中的构件间的交互和约束进行了动态描述,为构件系统集成测试阶段的功能测试和边界测试等提供了大量可用信息。在此基础上,进一步提出一种把TCSM转换成测试模型的方法,以UML协作图模型为原型,实现了构件系统从描述模型到测试模型的自动转换。最后,实现了一种在所产生的测试模型上自动生成测试用例的算法。TCSM更好地描述了构件的交互行为信息,进一步实现了系统的自动化测试,减少了通常需要在构件系统搭建完成后,针对测试对系统手工建立测试模型的工作,提高了构件系统开发的效率和可靠性。     

模型检测在软件测试中的应用

随着计算机软硬件系统日益复杂,如何保证其正确性和可靠性成为日益紧迫的问题。在为此提出的诸多理论和方法中,模型检测（model checking）以其简洁明了和自动化程度高而引人注目。具体介绍了模型检测的一些理论,同时将它应用于具体的软件程序,运用模型检测方法对软件进行测试。从而证明了模型检测方法与测试结合对于软件可靠性和正确性所起的巨大作用。     

任务流模型检验的研究

对任务流模型检验技术进行了讨论。任务流方法不关心状态数量、能否从一个指定状态到达另一指定状态及系统必须的状态是否存在,而是关心状态组合提供的功能是否存在及各状态组合之间是否存在指定的转换关系,从而避免了状态空间爆炸问题。模块搜索算法以模块为基础对任务流模型进行搜索来验证给定系统是否满足规范要求。     

RSTT模型在空间数据检查软件中的应用

针对如何保证大量测绘采集的图形数据能满足空间数据建库的要求,提出一套可以提供规范、通用、自动、高效的数据检查软件,通过质检任务、质检方案、质检模板和质检规则的四要素质检模型,实现质检软件的可配置化和工程化解决思路,支持质检方案的动态定制。结果证明该软件可实现大部分空间数据类型的质量检测。     

一种合约检查的构件测试方法

构件复用是提高软件开发效率的有效途径,构件测试是保证构件质量的重要手段。针对目前构件测试的现状,对构件测试进行了深入研究,提出了一种合约检查的构件测试方法,将Bertrand Meyer的合约概念引入到构件设计开发测试过程中,从构件开发者和复用者的角度分析构件及构件的测试,违反构件合约时抛出异常信息,快速定位异常位置,提高软件开发的效率。     

变量极小不可满足在模型检测中的应用

提出一个结合变量抽象和有界模型检测(BMC)的验证框架,用于证明反例不存在或输出存在反例.引入变量极小不可满足(VMU)的数学概念来驱动抽象精化的验证过程.一个VMU公式F的变量集合是保证其不可满足性的一个极小集合.严格证明了VMU驱动的精化满足抽象精化框架中的两个理想性质:有效性和极小性.虽然VMU的判定问题和极小不可满足(MU)一样难,即DP完全的,该案例研究表明,在变量抽象精化过程中,VMU比MU更为有效.     

模型检测在软件测试中的应用研究

以测试为基础的模型或规格是产生测试用例的一种很有潜力技术。在这种方法中,先要建立一个系统的规格或模型,再由规格或模型产生测试用例。文章对结合模型检测来进行测试的方法进行了研究,从整体上对测试进行考虑,不仅包含了对系统所希望具有的功能进行测试,还包括了对系统不应具有的功能进行测试。通过这种方法,我们可以进一步保证系统的正确性和可靠,大大降低人力和资源的开销,为进一步优化测试奠定了基础。     

An Experimental Evaluation of Data Flow and Mutation Testing

Two experimental comparisons of data flow and mutation testing are presented. These techniques are widely considered to be effective for unit-level software testing, but can only be analytically compared to a limited extent. We compare the techniques by evaluating the effectiveness of test data developed for each. We develop ten independent sets of test data for a number of programs: five to satisfy the mutation criterion and five to satisfy the all-uses data-flow criterion. These test sets are developed using automated tools, in a manner consistent with the way a test engineer might be expected to generate test data in practice. We use these test sets in two separate experiments. First we measure the effectiveness of the test data that was developed for one technique in terms of the other. Second, we investigate the ability of the test sets to find faults. We place a number of faults into each of our subject programs, and measure the number of faults that are detected by the test sets. Our results indicate that while both techniques are effective, mutation-adequate test sets are closer to satisfying the data flow criterion, and detect more faults.     

含信息流检测的扩展的访问控制模型

介绍了一种含信息流检测的扩展的XACML(可扩展的访问控制标记语言)访问控制模型,解决了一些现有模型中存在的两个问题,给出信息流检测的算法,并提出和分析了有待进一步研究的方向和问题.     

反例引导的C代码空间流模型检测方法

软件验证一直是确保软件正确性和安全性的热点研究问题.然而,由于程序语言复杂的语法语义特性,应用形式化方法验证程序的正确性存在准确度低和效率差的问题.其中,由指针操作带来的地址空间的状态变化使得现有模型检测方法的检测准确度难以得到保证.为此,通过结合模型检测与稀疏值流分析方法,设计了一种空间流模型,实现了对C程序在符号变量层面和地址空间层面的状态行为的有效描述,并提出了一种反例引导的抽象细化和稀疏值流强更新算法(CEGAS),实现了C程序指向信息敏感的形式化验证.建立了包含多种指针操作的C代码基准库,并基于该基准库进行了对比实验.实验结果表明:所提出的模型检测算法CEGAS在分析含有多种C代码特性的任务中,与现有模型检测工具相比均能取得突出的结果,其检测准确度为92.9%,每行代码的平均检测时间为2.58 ms,优于现有检测工具.     

Counterexample-guided Spatial Flow Model Checking Methods for C Code

Software verification has always been a popular research topic to ensure the correctness and security of software. However, due to the complex semantics and syntax of programming languages, the formal methods for verifying the correctness of programs have the problems of low accuracy and low efficiency. In particular, the state change in address space caused by pointer operations makes it difficult to guarantee the verification accuracy of existing model checking methods. By combining model checking and sparse value-flow analysis, this paper designs a spatial flow model to effectively describe the state behavior of C code at the symbolic-variable level and address-space level and proposes a model checking algorithm of CounterExample-Guided Abstraction refinement and Sparse value-flow strong update (CEGAS), which enables points-to-sensitive formal verification for C code. This paper establishes a C-code benchmark containing a variety of pointer operations and conducts comparative experiments on the basis of this benchmark. These experiments indicate that in the task of analyzing multi-class C code features, the model checking algorithm CEGAS proposed in this paper can achieve outstanding results compared with the existing model checking tools. The verification accuracy of CEGAS is 92.9%, and the average verification time of each line of code is 2.58 ms, both of which are better than those of existing verification tools.