Phần mềm tương tranh, một phần mềm được ứng dụng rộng rãi trong các hệ thống nhúng và các hệthống điều khiển. Chúng có vai trò vô cùng quan trọng trong việc điều khiển các hệthống đó. Chỉcần một lỗi nhỏcủa phần mềm có thểgây ra hậu quả vô cùng nghiêm tr ọng vì những hệ thống này có thể trực tiếp và gián tiếp ảnh hưởng đến cuộc sống của con người. Chính vì vậy phần mềm tương tranh phải được kiểm chứng để giảm thiểu tối đa lỗi của chương trình. Vì những lý do đó, đềtài “Đặc tảvà kiểm chứng các phần mềm tương tranh” đềcập tới phương pháphình thức, các lý thuyết vềmáy hữu hạn trạng thái(Finite State Process, FSP)và sửdụng máy hữu hạn trạng tháiđểđặc tảthiết kếvà mã nguồn của phần mềm tương tranh. Từđó sửdụng công cụphân tích máy hữu hạn trạng thái đểkiểm chứng xem thiết kếvà mã nguồn của phần mềm có lỗi và chạy đúng theo yêu cầu không. Do thời gian có hạn nên phần thực nghiệm trong khóa luận này em chỉthực hiện kiểm chứng một applet được viết bằng Java. Thiết kếcủa bài toàn đã được đặc tảsẵn bằng FSP. Nhiệm vụcủa em là kiểm chứng xem thiết kếđó có lỗixác hay không và chuyển mã nguồn Java của applet thành FSP đểkiểm chứng xem mã nguồn cóchạy đúng theo thiết kếhay không