Phương pháp kiểm chứng hệ thời gian thực bằng thuật toán

LỜI CAM ĐOAN

LỜI CẢM ƠN

MỤC LỤC

DANH MỤC TỪ VIẾT TẮT

DANH MỤC BẢNG VÀ THUẬT TOÁN

DANH MỤC HÌNH VẼ

TÓM TẮT NỘI DUNG

1. CHƯƠNG 1: KIỂM CHỨNG MÔ HÌNH VÀ HỆ THỜI GIAN THỰC

1.1. Đặc tả và kiểm tra hệ thống

1.2. Kiểm chứng mô hình

1.3. Kiểm chứng mô hình với hệ thời gian thực

1.4. Kiểm chứng mô hình với các tính chất khoảng

2. CHƯƠNG 2: ĐẶC TẢ HỆ THỐNG VÀ TÍNH CHẤT

2.1. Mô hình thời gian

2.2. Thể hiện đồng hồ và ràng buộc thời gian

2.3. Kỹ thuật phân vùng đồng hồ

2.4. Ôtômat thời gian

2.4.1. Cú pháp và ngữ nghĩa

2.4.2. Đường chạy và dáng điệu của ôtômat thời gian

2.4.3. Hợp song song của các ôtômat thời gian

2.5. Mô hình trong Lôgic khoảng

2.5.1. Công thức khoảng và bài toán kiểm chứng mô hình

3. CHƯƠNG 3: KIỂM CHỨNG MÔ HÌNH VỚI KỸ THUẬT QUI HOẠCH TUYẾN TÍNH

3.1. Biểu thức chính quy thời gian và bài toán qui hoạch tuyến tính

3.1.1. Biểu thức chính quy thời gian - TRE

3.1.2. Biểu thức TRE hữu hạn

3.1.3. Xây dựng bài toán qui hoạch tuyến tính

3.2. Chuyển TRE về hợp của các TRE hữu hạn

3.2.1. Cận thời gian của biểu thức TRE

3.2.2. Khử phép toán * trong biểu thức TRE

3.2.3. Kiểm chứng tính an toàn của hệ chắn tàu

3.2.4. Kiểm tra tính rỗng và khử * xuất hiện dưới ⊗

3.3. Các công trình liên quan và nhận xét về phương pháp

3.3.1. Các công trình liên quan

3.3.2. Vài nhận xét về phương pháp

4. CHƯƠNG 4: KỸ THUẬT RỜI RẠC HOÁ VÀ DUYỆT ĐỒ THỊ ĐẠT ĐƯỢC

4.1. Tính rời rạc hoá được và đồ thị vùng nguyên

4.1.1. Tập mô hình DC của ôtômat thời gian

4.1.2. Khái niệm nguyên hoá và một vài tính chất

4.1.3. Tính rời rạc hoá được của các công thức LDP, LDI

4.1.4. Đồ thị vùng đạt được nguyên

4.2. Kiểm chứng công thức LDP

4.2.1. Tính tương đương của M(A) và Muv (A) đối với LDP

4.2.2. Đồ thị trọng số G phục vụ kiểm chứng LDP

4.2.3. Thuật toán kiểm chứng LDP

4.3. Kiểm chứng công thức LDI

4.3.1. Quan hệ giữa lớp mô hình Muv (A) và đồ thị đạt được RG hướng tới LDI

4.3.2. Đồ thị trọng số G phục vụ kiểm chứng LDI

4.3.3. Thuật toán kiểm chứng LDI

4.4. Kiểm chứng tính an toàn của hệ chắn tàu bằng rời rạc hoá

KẾT LUẬN

DANH MỤC CÔNG TRÌNH CỦA TÁC GIẢ

TÀI LIỆU THAM KHẢO

PHỤ LỤC

A. Bộ kiểm chứng mô hình LDP, LDI

A.1. Công thức và kí hiệu

A.2. Thuật ngữ Anh - Việt

I. Kiểm chứng mô hình và hệ thời gian thực

Mục đích chính của các phương pháp hình thức là giúp xây dựng và phát triển các hệ thống hoạt động đúng đắn, đáng tin cậy. Các hệ thống (phần cứng và phần mềm) ngày càng phát triển, do đó bài toán kiểm tra tính đúng đắn của chúng cũng ngày càng phức tạp. Một số trường hợp thực tế đã chứng minh rằng chỉ một lỗi nhỏ cũng có thể phá hủy toàn bộ hệ thống, gây ra hậu quả nghiêm trọng về an toàn và tốn kém. Việc kiểm tra tính đúng đắn của hệ thống thời gian thực đã được phát triển trong khoảng hơn 10 năm qua. Các phương pháp hình thức đã ra đời và phát triển mạnh mẽ, đạt được nhiều thành tựu. Kiểm chứng mô hình đã sản sinh ra các bộ kiểm chứng cho phép kiểm tra hệ thống một cách tự động. Điều này giúp giảm thiểu thời gian và công sức trong quá trình kiểm tra. Các bộ kiểm chứng ngày càng đóng vai trò quan trọng trong việc kiểm tra tính đúng đắn của hệ thống.

1.3. Kỹ thuật rời rạc hoá và duyệt đồ thị đạt được

Kỹ thuật rời rạc hoá và duyệt đồ thị đạt được là một phần quan trọng trong kiểm chứng mô hình. Tính rời rạc hoá được và đồ thị vùng nguyên giúp xây dựng các đồ thị trọng số phục vụ kiểm chứng. Các thuật toán kiểm chứng LDP và LDI đã được phát triển để kiểm tra tính an toàn của hệ thống. Việc áp dụng các kỹ thuật này giúp cải thiện hiệu quả kiểm chứng và giảm thiểu thời gian xử lý. Các đồ thị trọng số được xây dựng từ các công thức và thuật toán kiểm chứng giúp xác định tính chính xác của hệ thống trong các tình huống thực tế.

Luận văn thạc sĩ: Kiểm chứng tính đúng đắn của hệ thời gian thực bằng thuật toán