tailieunhanh - Đề 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. | TRƯỜNG ĐẠI HỌC CÔNG NGHỆ -- 2 - 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ẩn SPIN 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ộ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. Bên cạnh đó ngôn ngữ này cũng hỗ trợ việc quy định xác minh 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ồm mộ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ục Contents Tóm Mục I. Khái 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 II. Nội 1. Mô hình hệ thống máy khách-máy . Xây dựng hệ thống mong . Mô tả chi tiết hệ . . . Mô phỏng hệ thống thực thi của mô hình 2. Quy định và xác minh hệ thống đồng . Quy định hệ . Xác minh hệ 3. Quy định và xác minh hệ thống phản ứng. 14 . Quy định hệ . Xác minh hệ III. Kết IV. Các tài liệu tham SPIN and specifying and verifying of concurrent systems and reactive systems