1 Số hóa bởi Trung tâm Học liệu

ĐẠI HỌC THÁI NGUYÊN
TRƢỜNG ĐẠI HỌC CÔNG NGHỆ THÔNG TIN VÀ TRUYỀN THÔNG Trần Quốc Tuấn CÁC KỸ THUẬT ĐẶC TẢ VÀ KIỂM CHỨNG
CHO CÁC BÀI TOÁN TƢƠNG TRANH

Chuyên ngành: Khoa học máy tính
Mã số: 60 48 01

LUẬN VĂN THẠC SĨ KHOA HỌC MÁY TÍNH NGƢỜI HƢỚNG DẪN KHOA HỌC
PGS TS Nguyễn Xuân Huy

Thái Nguyên, năm 2014
2
Tôi gửi lời cảm ơn đến Ban giám hiệu, các Thầy, Cô phòng Đào tạo sau
đại học, trƣờng Đại học Công nghệ thông tin và truyền thông – Đại học Thái
Nguyên đã quan tâm đến lớp Cao học K11C đặt tại Hải Phòng.
Tôi gửi lời cảm ơn đến Ban giám hiệu Trƣờng Đại học Hải Phòng, khoa
Công nghệ thông tin, đã tạo điều kiện về thời gian, kinh phí để tôi hoàn thành
khóa học.
Tôi muốn cảm ơn gia đình, bạn bè cũng nhƣ các đồng nghiệp đã chia sẻ
và tạo điều với tôi những lúc khó khăn nhất để tôi có thể hoàn thành khóa học
này. 4 Số hóa bởi Trung tâm Học liệu

MỤC LỤC

LờI CAM ĐOAN 2
LờI CảM ƠN 3
MụC LụC 4
DANH MụC Từ VIếT TắT 6
DANH MụC BảNG 7
DANH MỤC HÌNH VẼ 8
LỜI NÓI ĐẦU 9
CHƢƠNG 1 11
MộT Số BÀI TOÁN TƢƠNG TRANH 11
1.1. Giới thiệu 11
1.2. Bài toán Đọc-Ghi 14
1.3. Bài toán Cung-Tiêu (producer-consumer problem) 14

3.2.2 Đặc tả FSP cho bài cung cấp tiêu thụ 41
3.3. Kết luận 42
CHƢƠNG 4 43
CÀI ĐẶT THỰC NGHIỆM 43
4.1. Mô hình Đọc và Ghi đơn giản 43
4.2. Thuật toán kiểm tra tính khả tuần tự 44
4.3. Nghi thức khóa chốt hai pha 47
4.4. Mô hình Đọc và Đọc-ghi 47
4.5. Thuật toán kiểm tra tính khả tuần tự của các lịch biểu với các khóa đọc
và đọc-ghi. 48
4.6. Cài đặt thực nghiệm 50
4.6.1. Kiểm tra tính khả tuần tự trong mô hình Đọc-Ghi đơn giản 50
4.6.2. Kiểm tra tính khả tuần tự trong mô hình Đọc và Đọc-ghi 53
KếT LUậN 54
TÀI LIệU THAM KHảO 55 6 Số hóa bởi Trung tâm Học liệu DANH MụC Từ VIếT TắT

Từ viết tắt
Từ đầy đủ
Diễn giải
FSP
Finite state process


DANH MụC BảNG

Bảng 1.1. Mô tả các bƣớc chuyển khoản của tiến trình P 11
Bảng 1.2. Mô tả các bƣớc chuyển khoản của tiến trình Q 11
Bảng 1.3. Mô tả thực hiện đan xen hai tiến trình P và Q 12
Bảng 3.1. Kết quả chứng minh 38
Bảng 3.2. Đặc tả FSP cho bài toán đọc ghi 39
Bảng 3.3. Đặc tả FSP cho bài toán cung cấp tiêu thụ 41

8 Số hóa bởi Trung tâm Học liệu DANH MỤC HÌNH VẼ

