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

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.
Nội dung trích xuất từ tài liệu:
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 Tạp chí KHOA HỌC & CÔNG NGHỆ 99(11): 79 - 84 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. 79 Nguyễn Hồng Tân và Đtg Tạp chí KHOA HỌC & CÔNG NGHỆ 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 T = (S , I , A, δ ) . 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 → 2 AP với AP là mệnh đề cơ sở; δ ⊆ S × S là phép chuyển trạng thái. Một đồ thị luồng G = V , v s , v f , A là một đồ thị có hướng. Trong đó, V: là tập hữu hạn các trạng thái; vs ∈ V là đỉnh ban đầu; v f ∈ V 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 ϕ ::= true | α | ϕ1 ∧ ϕ 2 | ¬ϕ | Οϕ | ϕ1 ∪ ϕ 2 , 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 ( 80 ) 99(11): 79 - 84 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ể ...