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ến1 1Trườ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: nhtan@ictu.edu.vn 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 Nguyễn Hồng Tân và Đtg Tạp chí KHOA HỌC & CÔNG NGHỆ 102(02): 27 - 32 28 (biểu diễn phép chuyển từ trạng thái này đến trạng thái khác); : 2APL S− > là chức năng của trạng thái được gán nhãn với phần tử cơ sở (nguyên tử đề xuất) từ một ngôn ngữ đưa ra. Logic thời gian (Temporal logic) được sử dụng để kiểm chứng hành vi của hệ thống theo cấu trúc Kripke. Một hành vi trong cấu trúc Kripke bắt đầu từ trạng thái S I∈ và đạt đến một trạng thái khác thuộc S thông qua R . -CTL và LTL[3] - LTL (Linear-Time-Temporal Logic): Logic thời gian tuyến tính. Thời gian có cấu trúc tuyến tính, mỗi trạng thái chỉ có một trạng thái ngay tiếp sau nó. Cú pháp: :: | | | |p X UΦ = ¬Φ Φ ∨ Φ Φ Φ Φ - CTL (Branching-Time-Temporal Logic): Logic thời gian rẽ nhánh. Thời gian có cấu trúc tuyến tính, mỗi trạng thái có nhiều trạng thái ngay tiếp sau nó. Cú pháp: :: | | | | | ( )| ( )p U EX E U A UΦ = ¬Φ Φ∨Φ Φ Φ Φ Φ Φ Φ Φ Trong đó: X: toán tử Next, U: toán tử Until, E: toán tử Exit. -Chuẩn bao phủ test Dựa vào chuẩn bao phủ test để xác minh và sinh bộ test cho ứng dụng web được khách quan và đầy đủ. Các chuẩn bao phủ gồm [2]: - Bao phủ trạng thái: mọi trạng thái của mô hình được thăm ít nhất một lần. - Bao phủ đường truyền: mọi đường truyền của mô hình phải được đi qua ít nhất một lần. - Bao phủ cặp đường truyền: mọi cặp đường truyền liền kề trong mô hình hoặc trong biểu đồ trạng thái phải được đi qua ít nhất một lần. - Bao phủ đường thực thi: mọi đường thực thi phải được đi qua ít nhất một lần. Tất cả các đường thực thi là tiêu chí tương ứng để kiểm tra đầy đủ cấu trúc điều khiển của mô hình. Trong thực tế điều này là không thể bởi vì mô hình như vậy thường chứa một số lượng vô hạn đường thực thi do vòng lặp. Một bộ test bắt đầu từ trạng thái khởi tạo và kết thúc ở trạng thái kết thúc. -Ngôn ngữ SMV và công cụ NuSMV + Công cụ NuSMV [1] NuSMV là công cụ kiểm chứng mô hình được phát triển bởi trường Carnegie Mellon và viện per Ricerca Scientifica e Tecnolgica (IRST). NuSMV được viết bằng ngôn ngữ ANSI C. NuSMV được thiết kế với kiến trúc mở, mềm dẻo và được mô tả đầy đủ để phục vụ cho việc kiểm chứng mô hình phần mềm. Nếu được sử dụng trong các dự án chuyển giao công nghệ, NuSMV được thiết kế rất mạnh mẽ, thay đổi dễ dàng và gần với các yêu cầu chuẩn của công nghệ. Công cụ NuSMV có chức năng tạo ra một mô hình ảo (simulate) cho phép người sử dụng kiểm tra xem mô hình có đúng với đặc tả hay không. +Ngôn ngữ SMV [1] Ngôn ngữ đầu vào của công cụ NuSMV là ngôn ngữ SMV. Ngôn ngữ này mô tả được các hệ thống hữu hạn trạng thái. Các kiểu dữ liệu mà ngôn ngữ này cung cấp bao gồm: kiểu logic (boolean), kiểu số nguyên (bounded interger subrange) và các kiểu dữ liệu liệt kê symbolic enum. Các mô tả của một hệ thống phức tạp có thể được chia nhỏ thành các module và mỗi một module này có thể được thực thi nhiều lần. PHƯƠNG PHÁP SINH BỘ KIỂM THỬ CHO CÁC ỨNG DỤNG WEB DỰA VÀO KIỂM CHỨNG MÔ HÌNH. Phương pháp kiểm chứng mô hình hành vi và sinh dữ liệu kiểm thử cho các dịch vụ Web được nhóm nghiên cứu đề xuất qua 5 bước như hình vẽ 1 sau đây. Hình 1: Phương pháp thực hiện Nguyễn Hồng Tân và Đtg Tạp chí KHOA HỌC & CÔNG NGHỆ 102(02): 27 - 32 29 Các bước thực hiện: 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à hành vi thực thi. 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 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 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à 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, 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 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: Hình 2: Mô hình hành vi thực thi Hình 3: Mô hình hành vi điều khiển Ta xác định được cấu trúc Kripke: Hình 4: Cấu trúc Kripke của mô hình hành vi Nguyễn Hồng Tân và Đtg Tạp chí KHOA HỌC & CÔNG NGHỆ 102(02): 27 - 32 30 Trong đó, Na: trạng thái không hoạt động; Re: trạng thái nhận; In: trạng thái gọi; Pr: trạng thái xử lý; Ab: trạng thái hủy bỏ; Do: trạng thái thực hiện; En: trạng thái kết thúc. Dựa vào thuật toán giảm trạng thái và đường truyền [3][4] để giảm số trạng thái cho mô hình trên: - Nếu (s1,s2) và (s2,s1) là hai đường truyền thì chúng sẽ được thay thế bằng đường truyền (s1, s1). - Nếu chỉ một trong hai đường truyền tồn tại thì nó sẽ bị xóa đi. - Cho mọi x, nếu (sx,s2) là một đường truyền thì nó sẽ bị bỏ đi và thay thế bằng đường truyền (sx,s1) nếu như một đường truyền không tồn tại. - Cho mọi y, nếu (s2,sy) là một đường truyền thì nó sẽ bị bỏ đi và thay thế bằng đường truyền (s1,sy) nếu như một đường truyền không tồn tại. Hình 5: Cấu trúc Kripke của mô hình sau khi giảm trạng thái Bước 2: Chuyển mô hình hành vi thực thi thành ngôn ngữ mô hình SMV. Từ cấu trúc Kripke hình 5 ta chuyển thành ngôn ngữ SMV như sau: MODULE main VAR state:{Na,Re,In,Ab,Pr,Do,Su,En,Co}; ASSIGN init(state):=Na; next(state):= case (state=Do):{En}; (state=Re):{Do}; (state=In):{Ab,Pr}; (state=Pr):{Re,In}; (state=Ab):{En}; (state=Na):{Re}; (state=En):{Na}; 1:state; esac; Bước 3: Dựa vào chuẩn bao phủ test và mô hình hành vi điều khiển để viết công thức CTL và LTL. LTL: G (state = Na -> X F (state = In | state = En)). CTL: AG (state = Na -> AF state = En). AG (state = Re -> EX (state = In | state = Do)). AG (state = Re -> EF state = En). AG (state = In -> EX ((state = Ab | state = Re) | state = Pr)). AG (state = In -> EF state = En). AG (state = Pr -> EX ((state = Ab | state = Re) | state = In)) AG (state = Pr -> EF state = En). Bước 4: Kiểm chứng mô hình nhờ bộ kiểm chứng NuSMV. Ta dựa vào bộ kiểm chứng NuSMV để kiểm tra mô hình và có kết quả như hình vẽ sau. Hình 6. Kết quả sau khi kiểm tra mô hình trên bộ kiểm chứng NuSMV Nguyễn Hồng Tân và Đtg Tạp chí KHOA HỌC & CÔNG NGHỆ 102(02): 27 - 32 31 Hình 7. Các bộ test sau khi tìm ra các phản ví dụ Bước 5: Tìm các trường hợp phản ví dụ (counter example) để sinh dữ liệu test và thực thi test. Counter example là do lỗi hệ thống hoặc thiết kế, lỗi mô hình, hoặc lỗi trong yêu cầu. Chẳng hạn, Lỗi yêu cầu: đảm bảo trạng thái Re được thực thi tốt. Ta có công thực sau F G state = Re. Sau khi thực thi test bộ test được sinh tự động dựa vào lưu vết đường đi của mô hình trong NuSMV. KẾT LUẬN Trong bài báo này, 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 được trình bày để giải quyết các vấn đề về tìm lỗi thiết kế trong các dịch vụ Web. Mô hình hành vi được mô hình hóa dựa trên hành vi thực thi và hành vi điều khiển. Hành vi thực thi thể hiện tầng nghiệp vụ của dịch vụ web. Hành vi điều khiển thể hiện các ràng buộc và trạng thái trong hành vi thực thi. Đồng bộ hóa hành vi thực thi và hành vi điều khiển là vấn đề để đảm bảo một thiết kế dịch vụ web là tốt. Phương pháp xác minh và tự động sinh dữ liệu test được sử dụng dựa trên mô hình hành vi của ứng dụng web, dữ liệu test được sinh tự động nhờ vào các thuộc tính từ mô hình và thuộc tính CLT/LTL dựa trên chuẩn bao phủ test. Kết quả đạt được là sinh được dữ liệu test một cách tự động để đảm bảo chất lượng dịch vụ web. TÀI LIỆU THAM KHẢO [1]. A.Cimatti, E.Clarke, F.Giunchiglia, M.Roveri, NuSMV: a new symbolic model checker, ITC- IRST, Italy 2000. [2]. M.Mark Utting, Bruno Legeard, Practical model-based testing, Elsevier, 2007. [3]. Melissa KOVA, Jamal BENTAHAR, Zakaria MAAMAR and Hamdi YAHYAOUI. A Formal Verification Approach of Conversations in Composite Web Services using NuSMV, Artificial Intelligence and Application, IOS Press, pp. 245- 261, 2009. [4]. Quan Z. Sheng, Zakaria Maamar, Lina Yao, Claudia Szabo, Scott Bourne Behavior modeling and automated verification of Web services, Elsevier Inc 2012. [5]. Yongyan Zheng, Jiong Zhou. A Model Checking based Test Case Generation Framework for Web Services, International Conference on Information Technology (ITNG'07)0-7695-2776- 0/07, IEEE 2007. Nguyễn Hồng Tân và Đtg Tạp chí KHOA HỌC & CÔNG NGHỆ 102(02): 27 - 32 32 SUMMARY A MODEL CHECKING BASED VERIFICATION AND TEST CASE GENERATION METHOD FOR WEB SERVICES Nguyen Hong Tan1*, Nguyen Truong Thang2, Bui Anh Tu1, Nguyen Thi Tuyen1 1College of Information and Communication Techonology – TNU 2 Institute of Information Technology - Vietnamese Academy of Science and Technology Nowadays, the web service applications are very popular and have an important role in the fields of social life. This paper, we propose a new method to verify and test the behavior model and control model of web service applications. With this method, web application behavior model is converted into the SMV language, the test coverage standard is specified in the language LTL/CTL, and then NuSMV tool is used to verified behavioral model and automatically generates counter example which generates the test. Key word: web service, Model checking, Test Case, NuSMV Ngày nhận bài:22/1/2013, ngày phản biện:05/2/2013, ngày duyệt đăng: 26/3/2013 * Tel: 0943 252165, Email: nhtan@ictu.edu.vn