Tài liệu Kiểm chứng giao diện phần mềm bằng phƣơng pháp mô hình hóa event – b.

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƢỜNG ĐẠI HỌC CÔNG NGHỆ NGUYỄN XUÂN TRƢỜNG KIỂM CHỨNG GIAO DIỆN PHẦN MỀM BẰNG PHƢƠNG PHÁP MÔ HÌNH HÓA EVENT – B LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN HÀ NỘI, 2016 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƢỜNG ĐẠI HỌC CÔNG NGHỆ NGUYỄN XUÂN TRƢỜNG KIỂM CHỨNG GIAO DIỆN PHẦN MỀM BẰNG PHƢƠNG PHÁP MÔ HÌNH HÓA EVENT – B 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 TRƢƠNG NINH THUẬN HÀ NỘI, 2016 LỜI CAM ĐOAN Tôi xin cam đoan toàn bộ nội dung bản luận văn là do tôi tìm hiểu, nghiên cứu, tham khảo và tổng hợp từ các nguồn tài liệu khác nhau và làm theo hướng dẫn của người hướng dẫn khoa học. Các nguồn tài liệu tham khảo, tổng hợp đều có nguồn gốc rõ ràng và trích dẫn theo đúng quy định. Tôi xin chịu hoàn toàn trách nhiệm về lời cam đoan của mình. Nếu có điều gì sai trái, tôi xin chịu mọi hình thức kỷ luật theo quy định. Hà Nội, tháng 06 năm 2016 Ngƣời cam đoan Nguyễn Xuân Trường LỜI CẢM ƠN Em xin gửi lời cảm ơn chân thành đến các thầy, các cô 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 dạy dỗ, truyền đạt cho chúng em nhiều kiến thức, kinh nghiệm quý báu trong suốt quá thời gian học tập tại trường. Em xin gửi lời cảm ơn sâu sắc tới thầy PGS.TS Trương Ninh Thuận – Phó chủ nhiệm khoa công nghệ thông tin – Trường Đại học Công nghệ – ĐHQGHN đã tận tình chỉ bảo, hướng dẫn, định hướng cho em để em hoàn thành luận văn tốt nghiệp này. Cuối cùng em xin cảm ơn gia đình, bạn bè, đồng nghiệp đã luôn động viên ủng hộ và tạo mọi điều kiện tốt nhất trong suốt quá trình học tập và hoàn thành luận văn này. Với việc tìm hiểu và nghiên cứu về lĩnh vực, công cụ còn tương đối mới mẻ cùng với kiến thức còn nhiều hạn chế, nên không tránh khỏi những thiếu sót. Em rất mong nhận được những ý kiến đóng góp quý báu của thầy cô và các bạn để luận văn được hoàn thiện hơn. Hà Nội, tháng 06 năm 2016 Học viên Nguyễn Xuân Trường 1 MỤC LỤC MỤC LỤC ............................................................................................................ 1 DANH MỤC KÝ HIỆU VÀ CHỮ VIẾT TẮT ................................................. 3 DANH MỤC CÁC BẢNG .................................................................................. 4 DANH MỤC CÁC HÌNH VẼ............................................................................. 5 Chƣơng 1. GIỚI THIỆU..................................................................................... 7 1.1. Sự cần thiết của đề tài ............................................................................... 7 1.2. Nội dung nghiên cứu ................................................................................ 9 1.3. Đóng góp của đề tài .................................................................................. 9 1.4. Cấu trúc của luận văn ............................................................................... 9 Chƣơng 2. TỔNG QUAN VỀ KIỂM CHỨNG GIAO DIỆN PHẦN MỀM VÀ PHƢƠNG PHÁP MÔ HÌNH HÓA EVENT-B........................................ 11 2.1. Giao diện người dùng ............................................................................. 11 2.2. Các phương pháp kiểm chứng giao diện ................................................ 12 2.2.1. Phương pháp tĩnh ............................................................................. 14 2.2.2. Phương pháp động............................................................................ 14 2.3. Tổng quan về Event-B ............................................................................ 16 2.3.1 Context .................................................................................................... 17 2.3.2 Machine .................................................................................................. 18 2.3.3 Ký hiệu toán học trong Event-B ............................................................. 21 2.3.4 Tinh chỉnh ............................................................................................... 22 2.3.5 Mệnh đề chứng minh .............................................................................. 23 2.3.6 Công cụ Rodin ........................................................................................ 24 2 Chƣơng 3. KIỂM CHỨNG GIAO DIỆN PHẦN MỀM BẰNG PHƢƠNG PHÁP MÔ HÌNH HÓA EVENT-B ................................................................. 27 3.1. Phương pháp chung ................................................................................ 27 3.2. Phương pháp chi tiết ............................................................................... 28 3.3. Mô hình hóa giao diện phần mềm .......................................................... 31 3.4. Mệnh đề chứng minh .............................................................................. 32 Chƣơng 4. ÁP DỤNG PHƢƠNG PHÁP KIỂM CHỨNG GIAO DIỆN ỨNG DỤNG TRÊN THIẾT BỊ DI ĐỘNG VỚI EVENT-B .................................... 34 4.1. Tổng quan về các ứng dụng trên điện thoại di động .............................. 34 4.1.1. Các thành phần cơ bản của một ứng dụng Android ........................ 35 4.1.2. Cơ chế quản lý các Activity ............................................................ 35 4.2. Ứng dụng Note ....................................................................................... 38 4.2.1. Giới thiệu chung ............................................................................... 38 4.2.2 Ứng dụng Note ................................................................................. 38 4.3. Mô hình hóa và kiểm chứng giao diện ứng dụng Note .......................... 44 KẾT LUẬN VÀ HƢỚNG PHÁT TRIỂN ....................................................... 56 Kết luận ............................................................................................................ 56 Hướng phát triển .............................................................................................. 57 PHỤ LỤC ........................................................................................................... 58 A. Đặc tả context Note_C của ứng dụng Note ............................................ 58 B. Đặc tả machine Note_M của ứng dụng Note ......................................... 58 TÀI LIỆU THAM KHẢO ................................................................................ 62 3 DANH MỤC KÝ HIỆU VÀ CHỮ VIẾT TẮT IDE Integrated Development Environment GUI Graphical User Interface POS Proof Obligations INV Invariant DLF Deadlock Freeness VAR Variant WD well-definedness 4 DANH MỤC CÁC BẢNG Bảng 2.1 Các phép toán logic ......................................................................... 21 Bảng 2.2 Luật chứng minh INV với sự kiện evt ............................................. 24 Bảng 3.1 Chuyển đổi từ GUI tới Event-B....................................................... 32 Bảng 4.1 Bảng CSDL ghi chú Note ................................................................ 38 Bảng 4.2 Mô tả cửa sổ giao diện MainActivity .............................................. 39 Bảng 4.3 Mô tả sơ bộ các đối tượng của cửa sổ giao diện CreateActivity ..... 40 Bảng 4.4 Mô tả sơ bộ các đối tượng của cửa sổ giao diện EditActivity ......... 41 Bảng 4.5 Mô tả sơ bộ các đối tượng của cửa sổ giao diện ViewActivity....... 43 5 DANH MỤC CÁC HÌNH VẼ Hình 2.1 Giao diện đồ họa người dùng ................................................ 11 Hình 2.2 Giao diện dòng lệnh .............................................................. 12 Hình 2.3 Cấu trúc và mối quan hệ của các thành phần mô hình trong EventB ................................................................................................................. 17 Hình 2.4 Cấu trúc context..................................................................... 18 Hình 2.5 Ví dụ về context trong Event-B ............................................ 18 Hình 2.6 Cấu trúc machine trong Event-B ........................................... 20 Hình 2.7 Cấu trúc của Event trong Event-B ........................................ 20 Hình 2.8 Ví dụ machine trong Event-B ............................................... 20 Hình 2.9 Ví dụ Event trong Event-B .................................................... 21 Hình 2.10 Ví dụ về mối quan hệ Refinement trong Event-B................. 22 Hình 2.11 Sơ đồ định nghĩa sự kiện ....................................................... 23 Hình 2.12 Định nghĩa sự kiện evt .......................................................... 24 Hình 2.13 Giao diện đồ họa của công cụ Rodin .................................... 25 Hình 2.14 Symbols View ....................................................................... 36 Hình 2.15 Event-B Explorer................................................................... 36 Hình 2.16 Menu bar................................................................................ 36 Hình 3.1 Quy trình kiểm chứng tổng quát ........................................... 27 Hình 3.2 Quy trình kiểm chứng chi tiết ............................................... 30 Hình 4.1 Cơ chế Back Stack ................................................................ 36 Hình 4.2 Activity State ......................................................................... 37 Hình 4.3 MainActivity.XML ............................................................... 40 Hình 4.4 CreateActivit.XML ............................................................... 41 Hình 4.5 EditActivit.XML ................................................................... 42 Hình 4.6 ViewActivity.XML ............................................................... 43 Hình 4.7 Quy trình xây dựng Activity Diagram .................................. 44 Hình 4.8 Sơ đồ Activity Diagram ........................................................ 45 6 Hình 4.9 Quá trình mô hình hóa từ đặc tả vào trong Event-B ............. 46 Hình 4.10 Context Note_C ..................................................................... 47 Hình 4.11 Một phần của machine Note_M ............................................ 49 Hình 4.12 Event thoát ứng dụng ............................................................ 50 Hình 4.13 Event chọn chức năng Create ................................................ 50 Hình 4.14 Event chọn chức năng Edit.................................................... 50 Hình 4.15 Event chọn chức năng View.................................................. 51 Hình 4.16 Event chọn chức năng Delete ................................................ 51 Hình 4.17 Các Event trên các đối tượng của các cửa sổ ........................ 51 Hình 4.18 Cửa sổ sinh kiểm chứng tự động ........................................... 53 Hình 4.19 Bảng kết quả Statistics .......................................................... 53 Hình 4.20 Thông báo mệnh đề chưa chứng minh được tự động............ 54 Hình 4.21 Cửa sổ Goal ........................................................................... 54 Hình 4.22 Cửa sổ Statistics trong trường hợp lỗi................................... 55 Hình 4.23 Cửa sổ Statistics trong trường hợp lỗi................................... 55 7 Chƣơng 1. GIỚI THIỆU 1.1. Sự cần thiết của đề tài Ngày nay phần mềm có mặt trong hầu hết các lĩnh vực: Giáo dục, truyền thông, ngân hàng, sản xuất chế tạo, quản trị, y tế, khoa học kỹ thuật, hàng không vũ trụ, giải trí, … Giúp con người giải quyết hầu hết các công việc và dần thay thế con người. Đại đa số phần mềm hiện nay được xây dựng với một giao diện đồ họa người dùng Graphical User Interface (GUI) thân thiện và người sử dụng chỉ việc tương tác với giao diện của phần mềm. Việc phát triển phần mềm dần hướng tới đưa ra sản phẩm có giao diện dễ sử dụng, có tính thẩm mỹ cao và đảm bảo được các chức năng cần thiết. Tuy nhiên không phải lúc nào các GUI của phần mềm khi được xây dựng điều đảm bảo được tính dễ dùng, bố cục hợp lý, các chức năng hoạt động một cách chính xác như mong muốn. Lỗi phần mềm chủ yếu xuất hiện trong quá trình tương tác như: Các phần tử trên GUI hiển thị bất thường khó quan sát và thao tác, các chức năng thực hiện không như dự định, các thông báo hiển thị sai, thứ tự xuất hiện của các cửa sổ không chính xác,…, dẫn tới thực hiện sai, gây mất mát dữ liệu, gây mất an toàn thiệt hại về kinh tế và có thể nguy hại tới tính mạng của người sử dụng,... Vì vậy, Cần phải thực hiện kiểm thử giao diện phần mềm để kiểm tra các chức năng, sự nhất quán, khả năng tầm nhìn, khả năng tương thích đảm bảo phù hợp với các thông số trong đặc tả thiết kế, phát hiện lỗi và sửa chữa kịp thời hoặc bất cứ vấn đề bất thường nào có thể có của giao diện là vô cùng quan trọng và là một thách thức lớn trong quá trình xây dựng phần mềm. Kiểm chứng giao diện phần mềm là một quy trình gồm nhiều công việc khác nhau trên nhiều đối tượng của giao diện. Trong đó việc kiểm chứng thứ tự hiển thị của các cửa sổ giao diện là một yếu tố quan trọng và cần thiết, có thể thấy người sử dụng làm việc với phần mềm chủ yếu thông qua các cửa sổ giao diện qua đó người dùng có thể giao tiếp, tương tác, trao đổi nhập xuất thông tin với phần mềm. Từ một chức năng trong cửa sổ này có thể gọi tới một hoặc nhiều 8 cửa sổ khác, tại mỗi một thời điểm chỉ có một cửa sổ được làm việc. Các trạng thái và thứ tự xuất hiện của các giao diện cần đảm bảo chính xác với lời gọi tới nó. Khi cửa sổ hiển thị không đúng với thứ tự ứng chức năng định sẵn sẽ đưa tới người dùng những thông tin và hành động sai điều này gây ra những hậu quả khó lường. Từ trước tới nay có nhiều phương pháp kiểm chứng, kiểm thử được áp dụng để kiểm chứng, kiểm thử các bản đặc tả thiết kế giao diện phần mềm như kiểm chứng tĩnh, kiểm chứng động, kiểm thử hộp đen,.... Tuy nhiên mỗi phương pháp lại bộc lộ những ưu và nhược điểm riêng. Với kiểm chứng tĩnh lại phụ thuộc chủ yếu vào kiến thức với kinh nghiệm khả năng phân tích của người kiểm thử và thường tốn nhiều thời gian. Trong khi đó kiểm chứng động thì lại được áp dụng trong quá trình thực hiện của phần mềm và sử dụng các kỹ thuật kiểm thử tùy theo cấp độ như kiểm thử modul hay kiểm thử đơn vị, phương pháp này tốt cho việc tìm lỗi nhưng lại đòi hỏi thực hiện chương trình tức là việc kiểm chứng chỉ thực hiện sau khi đã có mã nguồn. Phương pháp Event-B là một phương pháp mô hình hóa cho phép mô hình hóa các thành phần, đối tượng của hệ thống phần mềm dựa trên các ký hiệu toán học, logic mệnh đề và lý thuyết tập hợp kết hợp với công cụ mã nguồn mở Rodin cho phép sinh và kiểm chứng một cách tự động. Nhận thấy được tầm quan trọng của việc kiểm chứng giao diện người dùng của phần mềm mà cụ thể là kiểm chứng thứ tự xuất hiện của các cửa sổ giao diện cùng với ưu điểm của phương pháp Event-B và công cụ Rodin, nên tác giả đã mạnh dạn đề xuất đề tài “Kiểm chứng giao diện phần mềm bằng phƣơng pháp mô hình hóa Event – B” nhằm nghiên cứu phương pháp kiểm chứng giao diện chung và tập trung vào xây dựng phương pháp kiểm chứng thứ tự xuất hiện của các cửa sổ giao diện phần mềm cho các ứng dụng trên thiết bị di động. 9 1.2. Nội dung nghiên cứu Đề tài tập trung vào việc nghiên cứu đặc điểm của giao diện phần mềm, các vấn đề liên quan tới kiểm chứng giao diện phần mềm, các phương pháp kiểm chứng giao diện. Nghiên cứu mô hình, cấu trúc, ký pháp của phương pháp mô hình hóa Event-B. Tìm hiểu nguyên lý, chức năng của công cụ Rodin. Từ những nghiên cứu có được xây dựng một phương pháp mô hình hóa và kiểm chứng chung, xây dựng phương pháp kiểm chứng thứ tự xuất hiện của các cửa sổ giao diện người dùng của các ứng dụng di động, toàn bộ quá trình nghiên cứu được triển khai gồm các công việc: xây dựng quy trình thực hiện tổng quát, xây dựng quy trình chi tiết, xây dựng các mô hình giao diện trừu tượng tổng quát thông qua các định nghĩa, xây dựng các bộ quy tắc chuyển đổi tham chiếu tương ứng từ mô hình trừu tượng vào trong Event-B. Áp dụng vào kiểm chứng tự động thứ tự thực hiện của các cửa sổ giao diện của ứng dụng tạo ghi chú Note chạy trên hệ điều hành Android của thiết bị di động. 1.3. Đóng góp của đề tài Nghiên cứu đề xuất phương pháp để kiểm chứng giao diện người dùng phần mềm ở giai đoạn thiết kế bằng phương pháp mô hình hóa Event-B, đó chính là kiểm chứng sự tuân thủ về thứ tự của các cửa sổ giao diện, giúp các nhà phát triển có thể phát hiện và tránh các lỗi không mong muốn của giao diện hoặc những giả thiết không hợp lý của bản đặc tả thiết kế của giao diện trong quá trình xây dựng phần mềm trước khi cài đặt. 1.4. Cấu trúc của luận văn Phần nội dung của luận văn được cấu trúc thành 4 chương chính như sau: Chƣơng 1. Giới thiệu Giới thiệu về các yêu cầu khách quan, chủ quan, cơ sở khoa học, thực tiễn nghiên cứu và xây dựng đề tài. 10 Chƣơng 2. Tổng quan về kiểm chứng giao diện phần mềm và Phƣơng pháp mô hình hóa Event-B Giới thiệu một cách chi tiết về giao diện phần mềm cũng như các vấn đề về kiểm chứng giao diện phần mềm, các phương pháp kiểm chứng giao diện. Bao gồm những kiến thức tổng quan về phương pháp mô hình hóa Event-B, mô tả cấu trúc của mô hình, các thành phần, giải thích ý nghĩa của các thành phần, cấu trúc của mệnh đề chứng minh và phân loại. Nêu rõ tập các ký hiệu toán học trong cú pháp của mô hình. Trình bày cách sử dụng và kiểm chứng tự động với công cụ Rodin. Chƣơng 3: Kiểm chứng giao diện phần mềm bằng phƣơng pháp Event-B Tập trung vào việc xây dựng quy trình kiểm chứng tổng quát và chi tiết cho các giao diện ứng dụng như: xây dựng quy trình thực hiện, xây dựng mô hình chung trên các định nghĩa, xây dựng quy trình chi tiết, đưa ra các luật chuyển đổi tổng quát và mệnh đề chứng minh tổng quát chung. Chƣơng 4. Áp dụng phƣơng pháp kiểm chứng giao diện ứng dụng trên thiết bị di động với Event-B Trình bày tổng quan về ứng dụng trên thiết bị di động Android và ứng dụng Note. Áp dụng phương pháp đã nghiên cứu được vào mô hình hóa và kiểm chứng thứ tự các cửa sổ của ứng dụng Note. Soạn thảo, biên tập mô hình thu được và kiểm chứng tự động với công cụ Rodin. Kết luận và hƣớng phát triển Kết luận tổng thể về các kết quả đã đạt được của luận văn và hướng phát triển tiếp theo. Phụ lục Trình bày một cách chi tiết về các mô hình trong Event-B của ứng dụng Note đã chuyển đổi và mô hình hóa 11 Chƣơng 2. TỔNG QUAN VỀ KIỂM CHỨNG GIAO DIỆN PHẦN MỀM VÀ PHƢƠNG PHÁP MÔ HÌNH HÓA EVENT-B 2.1. Giao diện ngƣời dùng Giao diện người dùng Graphical user interfaces (GUI) là giao diện đồ họa của chương trình cho phép người sử dụng giao tiếp với máy tính và các thiết bị điện tử thông qua tương tác với các đối tượng đồ họa như: nút ấn, menu, hộp nhập,…, thay vì chỉ là các dòng lệnh đơn thuần như trong Hình 2.2. GUI được sử dụng phổ biến trong máy tính, các thiết bị cầm tay, các thiết bị đa phương tiện trong văn phòng hoặc nhà ở. Con người tương tác với phần mềm thông qua các đối tượng đồ họa: cửa sổ, biểu tượng và các menu. Có nhiều phương pháp để tương tác, điều khiển như thông qua việc sử dụng một con chuột, bàn phím hoặc cũng có thể sử dụng bằng cách sử dụng các phím tắt bàn phím, phím mũi tên, hoặc thông qua giao diện cảm ứng. GUI cung cấp cho người dùng một cách giao tiếp khác với các chương trình máy, biến các chương trình phức tạp trở nên bắt mắt và dễ dùng hơn. Một ví dụ minh họa về GUI thể hiện trong Hình 2.1. Hình 2.1 Giao diện đồ họa người dùng 12 Hình 2.2 Giao diện dòng lệnh 2.2. Các phƣơng pháp kiểm chứng giao diện Kiểm chứng giao diện là quá trình gồm nhiều kỹ thuật kiểm tra, kiểm thử giao diện phần mềm để đảm bảo các chức năng tương ứng của giao diện đồ họa người dùng của phần mềm phải phù hợp với thông số kỹ thuật bằng văn bản tức là các bản đặc tả, thiết kế của nó [1]. Kiểm chứng những khiếm khuyết trong giao diện rất khó khăn bởi vì một số lỗi giao diện chỉ biểu lộ trong những điều kiện đặc biệt. Các lỗi thường xảy ra trên giao diện khi: một thành phần gọi tới các thành phần khác và gây ra lỗi trong khi sử dụng giao diện của nó, thành phần được gắn với các giả thiết về ứng xử của nó với thành phần được gọi, nhưng thành phần này lại sai, các thành phần gọi và thành phần được gọi thao tác với tốc độ khác nhau và những dữ liệu cũ lại được truy nhập, .v.v. Ngoài chức năng phát hiện lỗi, kiểm chứng giao diện còn đánh giá các yếu tố thiết kế như bố cục, màu sắc, phông chữ, cỡ chữ, nhãn, hộp văn bản, định dạng văn bản, ghi chú, các nút, danh sách, các biểu tượng, liên kết, xử lý các sự kiện bàn phím, sự kiện chuột và nội dung. Kiểm chứng giao diện có thể phân chia vào việc xem xét hai khía cạnh chính [5]:  Khả năng sử dụng của giao diện  Tính thẩm mỹ, bắt mắt  Màu sắc. 13  Hình khối và biểu tượng (Icon).  Vị trí, kích thước của các đối tượng nút ấn, hộp nhập, …  Ngôn ngữ, các ký hiệu, từ viết tắt, chính tả.  …  Sự điều hướng  Thông qua thao tác để truy cập qua công cụ hoặc thực đơn.  Số lượng các thao tác chọn và các thao tác chọn kết hợp.  Các phím tắt và các tùy chọn nâng cao.  Tính logic của giao diện  Phạm vi của vùng dữ liệu vào/ra  Input box.  Check box.  Drop down window list.  Button lựa chọn.  …  Hành vi của giao diện được cài đặt chặt chẽ với từng bối cảnh  Khi người dùng gọi trình tự các chức năng trên GUI.  … Quá trình kiểm chứng giao diện người dùng của ứng dụng để phát hiện nếu ứng dụng có chức năng không chính xác. Kiểm chứng giao diện áp dụng các kỹ thuật kiểm thử, các kỹ thuật kiểm thử này đề cập đến việc thiết lập các nhiệm vụ thực hiện và so sánh kết quả cùng với kết quả dự kiến và khả năng lặp lại cùng một tập các nhiệm vụ nhiều lần với dữ liệu đầu vào khác nhau và cùng một mức độ chính xác. Kiểm chứng giao diện thực hiện kiểm tra cách xử lý ứng dụng bàn phím và chuột sự kiện, làm thế nào các thành phần GUI khác nhau như: menubars, thanh công cụ, hộp thoại, nút nhấn, hình ảnh, sự kiện..., khi người sử dụng tương tác có thực hiện theo đúng cách mong muốn hay không. Thực hiện kiểm chứng giao diện cho ứng dụng sớm trong chu kỳ phát triển phần mềm sẽ tăng tốc độ phát triển, cải thiện chất lượng và giảm thiểu rủi ro về phía 14 cuối của chu kỳ. Kiểm chứng giao diện có nhiều phương pháp khác nhau mỗi phương pháp sẽ có những ưu nhược điểm riêng, có thể được thực theo hướng tĩnh hoặc động và có thể áp dụng tương ứng nhiều kỹ thuật kiểm thử một cách thủ công hoặc có thể được thực hiện tự động với việc sử dụng một chương trình phần mềm. 2.2.1. Phương pháp tĩnh Trong phương pháp này áp dụng kỹ thuật phân tích tĩnh, kiểm thử bằng tay dựa trên kinh nghiệm và kiến thức của người kiểm thử, nó được thực hiện bởi chính người kiểm thử. Phương pháp Heuristic được sử dụng trong kiểm thử bằng tay, trong đó một nhóm các chuyên gia nghiên cứu các phần mềm để tìm ra vấn đề. Màn hình giao diện được kiểm thử bằng tay bởi các người kiểm thử, những hành động và phản hồi của giao diện được so sánh với mục tiêu thiết kế và các yêu cầu của người sử dụng, sự khác biệt giữa mong đợi của người sử dụng và các bước thiết kế thiết kế cần thiết bởi giao diện, khả năng sử dụng của giao diện. Việc kiểm thử bằng tay giúp phát hiện nhiều lỗi qua mỗi ca kiểm thử, lỗi được tìm thấy sẽ cung cấp gợi ý để tìm lỗi khác, có thể tìm được những lỗi mà các phương pháp chứng tự động khó có thể tìm thấy. Kiểm thử bằng tay thường được sử dụng tốt cho kiểm thử giao diện ứng dụng đầu, thăm dò. Mặt khác kiểm chứng bằng tay thường tỏ ra không hiệu quả và gây tốn thời gian khi việc kiểm chứng cần lặp lại ca kiểm thử nhiều lần, phụ thuộc vào kiến thức và khả năng của người kiểm thử [1]. 2.2.2. Phương pháp động Phương pháp thường áp dụng một số kỹ thuật kiểm thử và kiểm thử giao diện tự động như kỹ thuật kiểm thử black-box (hộp đen) với các mô hình blackbox được sử dụng để tạo các ca kiểm thử cho kiểm thử giao diện, phương pháp động là quy trình áp dụng nhiều kỹ thuật và công cụ kiểm thử thực hiện một tập hợp các nhiệm vụ kiểm chứng tự động và so sánh kết quả thu được với đầu ra mong đợi. Kỹ thuật kiểm chứng giao diện tự động được áp dụng là một giải 15 pháp khắc phục cho tất cả các vấn đề mà kiểm thử giao diện bằng tay trong kiểm chứng tĩnh còn chưa làm được. Phương pháp áp dụng kiểm thử tự động được thực hiện thông qua các công cụ được xây dựng sẵn miễn phí hoặc mất phí:  Công cụ Capture-Replay: là một công cụ nắm bắt và chạy lại các thử nghiệm đã chụp của phiên làm việc của người sử dụng (đầu vào và các sự kiện) và lưu trữ chúng trong các kịch bản (mỗi phiên) phù hợp sẽ được sử dụng để chạy lại các phiên người dùng. Hoạt động bằng hai chế độ tương tác thực hiện khác nhau và cung cấp lợi thế kiểm tra đầu ra, đầu ra của ca kiểm thử được ghi lại [1].  Unit-Testing frameworks: cung cấp sự linh hoạt, hỗ trợ kiểm tra hướng phát triển và thực hiện công việc kiểm tra tự động.  Model based testing: Một mô hình là một mô tả đồ họa hành vi của hệ thống. Nó giúp người phát triển hiểu và dự đoán các hành vi hệ thống. Mô hình giúp tạo các ca sử dụng kiểm thử hiệu quả các yêu cầu của hệ thống. Theo nhu cầu sử dụng để được xem xét để thử nghiệm mô hình này dựa trên thực thi phiên làm việc của người sử dụng lựa chọn từ một mô hình của giao diện, quá trình này gồm: xây dựng mô hình, xác định đầu vào cho mô hình, tính toán kết quả dự kiến cho các mô hình, chạy thử nghiệm, so sánh kết quả thực tế với kết quả dự kiến, quyết định về hành động khác trên mô hình. 16 2.3. Tổng quan về Event-B Event-B được phát triển bởi tác giả J.R Abrial, là một phương pháp hình thức để mô hình hóa và phân tích hệ thống phân cấp, được phát triển từ phương pháp B. Event-B sử dụng chủ yếu các ký hiệu toán học, logic mệnh đề, lý thuyết tập hợp để mô hình hóa hệ thống. Cho phép tinh chỉnh mô hình hóa hệ thống theo các mức từ trừu tượng tới cụ thể và sử dụng các chứng minh toán học để xác minh tính nhất quán giữa các mức độ tinh chỉnh. Các ký hiệu, cú pháp của Event-B có thể được soạn thảo và chứng minh tự động bằng công cụ Rodin Platfrom được tích hợp trong Eclipse-IDE (Integrated Development Environment), Công cụ Rodin hỗ trợ cho phép soạn thảo các ký hiệu và chứng minh các tính chất toán học một cách hiệu quả, là một công cụ mã nguồn mở được cập nhật liên tục tại trang web Event-B.org [9]. Một mô hình Event-B thường mã hóa các hệ thống chuyển đổi trạng thái trong đó các biến sẽ đại diện cho các trạng thái, các sự kiện event đại diện cho việc chuyển từ trạng thái tới một trạng thái khác của hệ thống. Một mô hình trong Event-B được tạo thành bởi hai loại thành phần cơ bản sau: machines và context. Machines bao gồm các phần đặc tả động của mô hình, trong khi đó contexts chứa các phần đặc tả tĩnh của mô hình. Một mô hình có thể chỉ chứa các contexts hoặc các machines hoặc là cả hai loại. Machines và contexts có các mối quan hệ qua lại với nhau: một machine có thể refined bởi một machine khác và một context có thể extended bởi một context khác, một machine có thể sees một hoặc một vài context. Mối quan hệ và cấu trúc của machines và contexts được thể hiện trong Hình 2.3. [4].