Luận văn: Đặc tả và kiểm chứng các hệ thống thời gian thực sử dụng Uppaal

Đặ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, tìm hiểu ngôn ngữ đặc tả của Uppaal, cách đặc tả hệ thống phần mềm dưới dạng ô-tô-mát thời gian, điều khiển vận hành hệ thống thông qua ngôn ngữ C++, và cơ chế kiểm chứng của bộ công cụ này cho các hệ thống thời gian thực. Từ đó, luận văn xây dựng và áp dụng bốn ví dụ về các hệ thống thời gian thực để đặc tả và kiểm chứng bằng bộ công cụ Uppaal. Phương pháp kiểm tra mô hình, bao gồm việc áp dụng các kỹ thuật toán học vào đặc tả và phân tích hệ thống để xây dựng mô hình hệ thống, được sử dụng để kiểm chứng các hệ thống.

Mục lục chi tiết:

Chương 1: Giới thiệu

Chương 2: Cơ sở lý thuyết

Chương 3: Đặc tả và kiểm chứng trong Uppaal

Chương 4: Áp dụng đặc tả và kiểm chứng một số hệ thống thời gian thực bằng công cụ Uppaal