Kiểm chứng phần mềm là một trong những lĩnh vực nghiên cứu rất cơ bản của kỹ nghệ phần mềm. Mục đích chung chính là kiểm chứng xem khi nào thì một chương trình phần mềm được cho là chính xác, hay nói cách khác là khi nào thì cài đặt của một chương trình phù hợp với đặc tả của nó. Bài toán kiểm tra mô hình (Model Checking) thường tập trung vào việc kiểm chứng các chương trình phản ứng hữu hạn trạng thái. Để chỉ ra các tính chất của một chương trình như vậy, chúng ta sử dụng logic thời gian tuyến tính (Linear Temporal Logic - LTL).

Vậy thì thế nào là một chương trình phản ứng. Mô hình thực thi của một chương trình thường bao gồm các bước sau: nó nhận vào một tập các giá trị đầu vào, thực hiện các tính toán cần thiết, rồi đưa ra một giá trị đầu ra nào đó. Như vậy, một chương trình thông thường có thể được xem xét giống như một hàm trừu tượng từ miền đầu vào đến miền đầu ra trong đó, quá trình thực thi là quá trình chuyển đổi từ các trạng thái ban đầu tới các trạng thái kết thúc.

Ngược lại, một chương trình phản ứng không hướng tới việc kết thúc. Giống như tên gọi của nó, các hệ thống như vậy “phản ứng” lại môi trường của chúng một cách liên tục, đáp lại một cách tương ứng với các giá trị đầu vào. Một số ví dụ của các hệ thống như vậy bao gồm hệ điều hành, bộ lập lịch… (thông thường, các hệ thống phản ứng là các chương trình phân tán phức tạp, nên việc thực thi song song cần phải được tính đến).

Để chỉ ra các tính chất của một hệ thống phản ứng, chúng ta cần một kỹ thuật để nói về cách mà hệ thống đó thực thi, tiến triển theo những dãy tính toán vô hạn có thể xảy ra. Các logic về thời gian [1] đã trở thành một phương pháp hình thức được sử dụng rất rộng rãi cho mục đích này. Đã có rất nhiều loại logic thời gian khác nhau được định nghĩa trong khoảng hai thập kỷ qua – chúng ta sẽ chỉ tập trung vào một loại đó là logic thời gian tuyến tính.

Phần nội dung: Kết cấu gồm hai phần, được chia làm 7 chương

•Phần 1: Đặt vấn đề và định hướng giải pháp

•Phần 2: các kết quả đã đạt được