Hình 1.1.Mô tả bài toánĐọc-Ghi bằng hai tiến trình 13
Hình 1.2.Đặc tả bài toán Cung-Tiêu 14
Hình 2.1. Kiểm chứng mô hình 18
Hình 2.2. Mô hình Event-B với máy và ngữ cảnh 20
Hình 2.3. Cấu trúc tổng quát của sự kiện 22
Hình 2.4.Máy trạng thái biểu diễn các hành động bật tắt bóngđèn 23
Hình 2.5.Biểu diễn máy trạng thái
cho các hành động của một giảng viên 24
Hình 2.6.Máy trạng thái biểu diễn tiến trình tuần tự BOMP 27

những thiệt hại về mặt kinh tế mà còn làm tổn thất trực tiếp sinh mạng con
ngƣời. Đến nay, trong công nghiệp phần mềm đã có nhiều phƣơng pháp khác
nhau đƣợc đề xuất và phát triển để giảm lỗi phần mềm từ pha thiết kế đến cài
đặt nhƣ các phƣơng pháp kiểm chứng (verification) và kiểm thử (testing)[1].
Các phần mềm (chƣơng trình) tƣơng tranh thƣờng gồm nhiều tiến trình,
mỗi tiến trình là một chƣơng trình tuần tự thực hiện một tập các câu lệnh tuần
tự. Các tiến trình thƣờng cộng tác với nhau thông qua các biến chia sẻ hoặc cơ
chế truyền thông điệpđể đồng bộ hay đểtrao đổi dữ liệu.
Truy xuất bộ nhớ dùng chung là một trong những hoạt động tƣơng tranh
giữa các tiến trình. Vấn đề tƣơng tranh trên một tài nguyên dùng chung là vấn
đề lớn cần phải giải quyết triệt để vì nếu nhiều tiến trình truy xuất đồng thời
vàomộttài nguyên dùng chung màkhông có sự kiểm soát thì dễ xảy ra lỗi làm
hƣ hỏng tài nguyên.
Các phƣơng pháp kiểm thử (testing) phần mềm chỉ phát hiện đƣợc các lỗi
ở mức mã nguồn, chƣa phát hiện đƣợc các lỗi ở mức logic nhƣ các lỗi thiết
kế. Với các hệ thống tƣơng tranh việc kiểm thử nhƣ quan sát các dữ liệu vào
ra là không khả thi do mỗi lần thực thi các phần mềm tƣơng tranh thƣờng cho
các kết quả đầu ra là khác nhau. Hơn nữa, việc kiểm chứng phần mềm tại mức
10 Số hóa bởi Trung tâm Học liệu

thiết kế nhằm phát hiện lỗi sớm, giảm chi phí phát triển. Chính vì vậy vấn đề
kiểm chứng bài toán tƣơng tranh tại mức thiết kế là cần thiết.
Đề tài tập trung tìm hiểu các kỹ thuật, phƣơng pháp, công cụ tự động kiểm
chứng một số bài toán tƣơng tranh ở mức thiết kế.Các mục tiêu đƣợc đặt ra
nhƣ sau:
Khảo sát, đánh giá tổng hợp kiến thức, kết quả nghiên cứu trong lĩnh
vực kiểm chứngphần mềm tƣơng tranh, các vấn đề nghiên cứu liên quan.

Các tiến trình trong một hệ thống tƣơng tranh thƣờng phải đƣợc đồng bộ
hóa. Sự đồng bộ hóa giữa các tiến trình đƣợc phân thành hai loại cộng tác
hoặc cạnh tranh. Một trong những ví dụ điển hình về sự cộng tác giữa các tiến
trình là vấn đề cung cấp-tiêu thụ (producer-consumer) với hai tiến trình
producer và consumer. Trong đó tiến trình producer cung cấp các phần tử dữ
liệu, sau đó tiến trình consumer sẽ tiêu thụ nó. Cấp phát tài nguyên cho các
tiến trình phải giải quyết vấn đề xung đột khi nhiều tiến trình cùng muốn sử
dụng tài nguyên chia sẻ nhƣ dữ liệu, tệp, máy in, Tính nhất quán của dữ liệu
sẽ bị phá vỡ nếu hai tiến trình đọc-ghi cùng cập nhật chung một tệp tại cùng
một thời điểm.
Ví dụ[2], giả sử trên máy chủ lƣu trữ các tài khoản A, B và C với các giá
trị hiện có là A = B = C = 10 triệu đồng. Máy chủ cần thực hiện đồng thời hai
tiến trình P và Q nhƣ sau:
Tiến trình P: chuyển 1 triệu tiền từ tài khoản A sang tài khoản B.
Tiến trình Q: chuyển 1 triệu tiền từ tài khoản C sang tài khoản B.
Giả sử, thực hiện tuần tự hai tiến trình P,Q. Tiến trình P đƣợc thực hiện
trƣớc sau đó đến tiến trình Q đƣợc thực hiện.

