Ngày nay, cùng với sự phát triển mạnh mẽ của máy móc phục vụ đời sống con người là sự phát triển âm thầm của các hệ thống tương tranh. Chúng được tạo ra để điều khiển hoạt động của những máy móc đó. Một hệ thống tương tranh có thể bao gồm cả phần mềm và phần cứng nhưng cũng có thể chỉ có phần mềm. Phần mềm tương tranh chính là linh hồn của hệ thống, giúp chúng hoạt động chính xác theo những gì mà con người yêu cầu. Hiện nay, phần mềm tương tranh được ứng dụng rất nhiều trong các hệ thống nhúng và điều khiển. Từ những vật dụng rất đơn giản trong đời sống hàng ngày như nồi cơm điện, ti vi, đến những hệ thống điều khiển phức tạp như hệ thống điều khiển tên lửa đều có một hoặc nhiều phần mềm tương tranh điều khiển. Những vật dụng, hệ thống điều khiển này gắn bó chặt chẽ với chúng ta, chỉ cần một lỗi nhỏ của phần mềm tương tranh cũng có thể gây ra hậu quả nghiêm trọng. Đã có những con tàu vũ trụ vừa mới rời khỏi mặt đất thì đã rơi, tiêu tốn hàng tỷ đô la để nghiên cứu, chế tạo nó. Nguyên nhân gây ra tai nạn đó chính là do lỗi của hệ thống điều khiển con tàu. Chính vì vậy, yêu cầu kiểm chứng an toàn cho các hệ thống tương tranh là hoàn toàn tất yếu. Hiện nay, song song với quá trình sản xuất phần mềm luôn có một quá trình kiểm thử (testing) phần mềm. Tuy nhiên, kiểm thử là chưa đủ vì các phương pháp kiểm thử hiện tại chỉ là kiểm tra dữ liệu đầu ra của phần mềm rồi so sánh với dữ liệu đầu vào để kiểm tra xem chương trình chạy có lỗi hay không. Chúng không hề kiểm tra được chi tiết hoạt động của chương trình và không kiểm soát được những lỗi tiềm ẩn ngay cả khi chương trình vẫn chạy đúng. Nếu phần mềm phát hành ra mà vẫn còn chứa lỗi thì nhà sản xuất phải thu hồi sản phẩm để sửa chữa. Điều này làm giảm uy tín và tiêu tốn nhiều tiền của nhà sản xuất. Chúng ta hoàn toàn có thể khắc phục được những vấn đề trên bằng cách sử dụng phương pháp hình thức để đặc tả và kiểm chứng những phần mềm đòi hỏi tính an toàn cao, nhất là các phần mềm tương tranh. Cách tiếp cận của khóa luận là: Trước hết, phải đảm bảo có một thiết kế đúng, chính xác bằng cách đặc tả thiết kế bằng FSP[1] và sử dụng công cụ LTSA[1][4] để kiểm chứng thiết kế đó. Sau khi thiết kế đã được kiểm tra và thẩm định tính đúng đắn, chúng ta tiến hành cài đặt chương trình. Sau khi đã xây dựng xong phần mềm, có một câu hỏi đặt ra là liệu cài đặt có đúng với thiết kế không? Chúng ta đã có công cụ để kiểm tra tính đúng đắn của thiết kế vì vậy giải pháp cho bài toán này chính là chuyển mã nguồn của cài đặt thành chính mô hình được đặc tả bằng FSP và sử dụng công cụ LTSA để kiểm chứng. Với cách tiếp cận này, ta có được một quy trình kiểm chứng đầy đủ hai chiều, có tính hệ thống từ pha kiểm thử đến pha cài đặt.