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Ộ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 /> LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN<br /> <br /> HÀ NỘI, 2016<br /> <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 /> LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN<br /> <br /> NGƢỜI HƢỚNG DẪN KHOA HỌC: PGS.TS TRƢƠNG NINH THUẬN<br /> <br /> HÀ NỘI, 2016<br /> <br /> LỜI CAM ĐOAN<br /> 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<br /> 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<br /> 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<br /> có nguồn gốc rõ ràng và trích dẫn theo đúng quy định.<br /> 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ó<br /> điều gì sai trái, tôi xin chịu mọi hình thức kỷ luật theo quy định.<br /> <br /> Hà Nội, tháng 06 năm 2016<br /> Ngƣời cam đoan<br /> <br /> Nguyễn Xuân Trường<br /> <br /> LỜI CẢM ƠN<br /> 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ệ<br /> Thông Tin – Trường Đại học Công nghệ – Đại học Quốc gia Hà Nội đã tận tình<br /> dạy dỗ, truyền đạt cho chúng em nhiều kiến thức, kinh nghiệm quý báu trong<br /> 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<br /> PGS.TS Trương Ninh Thuận – Phó chủ nhiệm khoa công nghệ thông tin –<br /> Trường Đại học Công nghệ – ĐHQGHN đã tận tình chỉ bảo, hướng dẫn, định<br /> hướng cho em để em hoàn thành luận văn tốt nghiệp này.<br /> Cuối cùng em xin cảm ơn gia đình, bạn bè, đồng nghiệp đã luôn động<br /> 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<br /> 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<br /> 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<br /> 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<br /> thầy cô và các bạn để luận văn được hoàn thiện hơn.<br /> <br /> Hà Nội, tháng 06 năm 2016<br /> Học viên<br /> <br /> Nguyễn Xuân Trường<br /> <br /> 1<br /> <br /> MỤC LỤC<br /> MỤC LỤC ............................................................................................................ 1<br /> DANH MỤC KÝ HIỆU VÀ CHỮ VIẾT TẮT ................................................. 3<br /> DANH MỤC CÁC BẢNG .................................................................................. 4<br /> DANH MỤC CÁC HÌNH VẼ............................................................................. 5<br /> Chƣơng 1. GIỚI THIỆU..................................................................................... 7<br /> 1.1. Sự cần thiết của đề tài ............................................................................... 7<br /> 1.2. Nội dung nghiên cứu ................................................................................ 9<br /> 1.3. Đóng góp của đề tài .................................................................................. 9<br /> 1.4. Cấu trúc của luận văn ............................................................................... 9<br /> Chƣơng 2. TỔNG QUAN VỀ KIỂM CHỨNG GIAO DIỆN PHẦN MỀM<br /> VÀ PHƢƠNG PHÁP MÔ HÌNH HÓA EVENT-B........................................ 11<br /> 2.1. Giao diện người dùng ............................................................................. 11<br /> 2.2. Các phương pháp kiểm chứng giao diện ................................................ 12<br /> 2.2.1. Phương pháp tĩnh ............................................................................. 14<br /> 2.2.2. Phương pháp động............................................................................ 14<br /> 2.3. Tổng quan về Event-B ............................................................................ 16<br /> 2.3.1 Context .................................................................................................... 17<br /> 2.3.2 Machine .................................................................................................. 18<br /> 2.3.3 Ký hiệu toán học trong Event-B ............................................................. 21<br /> 2.3.4 Tinh chỉnh ............................................................................................... 22<br /> 2.3.5 Mệnh đề chứng minh .............................................................................. 23<br /> 2.3.6 Công cụ Rodin ........................................................................................ 24<br /> <br />