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

SPIN and specifying and verifying of concurrent systems and reactive systems 1 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ẩn SPIN and specifying and verifying of concurrent systems and reactive systems 2 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 3 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] 2. PROMELA (Protocol/ Process Meta LAnguage) PROMELA là một ngôn ngữ mô hình xác minh ngôn ngữ. Ngôn ngữ cho phép việc tạo ra tính năng động của quá trình đồng thời để mô hình hóa hệ thống, ví dụ, hệ thống phân phối. Trong các mô hình PROMELA, thông tin liên lạc thông qua các kênh tin nhắn có thể được xác định là đồng bộ (ví dụ, render-vous port (điểm hẹn)), hoặc không đồng bộ (tức là có bộ đệm). Mô hình PROMELA có thể được phân tích với các mô hình kiểm tra SPIN, để xác minh rằng hệ thống mô hình sản xuất các hành vi mong muốn[2]. PROMELA chương trình bao gồm các quy trình, các kênh tin nhắn, và các biến. Quá trình này là các đối tượng toàn cục, đại diện cho các thực thể đồng thời của hệ thống phân phối. Kênh truyền tin nhắn và các biến thể được khai báo toàn cục hoặc tại địa phương trong một quá trình. Quy trình xác định hành vi, các kênh và các biến toàn cục xác định môi trường trong đó các quá trình chạy.[2] PROMELA là đầu vào của SPIN, nó tương tự ngôn ngữ C[4]. SPIN and specifying and verifying of concurrent systems and reactive systems 5 3. Concurrent system( Hệ thống đồng thời) Hệ thống đồng thời là hệ thống bao gồm các yếu tố có thể hoạt động đồng thời với nhau: các tiến trình đồng thời, các luồng đồng thời…. Mỗi tiến trình được xem như là một hệ thống phản ứng. Ví dụ: một quá trình có thể liên tục tương tác với môi trường của nó. Hầu hêt, đó đề là các ứng dụng trên hệ điều hành đa nhiệm, như RTOS(Real-Time Operate System).[5] Các tiến trình có thể giao tiếp với nhau thông qua môi trường. Điểm chung của hệ thống đồng thời là các hành vi phụ thuộc vào các quá trình khác trong hệ thống[9]. Các quá trình trong một hệ thống đồng thời có thể tương tác với nhau trong khi các quá trình đó đang thực hiện. Cho nên, số lượng các đường dẫn thực thi có thể có trong hệ thống có thể là rất lớn, và kết quả kết quả có thể là không xác định. Đồng thời sử dụng các nguồn tài nguyên chia sẻ có thể là một nguồn bất định dẫn đến các vấn đề như deadlock , và thiếu tài nguyên[6]. Các thiết kế của hệ thống đồng thời thường đòi hỏi phải tìm kiếm kỹ thuật đáng tin cậy trong việc phối hợp thực hiện của nó, trao đổi dữ liệu, cấp phát bộ nhớ, và lập kế hoạch thực hiện để giảm thiểu thời gian phản ứng và được tối ưu hóa[6]. 4. Reactive system(Hệ thống phản ứng) Một hệ thống phản ứng là một hệ thống thay đổi hành động của mình, đầu ra, điều kiện và trạng thái nhằm đáp ứng với các kích thích từ bên ngoài nó. Hệ thống này có thể tự định hướng hoặc được điều khiển định hướng để phản ứng lại với các kích thích bên ngoài đó. Hệ thống phản ứng được phát triển thông qua các hệ thống kĩ thuật chuyên ngành.[7] Điều kiện đầu vào của một hệ thống phải hồi luôn không được sẵn sàng, tức là, luôn không thể biết trước chính xác đầu vào, khác với việc cộng trừ 2 số: luôn biết được đầu vào. Một loại quan trọng nhất của hệ thống phản ứng là tương tác hệ thống. Các hệ thống này có thể phản ứng với các sự kiện bằng cách cung cấp đầu ra cho người sử dụng và lịch sử hoạt động của nó. Sản phẩm đầu ra có thể phản hồi các sự kiện lịch sử hoặc dấu hiệu về tình trạng hệ thống.[7] Một vài ví dụ về reactive system[8]: - Hệ thống điều khiển nhúng: điện thoại, ô tô, máy bay… - Hệ thống điều khiển tiến trình: điều khiển máy móc, rô-bốt… - Hệ điều hành máy tính và mạng. - Hệ thống giao diện người dùng. SPIN and specifying and verifying of concurrent systems and reactive systems 6 II. Nội dung Trước khi bắt đầu vào nội dung chính, chúng tôi đưa ra một mô hình Client-Server, bao gồm: một Server và hai Client. Mục đích là để hình dung một cách rõ ràng về hệ thống mà chúng tôi sẽ giới thiệu. Qua đó, chứng minh SPIN hỗ trợ cho việc quy định xác minh hệ thống đồng thời, hệ thống phản ứng. 1. Mô hình hệ thống máy khách-máy chủ - Hệ thống với 1 server và 2 clients: Ở đây có 3 tiến trình xảy ra đồng thời, thực hiện các chức năng của hệ thống. - Server quản lí một nguồn tài nguyên: Một đối tượng mà có thành phần (máy khách) có thể sử dụng bất cứ lúc nào. Ở đây, chúng tôi chỉ dùng 1 tài nguyên là: “MESSAGE”. - Client yêu cầu tài nguyên, nhận tài nguyên và sử dụng nó: Server sẽ bảo đảm rằng, cả 2 Client ko sử dụng cùng tài nguyên cùng 1 lúc. Server sẽ là người quyết định trả lời yêu cầu. 1.1. Xây dựng hệ thống mong muốn - Không bao giờ xảy ra trường hợp cả hai client cùng nhận tài nguyên tại 1 thời điểm. - Server sẽ chỉ chia sẻ tài nguyên cho 1 client, hai client thay nhau nhận tài nguyên. - Nếu client yêu cầu tài nguyên, thì ngay sau đó, client đó sẽ nhận được tài nguyên mong muốn. - Mỗi thành phần của hệ thống thực hiện chương trình riêng của mình. - Nhiều chương trình có thể cùng tồn tại tại mỗi thời điểm tại 1 khoảng thời gian. 1.2. Mô tả chi tiết hệ thống 1.2.1. Client - Gồm có 3 biến là: pc, request, answer. - Biến pc đại diện cho các chương trình truy cập. - Biến request là bộ đệm cho các yêu cầu xuất đi: Chứa các yêu cầu của Client tới máy chủ. Client Server Client Yêu cầu Yêu cầu Trả lời Trả lời SPIN and specifying and verifying of concurrent systems and reactive systems 7 - Biến answer là bộ đệm cho các yêu cầu đến: Chờ đợi 1 yêu cầu từ máy chủ đến. - Mã chương trình: Fig 1: Mã cho Client bằng ngôn ngữ PROMELA - Hệ thống hoạt động: Client(ident): param ident begin loop ... sendRequest() receiveAnswer() ... // critical region sendRequest() endloop end Client 1.2.2. Server - Gồm có các biến: given, waiting , sender , rbuffer , sbuffer. - Không có chương trình truy cập. - Server sử dụng các giá trị của người gửi để kiểm tra xem thời gian Server nhận yêu cầu hoặc Server trả lời. - Biến given, waiting , sender: nhận yêu cầu, chờ đợi yêu cầu, gửi trả lời. - Biến rbuffer: Bộ đệm cho các yêu cầu gửi từ khách hàng i. - Biến sbuffer: Bộ đệm cho câu trả lời đi cho khách hàng i. - Mã chương trình: proctype client(byte id) { do :: true -> request[id-1] ! MESSAGE; W: answer[id-1] ? MESSAGE; C: skip; // the critical region request[id-1] ! MESSAGE od; } proctype server() { unsigned given: 2 = 0; unsigned waiting : 2 = 0; SPIN and specifying and verifying of concurrent systems and reactive systems 8 F i g 3 . Fig 2: Mã cho server bằng ngôn ngữ PROMELA - Hệ thống hoạt động: Server: local given, waiting, sender begin given := 0; waiting := 0 loop sender := receiveRequest() if sender = given then if waiting = 0 then given := 0 else unsigned sender : 2; do :: true -> /* receiving the message */ R: if :: request[0] ? MESSAGE -> S1: sender = 1 :: request[1] ? MESSAGE -> S2: sender = 2 fi; /* answering the message */ if :: sender == given -> if :: waiting == 0 -> given = 0 :: else -> given = waiting; waiting = 0; answer[given-1] ! MESSAGE fi; :: given == 0 -> given = sender; answer[given-1] ! MESSAGE :: else waiting = sender fi; od; } SPIN and specifying and verifying of concurrent systems and reactive systems 9 given := waiting; waiting := 0 sendAnswer(given) endif elsif given = 0 then given := sender sendAnswer(given) else waiting := sender endif endloop end Server 1.2.3. Mô phỏng hệ thống thực thi của mô hình Server-Client Fig 3: Kết quả mô phỏng mô hình Server-Client 2. Quy định và xác minh hệ thống đồng thời Hệ thống đồng thời là một phần của khoa học máy tính, được đưa giới thiệu lần đầu tiên trong báo cáo của Carl Adam Petri trong hội thảo về sự hoạt động của Petri Nets trong những năm 1960[6]. Hệ thống đồng thời gồm có các thành phần hoạt động đồng thời với nhau tại một thời điểm và có thể tương tác được với nhau. SPIN với ngôn ngữ đầu vào là PROMELA, có khả năng quy định và xác minh hệ thống đồng thời tự động thay đổi số các tiến trình tương tác, nơi mà các tiến trình có thể được đồng bộ hóa hoặc không đồng bộ hóa. Trong mô hình Server-Client đã đưa ra, chúng tôi sẽ nêu rõ sự hỗ trợ của PROMELA trong việc quy định và xác minh hệ thống đồng thời. SPIN and specifying and verifying of concurrent systems and reactive systems 10 2.1.Quy định hệ thống PROMELA là ngôn ngữ đầu vào của SPIN, có thể dùng để quy đinh và xác minh hệ thống đồng thời dựa trên cú pháp và ngữ nghĩa của mình. Dựa trên 4 yếu tố[10]: - Đa luồng, đa tiến trình. - Một ít câu lệnh điều khiển và không có hiệu ứng(no-effect). - Cấu trúc dữ liệu hữu hạn và có ràng buộc cố định. - Đồng bộ hóa/không đồng bộ hóa và giao tiếp qua các kênh tin nhắn. 2.1.1. Đa luồng, đa tiến trình Trạng thái của một biến hoặc một kênh tin nhắn chỉ có thể được thay đổi hoặc được kiểm tra bằng các quá trình. Hành vi của các quá trình được định nghĩa bằng câu lệnh proctype: proctype pname(chan in, out; byte id) { statements; } Một quá trình được định nghĩa bằng proctype, có thể thực hiện chức năng với các quá trình khác và không phụ thuộc vào tốc độ của hành vi. Các quá trình có thể giao tiếp với các quá trình khác thông qua môi trường hoặc biến toàn cục. Ngay cả khi đang thực hiện chức năng của mình, các quá trình cũng có thể giao tiếp được với nhau. Các quá trình có thể được tạo ra từ một proctype. Với hệ thống Server-Client đã đưa ra, chúng tôi xây dựng hệ thống với vòng lặp vô hạn giữa gửi và nhận của máy khách và máy chủ. Qua đó có thể thấy, có 3 tiến trình cùng nhau hoạt động: - Gửi: Máy khách 1 gửi yêu cầu, máy khách 2 gửi yêu cầu, máy chủ nhận tin. - Nhận: Máy chủ gửi tài nguyên, máy khách 1 nhận, máy khách 2 chờ nhận. Trong PROMELA, các tiến trình được khởi chạy bằng câu lệnh run. Cụ thể với hệ thống Server-Client: run client(1); run client(2); SPIN and specifying and verifying of concurrent systems and reactive systems 11 run server(); 2.1.2. Các câu lệnh điều khiển - Vòng lặp vô hạn Để mô tả một cấu trúc lặp đi lặp lại trong PROMELA, ta dùng cấu trúc lệnh: do ::statement ::statement →break; od sau khi hoàn tất, việc hoạt động của lệnh này sẽ khiến cho cấu trúc lặp đi lặp lại. Việc lặp đi lặp lại đó chỉ kết thúc khi có một giá trị làm cho cấu trúc bị phá vỡ. Trong mô hình Server-Client, chúng tôi xây dựng một hệ thống kết nối giữa nhận và gửi được lặp lại vô điều kiện. Như mô hình máy khách ở Fig 1, khối các câu lệnh nằm giữa do…od được thực hiện với việc lặp này: do :: true -> request[id-1] ! MESSAGE; W: answer[id-1] ? MESSAGE; C: skip; // the critical region request[id-1] ! MESSAGE od; - Lựa chọn if-else Cấu trúc điều khiển đơn giản nhất là cấu trúc lựa chọn if-else. Được xây dựng bởi cấu trúc lệnh: if :: conditions 1 → option 1 :: conditions 2 → option 2 …. fi SPIN and specifying and verifying of concurrent systems and reactive systems 12 khối câu lệnh lựa chọn nằm trong từ khóa if..fi, mỗi điều kiện bắt đầu bằng dấu “::”, nếu điều kiện phù hợp thì sẽ thực hiện câu lệnh ở đằng sau dấu “→”. Ở mô hình server nêu ra trong Fig 2, khối câu lệnh lựa chọn được sử dụng: if :: request[0] ? MESSAGE -> S1: sender = 1 :: request[1] ? MESSAGE -> S2: sender = 2 fi; - Nhảy vô điều kiện Cấu trúc nhảy vô điều kiện: do ::statement 1 ::statement 2 → goto label; od label: //statement skip; 2.1.3. Cấu trúc dữ liệu Định nghĩa cấu trúc trong PROMELA dùng câu lệnh typedef, để giới thiệu một kiểu mới của đối tượng dữ liệu. Tên kiểu mới có thể được sử dụng để khai báo và khởi tạo đối tượng, dữ liệu mới có thể được sử dụng trong bất kỳ trường hợp phù hợp một cách rõ ràng: typedef mystruct { type field1; type field2; … } SPIN and specifying and verifying of concurrent systems and reactive systems 13 Cách truy vấn một miền được định nghĩa bởi typedef tương tự ngôn ngữ C. Ví dụ như sau: mystruc x; x.filed1 = 2; 2.1.4. Tính đồng bộ và giao tiếp qua các kênh tin nhắn Kênh tin nhắn dùng để chuyển giao dữ liệu từ một quá trình qua quá trình khác. Khai báo một kênh tin nhắn: chan = [dim] of {type} câu lệnh với ý nghĩa: tạo ra 1 bộ đệm có thể lưu [dim] số tin nhắn kiểu {type} vào biến . Câu lệnh: qname ! expr; dùng để gửi một giá trị của expr tới kênh tin nhắn với tên là qname. Câu lệnh: qname ? msg; dùng để nhận một tin nhắn được lưu trong biến msg; Một rendervous port(điểm hẹn) được định nghĩa tương tự như của kênh tin nhắn nhưng có điểm khác biệt là số tin nhắn lưu giữ bằng 0; chan = [0] of {type} định nghĩa một rendervous port có thể vượt quá giá trị của kiểu {type}. Tương tác tin nhắn thông qua rendervous port như vậy là bởi định nghĩa đồng bộ, nghĩa là người gửi hoặc nhận (một trong đó tại vị trí đầu tiên tại kênh) sẽ chặn cho người nhận hoặc gửi đến thứ hai . 2.2. Xác minh hệ thống Để xác minh một hệ thống, chúng ta cần quan tâm tới quy định của hệ thống đó, Trong báo cáo này, công việc của chúng tôi là đưa ra một ví dụ về SPIN, qua đó xác định các quy định của hệ thống. Đối với hệ thống đơn giản chỉ gồm Server-Client chúng ta sẽ phải quan tâm tới ngữ nghĩa của hệ thống. Điều này có nghĩa là: chúng ta phải xác định được các yếu tố[11]: SPIN and specifying and verifying of concurrent systems and reactive systems 14 - Không gian trạng thái của hệ thống(hữu hạn hoặc vô hạn). - Điều kiện trạng thái của hệ thống( xác định được yếu tố đầu vào). - Mối quan hệ chuyển tiếp vào các trạng thái.  Không gian trạng thái của hệ thống bao gồm không gian trạng thái thành phần.  Client + Không gian trạng thái: state := pc x N1 x N2 + Hệ thống bao gồm các biến: pc, request, answer. - Pc đại diện cho các chương trình truy cập. - Request đại diện cho bộ đệm yêu cầu gửi đi - Answer đại điện cho bộ đệm nhận yêu cầu tới.  Server + Không gian trạng thái: state := (N3) 3× ({1, 2} → N2) 2 . + Hệ thống bao gồm các biến: given, waiting , sender , rbuffer , sbuffer . - Biến given, waiting , sender: nhận yêu cầu, chờ đợi yêu cầu, gửi trả lời. - Biến rbuffer: Bộ đệm cho các yêu cầu gửi từ khách hàng i. - Biến sbuffer: Bộ đệm cho câu trả lời đi cho khách hàng i.  Mối quan hệ chuyển tiếp giữa các trạng thái: Ext := {REQ1, REQ2, ANS1, ANS2} + Quá trình chuyển đổi của nhãn REQ, truyền một yêu cầu từ máy khách thứ i tới máy chủ. - Cho phép khi request ≠ 0 ở máy khách i. - Thực hiện ở máy khách i: request’ = 0; - Thực hiện ở máy chủ: rbuffer’(i) = 0; + Quá trình chuyển đổi của nhãn ANS, truyền dữ liệu từ máy chủ về máy khách i: - Cho phép khi sbuffer(i) ≠ 0 ở máy chủ. - Thực hiện ở máy chủ sbuffer’(i) = 0. - Thực hiện ở máy khách i: answer = 0; 3. Quy định và xác minh hệ thống phản ứng Một hệ thống phản ứng lần đầu tiên được định ngh