Một Số Cải Tiến Phương Pháp Kiểm Chứng Giả Định Đảm Bảo Cho Phần Mềm Dựa Trên Thành Phần

Mục lục

Chương 1. GIỚI THIỆU . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1

1.1. Đặt vấn đề . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1

1.2. Các đóng góp chính của luận án . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

1.3. Bố cục của luận án . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

Chương 2. KIẾN THỨC NỀN TẢNG . . . . . . . . . . . . . . . . . . . . . . . . . . 9

2.1. Đặc tả và kiểm chứng giả định - đảm bảo cho các hệ thống đặc tả bằng

LTS. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

2.1.1. Hệ thống chuyển trạng thái được gán nhãn. . . . . . . . . . . . . . . . . . . . . . 9

2.1.2. Kiểm chứng giả định - đảm bảo cho các hệ thống đặc tả bằng LTS .

13

2.2. Đặc tả và kiểm chứng giả định - đảm bảo cho các hệ thống đặc tả bằng

lôgic mệnh đề . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

2.2.1. Đặc tả hệ thống chuyển trạng thái bằng lôgic mệnh đề . . . . . . . . . 16

2.2.2. Kiểm chứng giả định - đảm bảo cho các hệ thống đặc tả bằng lôgic

mệnh đề . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20

2.3. Đặc tả và kiểm chứng giả định - đảm bảo cho các hệ thống có ràng buộc

thời gian. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

2.3.1. Hệ thống chuyển trạng thái có ràng buộc thời gian. . . . . . . . . . . . . 21

2.3.2. Kiểm chứng giả định - đảm bảo cho các hệ thống có ràng buộc thời

gian . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25

2.4. Mô hình kiểm chứng giả định - đảm bảo . . . . . . . . . . . . . . . . . . . . . . . . . . . 26

2.5. Tổng kết. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27

Chương 3. PHƯƠNG PHÁP SINH GIẢ ĐỊNH NHỎ NHẤT VÀ

MẠNH NHẤT CỤC BỘ CHO VIỆC KIỂM CHỨNG PHẦN MỀM

DỰA TRÊN THÀNH PHẦN . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

3.1. Giới thiệu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

3.2. Các nghiên cứu liên quan . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31

3.3. Phương pháp sinh giả định dựa trên thuật toán học L

∗

. . . . . . . . . . . . 33

3.3.1. Thuật toán học L

∗

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33

i

3.3.2. Thuật toán sinh giả định sử dụng thuật toán học L

∗

. . . . . . . . . . . 34

3.4. Phương pháp sinh giả định nhỏ nhất và mạnh nhất cục bộ . . . . . . . . . 36

3.4.1. Phương pháp sinh giả định mạnh nhất cục bộ. . . . . . . . . . . . . . . . . . 37

3.4.2. Phương pháp sinh giả định nhỏ nhất và mạnh nhất cục bộ . . . . . 45

3.5. Thực nghiệm và thảo luận . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55

3.6. Tổng kết. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65

Chương 4. PHƯƠNG PHÁP KIỂM CHỨNG HỒI QUY GIẢ ĐỊNH

- ĐẢM BẢO CHO PHẦN MỀM TIẾN HÓA . . . . . . . . . . . . . . . . . . 67

4.1. Giới thiệu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67

4.2. Các nghiên cứu liên quan . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70

4.3. Phương pháp sinh giả định dựa trên thuật toán CDNF. . . . . . . . . . . . . 73

4.3.1. Thuật toán CDNF. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73

4.3.2. Thuật toán sinh giả định dựa trên CDNF . . . . . . . . . . . . . . . . . . . . . . 74

4.4. Phương pháp sinh giả định yếu nhất cục bộ. . . . . . . . . . . . . . . . . . . . . . . . 78

4.4.1. Biến thể của thuật toán trả lời các truy vấn thành viên . . . . . . . . 78

4.4.2. Thuật toán quay lui sinh giả định yếu nhất cục bộ . . . . . . . . . . . . . 80

4.4.3. Tính đúng đắn . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82

4.5. Phương pháp kiểm chứng từng phần cho phần mềm dựa trên thành phần

trong ngữ cảnh tiến hóa. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88

4.5.1. Phương pháp kiểm chứng giả định - đảm bảo cho phần mềm trong

ngữ cảnh tiến hóa . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90

4.5.2. Ví dụ minh họa. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91

4.6. Thực nghiệm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94

