Một phương pháp hiệu quả sinh dữ liệu kiểm thửu mức đơn vị - Nguyễn Hồng Tân

Nguyễn Hồng Tân và Đtg Tạp chí KHOA HỌC & CÔNG NGHỆ 99(11): 79 - 84 79 MỘT PHƯƠNG PHÁP HIỆU QUẢ SINH DỮ LIỆU KIỂM THỬ MỨC ĐƠN VỊ Nguyễn Hồng Tân*, Hà Thị Thanh Trường Đại học Công nghệ thông tin và truyền thông – ĐH Thái Nguyên TÓM TẮT Kiểm thử là một phương pháp quan trọng để nâng cao chất lượng của một sản phẩm phần mềm được tạo ra bằng cách kiểm tra lỗi trong việc thực hiện chương trình theo một số chuẩn được gọi là chuẩn bao phủ. Kiểm thử sẽ rất tốn kém nếu nó không được hỗ trợ bởi một phương pháp hoặc một công cụ để tạo ra các bộ test. Bài báo này, chúng tôi đề xuất một phương pháp sinh dữ liệu kiểm thử tự động cho các đơn vị phần mềm dựa vào kỹ thuật kiểm chứng mô hình. Các test case thu được một cách tự động dựa vào các phản ví dụ của công thức logic thời gian tuyến tính (LTL - Linear Temporal Logic) vi phạm các chuẩn bao phủ đã được lựa chọn. Từ khóa: Kiểm chứng mô hình, Test case, Kiểm thử đơn vị GIỚI THIỆU* Kiểm thử có thể chỉ ra sự xuất hiện của lỗi tồn tại trong phần mềm. Mặt khác, kiểm chứng mô hình là một kỹ thuật hiệu quả áp dụng để chỉ ra mô hình hệ thống có thỏa mãn được các tính chất hay không [10]. Mặc dù kiểm thử phần mềm và kiểm chứng mô hình đã được đề cập đến trước đây như hoạt động xác minh và thẩm định riêng biệt nhưng gần đây đã có một số nghiên cứu về tiềm năng của kiểm thử mô hình theo hướng giảm chi phí của kiểm thử phần mềm. Những phương pháp tiếp cận đó đều dựa trên các thuật toán kiểm chứng mô hình để phát hiện ra các thuộc tính vi phạm trong hệ thống khi thực hiện chương trình. Kiểm thử hộp trắng dựa trên các test case được tạo ra bằng kiểm chứng mô hình trước đó đã được giải quyết [5,6,7,8,9]. Các điểm chung của các kỹ thuật nói trên là sự phát triển của một tập hợp các công thức LTL mà khi áp dụng vào các chương trình mô hình tạo ra tập hợp các test case theo yêu cầu. Chương trình mô hình đại diện cho luồng điều khiển của đơn vị được kiểm thử và mặc dù sự tồn tại của nó như là tiền điều kiện thì rất khó để thực hiện nó một cách tự động. Một số nghiên cứu đã cố gắng để giảm chi phí cho việc tạo ra các test case bằng cách sử dụng thuật toán heuristic [8] để giảm thiểu tập các công thức LTL trong các bộ test. Kết quả nghiên cứu đề cấp đến việc sử dụng kỹ thuật kiểm chứng mô hình trong kiểm thử * Email: nhtan@ictu.edu.vn các đơn vị nhỏ nhất của phần mềm được gọi là các thành phần hoặc các module. Nghiên cứu của nhóm tập trung vào việc khai thác tự động các chương trình mô hình từ mã nguồn, một trong những nỗ lực để tiếp tục giảm chi phí cho việc tạo ra các test case. Việc tạo ra chương trình mô hình được xây dựng dành riêng cho việc tạo ra các test case, có nghĩa là thông tin được nhúng bổ sung vào chương trình và chương trình được biến đổi một cách tương đương, sau đó áp dụng phương pháp kiểm chứng mô hình cụ thể tạo ra các test case mong muốn. Bước đầu tiên, chương trình nguồn được phân tích cú pháp và trừu tượng hoá thành một chương trình mô hình. Chương trình mô hình được thể hiện trong một ngôn ngữ mô hình cụ thể, ngôn ngữ mô hình đó là đầu vào của một công cụ kiểm chứng mô hình. Các khối cơ bản của chương trình mô hình được phân biệt bằng cách truyền vào một breakpoint, được sử dụng như là các mục tiêu trong pha chọn đường thực thi. Bước thứ hai, việc lựa chọn breakpoint dựa trên các chuẩn bao phủ cho mọi đường thực thi được lựa chọn theo công thức tuyến tính logic thời gian thích hợp. Phản ví dụ thu được từ kiểm chứng mô hình dưới dạng công thức LTL tạo ra các bộ test thoả mãn chuẩn lựa chọn bao phủ. Các công cụ hỗ trợ hiện tại cho phép thực hiện nhiều điều kiện theo chuẩn bao phủ, mà được coi như là thay thế phạm vi bao phủ luồng điều khiển một cách toàn diện nhất. Nguyễn Hồng Tân và Đtg Tạp chí KHOA HỌC & CÔNG NGHỆ 99(11): 79 - 84 80 CÁC KIẾN THỨC NỀN TẢNG Phần này giới thiệu một phương pháp biểu diễn mã nguồn của đơn vị phần mềm như một chương trình mô hình và thảo luận về việc sử dụng các LTL cho việc tạo ra các bộ test tương ứng với một chuẩn bao phủ Chương trình mô hình Hệ thống được kiểm thử (System Under Test - SUT) được thể hiện theo cấu trúc Kripke ( )δ,,, AIST = . Trong đó, S là một tập hữu hạn các trạng thái của chương trình; I ⊂ S là tập khác rỗng các trạng thái ban đầu; A là một hàm gán nhãn A: S AP2→ với AP là mệnh đề cơ sở; SS ×⊆δ là phép chuyển trạng thái. Một đồ thị luồng ( )AvvVG fs ,,,= là một đồ thị có hướng. Trong đó, V: là tập hữu hạn các trạng thái; Vvs ∈ là đỉnh ban đầu; Vv f ∈ là đỉnh kết thúc và A ⊂ V ×V là tập hợp hữu hạn các cung kết nối các trạng thái. Mỗi đỉnh đại diện cho một câu lệnh và cung xác định luồng giữa các câu lệnh. Vai trò quan trọng nhất của mỗi đỉnh là định nghĩa và sử dụng các biến tham gia trong chương trình. Ví dụ với biến a, ta có thể định nghĩa là da và sử dụng là ua. Các cấu trúc Kripke T biểu diễn các SUT nếu S=V, I = {vs} và δ = A {(vf, vf)}. Bằng cách thể hiện SUT với một cấu trúc Kripke, chúng ta có thể thiết lập các đường thực thi của chương trình một cách tự động dựa vào chuẩn bao phủ. Mỗi đường thực thi là một test case và tập hợp các test case đạt được theo chuẩn bao phủ nhất định tạo thành các bộ test. Logic tuyến tính thời gian Cấu trúc Kripke T phản ánh hành vi có thể có của chương trình và nó được sử dụng để kiểm chứng mô hình, công thức LTL được xác định trên tập hợp các mệnh đề cơ sở AP. Công thức LTL được tạo ra bằng việc sử dụng các quy tắc ngữ pháp sau 2121 |||||:: ϕϕϕϕϕϕαϕ ∪Ο¬∧= true , với α đại diện cho mệnh đề cơ sở, Ο cho toán tử logic next và ∪ là toán tử logic Until. Hai toán tử khác có nguồn gốc từ những thể hiện trong các quy tắc ngữ pháp là toán tử ◊ - cuối cùng và toán tử □ - luôn luôn. Kiểm chứng được dùng để kiểm thử luồng dữ liệu [8]. Với đồ thị điều khiển luồng của hình 1, bao phủ rẽ nhánh sẽ tạo ra các test case bao gồm các đỉnh {v3, v4, v5, v6,v7 ,v8, v10} và bao phủ luồng dữ liệu sẽ tìm kiếm tất cả các đường thực thi có thể cho giữa việc định nghĩa và việc sử dụng biến chương trình d. Tuy nhiên, câu lệnh điều khiển luồng trạng thái ảnh hưởng đến phạm vi bao phủ luồng dữ liệu và sự phụ thuộc này có thể được mã hoá trong công thức LTL. Ví dụ cho đoạn chương trình 1 như sau: int method( int a, int b, int c) { int d=0; if (a<10) { if(b>=20 && a<5) d=50; else d=0; } else { if(b<50) d=30; else d=10; } if(c==3) d=40; return d; } ta sẽ thu được đồ thị luồng như hình vẽ 1 Hình 10: Mã nguồn và đồ thị luồng điều khiển của đơn vị phần mềm KIỂM CHỨNG MÔ HÌNH CHO KIỂM THỬ ĐƠN VỊ DỰA TRÊN MỨC ĐỘ BAO PHỦ Phương pháp được đề xuất cho kiểm thử đơn vị dựa trên mức độ bao phủ theo cách biểu diễn chương trình mô hình được trình bày trong phần trước. Các nhánh luồng điều khiển và các trạng thái của chương trình mô hình là đủ để đưa ra công thức LTL nhằm phát hiện Nguyễn Hồng Tân và Đtg Tạp chí KHOA HỌC & CÔNG NGHỆ 99(11): 79 - 84 81 các đường thực thi chương trình theo chuẩn bao phủ, nhưng ở dạng công thức LTL phức tạp. Thay vào đó, các phương pháp tiếp cận được thực hiện không chỉ dựa trên việc đưa ra một công thức thích hợp, mà còn được biểu diễn bởi một chương trình mô hình được cải tiến với thông tin bổ sung cho việc xây dựng các đường thực thi tương ứng. Tác động trực tiếp của công thức được sử dụng để phát hiện các đường thực thi chương trình là được đơn giản hoá, tức là một phần yêu cầu của công việc cho sự phát triển của công thức LTL thích hợp được chuyển giao cho việc xây dựng các chương trình mô hình. Cách tiếp cận này sẽ mở ra triển vọng để phát triển của LTL một cách tự động góp phần nâng cao mức độ tự động hoá trong việc xây dựng một bộ test. Chuyển dịch những câu lệnh điều khiển luồng Luồng thực thi chương trình được điều khiển bởi các câu lệnh điều khiển như if – then, if – then – else, switch và điều kiện kiểm soát vòng lặp. Trong tất cả các trường hợp, đường thực thi chương trình được xác định bởi các quyết định được thực hiện như là một hệ quả của biểu thức điều kiện bằng cách kết hợp một hoặc nhiều vị từ với toán tử boolean. Yêu cầu cơ bản của bao phủ nhánh là để tạo ra các test case mà sẽ bao phủ tất cả các nhánh của đồ thị luồng điều khiển. Mỗi vị từ mà không thể chia được thành các vị từ nhỏ hơn được gọi là mệnh đề. Tính chất mệnh đề được phát biểu như sau: chọn ci trong tập Mi = {ci, ci} và do đó mỗi quyết định tạo ra một biểu thức điều kiện là đưa ra như là hàm logic d sao cho liM B→ , trong đó B={0,1} và l là số mệnh đề trong biểu thức. Chúng ta xác định hàm f cho mỗi d( lim ) trong đó l li im M∈ trả về b khối cơ bản cho các cạnh tương ứng với điều kiện. Như vậy, mỗi câu lệnh điều kiện với 1 phần còn lại gọi là e, có: ( )emdfbmdf lili =¬∧= ))((()))(( Thuật toán kiểm chứng mô hình được xác định nếu có một cách định nghĩa các trạng thái khác nhau nhờ vào mô hình. Để hỗ trợ tạo ra sự khác nhau giữa các trạng thái ta có thể thêm thông tin vào mã nguồn của mô hình. Ta kí hiệu SP và EP là tập tất cả các điểm vào và tập tất cả các điểm ra tương ứng. Trong pha xử lý sau, các breakpoint được tổ chức thành các cấu trúc cây, với mỗi một câu lệnh luồng điều khiển không lồng nhau, được sử dụng để tối ưu hoá số lượng các test case cần thiết cho các chuẩn bao phủ. Lá của cây đưa ra các breakpoint không chi phối bất kỳ breakpoint nào khác của hệ thống phân cấp. Về bản chất, nó được hiển thị như trong hình 2, các breakpoint được tổ chức lồng nhau được gọi là độ sâu. Mỗi cây bao gồm tất cả các luồng dữ liệu có thể giữa các breakpoint trong câu lệnh điều khiển luồng tương ứng với nhiều cấp độ lồng nhau. Hình 11: Cấu trúc cây phân cấp của chương trình nguồn ở chương trình 1 Mô hình của công thức LTL cho việc tạo ra các test case Chương trình mô hình được cải tiến cung cấp một cơ sở cho việc tìm kiếm đường thực thi chương trình hay còn gọi là test case trả về phản ví dụ của việc thực thi mô hình kiểm chứng. Các công thức thích hợp mô tả đường thực thi chương trình tuân thủ theo một thuộc tính mẫu đơn giản và chúng ta gọi chúng là bằng chứng. Nhờ sự đơn giản của các bằng chứng, chúng có thể được tạo ra chúng một cách tự động nếu ta xem xét các chương trình mô hình và các cây breakpoint. Hình 12: Cấu trúc cây breakpoint trong chương trình 1 Nguyễn Hồng Tân và Đtg Tạp chí KHOA HỌC & CÔNG NGHỆ 99(11): 79 - 84 82 Để tận dụng khả năng của thuật toán kiểm chứng mô hình cho việc phát hiện một phản ví dụ, mọi bằng chứng đều trở thành thuộc tính cửa sập, tức là nếu p là bằng chứng thì chúng ta có một test case được tạo ra bởi kiểm chứng mô hình ¬p Các mô hình của LTL đưa ra trường hợp chứng minh là: ))(int(:: subltlbreakpoLtL s ◊∧◊= với breakpoints SP∈ )(int:: subltlbreakpoSubltl i ◊∧= | breakpointf với breakpointf EP∈ Tất cả các đường thực thi đều được biểu diễn dựa vào các thuộc tính cửa sập LTL được tạo ra một cách tự động. Số lượng thuộc tính LTL cần thiết phụ thuộc vào các tiêu chuẩn bao phủ. Cuối cùng, cần lưu ý rằng phải có ít nhất một test case trong bộ test cho tất cả các điểm vào và điểm ra. Sự kết hợp của các breakpoint thu được một cách tự động Cho trước một mô hình, mẫu dựa trên các công thức LTL có thể được xây dựng và thiết lập các breakpoint được tổ chức theo cấu trúc cây, nó có thể kết hợp với những breakpoint hạn chế trong các mẫu LTL, theo đó tự động tạo ra công thức LTL và sẽ tạo ra các test case. Phương pháp đơn giản nhất để kết hợp các breakpoint là sự kết hợp ngẫu nhiên mà không phân biệt chúng. Phương pháp này có kết quả là việc tạo ra một số lượng lớn công thức. Cũng có một trong số đó sẽ không hợp lệ, vì thứ tự kết hợp breakpoint thực hiện sai. Một vấn đề khác là việc thiếu thông tin cho chiều dài của đường thực thi. Một phương pháp thông minh hơn, sử dụng thông tin có sẵn trong mô hình nhằm giảm tối đa sự kết hợp các breakpoint. Dựa trên thông tin này, có thể thu được một trật tự cho các breakpoint trong các công thức LTL kể từ khi mã được thực hiện tuần tự. Giả sử, có một phần từ tập các SP và EP của breakpoint, phân tích của chúng đưa ra các tập IF1 và IF2. Trong trường hợp này, tập các kết hợp có thể là: EPIFIFSPC ×××= 21 . Trong trường hợp chung, một chương trình với n câu lệnh điều khiển thì tập các breakpoint có thể kết hợp là ∏ = ××= n i i EPIFSPC 1 Kết quả được sắp xếp tuần tự theo giới hạn một tập các kết hợp breakpoint, tuy nhiên vẫn bao gồm các đường thực thi dư thừa. Lý do là một số breakpoint chi phối breakpoint khác, điều đó có nghĩa là các đường dẫn cho các breakpoint chiếm ưu thế cũng chứa những breakpoint khác. Bằng cách lọc tập các breakpoint theo đó chỉ giữ lại những breakpoint có ảnh hưởng, tiếp tục làm giảm chiều dài của công thức LTL được sử dụng để tạo ra các test case. Ta kí hiệu, FIFi là bộ lọc của các IFi. Khi đó tập các kết hợp: ∏ = ××= n i i EPFIFSPC 1 . Công thức này tương ứng với các test case đại diện cho các đường thực thi riêng biệt. Trong thuật toán 1, chúng ta thấy quá trình kết hợp của breakpoint không ảnh hưởng. Hàm getNondominantsBreakpointsList không được mô tả theo chiều sâu, bởi vì mục đích của nó là truy xuất đến lá của cây. Điều đó xảy ra bởi bởi cây được cấu trúc theo cách mà các nút lá không bị chi phối bởi nút cha. Để đảm bảo tính đầy đủ, ta xem xét đến các đường được sinh ra, có thể cả trường hợp không hợp lệ. Điều đó xảy ra nguyên nhân do các câu lệnh điều khiển xảy ra xung đột. Một cách tiếp cận khác để vượt qua khó khăn này là tạo ra công thức LTL, một test case được tạo ra cho câu lệnh điều khiển tại thời điểm đó. Điều này sẽ giúp tạo ra tập các điểu khiển: [ ]{ }EPIFSPiniC i ××Ζ∈∈∀= ,,1 Khi các công thức LTL được tạo ra, quá trình còn lại bao gồm thực thi theo công thức LTL trong một bộ kiểm chứng mô hình. Mô hình kiểm chứng được sử dụng để kiểm tra các thuộc tính có trong mã nguồn của ngôn ngữ mô hình. Thuật toán cấu trúc LTL và thuật toán tìm tất cả các sự kết hợp được trình bày dưới đây: Procedure constructLTL(breakpointTrees) 1: for ∀ breakTree ∈ breakpointTrees do 2:nonDominantVector ←getNonDominantsB reakpointsList(breakTree) 3: end for 4: findAllCombinations(nonDominantVector) (Thuật toán 1) Nguyễn Hồng Tân và Đtg Tạp chí KHOA HỌC & CÔNG NGHỆ 99(11): 79 - 84 83 Procedure findAllCombinations(nonDominantVector) 1:if nonDominantVector.size > 1 then 2: nonDominands ←nonDominantVector.pop() 3:nextTreesCombinantions ← findAllCombin ations(nonDominantVector) 4: for∀ nonDominant∈nonDominands do 5:for∀ nextTreesCombination∈nextTreesCo mbinations do 6: combinationList.add(nonDominant, nextTreesCombination) 7: end for 8: end for 9: return combinationList 10:else 11: return nonDominantVector 12: end if (Thuật toán 2) KẾT LUẬN Trong bài báo này, chúng tôi đã giới thiệu một phương pháp cho việc tạo ra các test case trong kiểm thử đơn vị dựa trên tính chất bao phủ. Tư tưởng chính của phương pháp dựa trên việc chuyển đổi mã nguồn thành một mô hình với việc truyền vào các breakpoint. Các breakpoint phân biệt các khối cơ bản của chương trình và đồng thời cung cấp đầy đủ thông tin cho việc tạo ra các test case bằng công thức kiểm chứng mô hình LTL đơn giản. Mặc dù nhóm nghiên cứu đã thử nghiệm phương pháp đề xuất vận dụng vào kiểm thử một số module chương trình được viết trên ngôn ngữ Java và đã thu lại được các kết quả có ý nghĩa, tuy nhiên trong khuôn khổ bài báo này chúng tôi mới chỉ đưa ra những kết quả về mặt phương pháp, những kết quả thực nghiệm và ứng dụng sẽ tiếp tục được hoàn thiện và gửi đăng sau. Hướng nghiên cứu trong tương lai là làm thế nào để có thể tự động tạo ra các test case để lựa chọn cho các biến chương trình dựa trên các chuẩn bao phủ luồng dữ liệu đã được biết đến, kết hợp phương pháp nghiên cứu với một số công cụ hiện sẵn có mang lại hiệu quả cao hơn nữa trong hoạt động kiểm thử phần mềm. TÀI LIỆU THAM KHẢO [1]. P. Ammann, P. E. Black, and W. Majurski, “Using model checking to generate tests from specifications”, inICFEM, 1998. [2]. S. Rapps and E. J. Weyuker, “Selecting software test data using data flow information”, IEEE Trans. Software Eng., vol. 11, no. 4, pp. 367–375, 1985. [3]. J. Jacky, M. Veanes, C. Campbell, and W. Schulte, Model-Based Software Testing and Analysis with C#, 1st ed. Cambridge University Press, 2007. [4]. G. J. Holzmann, “The model checker spin”, IEEE Trans. Software Eng.,vol. 23, no. 5, pp. 279–295, 1997. [5]. P. Ammann, P. E. Black, and W. Ding, “Model checkers in software testing”, NIST-IR 6777, National Institute of Standards and Technology, Tech. Rep., 2002. [6]. H. S. Hong, I. Lee, O. Sokolsky, and H. Ural, “A temporal logic based theory of test coverage and generation”, in TACAS, ser. Lecture Notes in Computer Science, J.-P. Katoen and P. Stevens, Eds, vol. 2280. Springer, 2002, pp. 327–341. [7]. H. S. Hong and H. Ural, “Dependence testing: Extending data flow testing with control dependence”, in TestCom, ser. Lecture Notes in Computer Science, F. Khendek and R. Dssouli, Eds., vol. 3502. Springer, 2005, pp. 23–39. [8]. H. S. Hong, S. D. Cha, I. Lee, O. Sokolsky, and H. Ural, “Data flow testing as model checking”, in ICSE. IEEE Computer Society, 2003, pp. 232–243. [9]. S. Rayadurgam and M. P. E. Heimdahl, “Coverage based test-case generation using model checkers”, Engineering of Computer-Based Systems, IEEE International Conference on the, 2001. [10]. C. Baier and J.-P. Katoen, Principles of Model Checking. The MIT Press, 2008. Nguyễn Hồng Tân và Đtg Tạp chí KHOA HỌC & CÔNG NGHỆ 99(11): 79 - 84 84 SUMMARY AN EFFICIENT METHOD OF BIRTH CONTROL DATA FOLDER UNIT Nguyen Hong Tan*, Ha Thi Thanh College of Information and Communication Technology - TNU Testing is an important method to improve the quality of a software product created by checking for errors in program executions according to some criterion called coverage criterion. Testing will be very expensive if it is not supported by a method or a tool for generating test suites. This paper, we propose a method of automatic test suites for software module based on model checking. Test cases is obtained automatically as counterexamples of violated linear time logic. Keywords: Test models, test cases, unit testing Ngày nhận bài: 09/11/2012, ngày duyệt đăng: 26/11/2012, ngày phản biện:10/12/2012 * Email: nhtan@ictu.edu.vn