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
