Nguyễn Hồng Tân và Đtg<br />
<br />
Tạp chí KHOA HỌC & CÔNG NGHỆ<br />
<br />
102(02): 27 - 32<br />
<br />
MỘT PHƯỚNG PHÁP KIỂM CHỨNG VÀ SINH TEST CASE<br />
CHO CÁC DỊCH VỤ WEB DỰA VÀO KIỂM CHỨNG MÔ HÌNH<br />
Nguyễn Hồng Tân1*, Nguyễn Trường Thắng2,<br />
Bùi Anh Tú1, Nguyễn Thị Tuyến1<br />
1<br />
<br />
Trường Đại học Công nghệ thông tin và Truyền thông – ĐH Thái Nguyên<br />
2<br />
Viện Công nghệ thông tin – Viện khoa học và công nghệ Việt Nam<br />
<br />
TÓM TẮT<br />
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<br />
đờ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<br />
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<br />
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<br />
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<br />
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ụ<br />
từ đó sinh ra các bộ kiểm thử.<br />
Từ khóa: Dịch vụ web, Kiểm chứng mô hình, Test Case, NuSMV.<br />
<br />
GIỚI THIỆU*<br />
Các ứng dụng dịch vụ web đang phát triển rất<br />
nhanh và được sử dụng cho nhiều mục đích<br />
khác nhau như trong kinh doanh và hệ thống<br />
chính phủ điện tử [3]. Để đảm bảo chất lượng<br />
dịch vụ web, một số phương pháp đã được đề<br />
xuất dựa vào mô hình hành vi và mô hình<br />
điều khiển để xác minh dịch vụ web. Kết quả<br />
đạt được là dịch vụ web dễ dàng được bảo trì,<br />
kiểm thử tốt hơn, phân tích, gỡ lỗi và các thiết<br />
kế của ứng dụng được xác minh một cách tự<br />
động [3][4]. Tuy nhiên, các phương pháp đề<br />
xuất mới chỉ dừng lại ở mức độ kiểm chứng<br />
các mô hình mà chưa hỗ trợ sinh ra được các<br />
bộ dữ liệu test để đảm bảo khách quan vấn đề<br />
kiểm thử ứng dụng web. Phương pháp tự<br />
động sinh dữ liệu test dựa trên mô hình hành<br />
vi của ứng dụng web giải quyết được các vấn<br />
đề lỗi thiết kế. Hành vi của ứng dụng web<br />
được chia thành hai phần: hành vi thực thi và<br />
hành vi điều khiển. Hành vi thực thi là ứng<br />
dụng độc lập, đó là các chức năng ở tầng<br />
nghiệp vụ của một dịch vụ web. Hành vi điều<br />
khiển là một ứng dụng độc lập hoạt động như<br />
một bộ điều khiển thông qua hành vi thực thi<br />
và thực thi các xử lý. Biểu đồ trạng thái được<br />
sử dụng để mô tả hành vi của ứng dụng web.<br />
Từ biểu đồ trạng thái chuyển đổi hành vi ứng<br />
dụng web thành ngôn ngữ SMV để kiểm<br />
chứng sử dụng bộ công cụ NuSMV. Dựa vào<br />
*<br />
<br />
Tel: 0943 252165, Email: nhtan@ictu.edu.vn<br />
<br />
chuẩn bao phủ test để chuyển các thuộc tính<br />
bẫy của thành công thức LTL/CTL. Các bộ<br />
test được sinh tự động khi kiểm chứng mô<br />
hình hành vi ứng dụng web và áp dụng công<br />
thức LTL/CTL.<br />
CÁC KIẾN THỨC NỀN TẢNG<br />
- Mô hình hành vi dịch vụ web<br />
Hành vi của dịch vụ web được định nghĩa<br />
gồm 5 thành phần: B=(S, L, T, S0, F) [4].<br />
Trong đó, S là tập hữu hạn các trạng thái;<br />
S0 ∈ S là trạng thái khởi tạo; F ∈ S là trạng<br />
thái kết thúc; L là nhãn các đường chuyển<br />
trạng thái; T ⊆ S x L x S là các ràng buộc<br />
chuyển trạng thái với mỗi đường truyền<br />
t=(Ssrc, l, Stgt) là thành phần của một trạng thái<br />
nguồn Ssrc ∈ S, Stgt ∈ S, l ∈ L.<br />
-Kiểm chứng mô hình<br />
Kiểm chứng mô hình là một tập các kỹ thuật<br />
để phân tích sự biểu diễn trừu tượng của một<br />
hệ thống để xác định tính xác thực của một<br />
hay nhiều thuộc tính quan tâm. Cụ thể hơn, nó<br />
được định nghĩa là một thuật toán định dạng<br />
kỹ thuật xác minh với trạng thái hữu hạn cho<br />
hệ thống hiện tại (Clarke 1986, Queille 1982,<br />
NASA 2004).<br />
-Cấu trúc Kripke<br />
Một hệ thống hữu hạn trạng thái được mô tả<br />
như một bộ gồm các thành phần [2]:<br />
<br />
M =< S , I , R, L ><br />
Trong đó, S hữu hạn các trạng thái; I trạng<br />
thái khởi đầu; R ⊆ S × S là phép trạng thái<br />
27<br />
<br />
Nguyễn Hồng Tân và Đtg<br />
<br />
Tạp chí KHOA HỌC & CÔNG NGHỆ<br />
<br />
(biểu diễn phép chuyển từ trạng thái này đến<br />
trạng thái khác); L : S − > 2 AP là chức năng<br />
của trạng thái được gán nhãn với phần tử cơ sở<br />
(nguyên tử đề xuất) từ một ngôn ngữ đưa ra.<br />
Logic thời gian (Temporal logic) được sử<br />
dụng để kiểm chứng hành vi của hệ thống<br />
theo cấu trúc Kripke. Một hành vi trong cấu<br />
trúc Kripke bắt đầu từ trạng thái S ∈ I và đạt<br />
đến một trạng thái khác thuộc S thông qua R .<br />
-CTL và LTL[3]<br />
- LTL (Linear-Time-Temporal Logic): Logic<br />
thời gian tuyến tính. Thời gian có cấu trúc<br />
tuyến tính, mỗi trạng thái chỉ có một trạng<br />
thái ngay tiếp sau nó.<br />
Cú pháp:<br />
<br />
Φ ::= p | ¬Φ | Φ ∨ Φ | X Φ | ΦU Φ<br />
- CTL (Branching-Time-Temporal Logic):<br />
Logic thời gian rẽ nhánh. Thời gian có cấu<br />
trúc tuyến tính, mỗi trạng thái có nhiều trạng<br />
thái ngay tiếp sau nó.<br />
Cú pháp:<br />
<br />
Φ::= p| ¬Φ| Φ∨Φ| ΦUΦ| EXΦ| E(ΦUΦ)| A(ΦUΦ)<br />
<br />
Trong đó: X: toán tử Next, U: toán tử Until,<br />
E: toán tử Exit.<br />
-Chuẩn bao phủ test<br />
Dựa vào chuẩn bao phủ test để xác minh và<br />
sinh bộ test cho ứng dụng web được khách<br />
quan và đầy đủ. Các chuẩn bao phủ gồm [2]:<br />
- Bao phủ trạng thái: mọi trạng thái của mô<br />
hình được thăm ít nhất một lần.<br />
- Bao phủ đường truyền: mọi đường truyền<br />
của mô hình phải được đi qua ít nhất một lần.<br />
- Bao phủ cặp đường truyền: mọi cặp đường<br />
truyền liền kề trong mô hình hoặc trong biểu<br />
đồ trạng thái phải được đi qua ít nhất một lần.<br />
- Bao phủ đường thực thi: mọi đường thực thi<br />
phải được đi qua ít nhất một lần. Tất cả các<br />
đường thực thi là tiêu chí tương ứng để kiểm<br />
tra đầy đủ cấu trúc điều khiển của mô hình.<br />
<br />
Trong thực tế điều này là không thể bởi vì mô<br />
hình như vậy thường chứa một số lượng vô<br />
hạn đường thực thi do vòng lặp.<br />
Một bộ test bắt đầu từ trạng thái khởi tạo và<br />
kết thúc ở trạng thái kết thúc.<br />
-Ngôn ngữ SMV và công cụ NuSMV<br />
+ Công cụ NuSMV [1]<br />
NuSMV là công cụ kiểm chứng mô hình<br />
được phát triển bởi trường Carnegie Mellon<br />
và viện per Ricerca Scientifica e Tecnolgica<br />
(IRST). NuSMV được viết bằng ngôn ngữ<br />
ANSI C. NuSMV được thiết kế với kiến trúc<br />
mở, mềm dẻo và được mô tả đầy đủ để phục<br />
vụ cho việc kiểm chứng mô hình phần mềm.<br />
Nếu được sử dụng trong các dự án chuyển<br />
giao công nghệ, NuSMV được thiết kế rất<br />
mạnh mẽ, thay đổi dễ dàng và gần với các yêu<br />
cầu chuẩn của công nghệ.<br />
Công cụ NuSMV có chức năng tạo ra một<br />
mô hình ảo (simulate) cho phép người sử<br />
dụng kiểm tra xem mô hình có đúng với đặc<br />
tả hay không.<br />
+Ngôn ngữ SMV [1]<br />
Ngôn ngữ đầu vào của công cụ NuSMV là<br />
ngôn ngữ SMV. Ngôn ngữ này mô tả được<br />
các hệ thống hữu hạn trạng thái. Các kiểu dữ<br />
liệu mà ngôn ngữ này cung cấp bao gồm: kiểu<br />
logic (boolean), kiểu số nguyên (bounded<br />
interger subrange) và các kiểu dữ liệu liệt kê<br />
symbolic enum.<br />
Các mô tả của một hệ thống phức tạp có thể<br />
được chia nhỏ thành các module và mỗi một<br />
module này có thể được thực thi nhiều lần.<br />
PHƯƠNG PHÁP SINH BỘ KIỂM THỬ<br />
CHO CÁC ỨNG DỤNG WEB DỰA VÀO<br />
KIỂM CHỨNG MÔ HÌNH.<br />
Phương pháp kiểm chứng mô hình hành vi và<br />
sinh dữ liệu kiểm thử cho các dịch vụ Web<br />
được nhóm nghiên cứu đề xuất qua 5 bước<br />
như hình vẽ 1 sau đây.<br />
<br />
Hình 1: Phương pháp thực hiện<br />
<br />
28<br />
<br />
102(02): 27 - 32<br />
<br />
Nguyễn Hồng Tân và Đtg<br />
<br />
Tạp chí KHOA HỌC & CÔNG NGHỆ<br />
<br />
102(02): 27 - 32<br />
<br />
Các bước thực hiện:<br />
Bước 1: Từ mô hình hành vi của ứng dụng web chuyển thành mô hình hành vi điều khiển và<br />
hành vi thực thi.<br />
Ví dụ. Bài toán được phát biểu như sau: Dịch vụ dịch ngôn ngữ của Google Translatetor và cung<br />
cấp ngôn ngữ hỗ trợ từ dịch vụ Microsoft Translatetor. Đầu vào là chuỗi văn bản cần dịch. Trước<br />
hết, dịch vụ kiểm tra hỗ trợ ngôn ngữ. Sau đó, ngôn ngữ của văn bản được tự động phát hiện và<br />
văn bản được dịch. Nếu người dùng chọn ngôn ngữ thì ngôn ngữ được kiểm tra lại một lần nữa,<br />
sau đó văn bản có thể dịch được hoặc không dịch được. Từ đó bài toán được mô tả thành mô hình<br />
hành vi thực thi và mô hình hành vi điều khiển như hình vẽ 2 và 3 sau đây:<br />
<br />
Hình 2: Mô hình hành vi thực thi<br />
<br />
Hình 3: Mô hình hành vi điều khiển<br />
<br />
Ta xác định được cấu trúc Kripke:<br />
<br />
Hình 4: Cấu trúc Kripke của mô hình hành vi<br />
<br />
29<br />
<br />
Nguyễn Hồng Tân và Đtg<br />
<br />
Tạp chí KHOA HỌC & CÔNG NGHỆ<br />
<br />
Trong đó, Na: trạng thái không hoạt động;<br />
Re: trạng thái nhận; In: trạng thái gọi; Pr:<br />
trạng thái xử lý; Ab: trạng thái hủy bỏ; Do:<br />
trạng thái thực hiện; En: trạng thái kết thúc.<br />
Dựa vào thuật toán giảm trạng thái và đường<br />
truyền [3][4] để giảm số trạng thái cho mô<br />
hình trên:<br />
- Nếu (s1,s2) và (s2,s1) là hai đường truyền thì<br />
chúng sẽ được thay thế bằng đường truyền<br />
(s1, s1).<br />
- Nếu chỉ một trong hai đường truyền tồn tại<br />
thì nó sẽ bị xóa đi.<br />
- Cho mọi x, nếu (sx,s2) là một đường truyền<br />
thì nó sẽ bị bỏ đi và thay thế bằng đường<br />
truyền (sx,s1) nếu như một đường truyền<br />
không tồn tại.<br />
- Cho mọi y, nếu (s2,sy) là một đường truyền<br />
thì nó sẽ bị bỏ đi và thay thế bằng đường<br />
truyền (s1,sy) nếu như một đường truyền<br />
không tồn tại.<br />
<br />
Hình 5: Cấu trúc Kripke của mô hình sau khi<br />
giảm trạng thái<br />
<br />
Bước 2: Chuyển mô hình hành vi thực thi<br />
thành ngôn ngữ mô hình SMV.<br />
Từ cấu trúc Kripke hình 5 ta chuyển thành<br />
ngôn ngữ SMV như sau:<br />
<br />
MODULE main<br />
VAR state:{Na,Re,In,Ab,Pr,Do,Su,En,Co};<br />
ASSIGN<br />
init(state):=Na;<br />
next(state):=<br />
case<br />
(state=Do):{En};<br />
(state=Re):{Do};<br />
(state=In):{Ab,Pr};<br />
(state=Pr):{Re,In};<br />
(state=Ab):{En};<br />
(state=Na):{Re};<br />
(state=En):{Na};<br />
1:state;<br />
esac;<br />
Bước 3: Dựa vào chuẩn bao phủ test và mô<br />
hình hành vi điều khiển để viết công thức<br />
CTL và LTL.<br />
LTL: G (state = Na -> X F (state = In |<br />
state = En)).<br />
CTL: AG (state = Na -> AF state = En).<br />
AG (state = Re -> EX (state = In |<br />
state = Do)).<br />
AG (state = Re -> EF state = En).<br />
AG (state = In -> EX ((state = Ab |<br />
state = Re) | state = Pr)).<br />
AG (state = In -> EF state = En).<br />
AG (state = Pr -> EX ((state = Ab |<br />
state = Re) | state = In))<br />
AG (state = Pr -> EF state = En).<br />
Bước 4: Kiểm chứng mô hình nhờ bộ kiểm<br />
chứng NuSMV. Ta dựa vào bộ kiểm chứng<br />
NuSMV để kiểm tra mô hình và có kết quả<br />
như hình vẽ sau.<br />
<br />
Hình 6. Kết quả sau khi kiểm tra mô hình trên bộ kiểm chứng NuSMV<br />
<br />
30<br />
<br />
102(02): 27 - 32<br />
<br />
Nguyễn Hồng Tân và Đtg<br />
<br />
Tạp chí KHOA HỌC & CÔNG NGHỆ<br />
<br />
102(02): 27 - 32<br />
<br />
Hình 7. Các bộ test sau khi tìm ra các phản ví dụ<br />
<br />
Bước 5: Tìm các trường hợp phản ví dụ<br />
(counter example) để sinh dữ liệu test và thực<br />
thi test. Counter example là do lỗi hệ thống hoặc<br />
thiết kế, lỗi mô hình, hoặc lỗi trong yêu cầu.<br />
Chẳng hạn, Lỗi yêu cầu: đảm bảo trạng thái<br />
Re được thực thi tốt. Ta có công thực sau F<br />
G state = Re.<br />
Sau khi thực thi test bộ test được sinh tự động<br />
dựa vào lưu vết đường đi của mô hình trong<br />
NuSMV.<br />
KẾT LUẬN<br />
Trong bài báo này, phương pháp tự động sinh<br />
dữ liệu test dựa trên mô hình hành vi của ứng<br />
dụng web được trình bày để giải quyết các<br />
vấn đề về tìm lỗi thiết kế trong các dịch vụ<br />
Web. Mô hình hành vi được mô hình hóa dựa<br />
trên hành vi thực thi và hành vi điều khiển.<br />
Hành vi thực thi thể hiện tầng nghiệp vụ của<br />
dịch vụ web. Hành vi điều khiển thể hiện các<br />
ràng buộc và trạng thái trong hành vi thực thi.<br />
Đồng bộ hóa hành vi thực thi và hành vi điều<br />
khiển là vấn đề để đảm bảo một thiết kế dịch<br />
vụ web là tốt. Phương pháp xác minh và tự<br />
động sinh dữ liệu test được sử dụng dựa trên<br />
mô hình hành vi của ứng dụng web, dữ liệu<br />
<br />
test được sinh tự động nhờ vào các thuộc tính<br />
từ mô hình và thuộc tính CLT/LTL dựa trên<br />
chuẩn bao phủ test. Kết quả đạt được là sinh<br />
được dữ liệu test một cách tự động để đảm<br />
bảo chất lượng dịch vụ web.<br />
TÀI LIỆU THAM KHẢO<br />
[1]. A.Cimatti, E.Clarke, F.Giunchiglia, M.Roveri,<br />
NuSMV: a new symbolic model checker, ITCIRST, Italy 2000.<br />
[2]. M.Mark Utting, Bruno Legeard, Practical<br />
model-based testing, Elsevier, 2007.<br />
[3]. Melissa KOVA, Jamal BENTAHAR, Zakaria<br />
MAAMAR and Hamdi YAHYAOUI. A Formal<br />
Verification Approach of Conversations in<br />
Composite Web Services using NuSMV, Artificial<br />
Intelligence and Application, IOS Press, pp. 245261, 2009.<br />
[4]. Quan Z. Sheng, Zakaria Maamar, Lina Yao,<br />
Claudia Szabo, Scott Bourne Behavior modeling<br />
and automated verification of Web services,<br />
Elsevier Inc 2012.<br />
[5]. Yongyan Zheng, Jiong Zhou. A Model<br />
Checking based Test Case Generation Framework<br />
for Web Services, International Conference on<br />
Information Technology (ITNG'07)0-7695-27760/07, IEEE 2007.<br />
<br />
31<br />
<br />
Thêm vào BST
Báo xấu
Download
Vui lòng tải xuống để xem tài liệu đầy đủ
