Khóa luận Sinh ca kiểm thử tham số hóa cho chương trình Java

uyên thủy (int, float, double, long) thì giá trị của nó được đưa trực tiếp 
lên stack để so sánh và các giá trị tượng trưng của nó được kết hợp luôn cùng các 
thuộc tính của operand stack thì với kiểu dữ liệu String ở trên cũng như các đối tượng 
khác thì việc so sánh thực hiện với các giá trị số học đại diện cho chúng còn bản thân 
các đối tượng đó vẫn lưu trong vùng heap. Như ở ví dụ trên thì giá trị String “K50” 
chính là một đối tượng lưu trong vùng nhớ heap. Và ràng buộc ta muốn xây dựng với 
phương thức đó chính là (s=”K50”) và (s!=”K50”). Rõ ràng để có thể xây dựng được 
các ràng buộc như thế thì cần lấy các giá trị tượng trưng biểu thị cho biến s và hằng 
“K50” lưu trong vùng nhớ heap và xử lý cùng với các thao tác trên stack operand của 
 57
stack frame. Đó chính là việc ta phải làm nếu như muốn thay đổi ngữ nghĩa thực thi 
của chỉ thị bytecode IF_ACMPEQ ở trên theo ngữ nghĩa thực thi tương trưng. 
 Với những chương trình nhận đầu vào có kiểu tham chiếu thì trạng thái của 
chương được thực thi tượng trưng bao gồm cả trạng thái của vùng nhớ heap. Theo [21] 
trạng thái đó bao gồm một cấu trúc heap (heap configuration) chứa giá trị tượng trưng 
của các biến và các trường tham chiếu, một điều kiện đường đi (PC), và biến đếm 
chương trình (program counter). Với đối tượng thì cần phải xây dựng các ràng buộc 
liên quan tới các trường của nó. Và kỹ thuật khởi tạo lười được sử dụng để khởi tạo giá 
trị tượng trưng cho các trường của đối tượng. Với kiểu dữ liệu mảng thì có một giá trị 
tượng trưng biểu thị cho chiều dài của mảng (length), và danh sách các ô mảng (array 
cell). Mỗi ô mảng (phần tử mảng) gồm giá trị tượng trưng biểu thị cho vị trí của ô 
mảng (cell index) và giá trị tượng trưng lưu trong ô mảng đó. Trong JPF thì các lớp 
thư viện tượng trưng đã được xây dựng cho các mảng có kiểu int. Do đó ta cần sử 
dụng các thử viện hỗ trợ thực thi tượng trưng này cùng với khởi tạo lười để thay đổi 
ngữ nghĩa thực thi của các chỉ thị bytecode truy cập (getfield) hay cập nhật (putfield) 
và các chỉ thị bytecode tính toán và rẽ nhánh khác đối với kiểu tham chiếu để có thể 
xây dựng ràng buộc được cho đối tượng. Khi mà ràng buộc liên quan tới các trường 
của đổi tượng được xây dựng và xử lý thì cũng có nghĩa là sẽ có các đối tượng làm đầu 
vào mới được sinh ra. Tuy nhiên, việc mở rộng JPF chưa được thực hiện ngay trong 
khóa luận này mà sẽ là trong tương lai gần. 
 58
KẾT LUẬN 
 Kiểm thử đơn vị tham số hóa đang dần trở lên phổ biến và đóng vai trò vô cùng 
quan trọng trong phát triển phần mềm. Kiểm thử đơn vị tham số hóa giúp giảm đáng 
kể chi phí giành cho việc kiểm thử phần mềm, cải thiện khả năng phát hiện lỗi các 
phần mềm so với phương pháp kiểm thử đơn vị truyền thống trước đây. 
 Nghiên cứu về kiểm thử đơn vị tham số hóa liên quan tới một vấn đề rất rộng 
