ĐẠi học quốc gia hà NỘi trưỜng đẠi học công nghệ Trần Bình Dương sinh ca kiểm thử tham số HÓa cho chưƠng trình java khóa luận tốt nghiệP ĐẠi học hệ chính quy ngành: Công Nghệ Thông Tin
tải về 446.91 Kb.
|
- Điều hướng trang này:
- 3.4.1. Các phương pháp cũ
- 3.4.2. Hướng mở rộng
- KẾT LUẬN
- TÀI LIỆU THAM KHẢO
3.4. Mở rộng Symbolic JPFJPF đang ngày càng phổ biến trong cộng đồng mã nguồn mở. Đã có rất nhiều dự án liên quan đến việc mở rộng JPF để ứng dụng nó cho những mục đích khác nhau như kiểm tra mô hình lược đồ trạng thái UML(statechart), kiểm tra mô hình đối với các ứng dụng giao diện (ui) sử dụng javax.swing, java.awt. Khả năng của JPF không chỉ dừng lại ở việc kiểm chứng các chương trình Java đơn luồng mà nó có thể kiểm chứng với mọi chương trình Java đa luồng khác. Ngày nay, các công cụ và các nền hỗ trợ việc phát triển ứng dụng đều được thương mại hóa do đó việc ta nghiên cứu để mở rộng JPF là một việc làm vô cùng có ý nghĩa. Tuy nhiên như ta đã đề cập trong các chương trước, mục đích của ta là sử dụng khả năng của JPF để thực thi các ca kiểm thử tham số hóa viết cho ngôn ngữ Java. Vì vậy, ta chỉ tập trung vào việc nghiên cứu mở rộng khả năng thực thi tượng trưng của JPF để JPF có thể thực thi tượng trưng các chương trình Java nhận những tham số đầu vào có kiểu dữ liệu phức tạp hơn. Trong tương lai gần có thể biến JPF thành một cộng cụ (nền) hoàn thiện hỗ trợ việc thực thi các ca kiểm thử tham số hóa cho bất kỳ chương trình Java nào. 3.4.1. Các phương pháp cũĐã có những nghiên cứu khác nhau[16, 20, 26] áp dụng khả năng của JPF để thực thi tượng trưng các chương trình Java. Ý tưởng của các phương pháp này đó là sửa đổi các chương trình Java để hỗ trợ việc thực thi tượng trưng và JPF sẽ được sử dụng để thực thi các chương trình Java đã được sửa đổi đó. Quá trình sửa đổi mã nguồn Java ở các cách tiếp cận này không yêu cầu chuyển mã Java thành mã trung gian để thêm các phần mã hỗ trợ việc thực thi tượng trưng. Việc sửa đổi mã nguồn Java được thực hiện bằng cách thay các biến có kiểu cụ thể trong ngôn ngữ Java (int, float, string,…) thành các biến có kiểu tương trưng tương ứng và các hành động tính toán (các phép tính toán, so sánh,...) đối với các biến có kiểu cụ thể đó chuyển thành hành động tính toán với các biến có kiểu tượng trưng tương ứng. Ví dụ như trong Symbolic JPF, biến kiểu int có một kiểu tượng trưng tương ứng là SymbolicInteger, kiểu số thực thì có kiểu tượng trưng tương ứng là SymbolicReal. Nói cách khác, phương pháp sửa đổi ở đây chính là việc chuyển đổi mã nguồn (source-to-source) trực tiếp từ mã nguồn Java sang mã nguồn Java sử dụng các thư viện hỗ trợ thực thi tượng trưng sao cho mã nguồn Java sau khi được chuyển đổi có thể thực thi tượng trưng sử dụng JPF. Các thư viện hỗ trợ thực thi tượng trưng được xây dựng gồm các lớp để biểu thị cho các kiểu tượng trưng và các lớp với các phương thức được cài đặt để thực hiện hành động tính toán với các kiểu tượng trưng đó. Kỹ thuật phân tích phụ thuộc kiểu[22] được sử dụng để hỗ trợ quá trình chuyển đổi mã nguồn. Các cách tiếp cận này hướng tới việc thực thi tượng trưng các chương trình Java nhận đầu vào có cấu trúc dữ liệu phức tạp. Ý tưởng chính ở đây chính là việc kết hợp thực thi tượng trưng với khởi tạo lười[20]. Một phương thức bắt đầu được thực thi với các đối tượng làm đầu vào mà các trường của nó chưa được khởi tạo, khi các trường của đối tượng lần đầu tiên được truy cập trong quá trình thực thi thì khởi tạo lười sẽ được sử dụng để gán các giá trị cho các trường đó. Với các trường của đối tượng có kiểu dữ liệu nguyên thủy hoặc string thì chúng sẽ được khởi tạo với một giá trị tượng trưng tương ứng kết hợp với nó. Với các trường có kiểu tham chiếu thì chúng sẽ được khởi tạo với một giá trị null, hoặc một tham chiếu tới một đối tượng với các trường chưa được khởi tạo, hoặc một tham chiếu tới đối tượng đã được khởi tạo lúc trước có cùng kiểu. Trong thuật toán khởi tạo lười, các phương thức lấy (getter) và thiết lập (setter) được cài đặt cho mỗi trường của lớp. Các trường của lớp sẽ được truy cập và cập nhật bởi các getter và setter này. Một số ví dụ về việc chuyển đổi mã nguồn Java để hỗ trợ thực thi tượng trưng sử dụng JPF ta có thể tham khảo trong[16, 20, 26]. 3.4.2. Hướng mở rộngNhư đã trình bày ở trên, JPF được sử dụng để thực thi các chương trình Java đã được sửa đổi để hỗ trợ việc thực thi tượng trưng. Tuy nhiên, ta sẽ không quay lại để nghiên cứu xem làm sao có thể sử dụng JPF để thực thi các chương trình đã được sửa đổi như thế mà cách tiếp cận của ta ở đây là sẽ sử dụng các thư viện hỗ trợ thực thi tượng trưng và ý tưởng khởi tạo lười để thay đổi nghữ nghĩa thực thi các chỉ thị bytecode theo ngữ nghĩa thực thi tượng trưng sao cho JPF có thể thực thi tượng trưng các chương trình nhận đầu vào có kiểu cấu trúc dữ liệu phức tạp. Tất nhiên đó chỉ là việc đầu tiên ta cần làm để có thể mở rộng JPF. Một điều vô cùng quan trọng nữa là nghiên cứu để xây dựng các bộ xử lý ràng buộc để có thể xử lý các ràng buộc sinh ra từ việc thực thi tượng trưng đó. Ta đã được nghe nhiều tới các bộ xử lý ràng buộc hiệu quả như Z3[31], nhưng vấn đề là các bộ xử lý ràng buộc đó thường được viết trong các dạng ngôn ngữ không phải là ngôn ngữ Java. Do đó việc xây dựng các bộ xử lý ràng buộc để có thể tích hợp vào JPF cũng là một thách thức không nhỏ. Như ta đã đề cập ở trên, ta cần xây dựng các thư viện tượng trưng để hỗ trợ việc thực thi tượng trưng chương trình và cũng là để hỗ trợ việc cài đặt các lớp chỉ thị bytecode theo ngữ nghĩa thực thi tượng trưng. Tất nhiên ta sẽ không thay đổi ngữ nghĩa thực thi cho tất cả các chỉ thị bytecode mà chỉ những chỉ thị bytecode nào liên quan đến việc tạo và cập nhật các thông tin tượng trưng và các chỉ thi bytecode rẽ nhánh mới cần thay đổi ngữ nghĩa từ thực thi cụ thể sang ngữ nghĩa thực thi tượng trưng. Trong JPF phiên bản 4.1 mà ta đang nghiên cứu ở đây, ngoài các thư viện hỗ trợ thực thi tượng trưng với kiểu số học JPF còn cung cấp thư viện hỗ trợ thực thi tượng trưng với kiểu String. Việc cài đặt các lớp để biểu thị cho kiểu String tượng trưng và các hành động tính toán đối với kiểu String tượng trưng này cũng như việc cài đặt các lớp hỗ trợ thực thi tượng trưng với kiểu số học. Tuy nhiên có một điều quan trọng mà ta cần lưu ý đó là kiểu String cũng là kiểu tham chiếu như các đối tượng khác. Do đó việc lưu trữ và tính toán các giá trị tượng trưng với kiểu String không giống như đối với kiểu số học. Nếu như với kiểu số học thì các giá trị tượng trưng của các biến được kết hợp với các thuộc tính (attributes) của toán hạng ngăn xếp (stack operands) của ngăn xếp (operand stack) trong stack frame và ở các vùng biến cục bộ thì đối với kiểu String hay các kiểu tham chiếu đối tượng khác các giá trị tượng trưng sẽ được lưu trữ trong vùng nhớ heap. Như ta đã biết đối với máy ảo Java thì vùng nhớ heap chính là vùng nhớ lưu trữ các đối tượng được tạo ra trong quá trình thực thi một chương trình. Nhưng có một điều mà ta cần nhớ đó là mọi thao tác tính toán, so sánh, v.v. đều được thực hiện trên ngăn xếp toán hạng của stack frame với 2 thao tác là push (đẩy) và pop (lấy). Do đó để có thể thay đổi ngữ nghĩa thực thi đối với các chỉ thị bytecode mà thực hiện việc so sánh, tính toán với kiểu tham chiếu thì ta cần có cơ chế để lấy cũng như cập nhật các giá trị tượng trưng được kết hợp với các tham chiếu đó trong vùng nhớ heap để xử lý cùng với thao tác tính toán diễn ra trên ngăn xếp toán hạng của stack frame. Để minh họa điều này ta xét một ví dụ đơn giản với kiểu String như sau: public String Compare(String s){ if(s=="K50") return s + "CNPM"; return s; } Bytecodes tương ứng với phương thức Compare ở trên: // access flags 1 public Compare(Ljava/lang/String;)Ljava/lang/String; L0 LINENUMBER 3 L0 ALOAD 1 LDC "K50" IF_ACMPEQ L1 L2 LINENUMBER 4 L2 NEW java/lang/StringBuilder DUP
ALOAD 1 INVOKESTATIC java/lang/String.valueOf(Ljava/lang/Object;)... INVOKESPECIAL java/lang/StringBuilder. LDC "CNPM" INVOKEVIRTUAL java/lang/StringBuilder.append(Ljava/lang/String;)... INVOKEVIRTUAL java/lang/StringBuilder.toString()Ljava/lang/String; ARETURN L1
FRAME SAME ALOAD 1
ARETURN L3 LOCALVARIABLE this LBuffer; L0 L3 0 LOCALVARIABLE s Ljava/lang/String; L0 L3 1 MAXSTACK = 3 MAXLOCALS = 2 Chỉ thị bytecode IF_ACMPEQ chính là chỉ thị bytecode thực hiện việc so sánh bằng nhau giữa các tham chiếu đối tượng. Dưới đây là mã cài đặt của nó theo ngữ nghĩa thực thi cụ thể: import gov.nasa.jpf.jvm.ThreadInfo; public class IF_ACMPEQ extends IfInstruction { public boolean popConditionValue (ThreadInfo ti) { int v1 = ti.pop(); int v2 = ti.pop(); return (v1 == v2); } ... } Rõ ràng việc thông dịch chỉ thị này theo ngữ nghĩa thực thi cụ thể không khác gì so với chỉ thị IF_ICMPEQ đối với kiểu dữ liệu nguyên thủy mà ta đã trình bày trong ví dụ của phần trước. Mọi việc so sánh trên operand stack của stack frame đều là việc so sánh đối với các giá trị số học. Với chỉ thị IF_ACMPEQ này thì việc so sánh 2 tham chiếu đối tượng dẫn đến việc so sánh 2 giá trị số học biểu thị cho chúng. Nếu 2 giá trị đó bằng nhau có nghĩa là 2 tham chiếu tới cùng một đối tượng. Điều này cũng tương tự như bộ nhớ (Map) M ánh xạ một địa chỉ logic (logic address) là một số tự nhiên tới một đối tượng mà ta đã làm quen trong chương trước nếu như 2 địa chỉ logic này bằng nhau có nghĩa là chúng đang ánh xạ tới cùng một đối tượng. Nếu như với các biến có kiểu dữ liệu nguyê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 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. KẾT LUẬNKiể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.
[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. [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. [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] http://choco.sourceforge.net/ [28] http://javapathfinder.sourceforge.net/ [29] http://msdn2.microsoft.com/vs2008/ [30] http://research.microsoft.com/Pex, 2008 [31] http://research.microsoft.com/projects/Z3 [32] http://openjdk.java.net/ [33] http://www.junit.org/ [34] http://www.nunit.org/ Каталог: jspui -> bitstream -> 123456789 123456789 -> Nguyễn Ngọc Lý Giám đốc Trung tâm Nghiên cứu về Môi trường và Cộng đồng 123456789 -> Vò Quúnh Thu Cao häc K18 123456789 -> Khoa Báo chí Đhkhxh&NV 123456789 -> Acknowledgements 123456789 -> Danh mục chữ viết tắT 123456789 -> Chương TỔng quan vật liệu mao quản trung bình (mqtb) trật tự 1 Giới thiệu chung 123456789 -> Khoa hóa họC (141 142 báo cáo) tải về 446.91 Kb. Chia sẻ với bạn bè của bạn:
|