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

Đề 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 thứ tự của các cửa sổ giao diện phần mềm một 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 thiết bị di động. Mời các bạn cùng tham khảo đề tài.
Nội dung trích xuất từ tài liệu:
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 - B1ĐẠI HỌC QUỐC GIA HÀ NỘITRƯỜNG ĐẠI HỌC CÔNG NGHỆNGUYỄN XUÂN TRƯỜNGKIỂM CHỨNG GIAO DIỆN PHẦN MỀM BẰNG PHƯƠNG PHÁPMÔ HÌNH HÓA EVENT – BNgành: Công nghệ thông tinChuyên ngành: Kỹ thuật phần mềmMã số: 60.48.01.03TÓM TẮT LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TINHÀ NỘI, 20162Chương 1. GIỚI THIỆU1.1.Sự cần thiết của đề tàiNgà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ềnthông, ngân hàng, sản xuất chế tạo, quản trị, y tế, khoa học kỹ thuật, Hàngkhô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ầnthay thế con người. Đại đa số phần mềm hiện nay được xây dựng với một giaodiện đồ họa người dùng Graphical User Interface (GUI) và con người sẽ làmviệc thông qua tương tác với giao diện của phần mềm.Người sử dụng thường quan tâm tới giao diện dễ sử dụng và có tính thẩmmỹ đả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ủaphầ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ư dự kiến hay trả lại kết quả nhưmong muốn. Những lỗi phát sinh 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ệnkhô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àncó 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ầnphả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ấtquá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ôngsố 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 đề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ửachữa và bảo trì.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ửasổ 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ểnthị các phần tử giao diện thông qua đó người dùng có thể tương tác, trao đổinhậ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ặcnhiề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áctrạ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ời3gọ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ậuquả khó lường.Nhận thấy được tầm quan trọng của việc kiểm chứng giao diện ngườidù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 người dùng, nên tác giả đã mạnh dạn đề xuất đề tài “Kiểm chứng giaodiện phần mềm bằng phương pháp mô hình hóa Event – B” nhằm nghiêncứ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ộtcá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ênthiết bị di động.1.2.Nội dung nghiên cứuĐề 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ênquan tới kiểm chứng giao diện phần mềm, các phương pháp kiểm chứng giaodiệ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ôhình hóa Event-B. Tìm hiểu nguyên lý, cách sử dụng công cụ Rodin. Từ nhữngnghiên cứu có được đưa ra một phương pháp mô hình hóa và kiểm chứng chungcho 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ộ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ìnhthự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ựngcác bộ quy tắc chuyển đổi tham chiếu tương ứng từ mô hình 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ổ giaodiệ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àiNghiên cứu đề xuất phương pháp để kiểm chứng giao diện người dùngphần mềm 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áthiện và tránh các lỗi không mong muốn của giao diện hoặc những giả thiết4khô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ướckhi cài đặt.1.4.Cấu trúc của luận vănPhần nội dung của luận văn được cấu trúc thành 7 chương chính như sau:Chương 1. GIỚI THIỆUGiới thiệu về các yêu cầu khách quan, chủ quan, cơ sở khoa học, thực tiễnnghiên cứu và xây dựng đề tài.Chương 2. TỔNG QUAN VỀ KIỂM CHỨNG GIAO DIỆN PHẦN MỀMGiớ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.Chương 3. PHƯƠNG PHÁP MÔ HÌNH HÓA EVENT-BBao 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ànhphầ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ệutoán học tro ...