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

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: [email protected]

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.