? 对于包含字符串以及字符串函数的程序的自动化约束求解方法
Journal of Computer Science and Technology
Quick Search in JCST
 Advanced Search 
      Home | PrePrint | SiteMap | Contact Us | Help
 
Indexed by   SCIE, EI ...
Bimonthly    Since 1986
Journal of Computer Science and Technology 2017, Vol. 32 Issue (6) :1125-1135    DOI: 10.1007/s11390-017-1787-y
Special Section on Software Systems 2017 << Previous Articles | Next Articles >>
对于包含字符串以及字符串函数的程序的自动化约束求解方法
Xu-Zhou Zhang1, Yun-Zhan Gong1, Member, CCF, Ya-Wen Wang1, Member, CCF, Ying Xing2, Member, CCF, Ming-Zhe Zhang1
1 State Key Laboratory of Networking and Switching Technology, Beijing University of Posts and Telecommunications Beijing 100876, China;
2 Automation School, Beijing University of Posts and Telecommunications, Beijing 100876, China
Automated String Constraints Solving for Programs Containing String Manipulation Functions
Xu-Zhou Zhang1, Yun-Zhan Gong1, Member, CCF, Ya-Wen Wang1, Member, CCF, Ying Xing2, Member, CCF, Ming-Zhe Zhang1
1 State Key Laboratory of Networking and Switching Technology, Beijing University of Posts and Telecommunications Beijing 100876, China;
2 Automation School, Beijing University of Posts and Telecommunications, Beijing 100876, China

摘要
参考文献
相关文章
Download: [PDF 819KB]  
文章导读 null
摘要 对于各种类型的约束的支持是约束求解器首要指标。在编程语言中,字符串类型经常作为基本的数据类型出现,并且通过字符串库函数进行操作。当以字符串约束作为输入时,大多数约束求解器存在着无法处理复杂的字符串库函数约束或者无法求解混合约束等局限性。这些局限性阻碍了约束求解器在程序分析、自动测试等领域的应用。基于字符数组的数据模型,我们设计了一个包含有限原子操作的约束描述语言,来准确描述常用的字符串操作函数的约束。然后利用一个两步骤的约束求解过程求解转换之后的字符串约束和其他类型的约束:第一,得到关注字符串的字符成员位置约束的部分解,利用此部分解来将字符串约束约简为字符数组约束;第二,利用现成的约束求解器对约简之后的约束进行求解。
本文所提出的方法在一个自动测试工具中进行了实现,实验结果表明了本方法的有效性,对比试验表明本文所提出的技术相比于同类技术的应用效果有了提升。
关键词字符串约束求解   约束可满足性理论   程序分析   软件测试   自动测试用例生成     
Abstract: The ability to solve various constraints is a principal factor of automatic constraint solvers. Most object-oriented languages treat a character string as a primitive data type which is manipulated by string library functions. Most constraint solvers have limitations on their input constraints, such as strong restrictions on the expressiveness of constraints or lack of the ability to solve hybrid constraints. These limitations hinder applying automated constraint solvers on program analysis techniques for programs containing strings and string manipulation functions. We propose an approach to automatically solve program constraints involving strings and string manipulation functions. Based on the character array model, we design a constraint language which contains primitive operations to precisely describe the constraints of commonly used string manipulation functions. The translated string constraints together with numeric constraints are then solved by a twophase test generation procedure:firstly, a partial solution is obtained to satisfy the arithmetic constraints of the position variables, and the solution is utilized to simplify the string constraints into pure character array constraints; secondly, the pure array constraints are solved by an off-the-shelf array-specific theory based constraint solver. We integrate the approach into an automated testing tool to support the generation of string test cases, and then perform experiments. The results of the experiments prove that the integration of the proposed approach promotes the testing coverage of the existing testing tool, and the integrated tool has an advantage of handling specific string manipulation functions compared with an existing string solver.
Keywordsstring constraints solving   satisfaction module theory   program analysis   software testing   automated test input generation     
Received 2017-04-27;
本文基金:

This work was partially supported by the National Natural Science Foundation of China under Grant Nos. 61202080, 61702044, and 61502029.

About author: Xu-Zhou Zhang received his B.S.degree in computer science and technology from Huazhong University of Science and Technology,Wuhan,in 2010.He is currently a Ph.D.candidate in the State Key Laboratory of Networking and Switching Technology,Beijing University of Posts and Telecommunications,Beijing.His research interest is program analysis and software testing.
引用本文:   
Xu-Zhou Zhang, Yun-Zhan Gong, Ya-Wen Wang, Ying Xing, Ming-Zhe Zhang.对于包含字符串以及字符串函数的程序的自动化约束求解方法[J]  Journal of Computer Science and Technology , 2017,V32(6): 1125-1135
Xu-Zhou Zhang, Yun-Zhan Gong, Ya-Wen Wang, Ying Xing, Ming-Zhe Zhang.Automated String Constraints Solving for Programs Containing String Manipulation Functions[J]  Journal of Computer Science and Technology, 2017,V32(6): 1125-1135
链接本文:  
http://jcst.ict.ac.cn:8080/jcst/CN/10.1007/s11390-017-1787-y
Copyright 2010 by Journal of Computer Science and Technology