SPIN là một công cụ để xác minh tính chính xác của của một mô hình phần mềm một cách nghiêm ngặt và tự động. Ngôn ngữ đầu vào của SPIN có tên là PROMELA. PROMELA có thể dùng để quy định hệ thống đồng thời bằng cách tự động thay đổi số lượng các quá trình tương tác, nơi mà các quá trình tương tác có thể được đồng bộ hóa hoặc không đồng bộ hóa. Bên cạnh đó, ngôn ngữ này cũng hỗ trợ việc quy định, xác minh hệ thống đồng thời thông qua các kênh tin nhắn. Trong bài báo cáo này, chúng tôi đưa ra một ví dụ về hệ thống mạng đơn giản: gồm một máy chủ và 2 máy khách, nhằm chứng tỏ khả năng quy định và xác minh hệ thống đồng thời, hệ thống phản ứng.