4.6.1. So sánh các thuật toán sinh giả định . . . . . . . . . . . . . . . . . . . . . . . . . . . 94

4.6.2. Tính hiệu quả của các giả định được sinh ra trong ngữ cảnh tiến hóa

98

4.6.3. Thảo luận . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102

4.7. Tổng kết . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104

Chương 5. THỬ NGHIỆM CÀI ĐẶT PHIÊN BẢN MỘT PHA CHO

VIỆC KIỂM CHỨNG GIẢ ĐỊNH - ĐẢM BẢO CHO PHẦN MỀM

CÓ RÀNG BUỘC THỜI GIAN . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106

5.1. Giới thiệu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106

5.2. Các nghiên cứu liên quan . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108

5.3. Phương pháp sinh giả định hai pha . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108

5.3.1. Pha thứ nhất – pha sinh giả định không có ràng buộc thời gian 109

5.3.2. Pha thứ hai – pha sinh giả định có ràng buộc thời gian . . . . . . . 110

ii

5.4. Phiên bản một pha của phương pháp sinh giả định hai pha . . . . . . . 111

5.4.1. Phiên bản một pha của thuật toán sinh giả định . . . . . . . . . . . . . . 111

5.4.2. Phiên bản cài đặt các thuật toán thực thi Teacher . . . . . . . . . . . . 113

5.5. Thảo luận . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116

5.5.1. Một số vấn đề trong thực tế cài đặt. . . . . . . . . . . . . . . . . . . . . . . . . . . 116

5.5.2. Ví dụ cho quá trình sinh giả định vô hạn . . . . . . . . . . . . . . . . . . . . . 118

5.6. Tính đúng đắn . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119

5.7. Thực nghiệm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121

5.8. Tổng kết . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 124

Chương 6. KẾT LUẬN . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126

6.1. Các kết quả đạt được. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126

6.2. Hướng phát triển tiếp theo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 128

iii

Danh sách hình vẽ

1.1 Tổng quan về phương pháp kiểm chứng giả định - đảm bảo và các

vấn đề còn tồn tại. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

2.1 Mô hình kiểm chứng giả định - đảm bảo. . . . . . . . . . . . . . . . . 26

3.1 Tương tác giữa L

∗ Learner và T eacher. . . . . . . . . . . . . . . . . . . 33

3.2 Quá trình kiểm chứng thành phần tại bước thứ i. . . . . . . . . . . . 35

3.3 Một phản ví dụ cho thấy các giả định được sinh bởi phương pháp

của Cobleigh và cộng sự [29] không phải là mạnh nhất. . . . . . . . . 37

3.4 Mối quan hệ giữa s, L(A), and L(AW ). . . . . . . . . . . . . . . . . . . 38

3.5 Ý tưởng chính của phương pháp sinh giả định mạnh nhất cục bộ

dựa vào L

∗

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44

3.6 Ví dụ cho sự tồn tại của một giả định nhỏ hơn và mạnh hơn

(ALMS) giả định được sinh bởi Thuật toán 3.1 (A). . . . . . . . . . . . 46

3.7 Ý tưởng để tính tempQ, comF inalState, và Cikj . . . . . . . . . . . . . . 47

3.8 Ý tưởng của phương pháp sinh giả định nhỏ nhất và mạnh nhất cục bộ.53

4.1 Thuật toán CBAG. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77

4.2 Thuật toán LWAG sinh giả định yếu nhất cục bộ cho việc kiểm

chứng giả định - đảm bảo cho các CBS. . . . . . . . . . . . . . . . . . 80

4.3 Mối quan hệ giữa L(AO), L(AN ), và L(AW ). . . . . . . . . . . . . . . . 86

4.4 Mối quan hệ giữa ListNW và ListN . . . . . . . . . . . . . . . . . . . . . 87

4.5 Sử dụng lại giả định được sinh bởi thuật toán LWAG cho việc

kiểm chứng CBS trong ngữ cảnh tiến hóa. . . . . . . . . . . . . . . . . 89

4.6 Thuật toán sinh lại giả định cho CBS trong ngữ cảnh tiến hóa. . . . . 91

5.1 Phương pháp sinh giả định hai pha. . . . . . . . . . . . . . . . . . . . 109

5.2 Ví dụ về quá trình sinh giả định lặp vô hạn. . . . . . . . . . . . . . . . 119

5.3 Ứng viên cho giả định tương ứng. . . . . . . . . . . . . . . . . . . . . . 119

