面向构件接口变异的模型检验技术研究

随着构件技术在软件开发中的广泛应用,人们对构件化软件系统质量的要求也在不断提高。该文运用模型检验技术进行接口变异测试的相关研究工作。该文首先详细介绍了基于模型检验技术的变异测试的基本原理,随后通过对构件集成时接口之间的交互关系进行分析后,提出了通过构造接口函数调用关系模型进行基于模型检验的接口变异测试方法。最后,通过实例进行了对JavaBean构件的接口测试用例的自动生成。     

程序切片技术浅析

程序切片技术是一种重要的程序分析理解方法,可以帮助开发人员和维护人员理解程序的结构和作用。随着编程语言逐渐趋于人性化、多功能化和复杂化,为了适应编程语言的这种进步,程序切片技术也在不断的演化发展着。文章中主要介绍了程序切片技术的一些基本的准则,介绍了程序切片的一些类型,以及如何利用源程序和图形进行程序切片,并且进行了举例说明。     

并发程序的切片模型检验方法

提出了一种对并发程序进行切片以缩减模型检验状态空间的方法，首先针对并发程序中的同步与通信定义了一组依赖关系，包括并发分支与接合．非确定性，信道，共享变量等特征，对于从要验证的时态逻辑性质中提取的关于多个程序点的切片标准，文中给出算法根据相应的依赖关系通过不动点运算得到并发程序切片，可以证明得到的切片与原程序对于该性质具有相同的可满足性。     

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

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

基于交际接口的Web应用模型检验

为了验证Web应用的质量,首次采用了基于交际接口及其工具TICC的建筑智能化系统Web应用验证方法,通过一个简单的能源管理Web应用系统实例说明了整个建模、构件模块组合验证和系统性质验证过程.结果表明验证能够顺利实现,因而该方法是一种合适的Web应用验证方法.     

过程模型切片技术的研究

将程序切片技术引入到过程模型中,定义过程模型中的关联关系和数据连接关系,在此基础上给出了过程模型的切片定义,并定义了过程模型的三种切片：前向切片,后向切片和双向切片,提出了前向切片、后向切片和双向切片的算法,最后通过实例分析证明了该算法的可行性和实用性。     

一种基于Java程序分层模型的方法内切片生成算法

程序切片作为软件理解领域的一种重要的分析技术,可以将程序分解为独立的程序线程。系统依赖图的概念及两阶段图形可达性算法的出现,则有效解决了程序切片的过程调用问题。文章介绍了程序切片的基本概念,并给出了在面向对象程序中进行静态分层切片的思想。作为分层切片思想的应用,文章给出了在一种Java程序切片工具模型JSTM(JavaSlicingToolsModel)中运用系统依赖图进行方法内切片的具体算法。     

模型检验在构件数据流测试中的应用

模型检验输出的反例提供了一种自动产生测试用例的有效途径。提出了一种用模型检验进行构件数据流测试的方法。利用构件状态机描述构件的外部行为,用带有变量定义和使用标记的Kripke结构描述构件状态迁移中的数据流信息;给出了从构件状态机到Kripke结构的转换方法,并建立了全定义覆盖和全使用覆盖准则的陷阱性质构造公式。陷阱性质将使模型检验器NuSMV输出反例,从而产生构件的数据流测试序列。     

基于方法切片及入口依赖的回归测试研究

为了提高大型软件回归测试效率,将程序切片思想应用于回归测试用例选择过程,提出了方法切片及入口依赖的概念。切片算法MethodSlice以方法为基本单元进行切片,提取软件变化影响点,仅选择那些受源程序修改部分影响的测试用例进行回归测试。实验结果表明:与传统的程序切片相比,方法切片更易用于大型软件的回归测试过程中,其实现简单,不易出错,在一定程度上提高了软件回归测试效率。     

基于模型的软件接口故障注入测试平台技术

针对软件接口类型多、接口故障注入自动控制复杂的困难以及目前缺少有效的软件接口故障注入工具现状,对软件故障注入中的交联接口故障注入技术展开研究,提出了一种基于模型的软件接口故障注入测试平台技术。通过交联接口测试可视化建模和接口故障注入算子设计,自动生成XML 格式的测试用例,并且通过基于XSLT的脚本自动化生成与执行技术实现测试的控制与执行。故障注入测试主机与接口故障注入器网络连接,接口故障注入器将接口故障数据转换成以太网、串口或CAN网络数据注入到被测软件中,并返回被测件输出数据到测试主机实现测试数据收集与判断。基于模型的软件接口故障注入测试平台具有较强的通用性与易用性,提高了接口故障注入测试的效率,降低了接口测试的成本。     

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

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

基于场景构件式实时软件设计的一致性检验

