Kiểm chứng mô hình (model checking) là một phƣơng pháp hình thức dùng cho việc kiểm chứng hệ thống. Kiểm chứng mô hình khảo sát tất cả các trạng thái có thể của hệ thống và kiểm tra rằng chúng chứa sự đúng đắn đã đƣợc đặc tả. Việc sinh ra các trạng thái và kiểm tra có thể đƣợc thực hiện một cách tự động bằng phần mềm và Spin là một trong những bộ kiểm chứng (model checker) đƣợc sử dụng rộng rãi. Các bộ kiểm chứng không kiểm tra trực tiếp chƣơng trình mà kiểm tra một mô hình là thể hiện mức cao của hệ thống. Mô hình này mô tả hành vi của hệ thống. Để áp dụng đƣợc các công cụ kiểm chứng mô hình, việc đầu tiên là phải xây dựng mô hình của hệ thống. Các mô hình này cùng với đặc tả của thuộc tính cần kiểm tra là đầu vào của các bộ kiểm chứng. Khóa luận nghiên cứu việc kiểm chứng phần mềm sử dụng Spin, cụ thể là việc kiểm chứng mô hình máy hữu hạn trạng thái, sau đó đƣa ra một công cụ chuyển một mô tả ban đầu của hệ thống ở dạng máy hữu hạn trạng thái (chứa trong 1 tệp .txt) thành mô hình và kiểm chứng bằng Spin.