Tối ưu việc sinh giả thiết bằng giải thuật học L* cho kiểm chứng từng phần phần mềm dựa trên thành phần
Tối ưu việc sinh giả thiết bằng giải thuật học L* cho kiểm chứng từng phần phần mềm dựa trên thành phần
Xem bên trong

Tối ưu việc sinh giả thiết bằng giải thuật học L* cho kiểm chứng từng phần phần mềm dựa trên thành phần

Luận văn ThS. Khoa học máy tính — Trường Đại học Công nghệ. Đại học Quốc gia Hà Nội, 2014
Electronic Resources

0.00

Tải về miễn phí bản đầy đủ PDF luận văn tại Link bản đầy đủ 1

ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
ĐÀO ANH HIỂN
TỐI ƯU VIỆC SINH GIẢ THIẾT BẰNG GIẢI
THUẬT HỌC L* CHO KIỂM CHỨNG TỪNG PHẦN
PHẦN MỀM DỰA TRÊN THÀNH PHẦN
LUẬN VĂN THẠC SĨ

HÀ NỘI – 2014

ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
ĐÀO ANH HIỂN
TỐI ƯU VIỆC SINH GIẢ THIẾT BẰNG GIẢI
THUẬT HỌC L* CHO KIỂM CHỨNG TỪNG PHẦN
PHẦN MỀM DỰA TRÊN THÀNH PHẦN
Ngành: Công nghệ thông tin
Chuyên ngành: Khoa học máy tính
Mã số: 60480101
LUẬN VĂN THẠC SĨ
NGƯỜI HƯỚNG DẪN KHOA HỌC: PGS. TS NGUYỄN VIỆT HÀ
HÀ NỘI – 2014
i

LỜI CẢM ƠN
Lời đầu tiên, tôi muốn gửi lời cảm ơn chân thành nhất tới PGS. TS Nguyễn Việt
Hà, người thầy đã tận tình hướng dẫn, chỉ bảo và giúp đỡ tôi trong quá trình làm luận
văn.
Tôi xin bày tỏ lòng biết ơn sâu sắc tới TS Phạm Ngọc Hùng, thầy đã đóng góp
những định hướng, ý kiến quý báu, cũng như đã tạo ra những động lực để tôi hoàn
thành tốt luận văn này.
Tôi xin gửi lời cảm ơn tới các thầy cô giáo đã giảng dạy tôi trong suốt những
năm học qua, các thầy cô đã rất quan tâm tới lớp, giúp tôi và các bạn cùng lớp có được
kết quả học tập như hiện tại.
Trân trọng cảm ơn đề tài mã số QGTD.13.01 đã trợ giúp tôi trong quá trình
thực hiện luận văn này.
Cuối cùng, tôi xin cảm ơn gia đình và đồng nghiệp những người luôn ở bên
động viên cổ vũ tôi trong suốt quá trình học tập, những người đã ủng hộ và khuyến
khích tôi rất nhiều trong tất cả các năm học. Họ là nguồn động viên vô tận của tôi
trong cuộc sống.
Hà Nội, tháng 6 năm 2014
Đào Anh Hiển
ii

LỜI CAM ĐOAN

Tôi xin cam đoan rằng, đây là kết quả nghiên cứu của tôi trong đó có sự giúp đỡ
rất lớn của thầy hướng dẫn và sự nỗ lực của bản thân. Các nội dung nghiên cứu và kết
quả trong đề tài này hoàn toàn trung thực.
Trong luận văn, tôi có tham khảo đến một số tài liệu của một số tác giả đã được
liệt kê tại phần tài liệu tham khảo ở cuối luận văn.
Hà Nội, tháng 6 năm 2014
Học viên thực hiện
Đào Anh Hiển
iii