在复杂的实时软件系统中使用构件式设计方法,已成为目前软件工程中的研究热点.如何有效地验证实时软件的设计是否满足给定的时间规约,是实时计算领域中的主要挑战之一.通过在接口自动机模型中添加时间区间标记,来扩展其对实时系统接口行为的表达能力;使用实时接口自动机网络来描述实时软件系统的构件式设计模型;使用带布尔不等式时间约束的UML顺序图表示基于场景的需求规约,对系统设计阶段实时软件构件的动态行为进行形式化分析与检验.通过对实时接口自动机网络状态空间的分析,构造了其可兼容的整型状态等价类空间的可达图,并在此基础上给出了验证算法,以检验构件式实时软件系统的设计与带时间约束的场景式规约之间的一致性.     

基于程序依赖图的静态BPEL程序切片技术

传统程序切片技术在计算BPEL程序切片时会产生切片不完备问题,为此,提出一种基于程序依赖图的BPEL静态程序切片技术。该技术根据BPEL语言的特点,通过建立BPEL程序依赖图,计算BPEL程序切片。案例分析表明,该技术能够获得更加全面的程序切片,从而可以帮助软件工程人员更好地测试、调试和维护BPEL程序。     

面向体系结构的构件接口模型及其形式化规约

借鉴软件体系结构的思想,提出了面向体系结构的构件接口模型,它既能表达体系结构设计的高层抽象构件,又能表达底层代码级别的实现构件。同时基于该模型,运用顺序通信进程,提出了两级构件接口行为协议规约方法,能够有效规约大粒度复杂软件构件的行为交互协议。     

基于UML图和不同粒度切片的回归测试研究

针对面向对象软件回归测试的新特点,本文引入了基于UML图的不同粒度切片。首先,对描述类间关系的UML类图和描述状态变迁关系的UML状态图形式化定义。接着,对定义的图进行切片分析,其中类间测试提出一种基于UML类图的粗粒度切片工具;类内测试提出一种基于UML状态图细粒度切片的方法。最后,将其应用于销售订单系统,结果表明以上两种分析方法可以有效地提高回归测试效率。     

程序切片技术在并发程序模型检查中的应用

模型检查技术在硬件和协议设计方面已经取得很大成功,但在软件验证方面仍存在很多困难.其主要问题是如何从源代码中自动抽取验证所要模型并精简其状态空间.文中通过对程序切片技术的研究,来解决并发程序验证的建模问题,包括把验证公式映射到切片准则,并把得到的程序切片转化为验证所需的模型.经程序切片处理后,软件模型检查效率得到提高.     

程序切片技术在并发程序模型检查中的应用

模型检查技术在硬件和协议设计方面已经取得很大成功,但在软件验证方面仍存在很多困难。其主要问题是如何从源代码中自动抽取验证所要模型并精简其状态空间。文中通过对程序切片技术的研究,来解决并发程序验证的建模问题,包括把验证公式映射到切片准则．并把得到的程序切片转化为验证所需的模型。经程序切片处理后,软件模型检查效率得到提高。     

基于依赖模型的REST接口测试用例生成方法研究

REST接口中普遍存在依赖关系,导致生成合理的接口调用序列与输入参数变得十分困难。现有的大多数方法只考虑了其中一种依赖关系,并需要人工执行繁杂的前置操作,生成的测试用例有效性仍然较低。针对以上问题,文中提出了一种基于依赖模型的测试用例生成方法。通过解析OpenAPI文档,该方法提取了接口内的操作间依赖关系与参数间依赖关系,并据此建立了两种依赖模型,从模型生成测试用例,最后从3方面确定测试预言。实验结果表明,该方法的输入度量覆盖率达到了100%,状态码类别、状态码、响应资源类型的覆盖率分别达到了100%,91.67%,83.33%,并能在限定时间内检出接口内部缺陷;与RESTler和RESTest相比,该方法的输出度量覆盖率最大提高了36%,触发了最多次的异常响应状态码,检测到接口异常响应的比例最大提高了10%。该方法为REST接口的测试用例生成问题提供了有价值的参考。     

非经典切片技术及其在形式验证中的应用综述

切片技术最初是作为一种程序分解抽取的分析技术而出现的,经过20多年的不断发展和完善,应用范围已遍及软件工程学科的各个方面。特别是从本世纪初,随着非经典切片：计算切片和证明切片两个新兴研究方向的出现,其学术研究和工程价值越发突出。简要地介绍了切片技术思想的起源、发展过程,并着重介绍非经典的计算切片和证明切片技术及其在验证领域的应用。     

基于模型检验的规划综述

基于模型检验的规划是当今通用的规划研究的热点,其求解效率比较高.详细阐述了基于模型检验的规划的发展与研究现状.介绍了基于模型检验的规划的基本框架,分别阐述了模型检验技术在规划领域的重要应用,并介绍了两种典型的基于模型检验的规划工具,分析了今后的发展趋势.