Đang chuẩn bị nút TẢI XUỐNG, xin hãy chờ
Tải xuống
Luận án trình bày các nội dung chính sau: Giới thiệu các khái niệm cơ bản được sử dụng trong các nghiên cứu của luận án. Phương pháp sinh giả định nhỏ nhất và mạnh nhất cục bộ; Đề xuất một phương pháp sinh giả định yếu nhất cục bộ và sử dụng giả định đó một cách hiệu quả trong việc kiểm chứng các phần mềm trong ngữ cảnh tiến hóa; . | ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ TRẦN HOÀNG VIỆT KIỂM CHỨNG DỰA TRÊN PHƯƠNG PHÁP GIẢ ĐỊNH ĐẢM BẢO CHO PHẦN MỀM DỰA TRÊN THÀNH PHẦN TÓM TẮT LUẬN ÁN TIẾN SĨ NGÀNH CÔNG NGHỆ THÔNG TIN Hà Nội - 2020 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ TRẦN HOÀNG VIỆT KIỂM CHỨNG DỰA TRÊN PHƯƠNG PHÁP GIẢ ĐỊNH ĐẢM BẢO CHO PHẦN MỀM DỰA TRÊN THÀNH PHẦN Chuyên ngành Kỹ Thuật Phần Mềm Mã số 9480103.01 TÓM TẮT LUẬN ÁN TIẾN SĨ NGÀNH CÔNG NGHỆ THÔNG TIN NGƯỜI HƯỚNG DẪN KHOA HỌC 1. PGS. TS. Phạm Ngọc Hùng 2. TS. Võ Đình Hiếu Hà Nội - 2020 Mục lục 1 Giới thiệu 1 1.1 Đặt vấn đề . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Các đóng góp chính của luận án . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.3 Bố cục của luận án . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2 Kiến thức nền tảng 5 2.1 Đặc tả và kiểm chứng giả định - đảm bảo cho các hệ thống đặc tả bằng LTS . . . . . . . . . . . 5 2.1.1 Hệ thống chuyển trạng thái được gán nhãn . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.1.2 Kiểm chứng các hệ thống chuyển trạng thái được gán nhãn . . . . . . . . . . . . . . . . . 5 2.2 Đặc tả và kiểm chứng giả định - đảm bảo cho các hệ thống đặc tả bằng lôgic mệnh đề . . . . . . 5 2.2.1 Đặc tả hệ thống chuyển trạng thái bằng lôgic mệnh đề . . . . . . . . . . . . . . . . . . . . 5 2.2.2 Kiểm chứng giả định - đảm bảo cho các hệ thống đặc tả bằng lôgic mệnh đề . . . . . . . 5 2.3 Đặc tả và kiểm chứng giả định - đảm bảo cho các hệ thống có ràng buộc thời gian . . . . . . . . 6 2.3.1 Hệ thống chuyển trạng thái có ràng buộc thời gian . . . . . . . . . . . . . . . . . . . . . . 6 2.3.2 Kiểm chứng giả định - đảm bảo cho các hệ thống có ràng buộc thời gian . . . . . . . . . . 6 3 Phương pháp sinh giả định nhỏ nhất và mạnh nhất cục bộ cho việc kiểm chứng phần mềm dựa trên thành phần 7 3.1 Giới thiệu . . . . . . . . . . . . . . . . . . . . . . . . . . .