iv

Danh sách bảng

2.1 Các phép gán cho ví dụ về chuỗi . . . . . . . . . . . . . . . . . . . . . 18

3.1 Kết quả thực nghiệm so sánh Thuật toán 3.1 và Thuật toán 3.3 . . . 56

3.2 Kết quả thực nghiệm so sánh Thuật toán 3.1 và Thuật toán 3.4 . . . 59

3.3 Không gian trạng thái giảm được với giả định được sinh bởi Thuật

toán 3.4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60

4.1 Bảng chân lý của phép toán lôgic kéo theo . . . . . . . . . . . . . . . . 79

4.2 Sinh giả định đầu tiên sử dụng thuật toán LWAG . . . . . . . . . . . 92

4.3 Sinh giả định cho hệ thống trong ngữ cảnh tiến hóa sử dụng thuật

toán LWAG và phương pháp kiểm chứng đề xuất . . . . . . . . . . . . 93

4.4 So sánh các phương pháp sinh giả định . . . . . . . . . . . . . . . . . . 98

4.5 So sánh các phương pháp sinh lại giả định . . . . . . . . . . . . . . . . 101

5.1 Một bảng quan sát trong quá trình kiểm chứng M . . . . . . . . . . . 118

5.2 Kết quả thực nghiệm phiên bản một pha . . . . . . . . . . . . . . . . 123

v

Thuật ngữ và từ viết tắt

Từ viết

tắt Từ gốc Giải nghĩa -

tạm dịch

AG Assume-Guarantee Giả định - đảm bảo

AGV Assume-Guarantee

Verification Kiểm chứng giả định - đảm bảo

AMC Adaptive Model Checking Kiểm chứng mô hình thích nghi

CBAG CDNF-based assumption generation Thuật toán sinh giả định dựa trên thuật

toán CDNF

CBS Component-based software Phần mềm dựa trên thành phần

CDNF Conjunction of Disjunctive Normal

Form

Tên một thuật toán học hàm lôgic

dùng để sinh giả định

CIRC-AG Circular Assume-Guarantee Kiểm chứng giả định - đảm bảo quay

vòng

CNF Conjunctive Normal Form Dạng chuẩn hội

DFA Deterministic Finite State Automata Ô-tô-mát hữu hạn trạng thái đơn định

DNF Disjunctive Normal Form Dạng chuẩn tuyển

EQ Equivalence query Thuật toán trả lời truy vấn ứng viên

ERA Event-Recording Automaton Ô-tô-mát ghi sự kiện

FMS Flexible Manufacturing System Hệ thống sản xuất linh hoạt

GSS Gas station system Hệ thống trạm gas

IMQ Improved membership query Thuật toán trả lời truy vấn thành viên

cải tiến

IW Is witness Thuật toán phân tích phản ví dụ

LMAG Locally minimum and strongest

assumption generation tool

Công cụ sinh giả định nhỏ nhất và mạnh

nhất cục bộ

LSAG Locally strongest assumption

generation tool Công cụ sinh giả định mạnh nhất cục bộ

LTS Labelled transition system Hệ thống chuyển trạng thái được gán nhãn

LTSA Labelled transition system analyser Công cụ hỗ trợ đặc tả và kiểm chứng hệ

thống chuyển trạng thái được gán nhãn

LWAG Local weakest assumption generation Thuật toán sinh giả định yếu nhất cục bộ

MTBDD Multiterminal binary decision diagram Sơ đồ quyết định nhị phân đa chiều

NC-AG Non-circular assume-guarantee Kiểm chứng giả định - đảm bảo không

quay vòng

OMQ Original membership query Thuật toán trả lời truy vấn thành viên

ban đầu

PAT Process Analysis Toolkit Tên một công cụ đặc tả, kiểm chứng

phần mềm

Tivet Timed systems verification tool Công cụ kiểm chứng phần mềm có ràng

buộc thời gian

vi

Lời cam đoan

Tôi xin cam đoan đây là công trình nghiên cứu do tôi thực hiện dưới sự hướng

dẫn của thầy giáo, PGS. TS. Phạm Ngọc Hùng và thầy giáo, TS. Võ Đình Hiếu

tại Bộ môn Công nghệ Phần mềm, Khoa Công nghệ Thông tin, Trường Đại học

Công nghệ, Đại học Quốc gia Hà Nội. Các số liệu và kết quả trình bày trong

luận án là trung thực, chưa được công bố bởi bất kỳ tác giả nào hay ở bất kỳ

