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. 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 LUAN VAN CHAT LUONG download : add luanvanchat@agmail. 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.
LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 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. LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 4 CHƯƠNG 2. CÁC KIẾN THỨC CƠ BẢN 2. 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).