Tài liệu Nghiên cứu về kiểm thử dựa trên mô hình và ứng dụng

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ LÊ THỊ PHƯỢNG NGHIÊN CỨU VỀ KIỂM THỬ DỰA TRÊN MÔ HÌNH VÀ ỨNG DỤNG Ngành: Công nghệ thông tin Chuyên ngành: Kỹ thuật phần mềm Mã Số: 60 48 01 03 LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN NGƯỜI HƯỚNG DẪN KHOA HỌC: PGS.TS. NGUYỄN VIỆT HÀ Hà Nội – 2015 i MỤC LỤC MỤC LỤC .........................................................................................................................i LỜI CẢM ƠN ................................................................................................................ iii LỜI CAM ĐOAN ............................................................................................................ iv DANH MỤC THUẬT NGỮ VIẾT TẮT .......................................................................... v DANH MỤC HÌNH VẼ .................................................................................................. vi DANH MỤC BẢNG ......................................................................................................vii Chương 1: Giới thiệu ........................................................................................................ 8 Chương 2: Phương pháp đặc tả tương tác giao diện cho các ứng dụng Web .................... 10 2.1 Đặc tả tương tác giao diện của từng trang Web bằng ôtômát hữu hạn trạng thái.... 10 2.2 Xây dựng mô hình đặc tả tương tác giao diện cho toàn bộ ứng dụng Web ............ 16 2.3 Biểu diễn mô hình đặc tả dưới dạng các tệp tin MS Excel..................................... 19 Chương 3: Sinh và thực thi các ca kiểm thử tự động ....................................................... 26 3.1 Sinh các ca kiểm thử từ mô hình đặc tả hình thức ................................................. 26 3.1.1 Đường dẫn kiểm thử ...................................................................................... 26 3.1.2 Thuật toán sinh tự động các đường dẫn kiểm thử ........................................... 27 3.2 Thực hiện các ca kiểm thử .................................................................................... 32 3.4 Đánh giá phương pháp .......................................................................................... 33 Chương 4: Công cụ và thực nghiệm ................................................................................ 35 4.1 Giới thiệu các công cụ bổ trợ ................................................................................ 35 4.1.1 Giới thiệu Selenium và một số API WebDriver được sử dụng ....................... 35 4.1.2 Giới thiệu Jsoup............................................................................................. 37 4.2 Giới thiệu công cụ kiểm thử tự động tương tác giao diện cho các ứng dụng Web . 38 4.2.1 Kiến trúc của công cụ .................................................................................... 39 4.2.2 Đầu vào của công cụ...................................................................................... 40 4.2.3 Đầu ra của công cụ ........................................................................................ 42 4.3 Thực nghiệm ........................................................................................................ 44 4.4 Kết quả cải tiến công cụ ........................................................................................ 51 4.5 Ý nghĩa của công cụ thực nghiệm ......................................................................... 53 ii Chương 5: KẾT LUẬN .................................................................................................. 55 TÀI LIỆU THAM KHẢO .............................................................................................. 57 iii LỜI CẢM ƠN Trước tiên tôi xin gửi lời cảm ơn chân thành và sâu sắc đến thầy giáo PGS.TS Nguyễn Việt Hà và thầy giáo TS. Phạm Ngọc Hùng - người đã trực tiếp hướng dẫn, khuyến khích, chỉ bảo và đóng góp những ý kiến quý báu trong suốt quá trình tôi học tập, nghiên cứu cũng như từ khi tôi bắt đầu nghiên cứu đề tài đến khi hoàn thành luận văn này. Tôi xin chân thành cảm ơn các thầy cô giáo khoa Công nghệ thông tin, trường Đại học Công nghệ, Đại học Quốc Gia Hà Nội đã tận tình đào tạo, cung cấp cho tôi những kiến thức vô cùng quý giá, đã tạo điều kiện tốt nhất cho tôi trong suốt quá trình học tập, nghiên cứu tại trường. Đồng thời tôi xin chân thành cảm ơn những người thân trong gia đình cùng toàn thể bạn bè, đồng nghiệp đã luôn giúp đỡ, động viên tôi trong những lúc gặp phải khó khăn trong việc học tập và nghiên cứu. Cuối cùng, tôi xin chân thành cảm ơn Lê Khánh Trình người đã giúp đỡ, tạo điều kiện cho tôi nghiên cứu công cụ kiểm thử tự động ATWT và các đồng nghiệp của tôi tại Cục Công nghệ thông tin - Tổng cục IV - Bộ Công an đã giúp đỡ, tạo điều kiện thuận lợi cho tôi học tập và nghiên cứu chương trình thạc sĩ tại Đại học Công nghệ, ĐH QGHN. iv LỜI CAM ĐOAN Tôi xin cam đoan rằng luận văn thạc sĩ công nghệ thông tin “Nghiên cứu về kiểm thử dựa trên mô hình và ứng dụng” là công trình nghiên cứu của riêng tôi dưới sự hướng dẫn của thầy giáo PGS.TS Nguyễn Việt Hà và thầy giáo TS. Phạm Ngọc Hùng, không sao chép lại của người khác. Trong toàn bộ nội dung của luận văn, những điều đã được trình bày hoặc là của chính cá nhân tôi hoặc là được tổng hợp từ nhiều nguồn tài liệu. Tất cả các nguồn tài liệu tham khảo đều có xuất xứ rõ ràng và hợp pháp. Tôi xin hoàn toàn chịu trách nhiệm và chịu mọi hình thức kỷ luật theo quy định cho lời cam đoan này. Hà Nội, ngày 09 tháng 7 năm 2015 Lê Thị Phượng v DANH MỤC THUẬT NGỮ VIẾT TẮT STT Từ viết tắt Từ đầy đủ Ý nghĩa 1 API Application Interface Programming Giao diện lập trình ứng dụng 2 FSA Finite State Automaton Ôtômát hữu hạn trạng thái 3 MBT Model- base testing. Kiểm thử dựa trên mô hình. vi DANH MỤC HÌNH VẼ Hình 2.1. Trạng thái bắt đầu của trang tìm kiếm cán bộ Hình 2.2. Trạng thái đã nhập họ tên tìm kiếm Hình 2.3. Ôtômát hữu hạn trạng thái M1 Hình 2.4. Kết quả tìm kiếm cán bộ và nút sửa thông tin cán bộ Hình 2.5. Giao diện trang Web cập nhật thông tin cán bộ (update) Hình 2.6. Ôtômát hữu hạn trạng M2 Hình 2.7. Mô hình M sau khi thực hiện thuật toán ghép nối giữa M1 và M2 Hình 4.1. Kiến trúc của công cụ Auto Testing Web Application Hình 4.2. Lưu trữ các tệp tin đầu vào Hình 4.3. Cài đặt ôtômát hữu hạn trạng thái Hình 4.4. Giao diện nhập dữ liệu đầu vào của công cụ Hình 4.5. Kết quả kiểm thử. Hình 4.6. Ứng dụng Web quản lý thông tin cán bộ. Hình 4.7. Giao diện trang đăng nhập Hình 4.8. Giao diện các chức năng của người quản trị hệ thống. Hình 4.9. Trang quản lý người dùng Hình 4.10. Giao diện trang tìm kiếm cán bộ Hình 4.11. Trang thêm mới thông tin cán bộ Hình 4.12. Trang cập nhật thông tin cán bộ Hình 4.13. Thư mục các tệp tin đặc tả ứng dụng Quản lý thông tin cán bộ Hình 4.14. Giao diện của công cụ Hinh 4.15. Các đường dẫn kiểm thử được sinh tự động Hình 4.16. Kết quả thực hiện đường dẫn kiểm thử hiển thị trong tệp tin đầu ra Hình 4.17. Giao diện chức năng tạo menu động Hình 4.18. Giao diện pop-up vii DANH MỤC BẢNG Bảng 2.1. Các trạng thái Web của trang tìm kiếm cán bộ Bảng 2.2. Các sự kiện của trang tìm kiếm cán bộ Bảng 2.3. Bảng các phần tử Web của trang tìm kiếm cán bộ. Bảng 2.4. Bảng các trạng thái của trang tìm kiếm cán bộ Bảng 2.5. Bảng các sự kiện của trang tìm kiếm cán bộ Bảng 2.6. Bảng các transition của trang tìm kiếm cán bộ Bảng 2.7. tệp tin Excel đặc tả trang Web tìm kiếm cán bộ Bảng 3.1. Các transition của trang tìm kiếm thông tin cán bộ Bảng 3.2. Các testparth được sinh ra từ mô hình trang tìm kiếm thông tin cán bộ 8 Chương 1: Giới thiệu Trong ngành công nghiệp phát triển phần mềm ngày nay, hầu hết các phần mềm ứng dụng đều được phát triển trên nền Web. Do đó, việc kiểm thử đảm bảo chất lượng các ứng dụng Web là một vấn đề rất quan trọng. Tuy nhiên, các ứng dụng Web ngày càng trở nên phức tạp, việc kiểm thử thủ công bao gồm cả tạo các ca kiểm thử và thực thi chúng trên các trang Web, là công việc rất tốn kém về thời gian và công sức. Hơn nữa, mỗi khi có sự cập nhật lại phiên bản của phần mềm, để tránh rủi ro phát sinh lỗi trong khi thay đổi mã nguồn thì các kiểm thử viên phải kiểm thử lại toàn bộ phần mềm, kể cả các tính năng đã được kiểm thử tốt. Vì vậy, để hoàn thành công việc kiểm thử đúng tín độ, các công ty phần mềm cần phải áp dụng các phương pháp và công cụ nhằm tự động hóa các hoạt động kiểm thử. Kiểm thử tự động là một giải pháp hữu hiệu nhằm nâng cao tính chính xác và hiệu quả, cũng như giảm kinh phí và rút ngắn thời gian trong quá trình kiểm thử các sản phẩm phần mềm nói chung và các ứng dụng Web nói riêng [1]. Kiểm thử dựa trên mô hình đang được xem như là một phương pháp kiểm thử có khả năng tự động hóa cao. Kiểm thử dựa trên mô hình là một phương pháp kiểm thử, trong đó các ca kiểm thử được sinh ra từ mô hình đặc tả hành vi của hệ thống đang được kiểm thử [1]. Vì vậy, kiểm thử dựa trên mô hình được ứng dụng để giải quyết một số vấn đề khó khăn trong hoạt động kiểm thử các sản phẩm phần mềm. Một trong những ứng dụng của nó là kiểm thử tương tác giao diện người dùng cho các ứng dụng Web. Để ứng dụng phương pháp kiểm thử này, trước tiên chúng ta cần xây dựng mô hình đặc tả hành vi tương tác giao diện của ứng dụng Web. Mô hình này thường được biểu diễn bằng máy hữu hạn trạng thái hoặc ôtômát hữu hạn trạng thái. Tiếp đến, các ca kiểm thử được tự động sinh ra từ mô hình. Cuối cùng, các ca kiểm thử này được thực thi trên ứng dụng nhằm phát hiện các lỗi lập trình liên quan đến tương tác giao diện người dùng. Trong thực tế, có rất nhiều hướng nghiên cứu về kiểm thử dựa trên mô hình cho ứng dụng Web như kiểm thử khả năng chịu tải, tính bảo mật, hiệu năng, kiểm thử chức năng, v.v. [2,3,5,6]. Tuy nhiên, việc kiểm thử chức năng (theo luồng tương tác giao diện người dùng) vẫn chưa có giải pháp thỏa đáng. Một số nghiên cứu trước đã đề xuất các phương pháp và công cụ thực hiện việc kiểm thử chức năng ứng dụng Web [4,5,9]. Mặc dù vậy, các nghiên cứu này mới chỉ thực hiện kiểm thử tự động cho từng trang Web, hoặc cho các Website tĩnh [5] mà chưa có nhiều nghiên cứu hỗ trợ cho kiểm thử luồng tương tác người dùng. Trong số đó, phương pháp và công cụ kiểm thử tự động cho các ứng dụng Web được đề xuất bởi [5] đã giải quyết được một phần vấn đề nêu trên. Tuy 9 nhiên, phương pháp này chỉ thực hiện kiểm thử được cho một số phần tử Web cơ bản và chúng phải có thuộc tính id định danh. Trong khi, các hệ thống ứng dụng Web thực tế cần một công cụ kiểm thử tự động, có khả năng kiểm thử được cho nhiều loại phần tử Web và các phần tử Web đó được thiết kế một cách linh động. Nghiên cứu này được đưa ra nhằm giải quyết vấn đề trên. Đề tài đưa ra phương pháp đặc tả hình thức giao diện cho các ứng dụng Web. Từ đó, chúng tôi xây dựng thuật toán sinh tự động các ca kiểm thử từ bản đặc tả trên. Cuối cùng, đề tài dùng phương pháp đã được đề xuất trong [5] làm cơ sở để xây dựng một công cụ kiểm thử tự động tương tác giao diện các ứng dụng Web. Công cụ này kiểm thử được cho các ứng dụng Web có nhiều loại phần tử Web như: DropDownList, CheckBoxList, RadioList, DataGrid, v.v.; kể cả với các phần tử Web không có thuộc tính định danh (id) và các giao diện pop-up. Phần còn lại của luận văn được cấu trúc như sau. Chương 2 trình bày về phương pháp đặc tả giao diện cho các ứng dụng Web như là một ôtômát hữu hạn trạng thái và được biểu diễn dưới dạng các tệp tin MS Excel. Ở chương 3, luận văn này trình bày phương pháp sinh tự động các ca kiểm thử từ ôtômát hữu hạn trạng thái và thực thi chúng trên trên ứng dụng Web. Tiếp đến, chương 4 trình bày công cụ và kết quả thực nghiệm. Cuối cùng, kết luận của luận văn và định hướng nghiên cứu tiếp theo được trình bày trong chương 5. 10 Chương 2: Phương pháp đặc tả tương tác giao diện cho các ứng dụng Web Để áp dụng phương pháp kiểm thử dựa trên mô hình, chúng ta cần xây dựng mô hình đặc tả chính xác hành vi của hệ thống cần kiểm thử. Mô hình là một sự biểu đồ hóa, mô tả chi tiết hệ thống, đồng thời mô tả chi tiết các khía cạnh, các đặc tính của hệ thống. Mô hình cần phải đủ chi tiết để giúp ta hiểu và đoán nhận được hành vi của hệ thống. Có nhiều phương pháp đặc tả mô hình như: máy hữu hạn trạng thái, ôtômát trạng thái, máy trạng thái UML, chuỗi Markov, văn phạm, bảng quyết định, v.v. [1]. Phụ thuộc vào phương pháp và công cụ kiểm thử, chúng ta sẽ lựa chọn phương pháp đặc tả hệ thống tương ứng. Trong chương 2, chúng tôi chỉ trình bày một phương pháp đặc tả tương tác giao diện ứng dụng Web được sử dụng cho nghiên cứu này. 2.1 Đặc tả tương tác giao diện của từng trang Web bằng ôtômát hữu hạn trạng thái Theo quy trình kiểm thử dựa trên mô hình [1] thì việc đầu tiên chúng ta phải làm trong số các hoạt động kiểm thử tự động ứng dụng Web đó là xây dựng mô hình đặc tả hành vi của ứng dụng Web. Có nhiều hành vi có thể được sử dụng để đặc tả nhưng trong luận văn này, chỉ đề cập đến hành vi tương tác của người dùng đối với hệ thống ứng dụng Web, thông qua sự thay đổi trạng thái (hay sự thay đổi giao diện) của ứng dụng Web [5]. Chúng tôi dùng ôtômát trạng thái làm phương pháp đặc tả hình thức giao diện ứng dụng Web. Khi đó, mỗi giao diện người dùng của một trang Web, tại một thời điểm được mô hình hóa như là một trạng thái. Mỗi yêu cầu của người dùng được mô hình hóa như là một hành động tạo ra hàm chuyển trạng thái. Vậy, để mô hình hóa các hành vi tương tác giao diện người dùng ứng dụng Web như là một ôtômát trạng thái, chúng tôi cần thực hiện các bước sau: (1) Chia nhỏ hệ thống thành các mô-đun; (2) với mỗi mô-đun chúng ta cần xác định các giao diện người dùng; (3) với mỗi giao diện người dùng được đặc tả bằng một ôtômát trạng thái; (4) nối các ôtômát trạng thái đó lại thành một bản đặc tả hoàn chỉnh cho cả hệ thống. Phương pháp coi mỗi giao diện người dùng là một trang Web và được biểu diễn bằng một ôtômát trạng thái như định nghĩa 2.1 [5]. Định nghĩa 2.1: Hành vi tương tác giao diện của một trang Web được đặc tả bằng ôtômát trạng thái (Finite State Automaton - FSA) M = < S, s0, ∑, δ, F >, trong đó: 11 - S là tập ập hữu hạn khác rỗng các trạng thái của trang Web, s0 S là trạng ạng thái đầu tiên ti được tải lên của ủa trang Web, ∑ ứng với tập sự kiện có dạng [điều kiện]sự kiện, δ là hàm chuyển chuy trạng thái: δ: S × ∑→ S, và là tập ập các trạng thái kết thúc, ttương ứng với các giao diện di xuất hiện cuối cùng ùng sau một m chuỗi các sự kiện liên tiếp. Chú ý 2.1: Dạng <[điều ều kiện]sự kiện> kiện có nghĩa là ch chỉ xảy ra khi <điều kiện> được ợc thỏa mãn. m Ôtômát hữu hạn trạng ạng thái rỗng, ký hiệu llà M = ∏ là ôtômát hữu hạn trạng thái và có tập các trạng thái S = ∅ [5]. Sau đây là một ột số khái niệm căn bản giúp chúng ta đặc tả một trang Web như là một ôtômát hữu ữu hạn trạng thái. Phần ần tử Web (Web Element). Phần tử Web là các thành phần ần cơ c bản cấu tạo nên một trang Web. Mỗi ỗi phần tử Web có nhiều thành phần nhưng ưng để đặc tả một trang Web chúng ta cần ần mô tả một số các thành phần cơ bản như: th thẻ mở để khai báo bắt ắt đầu một phần tử Web; các thuộc tính, tính trong đó thuộc tính id, class, name thường được ợc sử dụng để xác định vị trí của phần tử Web ttrên rên trang Web; nội n dung của ủa phần tử Web th thường được ợc sử dụng để xác định trạng thái của phần tử Web và thẻẻ đóng nằm ở vị trí cuối ccùng của phần tử Web. Trạng thái trang Web. Trạng thái trang Web là giao diện ện của trang Web tại một ột thời điểm, mỗi trạng thái Web llà một ột tập hợp các trạng thái của từng phần tử trong một trang Web. Ví dụ 2.1: Ví dụ ụ về trạng thái trang Web tìm kiếm ếm thông tin cán bộ bộ. Giao diện trong hình 2.1 là một trạng ạng thái của trang We Web (trạng thái index).. Sau khi ngư người dùng nhập thông tin tìm ìm kiếm ki vào các ô tìm kiếm ếm (phần tử Web textbox hoặc dropdownlist) thì hệệ thống sẽ chuyển từ trạng thái bắt đầu sang trạng thái tiếp theo, như trong hình 2.2 là trạng thái người dùng đã nhập họ tên ên ccần tìm kiếm (trạng thái TEN). 12 Hình 2.1. Trạng thái bắt đầu của trang tìm kiếm cán bộ Hình 2.2. Trạng thái đã nhập họ tên tìm kiếm Sự kiện. Sự kiện bao gồm các hành động (action) tác động lên các phần tử Web tại một thời điểm, làm thay đổi trạng thái của trang Web đó. Có nhiều sự kiện tương tác người dùng trên giao diện Web, trong đó có 4 sự kiện chính được chúng tôi sử dụng để đặc tả hành vi Web như sau: sự kiện addtext dùng để nhập một đoạn ký tự vào ô textbox, sự kiện deltext dùng để xóa đoạn ký tự ở ô textbox, sự kiện click là sự kiện nhấp chuột vào một nút (button) hoặc một đường dẫn, sự kiện select dùng để chọn một hoặc nhiều, được sử dụng cho các phần tử combobox, checkbox, listbox, dropdown list, radio list. Như trong ví dụ 13 2.1 chúng ta thấy có một sự kiện người dùng nhập thông tin tìm kiếm (addtext) lên ô tìm kiếm theo họ tên cán bộ (ô textbox). Ví dụ 2.2: Ví dụ minh họa về đặc tả hình thức tương tác giao diện của trang Web tìm kiếm cán bộ và trang cập nhật thông tin cán bộ bằng ôtômát hữu hạn trạng thái. Hình 2.1 trên là giao diện đầu tiên được tải lên của trang Web tìm kiếm thông tin cán bộ. Giao diện này gồm 2 phần chính: phần thứ nhất là các chỉ tiêu tìm kiếm, phần thứ hai là kết quả tìm kiếm. Để xây dựng được mô hình cho trang Web này, chúng ta cần xác định chính xác các trạng thái và sự kiện của nó. Các trạng thái của trang tìm kiếm cán bộ (bảng 2.1) được xác định dựa trên các trạng thái của các phần tử Web sau: tiêu đề trang Web (Lable), ô nhập họ tên (TextBox) và ô nhập số hiệu (TextBox), ô chọn đơn vị (DropDownList), Nút tìm kiếm (Button) và Bảng kết quả tìm kiếm (DataGrid). Bảng 2.1. Các trạng thái Web của trang tìm kiếm cán bộ Stt 1 2 3 4 5 6 7 8 9 Tên trạng thái Index TEN SOHIEU DONVI TEN+SO TEN+DONVI SO+DONVI TEN+SO+DON KETQUA_TK Ý nghĩa Trạng thái ban đầu của trang Web Khi người dùng nhập họ tên cán bộ cần tìm Khi người dùng nhập số hiệu Khi người dùng chọn đơn vị Khi người dùng nhập cả tên và số hiệu Khi người dùng nhập tên và chọn đơn vị Khi người dùng nhập số hiệu và chọn đơn vị Khi người dùng chọn cả 3 chỉ tiêu tìm kiếm Trạng thái trang Web khi trả về kết quả tìm kiếm, cũng là trạng thái kết thúc của trang Web Các sự kiện người dùng tương tác lên trang Web tìm kiếm cán bộ như bảng 2.2 Bảng 2.2. Các sự kiện của trang tìm kiếm cán bộ Stt 1 2 3 4 5 Tên sự kiện add_hoten del_hoten add_sohieu del_sohieu sel_donvi Ý nghĩa Nhập họ tên tìm kiếm Xóa họ tên tìm kiếm Nhập số hiệu Xóa số hiệu Chọn đơn vị 14 6 7 del_donvi Timkiem Không chọn đơn vị Chọn tìm kiếm Trang tìm kiếm cán bộ được đặc tả bằng ôtômát hữu hạn trạng thái M1 = < S1, s01, ∑1, δ1, F1 > (hình 2.3), dựa trên tập trạng thái và tập sự kiện đã được nêu trên. Hình 2.3. Ôtômát hữu hạn trạng thái M1 Trong đó: S1= {index, TEN, SOHIEU, DONVI, TEN+SO, TEN+DONVI, SO+DONVI, TEN+SO+DONVI, KETQUA_TK} là tập các trạng thái của trang tìm kiếm cán bộ. s01=index là trạng thái bắt đầu của trang Web. ∑1= {add_hoten, del_hoten, add_sohieu, del_sohieu, sel_donvi, del_donvi, Timkiem} là tập các sự kiện. Hàm chuyển trạng thái δ1 gồm các đường chuyển trạng thái như trong hình 2.3. F1 = {KETQUA_TK} là tập các trạng thái kết thúc. Sau khi người dùng tìm kiếm cán bộ thành công. Giao diện của trang Web tìm kiếm (search) sẽ chuyển sang trạng thái kết quả tìm kiếm (KETQUA_TK). 15 Hình 2.4. Kết quả tìm kiếm cán bộ và nút sửa thông tin cán bộ Từ trạng thái này, người dùng lựa chọn nút sửa trên bản ghi kết quả cần sửa (như hình 2.4), thì trang Web tìm kiếm sẽ chuyển sang giao diện của trang Cập nhật thông tin cán bộ (trang update) như hình 2.5. Hình 2.5. Giao diện trang Web cập nhật thông tin cán bộ (update) Trang update được đặc tả bằng ôtômát hữu hạn trạng thái M2 = < S2, s02, ∑2, δ2, F2 > như trong hình 2.6. Tại giao diện của trang Web (CAPNHAT_TTCB), khi người dùng thực hiện thay đổi một số thông tin liên 16 quan đến cán bộ cần cập nhật (thực hiện sự kiện do_Something), hệ thống sẽ chuyển sang trạng thái TT_CAPNHAT. Tại trạng thái TT_CAPNHAT người dùng thực hiện sự kiện (capnhat) bằng cách chọn nút Cập nhật, hệ thống sẽ chuyển tới trạng thái cập nhật thành công (CN_THANHCONG). Hình 2.6. Ôtômát hữu hạn trạng M2 Trong M2 có: S2= {KETQUA_TK, CAPNHAT_TTCB, TT_CAPNHAT, CN_THANHCONG} là tập các trạng thái của trang cập nhật thông tin cán bộ. Trạng thái KETQUA_TK là trạng thái của trang Web như hình 2.4, trạng thái CAPNHAT_TTCB là giao diện của trang cập nhật thông tin cán bộ như hình 2.5, trạng thái TT_CAPNHAT là trạng thái khi người dùng chỉnh sửa một số thông tin của cán bộ, trạng thái CN_THANHCONG là trạng thái trang Web sau khi người dùng chọn nút Cập nhật. s02= KETQUA_TK là trạng thái bắt đầu của trang Web. ∑2= {sel_sua, do_Something, capnhat } là tập các sự kiện. Sự kiện sel_sua là sự kiện người dùng chọn nút sửa trên danh sách cán bộ, sự kiện do_something là sự kiện người dùng thực hiện sửa thông tin cán bộ, sự kiện capnhat là sự kiện người dùng chọn nút cập nhật để lưu thông tin chỉnh sửa. Hàm chuyển trạng thái δ2 gồm các đường chuyển trạng thái như trong hình 2.6. F1 = { CN_THANHCONG } là tập các trạng thái kết thúc. 2.2 Xây dựng mô hình đặc tả tương tác giao diện cho toàn bộ ứng dụng Web Các hệ thống ứng dụng Web ngày càng lớn và phức tạp. Vì vậy, việc xây dựng mô hình đặc tả cho toàn bộ ứng dụng Web là một công việc rất vất vả. Người xây dựng mô hình rất dễ mắc sai lầm khi xây dựng một mô hình quá lớn 17 như vậy. Trong giới ới hạn của luận văn n này, một ứng dụng Web đư được đặc tả hình thức bằng ằng cách xây dựng ôtômát hữu hạn trạng thái cho từng ừng trang Web nhỏ, sau đó ghép nối lần lượt ợt từng ôtômát hữu ữu hạn trạng thái nhỏ lại với nhau thành một ôtômát hữu ữu hạn trạng thái lớn cho cả ứng dụng Web. Trang Web mốc. M Một trang Web Mi = < Si, s0i, ∑i, δi, Fi > được gọi là trang Web mốc, nếu ếu trang Web đ được dùng làm mốc ốc để các trang Web khác ghép nối vào, hay nó là trang Web kh khởi đầu của ứng dụng Web. M = < S, s0, ∑, δ, F > là trang Web sau khi ghép nối, n với s0= s0i. Mô hình của toàn àn b bộ ứng dụng Web được ợc xây dựng bằng cách ghép nối mô hình của ủa tất cả các trang Web lại với nhau bằng ằng phép toán ghép nối được đ định nghĩa [5] như sau: Định nghĩa 2.2: Giảả sử M1 = < S1, s01, ∑1, δ1, F1 > và M2 = < S2, s02, ∑2, δ2, F2 > lần lượt là các ôtômát hữu ữu hạn trạng thái của 2 trang Web. Phép ghép nối của M1 và M2 là ôtômát M = < S, s0, ∑, δ, F >, kí hiệu là M = M1║M2 (M1 là trang Web mốc). Nếu M1 = ∏, M2 = ∏, hoặc s01  F2 và s02  F1 thì M = M1║M2 = ∏. Các trường ờng hợp khác M = M1║M2, với S = S1 S2, ∑ = ∑1 ∑2, δ = δ1 δ2 và F = F1 F2 và các trạng tr thái bắt đầu được ợc xác định theo quy tắc: - Nếu s01  F2 và s02  F1 thì M   , - Nếu s02 F1 thì M1 được đặt làm trang Web mốc và s0 = s01. - Các trường ờng hợp còn c lại thì s0 = s02. Chú ý 2.2: M =∏ làà ký hi hiệu ệu ôtômát hữu hạn trạng thái rỗng, tức nó có tập các trạng thái là rỗng. Ví dụ 2.3: Đểể minh họa cụ thể cho phép p toán ghép nối, chúng ta ti tiến hành ghép nối hai ôtômát hữu ữu hạn trạng thái của trang tìm kiếm cán bộ (search search) và trang cập ập nhật thông tin cán bộ (update), như ở ví dụ 2.2 lại thành ôtômát hữu hạn trạng thái M = M1 ║M2 = < S, s0, ∑, δ, F >, trong đó: M1 = < S1, s01, ∑1, δ1, F1 > với S1= {index, index, TEN, SOHIEU, DONVI, TEN+SO, TEN+DONVI, SO+DONVI, TEN+SO+DONVI, KETQUA_TK}; KETQUA_TK s01 = index ; F1 = { KETQUA_TK } là mô hình ccủa trang search. M2 = < S2, s02, ∑2, δ2, F2 > với S2= {KETQUA_TK, KETQUA_TK, CAPNHAT_TTCB, TT_CAPNHAT, CN_THANHCONG CN_THANHCONG}, s02 = KETQUA_TK KETQUA_TK; F2 = {CN_THANHCONG } là mô hình của c trang update. Thuật ật toán thực hiện các b bước sau: 18 - Thuật ật toán tiến h hành kiểm tra xem s01 F2 và s02 F1 hay không? Kết ết quả cho thấy s02 = KETQUA_TK F1 suy ra s0 = s01 = index - Tập trạng ạng thái kết thúc F = F1 F2 ={ KETQUA_TK, CN_THANHCONG } và S = S1 S2={ index, TEN, SOHIEU, DONVI, TEN+SO, TEN+DONVI, SO+DONVI, TEN+SO+DONVI, KETQUA_TK KETQUA_TK, CAPNHAT_TTCB, TT_CAPNHAT, CN_THANHCONG }, ∑ = ∑1 ∑2, δ = δ1 δ2 . del_sohieu sel _d TEN+SO sel_donvi m TEN+SO+DONVI vi on _d n do l_ vi d_h ote n l se de del_sohieu Tim kie m del_d on vi de l_h ote n Timkiem sel_d on vi DONVI m kie Tim _so hie u ad SOHIEU KETQUA_TK add on vi eu hi so l_ de Timkiem de ad l _so d_s hie oh u ieu iem Timk index TEN+DONVI T im kie m de l_h Tim kie Ti m kie m ote n del_donvi i nv do l_ de ad d_h ote n add_sohieu TEN SO+DONVI add_sohieu sel_sua KETQUA_TK CAPNHAT_TTCB do_S omet hin g TT_CAPNHAT TT capnhat CN_THANHCONG THANHCONG Hình 2.7. Mô hình M sau khi thực ực hiện thuật toán ghép nối giữa M1 và M2 Ta có M1 = < S1, s01, ∑1, δ1, F1 >, M2 = < S_2, s02, ∑2, δ2, F2 >,..., Mn = < Sn, s0n, ∑n, δn, Fn > lần lư ượt là các ôtômát hữu hạn của n trang Web với v M1 là trang Web mốc. Đầu tiên, ên, M1 ghép nối với Mi (2 <= i <= n) thành M1i, thuật j) Thuật toán toán sau đó sẽ tiến hành ành ghép n nối M1i với Mj (2 <= j <= n và i ≠ j). ghép nối ối kết thúc sau khi duyệt qua tất cả các ôtômát hữu ữu hạn trạng thái. Nhận xét: Phép ghép nối ối nh như định nghĩa trên có tính kết ết hợp nh nhưng không có tính giao hoán [5]. 19 2.3 Biểu diễn mô hình đặc tả dưới dạng các tệp tin MS Excel Phần này, chúng tôi sẽ trình bày cụ thể về cách biểu diễn các ôtômát hữu hạn trạng thái dưới dạng bảng chuyển trạng thái và được lưu bằng các tệp tin Excel. Mỗi tệp tin Excel tương ứng với một ôtômát hữu hạn trạng thái đặc tả cho một trang Web. Trong một tệp tin Excel có 4 phần: Phần 1 là bảng Element_html, mô tả các phần tử Web của trang Web. Phần 2 là bảng State, mô tả các trạng thái, mỗi trạng thái là tập hợp tất cả các trạng thái của các phần tử Web trong bảng Element_html. Phần 3 là bảng Event, mô tả các sự kiện, mỗi sự kiện là một hành vi tương tác của người dùng lên một phần tử Web. Phần 4 là bảng Transition, mô tả các hàm chuyển trạng thái giữa các trạng thái trong bảng State. Mỗi bảng đều gồm nhiều dòng, dòng đầu tiên chứa số các phần tử của bảng (giá trị này được ghi ở ô đầu tiên), dòng tiếp theo là tên các cột và các dòng sau đó là các phần tử của bảng. Sau đây, chúng tôi sẽ mô tả chi tiết từng bảng trong tệp tin Excel của trang tìm kiếm cán bộ (search Excel). Bảng Element_html (bảng các phần tử Web): Bảng này được thiết kế để đặc tả các phần tử Web của trang Web cần kiểm thử. Bảng 2.3. Bảng các phần tử Web của trang tìm kiếm cán bộ. 7 id html type Value Danh sách cán bộ chiến sỹ công 0 Labtitle texthtml an Hà Nội 1 txtHoTen textbox Son 2 txtSoHieu textbox 535 3 ddlDonVi dropdown quận Cầu Giấy, TP. Hà Nội 4 btnTimkiem btn 5 id:grdCBCS|tag:tr|head:1|end:1|1 grid Son 6 id:grdCBCS|tag:tr|head:1|end:1|1 grid 535 Bảng 2.3 là bảng mô tả các phần tử Web của trang tìm kiếm cán bộ. Cấu trúc của bảng này gồm có 4 cột chính: cột id, html, type và value. Mỗi cột của bảng mang ý nghĩa sau: - Cột id: là cột định danh phần tử Web, được đánh số thứ tự tăng dần.