ĐẠ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 (AssumeGuarantee 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 Q, M , , q0 , 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= Q,M , , q0 đượ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: M Q, M , , q0 và M ' Q' , M ' , ' , q0' . Chúng ta nói LTS
M biến đổi thành M’ qua hành động a, ký hiệu M a 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.
Input:
0
in
Output:
send
send
1
2
a
out
b
c
ack
ack
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 M Q, M , , q0 là một chuỗi hữu hạn
các hành động a1...ai ...an sao cho tồn tại một chuỗi các trạng thái q0 ,..., qi ,..., qn thỏa
mãn điều kiện (qi 1 , ai , qi ) 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
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,
M 1 (Q1 , M 1 , 1 , q 10 ) và M 2 (Q2 , M 2 , 2 , q 02 ) . 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 M (Q, M , , q 0 ) trong đó, Q = Q1 x Q2, αM = αM1
αM2, q0 q10 q02 , và phép biến đổi quan hệ δ được xác định như sau:
i)
M 1 M 2 , p, , p ' 1 , q, , q ' 2
p, q , , p' , q'
(2.1)
ii)
M 1 \ M 2 , p , , p ' 1
p, q , , p' , q
(2.2)
iii)
M 2 \ M 1 , q, , q ' 2
p, q , , p, q'
(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.
Input || Output
Input || Output
ack
in
out
0,b
0,a
in
1,b
1,a
ack
0,c
in
out
1,c
in
1,a
send
send
2,a
0,a
2,b
out
2,c
2,b
out
2,c
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
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
p Q , p , , q 0
tính
là perr Q ,p err , ' , q0 , trong đó αperr = αp
và ' q, a, | a p and 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.
in
in
i
i
out
ii
out
ii
out
in
LTS của thuộc tính p
LTS lỗi perr
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
L( M ) : ( p ) L( p) . Để 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.
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.
perr
Input || Output
ack
0,a
in
1,a
send
in
i
2,b
out
ii
out
2,c
out
Input || Output || perr
0,a,i
1,a,i
ack
send
1,a,ii
ack
send
in
0,a,ii
in
π unreachable!
2,b,i
2,c,i
out
out
2,b,ii
π
2,c,ii
in
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
8
thuộc tính của các thành phần sau đó thay vì kiểm tra trên toàn hệ thống chúng ta sẽ
chỉ cần kiểm tra độc lập trên từng thành phần.
Xét một hệ thống đơn giản gồm hai thành phần độc lập M1 và M2. Bài toán
quan trọng, cũng là xuyên suốt quá trình nghiên cứu của chúng ta là cần xác minh
xem, một hệ thống M1 || M2 có thoả mãn một thuộc tính p nào đó hay không? Nếu
chúng ta xác minh trên toàn bộ hệ thống M1 || M2, giải pháp này sẽ dẫn tới vấn đề
“bùng nổ không gian trạng thái”. Đảm bảo giả thiết nhằm đưa ra giải pháp để kiểm tra
hệ thống M1 || M2 có thoả thuộc tính p hay không mà không cần thực hiện phép ghép
nối song song giữa M1 và M2.
Đảm bảo giả thiết sử dụng tư tưởng của chiến lược “Chia để trị”, 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. Nếu M1
thoả mãn p với một điều kiện nào đó, và M2 cũng thoả mãn điều kiện đó, khi đó hệ
thống M gồm M1 và M2 cũng thoả mãn điều kiện p. Điều kiện ở đây được thể hiện bởi
các giả thiết (Assumptions). Như vậy để kiểm chứng hệ thống sử dụng phương pháp
này, đòi hỏi chúng ta phải xác định được giả thiết, bài toán này chúng ta sẽ xem xét
sau. Ở đây chúng ta giả thiết có một giả thiết A đã được xác định và thuật toán trên của
chúng ta đã được chứng minh là đúng đắn. Giả thiết A được đưa ra, yêu cầu phải trừu
tượng hơn M2 nhưng vẫn thể hiện được các đặc tính của M2. Hơn nữa, giả thiết phải đủ
mạnh để M1 thoả mãn p (Hình 2.6 minh hoạ tổng quan về mục tiêu và giải pháp cho
cách tiếp cận xác minh đảm bảo giả thiết). Như vậy, bài toán kiểm chứng hệ thống M
= M1 || M2 có thoả mãn thuộc tính p hay không? Ta đã đưa được về việc giải quyết hai
bài toán con:
A M1 P
true M 2 A .
Để kiểm chứng công thức A M 1 P ta thực hiện phép ghép nối song song
A||M1||perr. Trong đó, A, M1, p, perr được biểu diễn bởi các LTS. Nếu không có dẫn
xuất đến trạng thái lỗi xảy ra trong A||M1||perr thì công thức A M 1 P thỏa mãn. Hay
nói cách khác là A||M1 thỏa p. Ngược lại, A||M1 không thỏa p.
Hình 2.6: Bài toán và tư tưởng chính của cách tiếp cận xác minh đảm bảo giả thiết.
9
Với công thức true M 2 A , kiểm tra xem M2 có thoả mãn thuộc tính A hay
không với bất kỳ điều kiện gì của môi trường. Để kiểm chứng công thức này ta chỉ cần
thực hiện phép ghép nối M2||A, nếu LTS kết quả không tồn tại một dẫn xuất nào dẫn
tới trạng thái lỗi khi đó M2 thoả A, ngược lại M2 không thoả A.
Từ giải pháp trên, vấn đề chính trong cách tiếp cận này là làm thế nào để tìm ra
giả thiết A. Hiện tại, có hai phương pháp tạo giả thiết A một cách tự động như sau:
i. Phương pháp thứ nhất được đưa ra trong [6]. Cho trước thành phần M1, thuộc
tính p và phần giao diện của M1 với môi trường của nó, tạo giả thiết môi trường yếu
nhất AW sao cho M1 ╞ p. Giả thiết yếu nhất AW tức là nó ràng buộc môi trường không
nhiều hơn cũng không ít hơn những gì nó cần, cụ thể như sau: với mọi môi trường E
khi đó E || M1 ╞ p khi và chỉ khi E ╞ AW. Giả thiết yếu nhất AW chứa tất cả các dẫn
xuất trên bảng chữ cái ( M 1 p) M 2 không chứa trạng thái lỗi trong hệ thống
M1||p. Trong trường hợp này, M2 là không biết và được xem như là môi trường của M1.
ii. Phương pháp thứ hai được đưa ra trong [2, 4, 8] . Kỹ thuật này sử dụng thuật
toán học L* để thực hiện tạo giả thiết A đảm bảo rằng A là đủ yếu để được thoả mãn
bởi M2 và đủ mạnh để M1 thoả mãn thuộc tính p. Giả thiết A được tạo ra bởi phương
pháp này là mạnh hơn so với giả thiết yếu nhất AW.
10
CHƯƠNG 3. PHƯƠNG PHÁP SINH GIẢ THIẾT TỐI THIỂU BẰNG GIẢI
THUẬT HỌC L*
Chương 2 đã trình bày một cách tổng quan cách tiếp cận đưa ra nhằm xác minh
phần mềm hướng thành phần. Một bài toán quan trọng trong kỹ thuật này là làm thế
nào để tạo ra được một giả thiết. Chương này sẽ giới thiệu một cách để tạo ra một giả
thiết giữa hai thành phần M1 và M2. Thông tin chi tiết về giải thuật học L* cũng được
trình bày trong chương này.
3.1. Giải thuật học L*
Giả sử có một tập ký tự ∑ cho trước. Với mỗi ngôn ngữ chính quy U có bảng
chữ cái là tập con của ∑*. Chúng ta cần tìm một Ôtomat đơn định tối thiểu hữu hạn
trạng thái (DFA) M đoán nhận ngôn ngữ U, tức là L(M) = U.
Tư tưởng chính của giải thuật này dựa trên định lý: “Myhill – Nerode Theorem”
[15]: Giả sử có một tập ký tự ∑. Với mỗi ngôn ngữ chính quy U, có bảng chữ cái là tập
con của ∑* cho trước, khi đó tồn tại duy nhất một DFA đoán nhận nó.
Giải thuật học L* được phát triển bởi [1] và sau đó được cải tiến bởi Rivest và
Schapire [17]. Trong luận văn này, chúng tôi sẽ trình bày giải thuật đã được cải tiến
với cùng tên L*. Dựa trên tư tưởng học, giải thuật L* sẽ thực hiện xây dựng dần dần
từng bước nghiệm của bài toán. Để huấn luyện U, L* cần thiết phải kết hợp với
Minimally Adequate Teacher, từ bây giờ chúng ta sẽ gọi là Teacher (người huấn
luyện). Teacher sẽ phải trả lời chính xác hai loại câu hỏi từ L*:
Kiểm tra thành viên (Membership query), với một chuỗi * , câu trả
lời là true nếu U và false nếu ngược lại.
Loại câu hỏi thứ hai: kiểm tra sự phỏng đoán. Với mỗi ứng cử viên DFA
M, khi đó, ngôn ngữ của nó có đồng nhất với U hay không? Tức là L(M) = U? Câu trả
lời là true nếu L(M) = U, ngược lại, Teacher sẽ đưa ra một phản ví dụ để minh chứng
cho sự khác nhau giữa L(M) và U.
Mối liên hệ giữa bộ huấn luyện L* và nhà huấn luyện Teacher được minh họa
như Hình 3.1.
Chi tiết hơn, L* sử dụng một bảng T để ghi lại kết quả kiểm tra một chuỗi
s * có thuộc vào U hay không? Bảng quan sát T được cập nhật mỗi khi có sự thay
đổi bởi các thao tác kiểm tra thành viên. Ôtomat hữu hạn Mi được xây dựng dựa trên
bảng T, và khi đó với mỗi Mi, các nhà huấn luyện sẽ quyết định xem sự phỏng đoán đó
có đúng hay không? Nếu phỏng đoán là chính xác, thuật toán sẽ dừng ở đây, ngược lại,
L* sử dụng phản ví dụ mà nhà huấn luyện trả lại để cập nhật lại bảng T.
Giải thuật L* xây dựng một bảng quan sát (S, E, T), trong đó:
11
S * là tập tiền tố. Nó thể hiện các lớp tương đương hay các trạng thái.
E * là tập hậu tố. Nó thể hiện sự khác nhau giữa U và L(Mi).
T : S S . true, false , trong đó toán tử “.” thực hiện ghép nối hai
xâu được định nghĩa như sau: P.Q pq | p P, q Q . Như vậy, bảng T được sử dụng
để kiểm tra xem với mỗi chuỗi s * , s có thuộc vào tập U hay không. Tức là, T(s) =
true nếu s U , ngược T(s) = false nếu s U .
Hình 3.1: Minh hoạ mối quan hệ giữa Teacher và L* learner.
Bảng
quan
sát
(S,
E,
T)
được
gọi
là
đóng
nếu:
’
s S , a , s ' S , e E : T ( sae) T ( s ' e) . Trong trường hợp này, s là trạng thái tiếp
theo từ trạng thái s sau khi đi qua a. Bảng quan sát (S, E, T) là đóng, khi đó mỗi hàng
sa trong S.∑ sẽ tương ứng với một hàng s’ trong S.
Giải thuật L* được trình bày chi tiết từng bước như trong Giải thuật 1.
Giải thuật 1 Giải thuật học L*
Input: U, : một ngôn ngữ chính quy chưa biết U trên bộ chữ cái
Output: M: một DFA M sao cho M là một Ôtomat hữu đơn định cực tiểu tương ứng
với U và L(M) = U.
1: Khởi tạo, S = {}, E = {}
2: loop
3:
cập nhật bảng T sử dụng truy vấn thành viên
4:
while (S, E, T) chưa là bảng đóng do
5:
thêm sa vào S để tạo S đóng với s S và a
6:
cập nhật bảng T sử dụng truy vấn thành viên
7:
end while
8:
xây dựng một DFA ứng cử viên M từ bảng đóng (S, E, T)
9:
thể hiện một truy vấn tương đương: L(M) = U?
10:
if M là đúng then
12
11:
return M
12: else
13
thêm hậu tố e * của phản ví dụ cex vào E
14: end if
15: end loop
Đầu tiên, giải thuật L* khởi gán các tập S và E là tập rỗng {λ} (dòng 1) với λ
thể hiện cho chuỗi rỗng. Tiếp theo, giải thuật thực hiện cập nhật bảng quan sát (S, E,
T) bằng cách thực hiện các thao tác kiểm tra thành viên để có sự liên kết giữa các
chuỗi trong tập S S . .E (dòng 3). Giải thuật sau đó sẽ kiểm tra xem bảng quan sát
có đóng hay không (dòng 4). Nếu bảng quan sát là không đóng, khi đó sa được thêm
vào tập S, trong đó s S và a ∑ là các hàng mà không tồn tại s’ S sao cho T(sae)
= T(s’e) (dòng 5). Vì sa được thêm vào tập S, khi đó T phải được cập nhật lại sử dụng
các hành động kiểm tra thành viên (dòng 6). Dòng 5 và dòng 6 được lặp đi lặp lại cho
đến khi bảng quan sát (S, E, T) là bảng đóng.
Khi bảng quan sát (S, E, T) là bảng đóng, một DFA M sẽ được xây dựng (dòng
8) từ bảng đóng (S, E, T) như sau:
Một DFA M = được xây dựng từ một bảng đóng (S, E, T),
trong đó:
Q = S,
αM = ∑, trong đó ∑ là bảng chữ cái của ngôn ngữ U,
Biến đổi δ được định nghĩa như sau: δ(s, a) = s’ và e E: T(sae) =
T(s’e),
Trạng thái ban đầu q0 = λ,
F = {s S | T(s) = true}.
Một ứng cử viên DFA M được thể hiện như là một phỏng đoán tới Teacher
(dòng 9). Nếu Teacher trả lại kết quả true (tức là, L(M) = U) (dòng 10), L* trả lại M là
chính xác (dòng 11), ngược lại nó sẽ nhận được một phản ví dụ cex ∑* từ Teacher.
Phản ví dụ cex được phân tích bởi L* để tìm ra một hậu tố e của cex để minh chứng
cho sự khác nhau giữa L(M) và U. Sau đó, e phải được thêm vào tập E (dòng 13). Sau
khi e được thêm vào tập E, giải thuật L* sẽ lặp lại toàn bộ quá trình bằng cách quay
lại dòng 3.
Mỗi ứng cử viên DFA Mi được đưa ra bởi giải thuật L* là nhỏ nhất. Nó có
nghĩa là, với mỗi DFA bước i +1 tiếp theo luôn có số trạng thái luôn nhiều hơn hoặc ít
nhất cũng bằng với số trạng thái của Mi. Giả sử M1, M2, ..., Mn là các ứng cử viên
được đưa ra bởi giải thuật L* theo từng bước, dễ dàng kiểm tra được rằng |M1| ≤ |M2|
≤....≤ |Mn|, trong đó |Mi| kí hiệu cho số trạng thái của DFA Mi. Giả sử M là giả thiết
- Xem thêm -