12 Số hóa bởi Trung tâm Học liệu

Bảng 1.1. Mô tả các bƣớc chuyển khoản của tiến trình P
Tiến trình P
Diễn giải
A
X
B
Y

Open B;
Mở mục B 10

read B,Y;
Đọc dữ liệu từ B vào Y
10
Y := Y+1;
Cộng thêm 1 vào Y
11
write Y,B;
Ghi giá trị Y từ RAM vào B 11

close B;
Đóng mục B close C;
Đóng mục C

Open B;
Mở mục B 11

read B, V;
Đọc dữ liệu từ B vào V
11
V := V+1;
Cộng thêm 1 vào V
12
write V,B;
Ghi giá trị Y từ RAM vào B


Z
V
10
10
10 1
open A;
2
read A,X;


10

6

Z := Z-1;
9

7
write X,A;

9 11
open B;
11
read B,Y;
10 12

open B;
V := V+1;

11
15
write Y,B; 11
16
close B;

Do đó vấn đề đặt ra là phải đặc tả ràng buộc về thứ tự thực hiện giữa các
tiến trình nhằm bảo đảm tính nhất quán của dữ liệu chia sẻ. Không mất tính
tổng quát, học viên mô tả vấn đề này bằng hai bài toán Đọc-Ghi và Cung-
Tiêu nhƣ trong Mục 1.2 và Mục 1.3.
1.2. Bài toán Đọc-Ghi
Bài toán Đọc-Ghi (readers-writers problem) đƣợc mô tả bằng hai tiến
trình hoạt động nhƣ sau:
Trong đó:
R: là tiến trình chỉ đọc; W: là tiến trình có thể đọc hoặc ghi; FileF là một
đơn vị dữ liệu.
Tại mỗi thời điểm, trên FileF có thể có một hoặc nhiều tiến trình chỉ đọc
(R), nhƣng không có tiến trình nào đƣợc ghi.
Tiến trình ghi (W)chỉ đƣợc thực hiện khi không có tiến trình khác nào
đang đọc hoặc đang ghi ngoài tiến trình hiện tại.
1.3. Bài toán Cung-Tiêu (producer-consumer problem)
Bài toán Cung-Tiêu là một ví dụ điển hình về sự đồng bộ hóa giữa các
tiến trình tƣơng tranh. Bài toán này có thể đƣợc mô tả thông qua hai tiến trình
thực hiện theo các nguyên tắc nhƣ sau:
FileF
R

phƣơng thức push(Q) hoặc pop(Q) để bổ sung hoặc loại bỏ các phần tử của
hàng đợi.
Khi tiến trình producer gọi phƣơng thức stop() để chuyển sang trạng thái
CLOSED thì các phần tử khác sẽ không đƣợc bổ sung hoặc loại bỏ từ hàng
đợi.
start(Q)
push(Q)
pop(Q
)
OPENED
CLOSED
stop(Q)
16 Số hóa bởi Trung tâm Học liệu

