Tóm tắt Luận văn Thạc sĩ Công nghệ thông tin: Kiểm chứng giao diện phần mềm bằng phương pháp mô hình hóa Event - B

1<br /> ĐẠI HỌC QUỐC GIA HÀ NỘI<br /> TRƯỜNG ĐẠI HỌC CÔNG NGHỆ<br /> <br /> NGUYỄN XUÂN TRƯỜNG<br /> <br /> KIỂM CHỨNG GIAO DIỆN PHẦN MỀM BẰNG PHƯƠNG PHÁP<br /> MÔ HÌNH HÓA EVENT – B<br /> <br /> Ngành: Công nghệ thông tin<br /> Chuyên ngành: Kỹ thuật phần mềm<br /> Mã số: 60.48.01.03<br /> <br /> TÓM TẮT LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN<br /> <br /> HÀ NỘI, 2016<br /> <br /> 2<br /> Chương 1. GIỚI THIỆU<br /> <br /> 1.1.<br /> <br /> Sự cần thiết của đề tài<br /> 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<br /> <br /> 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<br /> 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<br /> 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<br /> diện đồ họa người dùng Graphical User Interface (GUI) và con người sẽ làm<br /> việc thông qua tương tác với giao diện của phần mềm.<br /> Người sử dụng thường quan tâm tới giao diện dễ sử dụng và có tính thẩm<br /> mỹ đảm bảo được các chức năng. Tuy nhiên không phải lúc nào các GUI của<br /> 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ý,<br /> các chức năng hoạt động một cách chính xác như dự kiến hay trả lại kết quả như<br /> mong muốn. Những lỗi phát sinh trong quá trình tương tác như: Các phần tử<br /> 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<br /> 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ổ<br /> 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<br /> có thể nguy hại tới tính mạng con người và thiệt hại về kinh tế,... Vì vậy, Cần<br /> 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<br /> 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<br /> số trong đặc tả thiết kế, phát hiện và sửa chữa kịp thời các lỗi hoặc bất cứ vấn đề<br /> bất thường nào có thể có trước khi đưa ra lưu hành, làm giảm các chi phí sửa<br /> chữa và bảo trì.<br /> Lỗi hiển thị sai các cửa sổ giao diện là tương đối nghiêm trọng. Các cửa<br /> sổ giao diện đại diện cho bộ mặt của ứng dụng phần mềm, là nơi chứa và hiển<br /> thị các phần tử giao diện thông qua đó người dùng có thể tương tác, trao đổi<br /> nhập xuất thông tin. Từ một chức năng trong cửa sổ này có thể gọi tới một hoặc<br /> nhiều 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<br /> 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<br /> <br /> 3<br /> 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ẽ<br /> đư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<br /> quả khó lường.<br /> Nhận thấy được tầm quan trọng của việc kiểm chứng giao diện người<br /> 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ổ<br /> giao diện người dùng, nên tác giả đã mạnh dạn đề xuất đề tài “Kiểm chứng giao<br /> diện phần mềm bằng phương pháp mô hình hóa Event – B” nhằm nghiên<br /> cứu phương pháp kiểm chứng thứ tự của các cửa sổ giao diện phần mềm một<br /> cách tự động dựa trên Event-B và thực hiện áp dụng cho giao diện ứng dụng trên<br /> thiết bị di động.<br /> 1.2.<br /> <br /> Nội dung nghiên cứu<br /> Đề tài tập trung vào việc nghiên cứu giao diện phần mềm, các vấn đề liên<br /> <br /> 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<br /> diện nghiên cứu mô hình. Nghiên cứu cấu trúc, ký pháp của phương pháp mô<br /> hình hóa Event-B. Tìm hiểu nguyên lý, cách sử dụng công cụ Rodin. Từ những<br /> nghiên cứu có được đưa ra một phương pháp mô hình hóa và kiểm chứng chung<br /> cho kiểm chứng thứ tự xuất hiện của các cửa sổ giao diện người dùng, toàn bộ<br /> 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<br /> thực hiện, xây dựng các mô hình tổng quát thông qua các định nghĩa, xây dựng<br /> các bộ quy tắc chuyển đổi tham chiếu tương ứng từ mô hình vào trong Event-B.<br /> Á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<br /> 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ị<br /> di động.<br /> 1.3.<br /> <br /> Đóng góp của đề tài<br /> Nghiên cứu đề xuất phương pháp để kiểm chứng giao diện người dùng<br /> <br /> phần mềm bằng phương pháp mô hình hóa Event-B, đó chính là kiểm chứng sự<br /> 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<br /> 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<br /> <br /> 4<br /> không hợp lý về thiết kế của giao diện trong quá trình xây dựng phần mềm trước<br /> khi cài đặt.<br /> 1.4.<br /> <br /> Cấu trúc của luận văn<br /> <br /> Phần nội dung của luận văn được cấu trúc thành 7 chương chính như sau:<br /> Chương 1. GIỚI THIỆU<br /> 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<br /> nghiên cứu và xây dựng đề tài.<br /> Chương 2. TỔNG QUAN VỀ KIỂM CHỨNG GIAO DIỆN PHẦN MỀM<br /> 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 đề<br /> 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.<br /> Chương 3. PHƯƠNG PHÁP MÔ HÌNH HÓA EVENT-B<br /> Bao gồm những kiến thức tổng quan về phương pháp mô hình hóa EventB, 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<br /> 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<br /> 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ự<br /> động với công cụ Rodin.<br /> Chương 4: KIỂM CHỨNG GIAO DIỆN PHẦN MỀM BẰNG PHƯƠNG<br /> PHÁP EVENT-B<br /> Tập trung vào việc xây dựng mô hình kiểm chứng chung cho các giao<br /> 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<br /> các định nghĩa, đưa ra các luật chuyển đổi tổng quát và mệnh đề chứng minh<br /> tổng quát chung.<br /> Chương 5. ÁP DỤNG PHƯƠNG PHÁP KIỂM CHỨNG GIAO DIỆN ỨNG<br /> DỤNG NOTE VỚI EVENT-B<br /> <br /> 5<br /> Trình bày tổng quan về Android và ứng dụng Note. Áp dụng phương<br /> 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<br /> ứng dụng Note. Soạn thảo mô hình thu được và kiểm chứng tự động với công cụ<br /> Rodin.<br /> Chương 6. KẾT LUẬN VÀ HƯỚNG PHÁT TRIỂN<br /> 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<br /> triển tiếp theo.<br /> Chương 7. PHỤ LỤC<br /> 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<br /> Note đã chuyển đổi và mô hình hóa<br /> <br />