Một phướng pháp kiểm chứng và sinh test case cho các dịch vụ web dựa vào kiểm chứng mô hình

Nguyễn Hồng Tân và Đtg Tạp chí KHOA HỌC & CÔNG NGHỆ 102(02): 27 - 32

27

MỘT PHƯỚNG PHÁP KIỂM CHỨNG VÀ SINH TEST CASE

CHO CÁC DỊCH VỤ WEB DỰA VÀO KIỂM CHỨNG MÔ HÌNH

Nguyễn Hồng Tân1*, Nguyễn Trường Thắng2

,

Bùi Anh Tú1

, Nguyễn Thị Tuyến

1

1

Trường Đại học Công nghệ thông tin và Truyền thông – ĐH Thái Nguyên

2Viện Công nghệ thông tin – Viện khoa học và công nghệ Việt Nam

TÓM TẮT

Ngày nay, các ứng dụng dịch vụ web rất phổ biến và có vai trò quan trọng trong các lĩnh vực của

đời sống xã hội. Bài báo này, chúng tôi đề xuất một phương pháp mới nhằm kiểm chứng và sinh

bộ kiểm thử cho mô hình hành vi và mô hình điều khiển của ứng dụng dịch vụ web. Với phương

pháp này, mô hình hành vi của ứng dụng web được chuyển đổi thành sang ngôn ngữ SMV, các

chuẩn bao phủ kiểm thử được đặc tả bằng ngôn ngữ LTL, CTL, sau đó bộ công cụ kiểm chứng

NuSMV được sử dụng để kiểm chứng một cách tự động mô hình hành vi và sinh ra các phản ví dụ

từ đó sinh ra các bộ kiểm thử.

Từ khóa: Dịch vụ web, Kiểm chứng mô hình, Test Case, NuSMV.

GIỚI THIỆU

*

Các ứng dụng dịch vụ web đang phát triển rất

nhanh và được sử dụng cho nhiều mục đích

khác nhau như trong kinh doanh và hệ thống

chính phủ điện tử [3]. Để đảm bảo chất lượng

dịch vụ web, một số phương pháp đã được đề

xuất dựa vào mô hình hành vi và mô hình

điều khiển để xác minh dịch vụ web. Kết quả

đạt được là dịch vụ web dễ dàng được bảo trì,

kiểm thử tốt hơn, phân tích, gỡ lỗi và các thiết

kế của ứng dụng được xác minh một cách tự

động [3][4]. Tuy nhiên, các phương pháp đề

xuất mới chỉ dừng lại ở mức độ kiểm chứng

các mô hình mà chưa hỗ trợ sinh ra được các

bộ dữ liệu test để đảm bảo khách quan vấn đề

kiểm thử ứng dụng web. Phương pháp tự

động sinh dữ liệu test dựa trên mô hình hành

vi của ứng dụng web giải quyết được các vấn

đề lỗi thiết kế. Hành vi của ứng dụng web

được chia thành hai phần: hành vi thực thi và

hành vi điều khiển. Hành vi thực thi là ứng

dụng độc lập, đó là các chức năng ở tầng

nghiệp vụ của một dịch vụ web. Hành vi điều

khiển là một ứng dụng độc lập hoạt động như

một bộ điều khiển thông qua hành vi thực thi

và thực thi các xử lý. Biểu đồ trạng thái được

sử dụng để mô tả hành vi của ứng dụng web.

Từ biểu đồ trạng thái chuyển đổi hành vi ứng

dụng web thành ngôn ngữ SMV để kiểm

chứng sử dụng bộ công cụ NuSMV. Dựa vào

*

Tel: 0943 252165, Email: [email protected]

chuẩn bao phủ test để chuyển các thuộc tính

bẫy của thành công thức LTL/CTL. Các bộ

test được sinh tự động khi kiểm chứng mô

hình hành vi ứng dụng web và áp dụng công

thức LTL/CTL.

CÁC KIẾN THỨC NỀN TẢNG

- Mô hình hành vi dịch vụ web

Hành vi của dịch vụ web được định nghĩa

gồm 5 thành phần: B=(S, L, T, S0, F) [4].

Trong đó, S là tập hữu hạn các trạng thái;

S0∈ S là trạng thái khởi tạo; F ∈ S là trạng

thái kết thúc; L là nhãn các đường chuyển

trạng thái; T S x L x S ⊆ là các ràng buộc

chuyển trạng thái với mỗi đường truyền

t=(Ssrc, l, Stgt) là thành phần của một trạng thái

nguồn Ssrc∈S, Stgt∈S,

l ∈ L.

-Kiểm chứng mô hình

Kiểm chứng mô hình là một tập các kỹ thuật

để phân tích sự biểu diễn trừu tượng của một

hệ thống để xác định tính xác thực của một

hay nhiều thuộc tính quan tâm. Cụ thể hơn, nó

được định nghĩa là một thuật toán định dạng

kỹ thuật xác minh với trạng thái hữu hạn cho

hệ thống hiện tại (Clarke 1986, Queille 1982,

NASA 2004).

-Cấu trúc Kripke

Một hệ thống hữu hạn trạng thái được mô tả

như một bộ gồm các thành phần [2]:

M S I R L =< > , , ,

Trong đó, S hữu hạn các trạng thái; I trạng

thái khởi đầu; R S S ⊆ × là phép trạng thái