- Phân tích, thiết kế và cài đặt kiểm chứng một hệ thời gian thực. - Hệ thời gian thực . - Bộ kiểm chứng. - Ngày nay, các hệ thống thời gian thực ngày càng phát triển, ứng dụng và phổ biến rộng rãi, chẳng hạn các hệ thống nhúng thời gian thực trong các thiết bị điện tử chuyên dụng, từ các đồ điện tử trong gia đình như tivi, máy giặt, lò vi sóng đến những hệ thống lớn như máy bay, tên lửa, vệ tinh nhân tạo, v.v…. - Các hệ thời gian thực hoạt động rất phức tạp và dù chỉ một lỗi nhỏ cũng có thể phá hủy toàn bộ hệ thống và gây ra những hậu quả nghiêm trọng, đáng tiếc, hao tốn nhiều thời gian, tiền của và công sức để khắc phục. - Chi phí để phát triển hệ thống thời gian thực cả về phần mềm lẫn phần cứng thường lớn hơn nhiều so với các hệ thống ứng dụng khác và đòi hỏi tính chính xác cao, không thể chấp nhận những ứng dụng có thể có lỗi dù là nhỏ nhất, vì vậy, việc tìm hiểu về các mặt của một hệ thời gian thực từ phân tích, thiết kế mô hình đến kiểm tra tính đúng đắn các hoạt động của hệ thống trước khi đưa chúng vào sản xuất là điều rất thiết thực và cấp thiết.. - Để phân tích, thiết kế mô hình của hệ thống thời gian thực có thể sử dụng nhiều công cụ như các văn phạm, ôtômat, và các lôgic liên quan đến thời gian thực như lôgic thời gian tuyến tính, lôgic khoảng, v.v…. - Xuất phát từ yêu cầu thực tiễn, và cũng để nâng cao kỹ năng thực hành và củng cố lý thuyết, đề tài “Phân tích, thiết kế và cài đặt kiểm chứng một hệ thời gian thực” được chọn làm đề tài luận văn của tôi với mục tiêu:. - Tìm hiểu các phương pháp đặc tả và kiểm tra tính đúng đắn của hệ thống thời gian thực.. - Tìm hiểu kỹ thuật kiểm tra tính đúng đắn của hệ thống thời gian thực bằng phương pháp kiểm chứng mô hình.. - Phân tích, thiết kế và cài đặt một công cụ kiểm chứng mô hình cho các đặc tả sử dụng công cụ ôtômat thời gian và lôgic khoảng.. - Chương 1 giới thiệu khái quát về hệ thời gian thực và bài toán kiểm tra tính đúng đắn của hệ. - Chương 2 trình bày về các công cụ đặc tả hệ thống và bài toán bếp ga. - [2] Phạm Hồng Thái (2005), Kiểm chứng tính chất thời gian thực bằng thuật toán, Luận án Tiến sỹ, Hà Nội.