Tóm tắt Luận văn Thạc sĩ Kỹ thuật: Nghiên cứu và ứng dụng kiểm chứng mô hình cho các hệ thống phát triển trên môi trường Lustre/SCADE

Nghiên cứu và ứng dụng kiểm chứng mô hình cho các hệ thống phát triển trên môi trường Lustre/SCADE

Tác giả: Nguyễn Văn Định

Lĩnh vực: Khoa học máy tính

Nội dung tài liệu:

Đề tài tập trung vào nghiên cứu và ứng dụng kỹ thuật kiểm chứng mô hình (Model Checking) để nâng cao độ tin cậy và tính an toàn cho các hệ thống phần mềm được phát triển trên môi trường Lustre/SCADE. Nghiên cứu này nhấn mạnh vào việc mô hình hóa hệ thống, mô phỏng, phân tích và tự động sinh mã, nhằm giảm thiểu chi phí phát triển và phát hiện sớm các lỗi tiềm ẩn trong giai đoạn thiết kế.

Kiểm chứng mô hình được đề xuất như một phương pháp luận hiệu quả để tăng độ tin cậy, giảm thời gian phát triển và hạn chế lỗi trong các hệ thống phần mềm, đặc biệt là các hệ thống phản ứng (reactive systems). Đề tài xem xét các khía cạnh lý thuyết của kiểm chứng mô hình, giới thiệu ngôn ngữ lập trình đồng bộ Lustre và môi trường phát triển SCADE, cũng như các công cụ kiểm chứng mô hình tiêu biểu.

Qua đó, đề tài xây dựng quy trình kiểm chứng mô hình cụ thể và thực nghiệm trên môi trường Lustre/SCADE, nhằm xác minh tính đúng đắn của các hệ thống phản ứng, góp phần nâng cao chất lượng sản phẩm phần mềm.

Mục lục chi tiết:

• PHẦN MỞ ĐẦU
• CHƯƠNG 1 – TỔNG QUAN KIỂM CHỨNG MÔ HÌNH
• CHƯƠNG 2 – CÁC HỆ THỐNG PHẢN ỨNG VÀ MÔI TRƯỜNG LUSTRE/SCADE
• CHƯƠNG 3 – ỨNG DỤNG KIỂM CHỨNG MÔ HÌNH CHO CÁC HỆ THỐNG PHÁT TRIỂN TRÊN MÔI TRƯỜNG LUSTRE/SCADE
• KẾT LUẬN VÀ HƯỚNG PHÁT TRIỂN