Đề tài: “SPIN and specifying and verifying in concurrent systems, reactive systems”

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.
Nội dung trích xuất từ tài liệu:
Đề tài: “SPIN and specifying and verifying in concurrent systems, reactive systems” TRƯỜNG ĐẠI HỌC CÔNG NGHỆ ---------- BÀI BÁO CÁO CÁC VẤN ĐỀ HIỆN ĐẠI CỦA CÔNG NGHỆ PHẦN MỀM Đề tài: “SPIN and specifying and verifying in concurrent systems, reactive systems” Giảng viên: Đặng Đức Hạnh Vũ Diệu Hương Thành viên: Lê Đức Tiến Nguyễn Lê DuẩnSPIN and specifying and verifying of concurrent systems and reactive systems 1 Tóm tắt 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ộtcá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óahoặ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ácminh 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ồmmộ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.SPIN and specifying and verifying of concurrent systems and reactive systems 2 Mục lụcContentsTóm tắt ............................................................................................................................... 2Mục lục............................................................................................................................... 3 Khái niệm ................................................................................................................... 4I. 1. SPIN ( Simple Promela INterpreter)..................................................................... 4 2. PROMELA (Protocol/ Process Meta LAnguage) ................................................ 4 3. Concurrent system( Hệ thống đồng thời) ............................................................. 5 4. Reactive system(Hệ thống phản ứng).................................................................... 5 Nội dung ................................................................................................................. 6II. Mô hình hệ thống máy khách-máy chủ............................................................... 6 1. 1.1. Xây dựng hệ thống mong muốn ...........................................................................6 1.2. Mô tả chi tiết hệ thống ........................................................................................6 1.2.1. Client ........................................................................................................ 6 1.2.2. Server........................................................................................................ 7 Mô phỏng hệ thống thực thi của mô hình Server-Client ..................... 9 1.2.3. Quy định và xác minh hệ thống đồng thời.......................................................... 9 2. 2.1. Quy định hệ thống ............................................................................................. 10 2.2. Xác minh hệ thống ............................................................................................. 13 Quy định và xác minh hệ thống phản ứng........................................................ 14 3. 3.1. Quy định hệ thống ............................................................................................. 15 3.2. Xác minh hệ thống ............................................................................................. 17 Kết luận ................................................................................................................ 17III. Các tài liệu tham khảo ........................................................................................ 18IV.SPIN and specifying and verifying of concurrent systems and reactive systems 3I. Khái niệm 1. SPIN ( Simple Promela INterpreter) SPIN là 1 công cụ dùng để kiểm tra tính lo-gic của của một đặc điểm kĩ thuật của hệ thống phân phối, đặc biệt là các giao thức truyền thông dữ liệu. Hệ thống được miêu tả bằng một ngôn ngữ mô hình có tên là PROMELA[1]. Ngôn ngữ này tạo ra sự năng động của các quá trình đồng thời. Với một hệ thống được quy đinh bởi PROMELA, SPIN có thể thực hiện mô phỏng ngẫu nhiên hoặc tương tác hệ thống; hay đơn giản là chỉ tạo ra một chương trình bằng ngôn ngữ C để nhanh chóng xác minh các hệ thống không gian trạng thái một cách đầy đủ, nhanh chóng[2]. Trong quá trình xác minh, SPIN báo cáo về deadlocks (sự bế tắc), unspecified receptions (các tiếp nhận không xác định), flags incompleteness, race conditions (điều kiện), các giả định không có cơ sở về tốc độ tương đối của các quá trình[1]. SPIN cũng có thể được sử dụng để chứng minh tính chính xác của hệ thống bất biến và nó có thể tìm thấy các chu kỳ thực hiện không tiến bộ.Cuối cùng, nó hỗ trợ việc xác minh các ràng buộc thời gian thời gian tuyến tính.[2] SPIN đã được sử dụng để theo dõi các lỗi thiết kế trong thiết kế hệ thống phân phối, chẳng hạn như hệ điều hành, các giao thức truyền dữ liệu, hệ thống chuyển mạch, các thuật toán đồng thời, tín hiệu giao thức đ ...