Luận Văn Thạc Sĩ Kiểm Chứng Tính Đúng Đắn Hệ Thống Tính Toán Của Chương Trình Bằng Kiểm Duyệt Mô Hình

Kiểm Chứng Tính Đúng Đắn Hệ Thống Tính Toán Của Chương Trình Bằng Kiểm Duyệt Mô Hình​

Trình bày về cơ sở lý thuyết của kiểm duyệt mô hình (Model checking): khái niệm và ý nghĩa của kiểm duyệt mô hình, quy trình hoạt động của kiểm duyệt mô hình, đặc trưng của kiểm duyệt mô hình, điểm mạnh và điểm yếu của kiểm duyệt dựa trên mô hình sử dụng logic thời gian (Temporal Logic) mô tả các thuộc tính cần kiểm chứng. Nghiên cứu về công cụ Spin, giao diện Xspin, và ngôn ngữ mô hình hóa Promela, máy trạng thái hữu hạn. Tiến hành xây dựng tiến trình đồng hồ, mô hình hóa hệ thống báo động, báo cháy, kết hợp tiến trình đồng hồ với kỹ thuật kiểm duyệt mô hình để kiểm chứng tính đúng đắn của hệ thống đó.

• Luận văn thạc sĩ Công nghệ thông tin
• Chuyên ngành Công nghệ phần mềm
• Người hướng dẫn khoa học: TS. Đặng Văn Hưng
• Tác giả: Nguyễn Thị Loan
• Số trang: 66
• Kiểu file: PDF
• Ngôn ngữ: Tiếng Việt
• Trường Đại học Công nghệ. Đại học Quốc gia Hà Nội 2012

Link Download
http://dlib.vnu.edu.vn/iii/cpro/DigitalItemViewPage.external?lang=vie&sp=1002899
https://drive.google.com/drive/folders/1yLBzZ1rSQoNjmWeJTM6cEZ3WGQHg04L1