công trình nào khác.

Tác giả

Trần Hoàng Việt

vii

Lời cảm ơn

Trước tiên tôi xin gửi lời cảm ơn chân thành và sâu sắc đến thầy giáo, PGS.

TS. Phạm Ngọc Hùng và thầy giáo, TS. Võ Đình Hiếu – những người đã hướng

dẫn, khuyến khích, truyền cảm hứng, chỉ bảo và tạo cho tôi những điều kiện tốt

nhất từ khi bắt đầu làm nghiên cứu sinh đến khi hoàn thành luận án này.

Tôi xin chân thành cảm ơn các thầy cô giáo khoa Công nghệ thông tin, Trường

Đại Học Công Nghệ, Đại Học Quốc Gia Hà Nội, đặc biệt là các Thầy Cô trong

Bộ môn Công Nghệ Phần Mềm đã tận tình đào tạo, cung cấp cho tôi những

kiến thức vô cùng quý giá, đã tạo điều kiện tốt nhất cho tôi về môi trường làm

việc trong suốt quá trình học tập, nghiên cứu tại Trường.

Tôi xin trân trọng cảm ơn đề tài mã số 102.03-2015.25 được tài trợ bởi Quỹ

phát triển khoa học và công nghệ quốc gia (NAFOSTED) đã hỗ trợ tôi trong

quá trình thực hiện luận án.

Cuối cùng, tôi xin chân thành cảm ơn những người thân trong gia đình cùng

toàn thể bạn bè đã luôn giúp đỡ, động viên tôi những lúc gặp phải khó khăn

trong suốt quá trình học tập và nghiên cứu.

viii

Tóm tắt

Kiểm chứng giả định - đảm bảo được biết đến như là một trong những giải

pháp quan trọng nhằm giải quyết bài toán bùng nổ không gian trạng thái trong

kiểm chứng mô hình cho các hệ thống phần mềm dựa trên thành phần. Ý tưởng

chính của phương pháp này là kiểm chứng từng phần nhỏ của phần mềm mà

không cần ghép chúng. Mặc dù có tiềm năng áp dụng lớn trong thực tế, các

nghiên cứu hiện tại cho thấy nhiều vấn đề còn tồn tại của phương pháp này

ngăn cản nó được áp dụng rộng rãi. Luận án đề xuất phương pháp giải quyết

một số trong các vấn đề đó của quá trình kiểm chứng cho phần mềm được đặc

tả bằng nhiều loại đặc tả và trong ngữ cảnh tiến hóa. Cụ thể, luận án đã đạt

được ba kết quả chính như sau.

Luận án đề xuất phương pháp sinh giả định nhỏ nhất và mạnh nhất cục bộ

cho bài toán kiểm chứng giả định - đảm bảo các phần mềm dựa trên thành phần

đặc tả bằng hệ chuyển trạng thái được gán nhãn (Labelled Transition System -

LTS). Các giả định này góp phần giảm chi phí tính toán sinh lại giả định mới

và giảm không gian trạng thái khi kiểm chứng các phần mềm tiến hóa. Ý tưởng

chính của phương pháp là sử dụng một biến thể của phương pháp trả lời các

truy vấn thành viên được đề xuất bởi Cobleigh và cộng sự. Biến thể này được

tích hợp trong thuật toán đề xuất để sinh được các giả định nhỏ nhất và mạnh

nhất cục bộ. Các chứng minh cho tính đúng đắn của phương pháp đề xuất cũng

được trình bày trong luận án. Một công cụ hỗ trợ đã được xây dựng và tiến

hành thực nghiệm với các hệ thống ban đầu cho những kết quả khả quan so với

các phương pháp hiện có.

Luận án đề xuất phương pháp sinh giả định yếu nhất cục bộ và phương pháp

sử dụng các giả định đó để giảm số lần sinh lại giả định khi kiểm chứng giả

định - đảm bảo phần mềm được đặc tả bằng lôgic mệnh đề trong ngữ cảnh tiến

hóa. Để làm việc này, luận án đề xuất một biến thể của thuật toán trả lời các

truy vấn thành viên được đề xuất bởi Chen và cộng sự. Biến thể này được tích

ix

hợp trong thuật toán quay lui sinh giả định yếu nhất cục bộ khi kiểm chứng.

Biến thể của phương pháp trả lời truy vấn thành viên và thuật toán quay lui

