.png){kind=icon}
.png){kind=icon}
Return
SIT-SE: A Specification-Based Incremental Testing Method With Symbolic Execution
.png){kind=icon}
OA
AI
DOI：10.1109/TR.2021.3078714.png)
.png){kind=icon}
.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
Symbolic execution is a powerful technique for automating software testing to detect many types of errors such as memory errors and assertion violations. However, it encounters the problem of path explosion, and by using only assertions, it still lacks the capability of going deep into checking the functional correctness of a path based on corresponding formal specifications. To address these problems, we propose a specification-based incremental testing method with symbolic execution, called SIT-SE, providing a much more rigorous way to automatically check the functional correctness of all the discovered program paths, by introducing theorems (instead of assertions) for path correctness and branch sequence coverage algorithm for guiding a moderate path exploration. Compared with Hoare logic for proving the correctness of an entire program, a theorem in the SIT-SE is made for verifying the correctness of a program path. The proposed method carefully treats the relationship between a path condition and the specification in a theorem to restrict the monotonous path exploration, whereas traditional concolic testing methods roughly use one test data to determine the path correctness by assertions during long path searching. We use a classic case to demonstrate how the method works and conduct an experiment to evaluate the performance of both the proposed method and the commonly used well-known concolic testing tool KLEE. The experimental results show that our method SIT-SE is effective and outperforms KLEE in detecting faulty paths based on specifications.
Keywords:
Testing
Java
Tools
Metals
Input variables
Software
Computer bugs
Bug detection
concolic testing
path correctness
specification-based testing (SBT)
symbolic execution
test data generation
AI Summary
Key information extracted from the uploaded paper, including a brief overview, abstract, background, key highlights, visual analysis, and future outlook.
Journal
IF:
5.7
Papers:
2.7K
Citations:
8.5K