MỤC LỤC
LỜI CẢM ƠN ……………………………………………………………………………………………….. i
LỜI CAM ĐOAN ………………………………………………………………………………………….. ii
MỤC LỤC …………………………………………………………………………………………………… iii
DANH MỤC TỪ VIẾT TẮT ………………………………………………………………………….. iv
DANH MỤC BẢNG ……………………………………………………………………………………… v
DANH MỤC HÌNH VẼ ………………………………………………………………………………… vi
CHƯƠNG 1. GIỚI THIỆU ……………………………………………………………………………… 1
CHƯƠNG 2. CÁC KIẾN THỨC CƠ BẢN ……………………………………………………….. 4
2.1. Labeled Transition Systems (LTSs) …………………………………………………………. 4
2.2. Dẫn xuất (Traces) …………………………………………………………………………………. 4
2.3. Ghép nối song song (Parallel Compostion) ……………………………………………….. 5
2.4. LTS an toàn và thuộc tính an toàn …………………………………………………………… 5
2.5. Sự thỏa mãn (Satisfiability) ……………………………………………………………………. 6
2.6. Ôtomat đơn định hữu hạn trạng thái ………………………………………………………… 6
2.7. Đảm bảo giả thiết (Assume-Guarantee Reasoning) …………………………………….. 7
CHƯƠNG 3. PHƯƠNG PHÁP SINH GIẢ THIẾT TỐI THIỂU BẰNG GIẢI THUẬT
HỌC L* ……………………………………………………………………………………………………… 10
3.1. Giải thuật học L* ………………………………………………………………………………… 10
3.2. Phương pháp sinh giả thiết bằng giải thuật học L* …………………………………… 13
3.3. Ví dụ tạo giả thiết ……………………………………………………………………………….. 16
CHƯƠNG 4. TỐI ƯU VIỆC SINH GIẢ THIẾT BẰNG GIẢI THUẬT HỌC L* …… 20
4.1. Giới thiệu ………………………………………………………………………………………….. 20
4.2. Định nghĩa giả thiết tối thiểu ………………………………………………………………… 20
4.3. Phương pháp sinh giả thiết tối thiểu ………………………………………………………. 20
4.3.1. Kỹ thuật cải tiến cho việc trả lời các câu hỏi kiểm tra thành viên ………….. 22
4.3.2. Giải thuật sinh giả thiết tối thiểu ……………………………………………………… 23
4.4. Tối ưu phương pháp sinh giả thiết tối thiểu …………………………………………….. 25
4.4.1. Tư tưởng của giải thuật ………………………………………………………………….. 25
4.4.2. Giải thuật cải tiến tạo giả thiết tối thiểu …………………………………………….. 25
4.4.3. Đặc điểm không gian tìm kiếm ……………………………………………………….. 29
4.4.4. Tính dừng và tính đúng đắn của giải thuật …………………………………………. 30
4.5. Ví dụ tạo giả thiết tối thiểu …………………………………………………………………… 31
CHƯƠNG 5. THỰC NGHIỆM …………………………………………………………………… 39
5.1. Mô tả công cụ …………………………………………………………………………………….. 39
5.2. Kết quả thực nghiệm …………………………………………………………………………… 40
CHƯƠNG 6. KẾT LUẬN …………………………………………………………………………….. 43
DANH MỤC CÔNG TRÌNH KHOA HỌC ĐÃ CÔNG BỐ ……………………………….. 44
TÀI LIỆU THAM KHẢO …………………………………………………………………………….. 45
PHỤ LỤC …………………………………………………………………………………………………… 47
iv

DANH MỤC TỪ VIẾT TẮT
AGM Asumption Generation Method
AGR Assume-Guarantee Reasoning
AGV Assume-Guarantee Verification
CBS Component-Based Software
CBSD Component-Based Software Development
DFA Deterministic Finite State Automata
FSP Finite State Processes
DLS Depth-Limited Search
LTSA Labelled Transition Systems Analyser
MAGM Minimized Asumption Generation Method
MC Model Checking
MMC Modular Model Checking
MV Modular Verification
IDDFS Iterative Deepening Depth – First Search
v