Các tiến trình producer và consumer phải bảo đảm không đẩy phần tử
dữ liệu vào hàng đợi nếu nó đã đầy và không lấy dữ liệu nếu nó rỗng.
1.4. Một số vấn đề trong chƣơng trình tƣơng tranh
Trong các chƣơng trình tƣơng tranh, có hai thuộc tính cơ bản cần phải bảo
đảm là an toàn (safety) và thực hiện đƣợc (liveness). Thuộc tính an toàn bảo
đảm chƣơng trình luôn thỏa mãn (luôn đúng) các ràng buộc của nó. Ví dụ nhƣ
ràng buộc về sự xung đột (interference) giữa các tiến trình. Thuộc tính thực
hiện đƣợc bảo đảm chƣơng trình cuối cùng sẽ thỏa mãn (sẽ đúng) các ràng
buộc của nó. Ví dụ nhƣ tính dừng của các tiến trình (process termination) và
các tiến trình khi muốn truy cập vào tài nguyên chia sẻ (shared resource) thì
cuối cùng nó sẽ truy cập đƣợc. Một số vấn đề về tƣơng tranh liên quan đến
hai thuộc tính này đƣợc mô tả nhƣ sau.
Sự xung đột (interference) xảy ra khi hai hoặc nhiều tiến trình đồng thời
Số hóa bởi Trung tâm Học liệu

CHƢƠNG 2
MộT Số PHƢƠNG PHÁP KIểM CHứNG
Trong chƣơng này luận văn trình bày một số kiến thức cơ sở về kiểm
chứng mô hình, phƣơng pháp hình thức với Event-B, máy hữu hạn trạng thái
FSP (Finite state process). Các phƣơng pháp hình thức này đƣợc sử dụng để
đặc tả và kiểm chứng một số bài toán tƣơng tranh trong chƣơng 1.
2.1. Kiểm chứng thiết kế
Đã có một vài phƣơng pháp, công cụ, đƣợc đề xuất để đặc tả và kiểm
chứng các chƣơng trình tƣơng tranh. Các nghiên cứu này đƣợc chia thành hai
hƣớng kiểm chứng thiết kế và kiểm chứng mã nguồn chƣơng trình.
Edmunds [6] đề xuất ngôn ngữ đặc tả trung gian Object-oriented
Concurrent-B(OCB) để nối liền giữa đặc tả bằng Event-B với sự cài đặt của
các chƣơng trình hƣớng đối tƣợng, tƣơng tranh. Đặc tả OCB sẽ đƣợc chuyển
tự động sang mô hình của Event-B và mã chƣơng trình Java. Các chƣơng
trình Java đƣợc chuyển đổi sẽ đƣợc kiểm chứng sự tuân thủ theo đặc tả OCB
của nó.
Ben Younes và L.J. Ben Ayed [7] đề xuất các luật để chuyển đổi từ đặc tả
bằng biểu đồ hoạt động Activity Diagram của UML sang đặc tả bằng Event-
B. Dựa vào cơ chế làm mịn dần của Event-B để đặc tả và kiểm chứng tự động
sự phân rã của các biểu đồ hoạt động của UML thỏa mãn các thuộc tính nhƣ
tắc nghẽn (deadlock), sự công bằng (fairness). Đóng góp chính của nghiên
cứu này là chuyển đổi từ một đặc tả trực quan sang hình thức và dựa vào công
cụ của nó để chứng minh tự động một mô hình thỏa mãn các thuộc tính của
nó. Tuy nhiên việc chuyển đổi chƣa đƣợc thực hiện tự động hoàn toàn, hơn
nữa nghiên cứu này mới đƣa ra một ví dụ để minh họa khả năng chuyển đổi
của nó.

đƣợc xây dựng từ hệ thống. Đặc tả các thuộc tính
cần kiểm chứng
(System properties)
Trả lời
TRUE, nếu mô hình thỏa
mãn đặc tính.
FALSE, nếu mô hình
không thỏa mãn, phản ví
dụ.
Mô hình hệ thống
(System requirements)
Công cụ kiểm chứng
(checking tool)
Hình 2.1.Kiểm chứng mô hình
20 Số hóa bởi Trung tâm Học liệu

2.3. Phƣơng pháp hình thức Event-B
B[11] là một phƣơng pháp hình thức dùng để đặc tả và kiểm chứng phần
mềm. Phƣơng pháp B dựa trên lý thuyết tập hợp, ngôn ngữ thay thế tổng quát
và logic vị từ bậc 1 (first order logic). Phƣơng pháp B hỗ trợ quá trình phát
triển phần mềm bằng cách làm mịn (refinement). Quá trình này bắt đầu bằng