này được tích hợp trong phương pháp đề xuất nhằm giảm được tối đa số lần giả

định cần được sinh lại khi kiểm chứng phần mềm tiến hóa. Việc này giúp giảm

chi phí cho quá trình kiểm chứng các phần mềm trong ngữ cảnh tiến hóa phần

mềm. Tính đúng đắn của thuật toán đề xuất cũng được chứng minh trong luận

án. Công cụ hỗ trợ cho phương pháp đã được cài đặt và tiến hành thực nghiệm

với các hệ thống phổ biến trong cộng đồng nghiên cứu và cho những kết quả tốt

so với các phương pháp hiện nay.

Luận án thực nghiệm cài đặt phiên bản một pha cho phương pháp kiểm chứng

giả định - đảm bảo hai pha được đề xuất bởi Lin và cộng sự cho phần mềm dựa

trên thành phần có ràng buộc thời gian. Phiên bản này loại bỏ pha sinh giả

định không có thời gian từ quá trình kiểm chứng. Luận án cũng trình bày một

số vấn đề phát sinh và phương pháp xử lý trong quá trình cài đặt phương pháp

kiểm chứng trong thực tế. Tính đúng đắn của phiên bản đề xuất được trình bày

và thảo luận trong luận án. Công cụ hỗ trợ đã được cài đặt và thực nghiệm với

một số hệ thống phổ biến trong cộng đồng nghiên cứu và cho các kết quả khả

quan.

Các đề xuất của luận án đóng góp các giải pháp về mặt lý thuyết và công cụ

hỗ trợ nhằm nâng cao hiệu quả của phương pháp kiểm chứng giả định - đảm

bảo góp phần làm cho các phương pháp kiểm chứng mô hình dễ dàng được áp

dụng hơn trong thực tiễn. Luận án góp phần nâng cao chất lượng trong công

nghiệp phần mềm nói chung và trong cộng đồng nghiên cứu nói riêng.

x

Chương 1

GIỚI THIỆU

1.1. Đặt vấn đề

Trong ba thập kỷ vừa qua, công nghệ phần mềm dựa trên thành phần

(Component-Based Software Engineering - CBSE) nổi lên như một cách tiếp

cận quan trọng trong công nghệ phần mềm vì các đặc tính cả về nghiệp vụ và

kỹ thuật của nó như: tăng hiệu quả, giảm chi phí, rút ngắn thời gian đưa sản

phẩm ra thị trường, tăng khả năng bảo trì, v.v. [99]. Từ đó, việc đảm bảo chất

lượng cho các phần mềm dựa trên thành phần (Component-Based Software -

CBS) đóng vai trò sống còn trong vòng đời phát triển của chúng do yêu cầu

ngày càng tăng về chất lượng. Với các sản phẩm phần mềm quan trọng có yêu

cầu chất lượng cao như các phần mềm điều khiển ô tô, tàu hỏa, máy bay, v.v.,

các phần mềm này được yêu cầu thỏa mãn một số thuộc tính (thuộc tính được

nghiên cứu trong luận án này là thuộc tính an toàn) cho trước, kiểm chứng là

bắt buộc để đảm bảo thuộc tính đã cho không bị vi phạm trong toàn bộ thời

gian hoạt động của chúng. Có hai hướng tiếp cận chính nhằm giải quyết vấn đề

này gồm: hướng tiếp cận chứng minh định lý (theorem proving) là hướng tiếp

cận bán tự động, đòi hỏi có sự tham gia của các chuyên gia trong quá trình

kiểm chứng [31, 35, 53, 60, 61, 95], cần nhiều công sức và chi phí [9] và hướng

tiếp cận kiểm chứng mô hình (model checking) là hướng tiếp cận hoàn toàn tự

động [12]. Trong hai hướng tiếp cận này, hướng tiếp cận kiểm chứng mô hình

[24, 25, 27, 54, 90] nhận được sự quan tâm đặc biệt trong cộng đồng nghiên cứu

và trong công nghiệp phần mềm vì tính tự động hoàn toàn của nó. Kiểm chứng

mô hình là hướng tiếp cận vét cạn thông qua việc duyệt qua toàn bộ không gian

trạng thái của phần mềm để kiểm tra xem phần mềm có vi phạm thuộc tính

1

đã cho hay không. Nếu không có sự vi phạm nào, hệ thống ban đầu thỏa mãn

thuộc tính đã cho. Ngược lại, một minh chứng về sự vi phạm sẽ được trả lại.