DANH MỤC BẢNG
Bảng 4.1: Bảng quan sát ban đầu ……………………………………………………………………. 32
Bảng 4.2: Bảng sau khi cập nhật T1 ………………………………………………………………… 32
Bảng 4.3: Bảng T1.1 …………………………………………………………………………………….. 33
Bảng 4.4: Bảng T1.1 …………………………………………………………………………………….. 33
Bảng 4.5: Bảng T1.2 …………………………………………………………………………………….. 33
Bảng 4.6: Bảng T1.3 …………………………………………………………………………………….. 33
Bảng 4.7: Bảng T1.2.1 ………………………………………………………………………………….. 34
Bảng 4.8: Bảng T1.2.1 sau khi cập nhật …………………………………………………………… 36
Bảng 4.9: Bảng quan sát T1.2.1.1 sau khi thêm send vào S …………………………………. 37
Bảng 4.10: Bảng quan sát T1.2.1.1.1 ………………………………………………………………. 37
Bảng 5.1. Kết quả thực nghiệm ………………………………………………………………………. 42
vi

DANH MỤC HÌNH VẼ
Hình 2.1: Ví dụ về LTSs …………………………………………………………………………………. 4
Hình 2.2: LTS của Input || Output …………………………………………………………………….. 5
Hình 2.3. LTS của thuộc tính an toàn ………………………………………………………………… 6
Hình 2.4: Tính ghép nối Input || Output || perr. …………………………………………………….. 7
Hình 2.5: Minh hoạ tạo LTS an toàn từ một DFA. ………………………………………………. 7
Hình 3.1: Minh hoạ mối quan hệ giữa Teacher và L* learner. ……………………………… 11
Hình 3.2: Một sơ đồ khối để tạo giả thiết sử dụng giải thuật L* [4]. ……………………… 13
Hình 3.3 Các thành phần và thuộc tính yêu cầu của hệ thống minh họa ………………… 16
Hình 3.4 Bảng quan sát rỗng và bảng quan sát sau khi cập nhật …………………………… 17
Hình 3.5: Bảng sau khi thêm out vào S, bảng đó sau khi cập nhật và giả thiết ứng cử
viên A1……………………………………………………………………………………………………….. 17
Hình 3.6: Bảng quan sát sau khi thêm ack và S và bảng sau khi cập nhật ………………. 18
Hình 3.7: Bảng sau khi thêm send vào S, bảng sau khi cập nhật và giả thiết ứng cử
viên A2. ………………………………………………………………………………………………………. 19
Hình 4.1: Các thành phần của hệ thống trong ví dụ được xét. ……………………………… 21
Hình 4.2: Giả thiết được tạo ra sau khi sử dụng giải thuật L*. ……………………………… 21
Hình 4.3: Giả thiết được tạo ra bởi giải thuật tạo giả thiết tối thiểu. ……………………… 21
Hình 4.4: Lý do chỉ ra tại sao giả thiết được sinh ra trong [4] không tối thiểu ………… 22
Hình 4.5: Biểu diễn LTSs của các thành phần. ………………………………………………….. 31
Hình 4.6: Mô hình cây tìm kiếm của các bảng quan sát. ……………………………………… 34
Hình 4.7: Giả thiết A1.2.1 ……………………………………………………………………………….. 35
Hình 4.8: Cây tìm kiếm sau khi duyệt đến bảng quan sát T1.2.1 ………………………….. 36
Hình 4.9: Giả thiết kết quả. ……………………………………………………………………………. 38
Hình 5.1 Công cụ IMAG và một ví dụ …………………………………………………………….. 39
Hình 5.2 Một ví dụ kiểm tra tính đúng đắn của công cụ IMAG trên LTSA ……………. 40

1

