Các kỹ thuật đặc tả và kiểm chứng cho các bài toán tương tranh

1

Số hóa bởi Trung tâm Học liệu http://www.lrc-tnu.edu.vn/

ĐẠ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

Số hóa bởi Trung tâm Học liệu http://www.lrc-tnu.edu.vn/

LỜI CAM ĐOAN

Tôi xin cam đoan luận văn: “Các kỹ thuật đặc tả và kiểm chứng cho các bài

toán tương tranh” hoàn toàn do tôi thực hiện. Các kết quả trình bày trong luận

văn là trung thực.

Hải Phòng, ngày 26 tháng 03 năm 2014

Ngƣời thực hiện

Trần Quốc Tuấn

3

Số hóa bởi Trung tâm Học liệu http://www.lrc-tnu.edu.vn/

LỜI CẢM ƠN

Trƣớc tiên, tôi muốn gửi lời cảm sâu sắc nhất đến PGS TSKH Nguyễn

Xuân Huy, ngƣời đã trực tiếp giảng dạy và tận tình hƣớng dẫn tôi trong suốt

quá trình học cao học.

Tôi cũng trân trong cảm ơn các Thầy, Cô đang công tác tại Viện Công

nghệ thông tin Việt Nam,các Thầy, Cô trƣờng Đại học Công nghệ thông tin

và truyền thông – Đại học Thái Nguyên đã về truyền thụ kiến thức để tôi hoàn

thiện luận văn này.

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 http://www.lrc-tnu.edu.vn/

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

1.4. Một số vấn đề trong chƣơng trình tƣơng tranh .................................... 16

1.5. Kết luận ................................................................................................ 17

CHƢƠNG 2..................................................................................................... 18

MộT Số PHƢƠNG PHÁP KIểM CHứNG ..................................................... 18

2.1. Kiểm chứng thiết kế ............................................................................. 18

2.2. Kiểm chứng mô hình............................................................................ 19

2.3. Phƣơng pháp hình thức Event-B.......................................................... 20

2.3.1. Máy và ngữ cảnh........................................................................... 20

2.3.2. Phân rã và kết hợp......................................................................... 22

2.4. Sinh mệnh đề cần chứng minh............................................................. 23

2.5. Máy hữu hạn trạng thái (Finite State Process - FSP)........................... 23

2.5.1. Cú pháp đặc tả trong FSP.............................................................. 25

2.5.2. Quy trình tuần tự ........................................................................... 28

2.5.3. Công cụ kiểm chứng LTSA .......................................................... 30

2.6. Kết luận ................................................................................................ 31

CHƢƠNG 3..................................................................................................... 32

MộT Số Kỹ THUậT ĐặC Tả VÀ KIểM CHứNG BÀI TOÁN TƢƠNG

TRANH ........................................................................................................... 32

5

Số hóa bởi Trung tâm Học liệu http://www.lrc-tnu.edu.vn/

3.1. Đặc tả và kiểm chứng bài toán tƣơng tranh sử dụng Event-B............. 32

3.1.1. Kỹ thuật kiểm chứng sử dụng Event-B......................................... 32

3.1.2. Đặc tả Event-B cho bài toán cung cấp tiêu thụ............................. 34

3.1.3. Đặc tả Event-B cho bài toán đọc ghi ............................................ 36

3.1.4. Kết quả chứng minh tự động......................................................... 39

3.2. Kỹ thuật đặc tả và kiểm chứng sử dụng FSP ....................................... 39

3.2.1. Đặc tả FSP cho bài toán đọc ghi ................................................... 39

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 http://www.lrc-tnu.edu.vn/

DANH MụC Từ VIếT TắT

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

FSP Finite state process Máy hữu hạn trạng thái

LTSA Labelled Transition System

Analyser

Công cụ kiểm chứng đặc

tả cho FSP

RODIN

Rigorous Open Development

Environment for Complex

Systems

Công cụ kiểm chứng đặc

tả cho Event-B

UML Unified Modeling Language

Ngôn ngữ mô hình hóa

thống nhất

OCB Object-oriented Concurrent-B

Ngôn ngữ đặc tả trung

gian giữa Event-B và

chƣơng trình hƣớng đối

tƣợng, tƣơng tranh