tổng quát của máy bên trái và ngữ cảnh bên phải.
Trong đó:
<machine_identifier>, <context_identifier > tƣơng ứng là định danh
của máy và ngữ cảnh,
refines, extends là từ khóa làm mịn, mở rộng từ một máy và ngữ cảnh
nào đó,
sees, set là các khai báo tham chiếu đến ngữ cảnh và khai báo các tập
hợp của ngữ cảnh;
variables, constants là các khai báo biến và hằng của máy và ngữ cảnh;
invariant, axiom là các bất biến và tiên đề;
Hình 2.2. Mô hình Event-B với máy và ngữ cảnh.
<context_identifier >
extends
<context_identifier_list >
sets
<set_identifier_list >
constants
<constant_identifier_list >


theorem, events tƣơng ứng là các định lý, sự kiện. Trong đó sự kiện mô
tả một hành động sẽ đƣợc xảy ra khi điều kiện của nó đƣợc thỏa mãn.
2.3.2. Phân rã và kết hợp
Mô hình hệ thống với Event-B đƣợc bắt đầu từ các sự kiện trừu tƣợng
quan sát đƣợc có thể xảy ra trong hệ thống, từ đó đặc tả các trạng thái và hành
vi của hệ thống ở mức trừu tƣợng cao hơn. Một sự kiện e tác động lên (một
danh sách) biến trạng thái v, với điều kiện G(v) và hành động A(v), sẽ đƣợc
mô tả nhƣ sau:
when G(v) then A(v) end
Vì thế, khi trạng thái v thỏa mãn điều kiện G(v) = true, hành động A(v) sẽ
đƣợc thực hiện. Hình 2.3 biểu diễn cấu trúc tổng quát của một sự kiện. Trong
đó:
Mệnh đề status có thể là ordinary, convergent (sự kiện phải làm tăng giá
trị các biến của nó), anticipated (sự kiện không đƣợc làm tăng giá trị các biến
của nó);
mệnh đề refine hiển thị danh sách các sự kiện trừu tƣợng đƣợc làm mịn;
mệnh đề any hiển thị các tham số nếu có;
mệnh đề where chứa các điều kiện để sự kiện đƣợc kích hoạt;
mệnh đề with chứa các tham số phải nhận giá trị trả về của sự kiện trừu
tƣợng tƣơng ứng;
mệnh đề then chứa các hành động của sự kiện. Các hành động này sẽ
đƣợc thực thi khi các điều kiện của sự kiện đƣợc thỏa mãn.
23 Số hóa bởi Trung tâm Học liệu

then
< label >:<action >
…
end Hình 2.3. Cấu trúc tổng quát của sự kiện.
24 Số hóa bởi Trung tâm Học liệu

Định nghĩa 2.1 (Máy hữu hạn trạng thái)Máy hữu hạn trạng thái là một
bộ 4 P =(S, A, , q). Trong đó:
S là tập hữu hạn các trạng thái;
, với biểu diễn tập các tiến trình P, L tập các nhãn,
tập các hành động;
∆ SxAxS biểu diễn mỗi quan hệ chuyển trạng thái;
qϵS là trạng thái bắt đầu.
Ví dụ 1: Giả sử chúng ta cần đặc tả các hành động bật, tắt một bóng đèn
điện nhƣ sau:
on → off → on → off → on → off → …
Nhƣ vậy, nếu bóng đèn còn hoạt động đƣợc thì các hành động này sẽ liên
tục xảy ra đến khi nào mà nó không đƣợc sử dụng nữa. Chính vì vậy việc đặc
tả nhƣ trên là không đầy đủ.
Tuy nhiên ta hoàn toàn có thể giải quyết vấn đề này bằng một đặc tả FSP
nhƣ sau:
SWITCH = (on – > off – >SWITCH ).
Trong đó: SWITCH là một tiến trình, on, off là các hành động.Hình 2.4
biểu diễn máy trạng thái cho các hành động bật, tắt một bóng đèn.


Hình 2.5.Biểu diễn máy trạng thái cho các hành động của một giảng viên

2.5.1. Cú pháp đặc tả trong FSP
Action prefix ((x – > P))[5]: Nếu x là một hành động và P là một tiến
trình thì một action frefix (x – > P) mô tả một tiến trình trong đó các hành
lenlop
giangbai
0
1
2
nghi