CHƯƠNG 1. GIỚI THIỆU
Quá trình phát triển phần mềm hướng thành phần được biết đến là sự phát triển
phần mềm bằng cách ghép nối các phần độc lập. Đây là một trong những kỹ thuật
quan trọng nhất trong kỹ nghệ phần mềm. Cách tiếp cận này vẫn đang thu hút sự chú ý
trong cộng đồng kỹ nghệ phần mềm và được xem là một cách tiếp cận mở, hiệu quả,
giảm thời gian và chi phí phát triển đồng thời tăng chất lượng của phần mềm. Đã có rất
nhiều khái niệm, kỹ thuật đề xuất nhằm phát triển cho ý tưởng này.
Tuy nhiên, một trong những hạn chế của phát triển phần mềm hướng thành
phần là vấn đề đảm bảo tính đúng đắn của hệ thống khi ghép nối các thành phần với
nhau vì các thành phần có thể được phát triển một cách độc lập hoặc được đặt mua từ
các công ty thứ 3 (third parties). Hiện tại, các công nghệ hỗ trợ phát triển phần mềm
hướng thành phần như CORBA (OMG), COM/DCOM or .NET (Microsoft), Java and
JavaBeans (Sun), … vv chỉ hỗ trợ việc ghép nối các thành phần (component plugging).
Chúng không có cơ chế kiểm tra liệu các thành phần có thể bị lỗi khi cộng tác với
nhau hay không. Điều này có nghĩa là cơ chế “plug-and-play” không được đảm bảo.
Một giải pháp phổ biến hiện nay để giải quyết cho vấn đề trên là áp dụng kiểm chứng
mô hình (Model Checking – MC) [5]. Kiểm chứng mô hình là một cách tiếp cận quan
trọng để giải quyết bài toán chứng minh độ tin cậy của phần mềm. Nó cũng tạo ra một
không gian trạng thái chi tiết có thể bao phủ được các hệ thống đang được kiểm tra
đồng thời đạt được hiệu quả đặc biệt trong quá trình dò các lỗi tổng hợp khá phức tạp
mà nguyên nhân chủ yếu do quá trình ghép nối các thành phần gây nên. Tuy nhiên,
một trong những hạn chế lớn nhất của kiểm chứng mô hình là “vấn đề bùng nổ không
gian trạng thái” khi kiểm chứng các phần mềm có kích thước lớn. Một trong những
cách tiếp cận tiềm năng để giải quyết vấn đề này là áp dụng kiểm chứng từng phần
(Modular Model Checking – MMC) [11, 12]. Thay vì tiến hành kiểm chứng trên toàn
bộ hệ thống gồm các thành phần được ghép nối với nhau, cách tiếp cận này tiến hành
kiểm chứng trên từng thành phần riêng biệt. Với cách tiếp cận này, vấn đề bùng nổ
không gian trạng thái hứa hẹn sẽ được giải quyết. Một trong những phương pháp kiểm
chứng hỗ trợ ý tưởng này là phương pháp kiểm chứng đảm bảo giả thiết (Assume-
Guarantee Verification – AGV) [2, 4, 6, 7] . Sử dụng tư tưởng của chiến lược “chia để
trị”, AGV phân chia bài toán kiểm chứng thành các bài toán con cùng dạng nhưng
kích thước nhỏ hơn sao cho chúng ta có thể kiểm chứng các bài toán con một cách
riêng biệt. AGV được đánh giá là một phương pháp hứa hẹn để kiểm chứng phần mềm
hướng thành phần thông qua phương pháp kiểm chứng mô hình. AGV không những
thích hợp cho phần mềm hướng thành phần mà còn có khả năng giải quyết vấn đề
bùng nổ không gian trạng thái trong kiểm chứng mô hình. Trong phương pháp này,
các giả thiết (assumptions) (có vai trò như là môi trường của các thành phần) sẽ được
tạo lập. Việc tạo lập các giả thiết chính là bài toán quan trọng nhất trong phương pháp
2

