Please use this identifier to cite or link to this item:
http://hdl.handle.net/10397/94343
Title: | Documentation-based functional constraint generation for library methods | Authors: | Jiang, R Chen, Z Pei, Y Pan, M Zhang, T Li, X |
Issue Date: | Dec-2021 | Source: | Software testing verification and reliability, Dec. 2021, v. 31, no. 8, e1785 | Abstract: | Although software libraries promote code reuse and facilitate software development, they increase the complexity of programme analysis tasks. To effectively analyse programmes built on top of software libraries, it is essential to have specifications for the library methods that can be easily processed by analysis tools. However, the availability of such specifications is seriously limited at the moment. Manually writing the specifications can be prohibitively expensive and error-prone, while existing automated approaches to inferring the specifications seldom produce results that are strong enough to be used in programme analysis. In this work, we propose the DOC2SMT approach to generating strong functional constraints in SMT for library methods based on their documentations. DOC2SMT first applies natural language processing (NLP) techniques and a set of rules to translate a method’s natural language documentation into a large number of candidate constraint clauses in OCL. Then, it utilizes a manually enhanced domain model to identify OCL candidate constraint clauses that comply with the problem domain in static validation, translates well-formed OCL constraints into the SMT-LIB format, and checks whether each SMB-LIB constraint rightly abstracts the functionalities of the method under consideration via testing in dynamic validation. In the end, it reports the first functional constraint that survives both validations to the user as the result. We have implemented the approach into a supporting tool with the same name. In experiments conducted on 451 methods from the Java Collections Framework and the Java IO library, DOC2SMT generated correct constraints for 309 methods, with the average generation time for each correct constraint being merely 2.7 min. We have also applied the generated constraints to facilitate symbolic-execution-based test generation with the Symbolic Java PathFinder (SPF) tool. For 24 utility methods manipulating Java container and IO objects, SPF with access to the generated constraints produced 51.2 times more test cases than SPF without the access. | Keywords: | Documentation analysis Domain model OCL SMT Specification generation |
Publisher: | John Wiley & Sons | Journal: | Software testing verification and reliability | ISSN: | 0960-0833 | EISSN: | 1099-1689 | DOI: | 10.1002/stvr.1785 | Rights: | © 2021 John Wiley & Sons Ltd. This is the peer reviewed version of the following article: Jiang, R, Chen, Z, Pei, Y, Pan, M, Zhang, T, Li, X. Documentation-based functional constraint generation for library methods. Softw Test Verif Reliab. 2021; 31:e1785, which has been published in final form at https://doi.org/10.1002/stvr.1785. This article may be used for non-commercial purposes in accordance with Wiley Terms and Conditions for Use of Self-Archived Versions. This article may not be enhanced, enriched or otherwise transformed into a derivative work, without express permission from Wiley or by statutory rights under applicable legislation. Copyright notices must not be removed, obscured or modified. The article must be linked to Wiley’s version of record on Wiley Online Library and any embedding, framing or otherwise making available the article or pages thereof by third parties from platforms, services and websites other than Wiley Online Library must be prohibited. |
Appears in Collections: | Journal/Magazine Article |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
Jiang_Documentation-based_Functional_Constraint.pdf | Pre-Published version | 1.23 MB | Adobe PDF | View/Open |
Page views
73
Last Week
1
1
Last month
Citations as of Oct 13, 2024
Downloads
18
Citations as of Oct 13, 2024
SCOPUSTM
Citations
1
Citations as of Oct 17, 2024
Google ScholarTM
Check
Altmetric
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.