và phức tạp trong kiểm thử phần mềm đó là sinh dữ liệu kiểm thử tự động. Tuy nhiên 
khóa luận cũng đã đạt được một số kết quả hết sức có ý nghĩa đó là đã làm rõ bản chất 
của kiểm thử đơn vị tham số hóa, phương pháp và các kỹ thuật để sinh dữ liệu kiểm 
thử tự động sao cho có thể kiểm tra được tất cả các trường hợp thực thi của một 
chương trình, mô tả về một hệ thống kiểm thử tổng quát nhất giúp cho việc thực thi 
các ca kiểm thử tham số hóa. Bên cạnh đó khóa luận cũng đã nghiên cứu và ứng dụng 
một nền kiểm chứng Java bytecode mã nguồn mở đang rất phổ biến hiện nay đó là 
Java PathFinder cho việc thực thi các ca kiểm thử tham số hóa viết cho ngôn ngữ Java. 
Từ khả năng của Java PathFinder ta đã xây dựng được một hệ thống kiểm thử để có 
thể thực thi các ca kiểm thử tham số hóa viết cho các chương trình Java đơn giản nhận 
tham số đầu vào có kiểu số học để sinh tự động các ca kiểm thử đơn vị JUnit. Trong 
khóa luận ta cũng đã đề xuất hướng mở rộng Java PathFinder để có thể thực thi tượng 
trưng những chương trình Java nhận đầu vào có kiểu cấu trúc dữ liệu phức tạp nhằm 
mục đích hoàn thiện nền kiểm thử mà ta đã xây dựng. Tất nhiên, việc mở rộng Java 
PathFinder là một vấn đề hết sức phức tạp đi kèm với những kiến thức rất rộng khác 
nữa đó là việc xử lý các ràng buộc, cũng như cơ chế thực thi của các chỉ thị bytecode. 
 Do thời gian có hạn nên nội dung trình bày trong khóa luận chắc chắn còn rất 
nhiều thiếu xót. Tuy nhiên, dựa trên khóa luận này ta có thể mở ra rất nhiều hướng 
nghiên cứu khác như việc mở rộng Java PathFinder để hỗ trợ việc thực thi tượng trưng 
các chương trình Java nhận đầu vào có kiểu cấu trúc dữ liệu phức tạp, nghiên cứu để 
cài đặt một hệ thống kiểm thử cho việc thực thi các ca kiểm thử tham số hóa viết trong 
ngôn ngữ Java sử dụng kỹ thuật thực thi tượng trưng động. 
TÀI LIỆU THAM KHẢO 
Tài Liệu Tiếng Anh 
[1] B. Beizer. Software Testing Techniques. Van Nostrand Reinhold Co., New 
York,NY, USA, 2nd edition, 1990. 
[2] Daniel Kroening · Ofer Strichman. Decision Procedures: An Algorithmic Point of 
View, © 2008 Springer-Verlag Berlin Heidelberg 
[3] E. Gamma, R. Helm, R. Johnson, and J. M. Vlissides. Design Patterns: Elements 
of Reusable Object-Oriented Software. Addison-Wesley, 1994. 
[4] Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. The 
MIT Press, January 2000. 
[5] H. Zhu, P. Hall, J. May. Software Unit Test Coverage and Adequacy. ACM 
Computing Surveys, 29 (4). ISSN 0360-0300, December 1997, pp. 366–427. 
[6] J. C. King. Symbolic execution and program testing. Commun. ACM, 19(7):385–
394, 1976 
[7] J. de Halleux and N. Tillmann. Parameterized unit testing with Pex (tutorial). In 
Proc. of Tests and Proofs (TAP’08), volume 4966 of LNCS, pages 171–181, 
Prato,Italy, April 2008. Springer. 
[8] Jon Edvardsson. Techniques for Automatic Generation of Tests from Programs and 
Specifications. Department of Computer and Information Science Linkoping SE-581, 
Sweden 2006 
[9]Koushik Sen. Scalable automated methods for dynamic program analysis. Electro-
nic version of doctoral thesis, Department of Computer Science, University of Illinois 
at Urubana Champaign, 2006. 
 [10] Michael, C.C.; McGraw, G.E.; Schatz, M.A.; Walton, C.C. Genetic algorithms 