này. Mục tiêu chính của cách tiếp cận này là nhằm kết hợp tốt nhất giữa lợi thế của hai
phần: kiểm chứng mô hình và phát triển hướng thành phần.
Hiện nay, đã có nhiều nghiên cứu về kiểm chứng mô hình từng phần cho phần
mềm hướng thành phần [2, 4, 6, 7, 11, 12, 16]. Mỗi khi thêm một thành phần nào đó
vào hệ thống, thì toàn bộ hệ thống gồm các thành phần đang tồn tại và thành phần mới
phải được kiểm chứng lại. Vì thế, đối với những phần mềm phức tạp, vấn đề “bùng nổ
không gian trạng thái” có thể xảy ra khi áp dụng các phương pháp trong các nghiên
cứu này. Cách tiếp cận trong [2, 4, 6, 7] đề xuất phương pháp kiểm chứng đảm bảo giả
thiết như đã trình bày ở trên. Xét một hệ thống đơn giản gồm hai thành phần M1 và
M2. Mục đích của cách tiếp cận này là kiểm chứng hệ thống này thoả mãn một thuộc
tính p mà không cần đến việc ghép nối giữa các thành phần với nhau. Dựa trên tư
tưởng này, AGV tìm ra một giả thiết A sao cho nó đủ mạnh cho M1 thoả mãn p và đủ
yếu để nó được thỏa mãn bởi M2 (tức là A M1 p và true M2 A gọi là các luật
đảm bảo giả thiết – AGR). Nếu tìm được một giả thiết A thỏa mãn các điều kiện trên
thì hệ thống khi ghép nối M1 || M2 sẽ thoả mãn thuộc tính p.
Như chúng ta đã biết, vấn đề quan trọng và cũng hết sức khó khăn của cách tiếp
cận đảm bảo giả thiết là làm sao để xác định được giả thiết A. Bên cạnh đó, kích thước
của giả thiết cũng đóng vai trò quyết định đến chi phí cho quá trình kiểm chứng hệ
thống hướng thành phần. Phương pháp đề xuất trong [4] tạo giả thiết bằng cách sử
dụng giải thuật học có tên là L*. Giải thuật này gồm nhiều bước lặp, bắt đầu từ giả
thiết rỗng để đạt được giả thiết thoả mãn yêu cầu của AGR. Tại mỗi bước lặp, giải
thuật sẽ sinh ra một giả thiết ứng cử viên. Sau đó, giải thuật sẽ kiểm tra xem ứng cử
viên đó có thoả mãn các yêu cầu của AGR hay không? Nếu thoả mãn, giải thuật sẽ
dừng và ứng cử viên đó chính là giả thiết cần tìm. Nếu yêu cầu của AGR không được
thoả mãn, quá trình kiểm tra sẽ đưa ra một phản ví dụ giúp cho giải thuật sẽ xác định
các ứng cử viên tiếp theo tốt hơn. Quá trình trên sẽ được lặp đi lặp lại cho đến khi tìm
được giả thiết hoặc chỉ ra một phản ví dụ chứng tỏ hệ thống không thỏa mãn thuộc tính
p. Tuy nhiên phương pháp này chỉ tập trung vào việc sinh giả thiết thỏa mãn các luật
đảo bảo giả thiết và kích thước của giả thiết không được đề cập tới trong phương pháp
này. Một cách tiếp cận để tối ưu cho việc kiểm chứng bảo bảo giả thiết sử dụng giải
thuật học L* được Chaki và đồng nghiệp đề xuất trong [3]. Các tác giả đề xuất 3 cách
tối ưu cho phương pháp sinh giả thiết dựa trên giải thuật học L* nhưng cũng không đề
cập tới việc tối ưu kích thước của giả thiết được sinh ra. Phương pháp sinh giả thiết tối
thiểu cho kiểm chứng phần mềm dựa trên thành phần đề xuất trong [9, 10] tập trung
vào việc sinh giả thiết có kích thước nhỏ nhất nhưng độ phức tạp của phương pháp này
là rất lớn bởi phương pháp này tìm giả thiết tối thiểu trên cây tìm kiếm bao gồm tất cả
các giả thiết ứng cử viên có thể bằng chiến lược tìm kiếm theo chiều rộng. Để lưu trữ
các bảng quan sát sinh giả thiết ứng cử viên phương pháp sử dụng cấu trúc dữ liệu
hàng đợi và kích thước hằng đợi này có thể sẽ tăng theo hàm số mũ bảng quan sát.
3