Vì đặc tính vét cạn không gian trạng thái của hệ thống cần kiểm chứng, hướng

tiếp cận này gặp vấn đề về sự bùng nổ không gian trạng thái đối với các hệ

thống lớn [24, 26, 90]. Để tận dụng được những ưu điểm của kiểm chứng mô

hình và giải quyết vấn đề về bùng nổ không gian trạng thái, phương pháp kiểm

chứng giả định - đảm bảo (Assume-Guarantee Verification - AGV) đã được đề

xuất [23, 44, 52, 81, 88]. Kiểm chứng giả định-đảm bảo là phương pháp kiểm

chứng dựa trên chiến lược chia để trị. Trong đó, hệ thống phần mềm lớn được

chia thành các thành phần nhỏ hơn để kiểm chứng. Từ đó, quá trình kiểm chứng

kết luận rằng hệ thống tổng thể có thỏa mãn thuộc tính đã cho hay không mà

không phải ghép nối toàn bộ các thành phần lại với nhau.

Trong phương pháp kiểm chứng giả định - đảm bảo, có hai phương pháp lập

luận: giả định - đảm bảo quay vòng (Circular Assume - Guarantee Reasoning -

CIRC-AG) [3, 64, 75, 77, 78, 84] và giả định - đảm bảo không quay vòng (Non￾Circular Assume - Guarantee Reasoning - NC-AG) [5, 21, 23, 41, 44, 68, 76, 96].

Trong luận án này, thuật ngữ “kiểm chứng giả định - đảm bảo quay vòng ” và

“kiểm chứng giả định - đảm bảo không quay vòng ” được sử dụng lần lượt để chỉ

“phương pháp kiểm chứng sử dụng lập luận quay vòng ” và “phương pháp kiểm

chứng sử dụng lập luận không quay vòng ”. Sau này, phương pháp kiểm chứng giả

định - đảm bảo không quay vòng được mở rộng, áp dụng cho các hệ thống được

đặc tả bằng nhiều phương pháp khác nhau như: hệ chuyển trạng thái được gán

nhãn (Labelled Transition Systems - LTS) [18, 22, 29, 41, 45, 46, 55, 56, 57, 58,

86], hệ thống có ràng buộc thời gian (timed systems) [68, 69], hệ thống chuyển

trạng thái được đặc tả bằng lôgic mệnh đề [21, 48, 94], hệ thống chuyển trạng

thái tượng trưng (symbolic transition systems) [6, 49, 82, 83], các hệ thống có

yếu tố xác suất (probalistic systems) [16, 20, 37, 62], v.v.

Bài toán quan trọng nhất trong phương pháp kiểm chứng giả định - đảm bảo

là làm sao để sinh được giả định. Để giải quyết vấn đề này, các phương pháp

hiện nay đều dựa vào các thuật toán học ngôn ngữ chính quy thông qua sự tương

tác của hai thực thể Learner và T eacher. Tùy vào loại hệ thống (có hoặc không

có ràng buộc thời gian) và tùy vào phương pháp đặc tả được sử dụng (đặc tả

bằng hệ chuyển trạng thái được gán nhãn, lôgic mệnh đề, và ô-tô-mát ghi sự

kiện, v.v.), thuật toán sinh giả định sẽ được lựa chọn tương ứng (L

∗

[8, 91], và

2

CDNF (Conjunction of Disjunctive Normal Form) [15, 21], T L∗

[68, 69], v.v.).

Mặc dù tồn tại nhiều phương pháp kiểm chứng giả định - đảm bảo, các phương

pháp này đều có những ưu và nhược điểm nhất định. Tổng quan về phương pháp

kiểm chứng giả định - đảm bảo và các vấn đề còn tồn tại được trình bày trong

Hình 1.1. Trong luận án này, phần mềm được đặc tả bằng các dạng đặc tả khác

nhau như LTS, lôgic mệnh đề, và ô-tô-mát ghi sự kiện và thuộc tính được kiểm

chứng là thuộc tính an toàn.

Mô hình phần mềm

Bùng nổ

không gian trạng thái?

· Yes + giả định A

· No + phản ví dụ cex

Mô hình phần mềm

tiến hóa

LTS Lôgic mệnh đề ERA

Kiểm chứng M với các

loại đặc tả khác nhau?

Tăng tốc độ

kiểm chứng?

Kiểm chứng M’ hiệu quả?