for dynamic test data generation. Automated Software Engineering, 1997. Procee-
dings., 12th IEEE International Conference Volume , Issue , 1-5 Nov 1997 
Page(s):307 – 308 
[11] N. Tillmann and W. Schulte. Unit tests reloaded: Parameterized unit testing with 
symbolic execution. IEEE Software, 23(4):38–47, 2006. 
[12] N. Tillmann and W. Schulte. Parameterized unit tests. In Proceedings of the 
10thEuropean Software Engineering Conference held jointly with 13th ACM SIG-
SOFT International Symposium on Foundations of Software Engineering, pages 253–
262. ACM, 2005. 
Field Code Changed
Formatted: Font: Italic
Field Code Changed
 2 
[13] Patrice Godefroid. Compositional dynamic test generation. In Proceedings ofthe 
34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 
(POPL), pages 47-54. ACM, 2007. 
[14] Patrice Godefroid, Nils Klarlund, and Koushik Sen. Dart: directed automated 
random testing. In Proceedings of the ACM SIGPLAN 2005 Conference on program-
ming Language Design and Implementation (PLDI), pages 213-223. ACM, 2005. 
[15] Peli de Halleux and Nikolai Tillmann, Parameterized Test Patterns For Effective 
Testing with Pex. Copyright Microsoft Corporation.October 21, 2008 
[16] Petri Ihantola. Automatic test data generation for programming exercises 
withsymbolic execution and Java PathFinder. Master's thesis, Helsinki University of 
Technology, Departement of Theoretical Computer Science, 2006. 
[17] Raja Vallée-Rai, Phong Co, Etienne Gagnon, Laurie J. Hendren, Patrick Lam, and 
Vijay Sundaresan. Soot - a Java bytecode optimization framework. In Proceedings of 
the 1999 conference of the Centre for Advanced Studies on Collaborative Research 
(CASCON), page 13. IBM, 1999. 
[18]R. Ferguson and B. Korel. The chaining approach for software test data 
generation. IEEE Transactions on Software Engineering, 5(1):63–86, January 1996. 
[19]S. Anand, P. Godefroid, and N. Tillmann. Demand-driven compositional symbolic 
execution. In Proc. of TACAS’08, volume 4963 of LNCS, pages 367–381. Springer, 
2008. 
[20] Sarfraz Khurshid, Corina S. Pasareanu, and Willem Visser. Generalized symbolic 
execution for model checking and testing. In 9th International Conference on Tools 
and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2619 
of Lecture Notes in Computer Science, pages 553-568. Springer, 2003. 
[21] Saswat Anand, Corina S. Pasareanu, and Willem Visser. Symbolic execution with 
abstraction. International Journal on Software Tools for Technology Transfer (STTT) 
Volume 11 , Issue 1 Pages 53-67 , January 2009 
[22] Saswat Anand, Alessandro Orso, and Mary Jean Harrold. Type-dependence 
analysis and program transformation for symbolic execution. In 13th International 
Conference on Tools and Algorithms for the Construction and Analysis of Systems 
(TACAS), volume 4424 of Lecture Notes in Computer Science, pages 117-133. 
Springer, 2007. 
[23] S. Khurshid and Y. Suen. Generalizing symbolic execution to library classes. In 
Proc. PASTE, pages 103-110, 2005. 
 3 
[24] T. Lev-Ami and M. Sagiv. TVLA: A system for implementing static analyses. In 
Proc. Static Analysis Symposium, Santa Barbara, CA, June 2000. 
[25]Tao Xie, Nikolai Tillmann, Peli de Halleux, and Wolfram Schulte. Fitness-Guided 
Path Exploration in Dynamic Symbolic Execution. To appear in Proceedings of the 
39th Annual IEEE/IFIP International Conference on Dependable Systems and 
Networks, Lisbon, Portugal, June-July 2009. 
[26] Willem Visser, Corina S. Pasareanu, and Sarfraz Khurshid. Test input generation 
with Java PathFinder. In Proceedings of the ACM/SIGSOFT International 
Symposium on Software Testing and Analysis (ISSTA), pages 97-107. ACM, 2004. 
 Các Trang Web 
[27]  
[28]  
[29]  
[30]  2008 
[31]  
[32]  
[33]  
[34]