Đăng ký Đăng nhập
Trang chủ Tối ưu việc sinh giả thiết bằng giải thuật học lcho kiểm chứng từng phần phần mề...

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

.PDF
58
293
96

Mô tả:

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

Tài liệu liên quan