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ế.
