中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
基于约束求解的自动化软件测试研究
作者: 严俊
答辩日期: 2007-05-29
授予单位: 中国科学院软件研究所
授予地点: 软件研究所
学位: 博士
关键词: 约束求解 ; 自动化软件测试 ; 测试生成 ; 最优测试集 ; 测试准则
其他题名: Automated Software Testing Based on Constraint Processing
摘要: 软件质量问题是工业界和学术界共同关注的热点问题. 软件测试是软件生产质量保障中的一项重要技术, 它的主要目的是尽可能地减少程序的错误. 本文着重研究了如何将约束求解应用到自动化软件测试. 这些研究大致可以分为如下三个方面. 本文第一方面的工作是关于白盒测试的研究. 白盒测试是面向程序代码的精确测试方法. 我们可以采用符号执行的方法来处理程序中的路径, 进而测试程序某些方面的性质. 然而, 由于符号执行的代价比较高, 测试程序的所有路径几乎不可能; 同时由于不可行路径的影响, 我们需要采用一些合适的测试准则或者路径选择策略来指导我们生成测试路径集合. 这一方面的工作包括两个部分.1) 本文提出了一种有效地产生可行基本路径的自动化方法, 能在可接受的时间内针对真实C 单元程序生成可行的基本路径. 这种方法产生的基本路径集合的带权路径长度的总和是最小的. 2) BPEL 是一种业务流程描述语言, 它可以表达程序复杂的并发行为. 本文提出了一种新颖的基于并发路径分析的BPEL 测试生成方法. 我们采用了一些限制组合的技术以及路径覆盖准则来避免测试路径的组合爆炸. 这个框架是模块化的, 所以很多测试中采用的技术, 比如不同的测 试准则和约束处理技术, 可以应用到其中. 本文第二方面的工作属于黑盒测试. 黑盒测试用于对程序的功能和接口进行测试. 我们可以用约束描述被测系统的规约或者测试准则, 在这种情况下, 黑盒测试用例的生成问题可以转化为有限约束满足问题. 这一部分的工作也包含两部分. 1) 提出了基于SAT 和回溯搜索算法的方法来解决组合测试生成问题. 并提出了一个新颖的剪枝策略SCEH, 用于提高算法的效率. 一些已有的启发式搜索策略, 以及一些对称打破技术, 也被应用到我们的回溯搜索算法中. 实验结果表明, 我们的方法在一些小规模实例上的表现优于其它的方法. 2) 对于针对布尔规范的MUMCUT 测试准则, 本文提出了一种基于SAT 的自动测试生成方法. 为了提高采用完备性SAT 工具时的求解效率, 我们采用了一些对称打破技术. 本文第三方面的工作是分析线性数值约束的逻辑关系. 在程序分析和验证中, 相同的约束可能会需要反复处理. 一种可能的加速方法就是预先找到约束之间的逻辑关系. 这种关系可以用规则来描述. 我们不大可能在多项式时间内找到所有的规则. 本文提出了一种基于搜索的算法, 以及一些启发式策略, 用于 寻找这些规则. 实验结果表明我们的方法能够在可接受的时间内产生足够的规则.
英文摘要: The quality of software is a hot topic attracting attentions from both researchers and practitioners. Software testing is an important technique to guarantee the quality of software. It aims to reduce the software faults as much as possible. The author studied the problem of how to apply the constraint satisfaction techniques to software testing automatically. The study can be divided into the following three parts. The first part of this article is related to white-box testing. White-box testing is an accurate code-based software testing method. We can employ symbolic execution techniques to process the program paths, so as to test some features of programs. However, the complexity of symbolic execution technique makes it impossible to test all the paths of the program under test. Furthermore, some of the program paths may be infeasible. Therefore we need some test criteria and path selection strategies to guide the generation of the test paths. This part of work includes the following two aspects. 1) An efficient method is presented to generate a set of feasible basis paths. This method can generate feasible basis paths for real-world C unit programs automatically in acceptable time. The basis path set generated by this method has the minimum sum of weighted length. 2) BPEL is a business description language that could express complex concurrent behaviors. This paper presents a novel method of BPEL test case generation, which is based on concurrent path analysis. To avoid the combination explosion of the path number, some techniques and test criteria are used to restrict the combination. This method is modularized so that many test techniques, such as various test criteria and complex constraint solvers, can be applied. The second part of work is about black-box testing. Black-box Testing is used to test the functions and interfaces of programs. We can use constraints to describe the test criteria and the specifications of Software Under Test. Therefore the test generation for black-box testing can be translated into the finite domain constraint satisfaction problem. This part also includes two aspects. 1) A SAT-based approach and a backtracking search algorithm are presented to solve the problem. A novel pruning strategy called SCEH is proposed to increase the efficiency of the methods. Several existing search heuristics and symmetry breaking techniques are also used in the backtracking search algorithm. The experiments show that our method outperforms other methods in many small size cases. 2) This paper proposes a SAT-based method to generate the test cases automatically for MUMCUT testing of boolean specifications. To speed up the processing for the complete SAT tools, we make use of some symmetry breaking techniques. The last part of this paper studies the problem of finding Boolean relations among a set of linear numerical constraints. In program analysis and verification, there are some constraints that have to be processed repeatedly. A possible way to speed up the processing is to find some relations among these constraints first. The relations can be represented by rules. It is believed that we can not generate all the rules in polynomial time. A search based algorithm with some heuristics to speed up the search process is proposed. Experimental results with various examples show that our method can generate enough rules in acceptable time.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/7056
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
10001_200418015029030严俊_paper.pdf(1140KB)----限制开放-- 联系获取全文

Recommended Citation:
严俊. 基于约束求解的自动化软件测试研究[D]. 软件研究所. 中国科学院软件研究所. 2007-05-29.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[严俊]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[严俊]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2017  中国科学院软件研究所 - Feedback
Powered by CSpace