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

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].

Đ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”.
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)
{

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

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

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

biến <name>.
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 <name> = [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 N
1

}
+ 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ĩa bởi Pnueli và Harel: một hệ thống
phản ứng là một hệ thống có vai trò duy trì sự tương tác liên tục với môi trường, chứ
SPIN and specifying and verifying of concurrent systems and reactive systems 15

không phải chỉ để cung cấp sản phẩm đầu ra[8]. Điều này có nghĩa rằng: một hệ thống
phản ứng không quan tâm tới kết quả đầu vào/ đầu ra, mà chỉ quan tâm tới sự tương tác
với môi trường của nó. Hệ thống phản ứng điển hình được mô tả qua các đặc tính
sau[12]:
- Nó liên tục tương tác với môi trường của nó, bằng cách sử dụng các yếu tố đầu
vào và đầu ra.
- Các yếu tố đầu vào và đầu ra thường không đồng bộ, có nghĩa là chúng ta có thể
đến và thay đổi giá trị tại bất kỳ thời điểm nào.
- Hoạt động và phản ứng đối với đầu vào thường phản ánh yêu cầu thời gian
nghiêm ngặt.
- Nó có rất nhiều kịch bản có thể hoạt động, tùy thuộc vào chế độ hiện hành hoạt
động và các giá trị hiện tại của dữ liệu của nó cũng như hành vi trong quá khứ
của nó.
- Thông thường, nó không phải là dự kiến sẽ chấm dứt.
- Nói chung, nó bao gồm nhiều quá trình tương tác hoạt động song song

Yêu cầu sẽ được lưu lại tại bộ đệm của máy chủ:
ch ! <expr1><expr2>…<exprn>
Ý nghĩa của câu lệnh là: gửi giá trị biểu hiện expr1, expr2… tới kênh tin nhắn với
tên là ch. Trong mô hình của chúng tôi, nó được khai báo:
request[id-1] ! MESSAGE
answer[given-1] ! MESSAGE
Máy chủ nhận tin nhắn yêu cầu từ bộ đệm và quyết định gửi tài nguyên cho máy
khách đã gửi tin nhắn yêu cầu:
ch ? <var1><var2>…<varn>
Các tin nhắn được lưu giữ tại bộ đệm trong các biến var1, var2…. Cơ chế hoạt động
gửi tin nhắn là first-in first-out: nhận vào 1 và gửi đi 1, máy khách nào gửi tin nhắn
trước thì sẽ được máy chủ nhận trước và được trả lời trước.
answer[id-1] ? MESSAGE
request[1] ? MESSAGE
SPIN and specifying and verifying of concurrent systems and reactive systems 17

Khi bộ đệm được lấp đầy với khả năng của mình, tức là số lượng tin nhắn yêu cầu
cung cấp tài nguyên của máy khách đã đạt tối đa, lúc này hành vi của hệ thống sẽ
được đồng bộ hóa, máy chủ sẽ tự động ngăn chặn việc gửi tin tiếp theo.
Như vậy, khi bộ đệm không đầy, máy chủ lưu tin nhắn vào bộ đệm. Khi bộ đệm
nhận của máy chủ đầy, máy chủ sẽ phản ứng lại bằng cách ngăn không cho máy
khách tiếp tục gửi yêu cầu, sau đó lấy tin nhắn từ bộ đệm rồi xử lí gửi tài nguyên cho
máy khách yêu cầu.
3.2. Xác minh hệ thống
Channel
i ,j
= (ICH , RCH ).
+ Không gian trạng thái: state := <Value>
- Trình tự thực hiện của các kiểu giá trị
+ Điều kiện trạng thái của hệ thống( xác định được yếu tố đầu vào).

[2] “PROMELA”, được sao chép từ .
[3] Ian Barland, “Promela and SPIN Reference”, được sao chép từ trang
.
[4] Theo C. Ruys, “SPIN beginer tutorial”, SPIN 2002 Workshop, Grenoble, 11-13 April
2002, 6.
[5] P. Godefroid, "Partial Order Methods for the Verification of Con-current Systems, 1.
[6] “Concurrent system”, được sao chép từ

[7] “Reactive system”, được sao chép từ
[8] Naoshi Uchihira, “A Programming Environment for Reactive and Concurrent
SystemsUsing Petri Nets and Temporal Logic”, 30.
[9] Deepak D'Souza, đọc từ “Model-Checking Concurrent Programs using Spin”, 3.
[10] Wolfgang Ahrendt, Josef Svenningsson, Meng Wang, “Software Engineering using
Formal Methods”,3.
[11] Tham khảo từ khóa học

[12] Nataliya Yustinova, “Abstractions and Static Analysis for Verifying Reactive
Systems”, 2.