Đặc tả và kiểm chứng phần mềm là một trong những phương pháp kiểm tra các hệ thống liệu có thỏa thiết kế hay không? Việc kiểm tra hệ thống được thực hiện trên nhiều pha trong quy trình sản xuất phần mềm,từ thiết kế,đặc tả,viết mã,kiểm thử,kiểm chứng,kiểm tra có thỏa yêu cầu người dùng (validation). Trong lập trình muốn có được một chương trình thì người lập trình không thể thành công trong lần chạy đầu tiên và chưa thể tốt được trong lần biên dịch đầu tiên.Một chương trình ban đầu trông có vẻ hoàn hảo và luôn đúng nhưng khi đưa vào chạy thật có thể chứa những lỗi ở đâu đó,khi đó nó sẽ gây ra những thiệt hại về thời gian và tiền bạc của chùng ta rất nhiều. Trong quá trình thiết kế và sản xuất phần cứng cũng như phần mềm,chúng ta tốn rất nhiều thời gian và công sức trong việc thiết kế,đôi khi nhiều hơn cả việc xây dựng chúng. Có rất nhiều ứng dụng mà khi có lỗi dù là nhỏ nhất được đưa vào sử dụng có thể dẫn đến thiệt hại về người, tài sản cũng như tốn thật nặng nề đến môi trường.Việc thiết kế phần mềm dành cho các hệ thống này là vô cùng khó khăn. Việc một lập trình viên phải làm để có một sản phẩm phần mềm luôn là phân tích,lập trình,kiểmtra lại,kiểm thử.Để việc kiểm chứng được nhẹ nhàng và nhanh chóng, tăngsự chính xác hơn thì chúng ta luôn tìm kiếm các công nghệ để giúp cho việc đó và SPIN chính là một trong các công cụ đó.