Đặc Tả Và Kiểm Chứng Các Hệ Thống Thời Gian Thực Sử Dụng Uppaaal

Đặc Tả và Kiểm Chứng Các Hệ Thống Thời Gian Thực Sử Dụng UPPAAL

Tác giả: PHẠM THỊ TỐ NGA

Lĩnh vực: Công nghệ thông tin

Nội dung tài liệu:

Luận văn này tập trung nghiên cứu về bộ công cụ kiểm chứng UPPAAL, đi sâu vào tìm hiểu ngôn ngữ đặc tả và cơ chế kiểm chứng của công cụ này cho các hệ thống thời gian thực. Từ đó, tác giả đã xây dựng và áp dụng bốn ví dụ minh họa để đặc tả và kiểm chứng các hệ thống thời gian thực bằng bộ công cụ UPPAAL. Đối với mỗi ví dụ, hệ thống thời gian thực được giả định, sau đó tiến hành đặc tả, mô hình hóa dưới dạng ô-tô-mát thời gian trên trình soạn thảo của UPPAAL, và cuối cùng là chạy mô phỏng, kiểm chứng sự hoạt động của hệ thống.

Mục lục chi tiết:

• Chương 1: Giới thiệu
• Chương 2: Đặc tả và kiểm chứng trong Uppaal
• Chương 3: Một số ví dụ áp dụng
• Chương 4: Kết luận