Hình 1.1: Tổng quan về phương pháp kiểm chứng giả định - đảm bảo và các vấn đề

còn tồn tại.

Phương pháp kiểm chứng giả định - đảm bảo cho hệ thống chuyển trạng thái

được gán nhãn là phương pháp phổ biến nhất trong cộng đồng nghiên cứu cũng

như trong việc áp dụng trong công nghiệp. Trong phương pháp này, các luật

kiểm chứng giả định - đảm bảo cho thấy rằng bản chất của bài toán kiểm chứng

là bài toán bao của các ngôn ngữ và độ phức tạp của quá trình kiểm chứng tỉ

lệ thuận với số trạng thái của giả định được sinh ra [100]. Theo đó, chi phí của

quá trình kiểm chứng (chi phí được đề cập trong luận án này là chi phí về thời

gian), đặc biệt trong ngữ cảnh tiến hóa (từ phần mềm M thành M0

), có thể nhỏ

hơn nếu sử dụng giả định có số trạng thái và ngôn ngữ nhỏ hơn.

Để sinh giả định cho bài toán kiểm chứng giả định - đảm bảo cho các hệ

thống được đặc tả bằng LTS, Giannakopoulou và cộng sự là nhóm tác giả đầu

tiên chỉ ra sự tồn tại của giả định yếu nhất (giả định có ngôn ngữ lớn nhất)

trong kiểm chứng giả định - đảm bảo [41, 87]. Tiếp đó, Cobleigh và cộng sự đề

xuất sử dụng thuật toán L

∗

[8, 91] sinh giả định cho bài toán kiểm chứng giả

định - đảm bảo [29]. Sau Cobleigh, có nhiều nghiên cứu mở rộng, cải tiến, tối ưu

3

cũng như áp dụng kết quả của Cobleigh cho nhiều ngữ cảnh khác của việc kiểm

chứng phần mềm [10, 39, 87, 22, 28, 93, 17, 18, 19, 46, 38, 101, 86, 55, 57, 58].

Mặc dù vậy, vẫn chưa có nghiên cứu nào đề xuất phương pháp sinh giả định nhỏ

nhất và mạnh nhất để giảm chi phí kiểm chứng phần mềm trong ngữ cảnh tiến

hóa (tăng hiệu quả, tốc độ kiểm chứng M0

).

Phương pháp kiểm chứng giả định - đảm bảo sử dụng đặc tả bằng LTS là

phương pháp phổ biến và thường được áp dụng cho các hệ thống được đặc tả

ở mức cao, như mức thiết kế, dưới dạng các hệ thống chuyển trạng thái. Tuy

nhiên, độ phức tạp của nó vẫn rất cao. Vì vậy, trường hợp hệ thống được đặc tả

ở mức thấp hơn dưới dạng lôgic mệnh đề, một số nghiên cứu khác đã sử dụng

phương pháp kiểm chứng được đề xuất bởi Chen và cộng sự để giảm độ phức

tạp của quá trình kiểm chứng [21, 48]. Các thuật toán kiểm chứng giả định -

đảm bảo sử dụng đặc tả bằng lôgic mệnh đề có những ưu điểm vượt trội so với

các thuật toán sử dụng đặc tả bằng ô-tô-mát. Thứ nhất, về khả năng biểu diễn,

đặc tả bằng lôgic mệnh đề tương đương với đặc tả bằng ô-tô-mát không đơn

định và nó có thể biểu diễn súc tích hơn nhiều lần so với đặc tả bằng ô-tô-mát.

Do đó, các thuật toán kiểm chứng sử dụng đặc tả bằng lôgic mệnh đề sinh các

giả định có số trạng thái ít hơn nhiều lần các giả định sinh bởi các phương pháp

sử dụng thuật toán L

∗

. Thứ hai, xét về tốc độ thì thuật toán sinh giả định sử

dụng đặc tả bằng lôgic mệnh đề sử dụng các thuật toán như CDNF [15], v.v.

có tốc độ tốt hơn các thuật toán kiểm chứng sử dụng thuật toán L

∗

[21]. Năm

2007, Sinha và cộng sự đã đề xuất sử dụng bộ giải nhằm kiểm tra tính thỏa mãn

của hàm lôgic (SAT solver) cho bài toán kiểm chứng giả định - đảm bảo với các

hệ thống được đặc tả bằng lôgic mệnh đề [94]. Năm 2010, Chen và cộng sự đã

đề xuất áp dụng thuật toán CDNF được đề xuất bởi Bshouty [15] cho bài toán