Điều này có nghĩa là chúng ta phải trả một chi phí cao cho việc sinh giả thiết tối thiểu.
Kết quả là phương pháp khó được áp dụng vào trong thực tế. Hơn nữa phương pháp
kiểm chứng đảo bảo giả thiết chỉ hiệu quả khi kích thước của giả thiết A luôn nhỏ hơn
hoặc bằng kích thước của thành phần M2. Vì lý do này, trong luận văn này chúng tôi đề
xuất một phương pháp cải tiến cho việc tối ưu phương pháp sinh giả thiết tổi thiểu
nhằm giảm độ phức tạp của phương pháp. Trong phương pháp cải tiến này thay vì việc
sử dụng chiến lược tìm kiếm theo chiều rộng trên toàn bộ không gian tìm kiếm là cây
chứa toàn bộ các giả thiết ứng cử viên bằng việc sử dụng chiến lược tìm kiếm theo
chiều sâu lặp (Iterative Deepening Depth-First Search – IDDFS) để tìm kiếm giả thiết
tối thiểu trên cây con của cây tìm kiếm bao gồm các gia thiết với kích thước nhỏ hơn
hoặc bằng kích thước của thành phần M2.
Phần còn lại của luận văn được tổ chức như sau: Chương 2 trình bày các kiến
thức cơ bản được sử dụng trong luận văn gồm: Hệ thống chuyển trạng thái có gán
nhãn (LTSs), dẫn xuất, phép toán ghép nối song song, LTS an toàn, thuộc tính an toán,
sự thảo mãn, automat đơn định hữu hạn trạng thái, vấn đề đảm bảo giả thiết. Giải thuật
học L* và phương pháp sinh giả thiết bằng giải thuật học L* sẽ được trình bày trong
chương 3. Chương 4 trình bày phương pháp sinh giả thiết tối thiểu cho việc kiểm
chứng phần mềm hướng thành phần. Trong chương này cũng sẽ trình bày chi tiết một
cải tiến cho phương pháp sinh giải thiết tối thiểu. Phương pháp này giúp giảm thời
gian và cả chi phí cho việc sinh giả thiết bằng cách áp dụng giải thuật tìm kiếm theo
chiều sâu lặp. Việc xây dựng một công cụ hỗ trợ được trình bày trong chương 5. Trong
chương này cũng trình bày kết quả thực nghiệm chứng minh cho tính đúng đắn và hiệu
quả của phương pháp cải tiến. Cuối cùng chúng tôi trình bày kết luận của luận văn,
thảo luận các nghiên cứu liên quan và những cải tiến trong tương lai trong chương 6.
4

CHƯƠNG 2. CÁC KIẾN THỨC CƠ BẢN
2.1. Labeled Transition Systems (LTSs)
Trong luận văn chúng tôi sử dụng LTSs[13] để đặc tả các hành vi của các thành
phần của hệ thống và thuộc tính cần kiểm chứng. Một LTS được xem như là một đồ
thị định hướng với các cạnh được gán nhãn. Thêm vào đó, tập trạng thái, các phép biến
đổi và tập các nhãn được kết hợp với nhau tạo nên một hệ thống. Đặt Act là tập các
hành động có thể quan sát được, và τ là hành động đại diện cho tất cả các hành động
bên trong của hệ thống.
Một LTS M là mộ bộ bốn 0,,, qMQ  , trong đó:
 Q là một tập các trạng thái không rỗng,
 αM  Act là tập các hành động có thể quan sát được gọi là bảng chữ cái của M,
  Q M Q      là hàm chuyển, và
 q0 Q là trạng thái ban đầu.
Một LTS M= 0,,, qMQ  được gọi là LTS không đơn định nếu nó có phép
biến đổi τ hoặc tồn tại (q, a, q’), (q, a, q’’)  δ trong đó q’ ≠ q’’. Ngược lại M được gọi
là đơn định (deterministic).
Giả sử có hai LTS: 0,,, qMQM  và

0,’,’,” qMQM  . Chúng ta nói LTS
M biến đổi thành M’ qua hành động a, ký hiệu ‘aM M nếu và chỉ nếu (q0, a, q

0)  δ
và αM = αM’ và δ = δ’. Chúng ta sử dụng π để ký hiệu một trạng thái lỗi cụ thể, để thể
hiện sự vi phạm trong hệ thống ghép nối. Chúng ta sử dụng  để ký hiệu cho LTS
{}, Act, , . Hình 2.1 biểu diễn cho 2 LTS Input và Output.
Hình 2.1: Ví dụ về LTSs
2.2. Dẫn xuất (Traces)
Một dẫn xuất [2, 4] t của một LTS 0, , ,M Q M q   là một chuỗi hữu hạn
các hành động 1… …i na a a sao cho tồn tại một chuỗi các trạng thái 0 ,…, ,…,i nq q q thỏa
mãn điều kiện 1( , , )i i iq a q   với i=1..n. Giả sử ,Act  ký hiệu t↑Σ, biểu diễn một
dẫn xuất thu được bằng cách loại bỏ khỏi t tất cả các hành động a mà a . Tập tất
cả các dẫn xuất của M được gọi là ngôn ngữ đoán nhận M, ký hiệu L(M). Với LTS
Input:
in
ack
send

