Luận Văn SPIN and specifying and verifying in concurrent systems, reactive systems

Mục lục
Contents
Tóm tắt . 2
Mục lục . 3
I. Khái niệm . 4
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 dung . 6
1. Mô hình hệ thống máy khách-máy chủ . 6
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
1.2.3. Mô phỏng hệ thống thực thi của mô hình Server-Client . 9
2. Quy định và xác minh hệ thống đồng thời 9
2.1. Quy định hệ thống . 10
2.2. Xác minh hệ thống . 13
3. Quy định và xác minh hệ thống phản ứng 14
3.1. Quy định hệ thống . 15
3.2. Xác minh hệ thống . 17
III. Kết luận 17
IV. Các tài liệu tham khảo 18
SPIN and specifying and verifying of concurrent systems and reactive systems 4


I. 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 đường sắt, vv [1]