kiểm chứng giả định - đảm bảo cho hệ thống chuyển trạng thái được đặc tả bằng

lôgic mệnh đề [21]. Sau Chen, năm 2016, He và cộng sự đã đề xuất một phương

pháp sinh giả định có tốc độ nhanh và hiệu quả sử dụng thuật toán CDNF để

sinh các giả định trong quá trình kiểm chứng giả định - đảm bảo cho hệ thống

phần mềm được đặc tả bằng lôgic mệnh đề [48]. Sau đó, phương pháp này được

áp dụng cho việc kiểm chứng hồi quy cho phần mềm tiến hóa. Tuy nhiên, trong

ngữ cảnh tiến hóa phần mềm, thuật toán vẫn cần sinh lại giả định trong tất cả

các trường hợp dù chỉ có sự thay đổi nhỏ trong các thành phần của phần mềm

ban đầu.

4

Trong phát triển phần mềm nói chung, ngoài các phần mềm không có ràng

buộc thời gian được đặc tả bằng LTS hoặc lôgic mệnh đề, v.v, các hệ thống có

ràng buộc thời gian cũng nhận được sự quan tâm đặc biệt của cộng đồng nghiên

cứu và trong công nghiệp. Do đó, việc kiểm chứng các phần mềm này trở thành

một xu hướng tất yếu do các đòi hỏi về chất lượng của các hệ thống thời gian

thực ngày càng cao và trong nhiều lĩnh vực của đời sống xã hội như Internet

vạn vật, khoa học vũ trụ, v.v. Một trong các phương pháp đặc tả các hệ thống

có ràng buộc thời gian là sử dụng các ô-tô-mát ghi sự kiện (Event - Recording

Automata - ERA) [4]. Năm 2010, Grinchtein và cộng sự đề xuất thuật toán học

T L∗

sg để học các ô-tô-mát ghi sự kiện [42]. Sau đó, năm 2014, Lin và cộng sự là

nhóm tác giả đầu tiên đề xuất bài toán kiểm chứng giả định - đảm bảo cho phần

mềm có ràng buộc thời gian được đặc tả bằng ô-tô-mát ghi sự kiện [68]. Phương

pháp được Lin đề xuất sử dụng thuật toán học ô-tô-mát ghi sự kiện T L∗

cũng

được đề xuất bởi cùng nhóm tác giả năm 2011 [69]. Thuật toán này được phát

triển từ thuật toán T L∗

sg được đề xuất trước đó bởi Grinchtein và cộng sự [42].

Thuật toán T L∗ được triển khai vào bộ công cụ hỗ trợ việc kiểm chứng hệ thống

có ràng buộc thời gian gọi là PAT [71, 97]. Tuy phương pháp của Lin có thể

sinh được giả định cho bài toán kiểm chứng giả định - đảm bảo cho phần mềm

có ràng buộc thời gian, phương pháp này có độ phức tạp cao nên vẫn rất khó

khăn để có thể được áp dụng rộng rãi trong cộng đồng nghiên cứu và trong công

nghiệp.

Từ các phân tích trên, luận án hướng tới các mục tiêu sau. Mục tiêu thứ nhất

là sinh giả định nhỏ nhất và mạnh nhất cho bài toán kiểm chứng giả định - đảm

bảo. Mục tiêu này hướng tới việc giảm chi phí thời gian khi sinh lại giả định

trong quá trình kiểm chứng phần mềm đã tiến hóa. Mục tiêu thứ hai là giảm chi

phí thời gian của quá trình kiểm chứng giả định - đảm bảo phần mềm đã tiến

hóa bằng cách giảm số lần sinh lại giả định khi kiểm chứng hồi quy. Luận án

đề xuất phương pháp sinh giả định yếu nhất cục bộ cho quá trình kiểm chứng

giả định - đảm bảo. Các giả định này được sử dụng trong phương pháp đề xuất

để giảm số lần sinh lại giả định khi kiểm chứng hồi quy phần mềm tiến hóa.

Mục tiêu cuối cùng của luận án là tiến hành thử nghiệm cài đặt phiên bản một

pha của phương pháp kiểm chứng giả định - đảm bảo hai pha cho phần mềm có

ràng buộc thời gian. Để đạt được mục tiêu này, luận án tiến hành nghiên cứu,

cài đặt, và xử lý các vấn đề phát sinh trong quá trình cài đặt phương pháp sinh

5