0 1 2

Output:
send
ack
out

a b c

5

Input được mô tả trong Hình 2.1 thì in, in send, in send ack là các dẫn xuất. Còn in in,
in send send không phải là các dẫn xuất.
2.3. Ghép nối song song (Parallel Compostion)
Ghép nối song song (ký hiệu là ||) [13] là phép toán giao hoán và kết hợp. Nó
kết hợp hành vi của hai thành phần phần mềm bằng cách đồng bộ hoá các hành động
chung tương ứng với bảng chữ cái, và chèn thêm các hành động còn lại. Xét hai LTS,
),,,( 101111 qMQM  và ),,,(
2
02222 qMQM  . Quá trình ghép nối song song giữa M1
và M2, ký hiệu M1 || M2, được định nghĩa như sau:
 Nếu M1 =  hoặc M2 =  , khi đó M1|| M2 =  .
 M1|| M2 là một LTS ),,,( 0qMQM  trong đó, Q = Q1 x Q2, αM = αM1
 αM2,
1 2
0 0 0q q q  , và phép biến đổi quan hệ δ được xác định như sau:
i)
   
     



‘,’,,,
‘,,,’,,, 2121
qpqp
qqppMM
(2.1)
ii)
 
     



qpqp
ppMM
,’,,,
‘,,, 121 (2.2)
iii)
 
     



‘,,,,
‘,,, 212
qpqp
qqMM
(2.3)
Ví dụ 2.1: Khi ta ghép nối hai mô hình được thể hiện bằng hai LTS Input và
Output trong Hình 2.1. Các hành động send và ack được đồng bộ trong khi các hành
động khác được xen kẽ. Các trạng thái không tới được từ trạng thái ban đầu (0,0) sẽ
bị loại bỏ. Kết quả của phép ghép nối song song LTS Input || Output được thể hiện
trong Hình 2.2.
Hình 2.2: LTS của Input || Output
2.4. LTS an toàn và thuộc tính an toàn
Một LTS an toàn (Safety LTS) là một LTS hữu hạn không chứa bất kỳ một
trạng thái lỗi π nào. Thuộc tính an toàn (Safte Property) [14] là thuộc tính đảm bảo
không lỗi xảy ra trong quá trình thực hiện của hệ thống. Một thuộc tính an toàn được
biểu diễn như là một LTS an toàn p trong đó ngôn ngữ L(p) xác định tập tất cả các
Input || Output
in
ack
send
0,a 0,b 0,c
1,a 1,b 1,c
2,a 2,b 2,c
in in
out
out
out
Input || Output
in
ack
send
0,a
1,a
2,b 2,c
out
6

