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 và Đtg<br /> <br /> Tạp chí KHOA HỌC & CÔNG NGHỆ<br /> <br /> 99(11): 79 - 84<br /> <br /> MỘT PHƯƠNG PHÁP HIỆU QUẢ SINH DỮ LIỆU<br /> KIỂM THỬ MỨC ĐƠN VỊ<br /> Nguyễn Hồng Tân*, Hà Thị Thanh<br /> Trường Đại học Công nghệ thông tin và truyền thông – ĐH Thái Nguyên<br /> <br /> TÓM TẮT<br /> 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<br /> đượ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à<br /> 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<br /> 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<br /> 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<br /> đượ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.<br /> Từ khóa: Kiểm chứng mô hình, Test case, Kiểm thử đơn vị<br /> <br /> GIỚI THIỆU*<br /> Kiểm thử có thể chỉ ra sự xuất hiện của lỗi tồn<br /> tại trong phần mềm. Mặt khác, kiểm chứng<br /> mô hình là một kỹ thuật hiệu quả áp dụng để<br /> chỉ ra mô hình hệ thống có thỏa mãn được các<br /> tính chất hay không [10]. Mặc dù kiểm thử<br /> phần mềm và kiểm chứng mô hình đã được<br /> đề cập đến trước đây như hoạt động xác minh<br /> và thẩm định riêng biệt nhưng gần đây đã có<br /> một số nghiên cứu về tiềm năng của kiểm thử<br /> mô hình theo hướng giảm chi phí của kiểm<br /> thử phần mềm. Những phương pháp tiếp cận<br /> đó đều dựa trên các thuật toán kiểm chứng mô<br /> hình để phát hiện ra các thuộc tính vi phạm<br /> trong hệ thống khi thực hiện chương trình.<br /> Kiểm thử hộp trắng dựa trên các test case<br /> được tạo ra bằng kiểm chứng mô hình trước<br /> đó đã được giải quyết [5,6,7,8,9]. Các điểm<br /> chung của các kỹ thuật nói trên là sự phát<br /> triển của một tập hợp các công thức LTL mà<br /> khi áp dụng vào các chương trình mô hình tạo<br /> ra tập hợp các test case theo yêu cầu. Chương<br /> trình mô hình đại diện cho luồng điều khiển<br /> của đơn vị được kiểm thử và mặc dù sự tồn<br /> tại của nó như là tiền điều kiện thì rất khó để<br /> thực hiện nó một cách tự động. Một số nghiên<br /> cứu đã cố gắng để giảm chi phí cho việc tạo<br /> ra các test case bằng cách sử dụng thuật toán<br /> heuristic [8] để giảm thiểu tập các công thức<br /> LTL trong các bộ test.<br /> Kết quả nghiên cứu đề cấp đến việc sử dụng<br /> kỹ thuật kiểm chứng mô hình trong kiểm thử<br /> *<br /> <br /> Email: nhtan@ictu.edu.vn<br /> <br /> các đơn vị nhỏ nhất của phần mềm được gọi<br /> là các thành phần hoặc các module. Nghiên<br /> cứu của nhóm tập trung vào việc khai thác tự<br /> động các chương trình mô hình từ mã nguồn,<br /> một trong những nỗ lực để tiếp tục giảm chi<br /> phí cho việc tạo ra các test case. Việc tạo ra<br /> chương trình mô hình được xây dựng dành<br /> riêng cho việc tạo ra các test case, có nghĩa là<br /> thông tin được nhúng bổ sung vào chương<br /> trình và chương trình được biến đổi một cách<br /> tương đương, sau đó áp dụng phương pháp<br /> kiểm chứng mô hình cụ thể tạo ra các test<br /> case mong muốn.<br /> Bước đầu tiên, chương trình nguồn được phân<br /> tích cú pháp và trừu tượng hoá thành một<br /> chương trình mô hình. Chương trình mô hình<br /> được thể hiện trong một ngôn ngữ mô hình cụ<br /> thể, ngôn ngữ mô hình đó là đầu vào của một<br /> công cụ kiểm chứng mô hình. Các khối cơ<br /> bản của chương trình mô hình được phân biệt<br /> bằng cách truyền vào một breakpoint, được sử<br /> dụng như là các mục tiêu trong pha chọn<br /> đường thực thi. Bước thứ hai, việc lựa chọn<br /> breakpoint dựa trên các chuẩn bao phủ cho<br /> mọi đường thực thi được lựa chọn theo công<br /> thức tuyến tính logic thời gian thích hợp.<br /> Phản ví dụ thu được từ kiểm chứng mô hình<br /> dưới dạng công thức LTL tạo ra các bộ test<br /> thoả mãn chuẩn lựa chọn bao phủ. Các công<br /> cụ hỗ trợ hiện tại cho phép thực hiện nhiều<br /> điều kiện theo chuẩn bao phủ, mà được coi<br /> như là thay thế phạm vi bao phủ luồng điều<br /> khiển một cách toàn diện nhất.<br /> 79<br /> <br /> Nguyễn Hồng Tân và Đtg<br /> <br /> Tạp chí KHOA HỌC & CÔNG NGHỆ<br /> <br /> CÁC KIẾN THỨC NỀN TẢNG<br /> Phần này giới thiệu một phương pháp biểu<br /> diễn mã nguồn của đơn vị phần mềm như một<br /> chương trình mô hình và thảo luận về việc sử<br /> dụng các LTL cho việc tạo ra các bộ test<br /> tương ứng với một chuẩn bao phủ<br /> Chương trình mô hình<br /> Hệ thống được kiểm thử (System Under Test<br /> - SUT) được thể hiện theo cấu trúc Kripke<br /> T = (S , I , A, δ ) . Trong đó, S là một tập hữu<br /> hạn các trạng thái của chương trình; I ⊂ S là<br /> tập khác rỗng các trạng thái ban đầu; A là một<br /> hàm gán nhãn A: S → 2 AP với AP là mệnh<br /> đề cơ sở; δ ⊆ S × S là phép chuyển trạng<br /> thái. Một đồ thị luồng G = V , v s , v f , A là<br /> một đồ thị có hướng. Trong đó, V: là tập hữu<br /> hạn các trạng thái; vs ∈ V là đỉnh ban đầu;<br /> v f ∈ V là đỉnh kết thúc và A ⊂ V × V là tập<br /> hợp hữu hạn các cung kết nối các trạng thái.<br /> Mỗi đỉnh đại diện cho một câu lệnh và cung<br /> xác định luồng giữa các câu lệnh. Vai trò<br /> quan trọng nhất của mỗi đỉnh là định nghĩa và<br /> sử dụng các biến tham gia trong chương trình.<br /> Ví dụ với biến a, ta có thể định nghĩa là da và<br /> sử dụng là ua.<br /> Các cấu trúc Kripke T biểu diễn các SUT nếu<br /> S=V, I = {vs} và δ = A {(vf, vf)}. Bằng cách<br /> thể hiện SUT với một cấu trúc Kripke, chúng<br /> ta có thể thiết lập các đường thực thi của<br /> chương trình một cách tự động dựa vào chuẩn<br /> bao phủ. Mỗi đường thực thi là một test case<br /> và tập hợp các test case đạt được theo chuẩn<br /> bao phủ nhất định tạo thành các bộ test.<br /> Logic tuyến tính thời gian<br /> Cấu trúc Kripke T phản ánh hành vi có thể có<br /> của chương trình và nó được sử dụng để kiểm<br /> chứng mô hình, công thức LTL được xác định<br /> trên tập hợp các mệnh đề cơ sở AP. Công<br /> thức LTL được tạo ra bằng việc sử dụng các<br /> quy<br /> tắc<br /> ngữ<br /> pháp<br /> sau<br /> ϕ ::= true | α | ϕ1 ∧ ϕ 2 | ¬ϕ | Οϕ | ϕ1 ∪ ϕ 2 ,<br /> với α đại diện cho mệnh đề cơ sở, Ο cho<br /> toán tử logic next và ∪ là toán tử logic Until.<br /> Hai toán tử khác có nguồn gốc từ những thể<br /> 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.<br /> Kiểm chứng được dùng để kiểm thử luồng dữ<br /> liệu [8]. Với đồ thị điều khiển luồng của hình<br /> <br /> (<br /> <br /> 80<br /> <br /> )<br /> <br /> 99(11): 79 - 84<br /> <br /> 1, bao phủ rẽ nhánh sẽ tạo ra các test case bao<br /> gồm các đỉnh {v3, v4, v5, v6,v7 ,v8, v10} và bao<br /> phủ luồng dữ liệu sẽ tìm kiếm tất cả các<br /> đường thực thi có thể cho giữa việc định<br /> nghĩa và việc sử dụng biến chương trình d.<br /> Tuy nhiên, câu lệnh điều khiển luồng trạng<br /> thái ảnh hưởng đến phạm vi bao phủ luồng dữ<br /> liệu và sự phụ thuộc này có thể được mã hoá<br /> trong công thức LTL. Ví dụ cho đoạn chương<br /> trình 1 như sau:<br /> int method( int a, int b, int c) {<br /> int d=0;<br /> if (a=20 && a