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

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ử.
Nội dung trích xuất từ tài liệu:
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<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 /> Tron ...