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 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.
Nội dung trích xuất từ tài liệu:
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ĐẠ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 – BLUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TINHÀ NỘI, 2016ĐẠ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.03LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TINNGƢỜI HƢỚNG DẪN KHOA HỌC: PGS.TS TRƢƠNG NINH THUẬNHÀ NỘI, 2016LỜI CAM ĐOANTô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êncứ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ướngdẫ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 đềucó 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 2016Người cam đoanNguyễn Xuân TrườngLỜI CẢM ƠNEm 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ìnhdạy dỗ, truyền đạt cho chúng em nhiều kiến thức, kinh nghiệm quý báu trongsuố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ầyPGS.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, địnhhướ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 độngviê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ànthà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òntươ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ỏinhững thiếu sót. Em rất mong nhận được những ý kiến đóng góp quý báu củathầ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 2016Học viênNguyễn Xuân Trường1MỤC LỤCMỤC LỤC ............................................................................................................ 1DANH MỤC KÝ HIỆU VÀ CHỮ VIẾT TẮT ................................................. 3DANH MỤC CÁC BẢNG .................................................................................. 4DANH MỤC CÁC HÌNH VẼ............................................................................. 5Chương 1. GIỚI THIỆU..................................................................................... 71.1. Sự cần thiết của đề tài ............................................................................... 71.2. Nội dung nghiên cứu ................................................................................ 91.3. Đóng góp của đề tài .................................................................................. 91.4. Cấu trúc của luận văn ............................................................................... 9Chương 2. TỔNG QUAN VỀ KIỂM CHỨNG GIAO DIỆN PHẦN MỀMVÀ PHƢƠNG PHÁP MÔ HÌNH HÓA EVENT-B........................................ 112.1. Giao diện người dùng ............................................................................. 112.2. Các phương pháp kiểm chứng giao diện ................................................ 122.2.1. Phương pháp tĩnh ............................................................................. 142.2.2. Phương pháp động............................................................................ 142.3. Tổng quan về Event-B ............................................................................ 162.3.1 Context .................................................................................................... 172.3.2 Machine .................................................................................................. 182.3.3 Ký hiệu toán học trong Event-B ............................................................. 212.3.4 Tinh chỉnh ............................................................................................... 222.3.5 Mệnh đề chứng minh .............................................................................. 232.3.6 Công cụ Rodin ........................................................................................ 24 ...