thuộc tính chấp nhận được. Một LTS lỗi (error LTS), ký hiệu perr phát sinh trong quá
trình kiểm chứng LTS M thoả mãn thuộc tính p. Về cơ bản, error LTS của một thuộc
tính 0,,, qpQp  là   0,’,, qpQp errerr  , trong đó αperr = αp
và  ’ , , | and q a a p       ’ ‘ q : ( , , )Q q a q   . Hình 2.3 biểu diễn LTS của thuộc
tính an toàn p và LTS lỗi perr được tạo từ LTS p.
Hình 2.3. LTS của thuộc tính an toàn
2.5. Sự thỏa mãn (Satisfiability)
Cho một LTS M, ta nói M thoả mãn thuộc tính p, ký hiệu M╞ p, nếu và chỉ nếu
)()(:)( pLpML   . Để kiểm chứng một thành phần M thoả mãn một thuộc
tính p, khi đó cả M và perr phải được biểu diễn dưới dạng của LTS an toàn (Safety
LTS), sau đó thực hiện phép toán ghép nối song song M || perr. Nếu LTS thu được sau
phép ghép nối tồn tại một dẫn xuất có thể tới trạng thái π, khi đó ta nói thành phần M
vi phạm thuộc tính p. Ngược lại, M thoả mãn thuộc tính p.
Ví dụ 2.2: Để kiểm tra hệ thống ghép nối Input ||Output có thỏa mãn thuộc tính
p, hệ thống ghép nối song song Input||Output || perr được tính như trong hình 2.4. Dễ
dàng kiểm tra được rằng trạng thái lỗi π không đạt tới được trong hệ thống ghép nối
này. Vì vậy, chúng ta kết luận hệ thống ghép nối Input ||Output thỏa mãn thuộc tính p.
2.6. Ôtomat đơn định hữu hạn trạng thái
Chúng tôi sử dụng thuật toán học có tên L* [1, 17] để tạo giả thiết từ hai thành
phần phần mềm. Trong thuật toán này, tại mỗi bước lặp, một ôtomat đơn định hữu hạn
trạng thái (Deterministic Finite State Automata – DFA) Mi được tạo ra. Mi sau đó sẽ
được biến đổi thành giả thiết ứng cử viên Ai, trong đó Ai được thể hiện như là một
LTS an toàn. DFA được định nghĩa như sau:
Ôtomat hữu hạn có thể xem như “máy trừu tượng” để đoán nhận ngôn ngữ.
Ôtomat hữu hạn là bộ M = , trong đó:
 Q, αM, δ, qo được định nghĩa như trong định nghĩa của các LTS hữu hạn.
 F  Q là tập các trạng thái kết thúc.
LTS lỗi perr
out

in

in
out

ii i

in
out

ii i
LTS của thuộc tính p
7

Cho một DFA M và một chuỗi σ, ký hiệu δ(q, σ) là trạng thái kết quả sau khi M
đọc chuỗi σ bắt đầu tại trạng thái q. Ta nói DFA M đoán nhận chuỗi σ hay chuỗi σ
được đoán nhận bởi ôtomat hữu hạn M nếu δ(q0, σ)  F. Tập L(M) = {σ | δ(q0, σ) 
F} được gọi là ngôn ngữ được đoán nhận bởi Ôtomat M.
Hình 2.4: Tính ghép nối Input || Output || perr.
Cho một DFA M, chúng ta cũng dễ dàng thu được một LTS an toàn A từ M
bằng cách loại bỏ tất cả các trạng thái không phải là trạng thái kết thúc và các biến đổi
liên quan đến trạng thái này bên trong M. Hình 2.4 mô tả một ví dụ để biến đổi một
DFA thành một LTS an toàn:

Hình 2.5: Minh hoạ tạo LTS an toàn từ một DFA.
2.7. Đảm bảo giả thiết (Assume-Guarantee Reasoning)
Xác minh đảm bảo giả thiết các phần mềm hướng thành phần là một cách tiếp
cận được đưa ra bởi D.Giannakopoulou [2, 4, 6, 7]. Cách tiếp cận này dựa trên tư
tưởng của kiểm chứng mô hình giả thiết. Nó đưa ra một cách tiếp cận đầy hứa hẹn để
giải quyết vấn đề xác minh đối với những hệ thống lớn. Cách tiếp cận này dựa trên tư
tưởng của chiến lược “Chia để trị”, thuộc tính của hệ thống được biến đổi thành các
out

in

in
out

ii i

perr
in
0,a,i 1,a,i 2,b,i 2,c,i
0,a,ii 1,a,ii 2,b,ii 2,c,ii
π

Input || Output || perr π unreachable!
in
ack
ack
send
send
out
out
Input || Output
ack
send
0,a 1,a 2,b 2,c
out

in

Tác giả

Đào Anh Hiển

Nhà xuất bản

Đại học Công nghệ,

Năm xuất bản

2014

Người hướng dẫn

Nguyễn Việt Hà

Định danh

00050003616

Kiểu

text

Định dạng

text/pdf

Nhà xuất bản

Khoa công nghệ thông tin,

Trường đại học Công nghệ

Các đánh giá

Hiện chưa có đánh giá cho sản phẩm.

Hãy là người đầu tiên đánh giá “Tối ưu việc sinh giả thiết bằng giải thuật học L* cho kiểm chứng từng phần phần mềm dựa trên thành phần”

Email của bạn sẽ không được hiển thị công khai. Các trường bắt buộc được đánh dấu *