THỰC THI TƯỢNG TRƯNG TRONG SINH TỰ ĐỘNG DỮ LIỆU KIỂM THỬ PHẦN MỀM

Tô Hữu Nguyên, Nguyễn Hồng Tân, Hà Thị Thanh, Đỗ Thanh Mai

Tóm tắt


Trong hoạt động kiểm thử phần mềm, các ca kiểm thử thường được tạo ra một cách thủ công, gây tốn kém về chi phí cũng như thời gian để hoàn thành công đoạn này. Thực thi tượng trưng (Symbolic execution) được biết đến là một kỹ thuật nổi tiếng với khả năng tự động sinh những bộ test case có độ bao phủ cao với các tiêu chí kiểm thử nhằm phát hiện những lỗi sâu trong các hệ thống phần mềm phức tạp. Bài báo trình bày các vấn đề tổng quan và một số kết quả của các nghiên cứu gần đây về kỹ thuật thực thi tượng trưng. Bài báo cũng đưa ra những thách thức cần giải quyết trong lĩnh vực này như: sự bùng nổ đường thực thi của chương trình, khả năng giải các ràng buộc, mô hình hóa bộ nhớ, các vấn đề về tương tranh vv.. đồng thời đưa ra một số đánh giá từ những kết quả đã công bố.

Từ khóa


Dữ liệu kiểm thử; Giải ràng buộc; Ràng buộc; Sinh dữ liệu kiểm thử; Thực thi tượng trưng; Thực thi tượng trưng động.

Toàn văn:

PDF

Các tài liệu tham khảo


R. S. Boyer, B. Elspas, and K. N. Levitt. SELECT – a formal system for testing and debugging programs by symbolic execution. SIGPLAN Not., 10:234–245, (1975).

A. I. Baars, M. Harman, Y. Hassoun, K. Lakhotia, P. McMinn, P. Tonella, and T. E. J. Vos. Symbolic search-based testing. In ASE’11, (2011).

H. Zhu, P. Hall, J. May. Software Unit Test Coverage and Adequacy. ACM Computing Surveys, 29 (4). ISSN 0360-0300, December, pp. 366–427, (1997).

C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI’08, Dec (2008).

J. Burnim and K. Sen. Heuristics for scalable dynamic test generation. In ASE’08, Sept. (2008).

D. Bird and C. Munoz, “Automatic Generation of Random Self- Checking Test Cases,” IBM Systems Journal, vol. 22, no. 3, pp. 229–245, (1983).

C. Cadar and D. Engler. Execution generated test cases: How to make systems code crash itself (invited paper). In SPIN’05, Aug (2005).

C. Cadar, V. Ganesh, P. Pawlowski, D. Dill, and D. Engler. EXE: Automatically generating inputs of death. In CCS’06, Oct–Nov 2006. An extended version appeared in ACM TISSEC 12:2, (2008).

] P. Collingbourne, C. Cadar, and P. H. Kelly. Symbolic crosschecking of floating-point and SIMD code. In EuroSys’11, Apr (2011).

L. A. Clarke. A program testing system. In Proc. of the 1976 annual conference, pages 488–491, (1976).

L. De Moura and N. Bjorner. Satisfiability modulo theories: introduction and applications. Commun. ACM, 54:69–77, Sept. (2011).

B. Elkarablieh, P. Godefroid, and M. Y. Levin. Precise pointer reasoning for dynamic test generation. In ISSTA’09, (2009).

V. Ganesh and D. L. Dill. A decision procedure for bit-vectors and arrays. In CAV’07, July (2007).

P. Godefroid. Compositional dynamic test generation. In POPL’07, Jan. (2007).

P. Godefroid. Higher-order test generation. In PLDI’11, (2011).

P. Godefroid, N. Klarlund, and K. Sen. DART: Directed Automated Random Testing. In PLDI’05, June (2005).

P. Godefroid, M. Levin, and D. Molnar. Automated Whitebox Fuzz Testing. In NDSS’08, Feb. (2008).

W. Howden. Symbolic testing and the DISSECT symbolic evaluation system. IEEE Transactions on Software Engineering, 3(4):266–278, (1977).

K. Inkumsah and T. Xie. Improving structural testing of object-oriented programs via integrating evolutionary testing and symbolic execution. In ASE’08, (2008).

Y. Jia and M. Harman. An analysis and survey of the development of mutation testing. IEEE Trans. Software Eng., 37(5):649–678, (2011).

J. C. King. Symbolic execution and program testing. Commun. ACM, 9:385–394, July (1976).

K. Lakhotia, P. McMinn, and M. Harman. An empirical investigation into branch coverage for C programs using CUTE and AUSTIN. J. Systems and Software, 83(12):2379–91, (2010).

R. Majumdar and K. Sen. Latest: Lazy dynamic test input generation. Technical Report UCB/EECS-2007-36, EECS Department, University of California, Berkeley, Mar (2007).

K. Sen and G. Agha. Automated systematic testing of open distributed programs. In FASE’06, (2006).

K. Sen and G. Agha. CUTE and jCUTE : Concolic unit testing and explicit path model-checking tools. In CAV’06, (2006).

K. Sen, D. Marinov, and G. Agha. CUTE: A concolic unit testing engine for C. In ESEC/FSE’05, Sep (2005).

T. Xie, N. Tillmann, J. de Halleux, and W. Schulte. Fitnessguided path exploration in dynamic symbolic execution. In DSN’09, pages 359–368, (2009).

N. Tillmann and J. de Halleux. Pex - white box test generation for .NET. In TAP’08, Apr (2008).

R. S. Boyer, B. Elspas, and K. N. Levitt. SELECT – a formal system for testing and debugging programs by symbolicexecution. SIGPLAN Not., 10:234–245, (1975).

C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI’08, Dec (2008).Web site

http://msdn2.microsoft.com/vs2008/

http://www.junit.org/

http://www.nunit.org/

http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-symbc




DOI: http://dx.doi.org/10.37569/DalatUniversity.6.2.44(2016)

Các bài báo tham chiếu

  • Hiện tại không có bài báo tham chiếu.


Copyright (c) 2016 Tô Hữu Nguyên, Nguyễn Hồng Tân, Hà Thị Thanh, Đỗ Thanh Mai

Creative Commons License
Công trình này được cấp phép theo Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
Văn phòng Tạp chí Đại học Đà Lạt
Nhà A25 - Số 1 Phù Đổng Thiên Vương, Đà Lạt, Lâm Đồng
Email: tapchikhoahoc@dlu.edu.vn - Điện thoại: (+84) 263 3 555 131

Creative Commons License
Trên nền tảng Open Journal Systems
Thực hiện bởi Khoa Công nghệ Thông tin