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

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 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 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). 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). 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). 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 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. 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 đề 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. 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.

Tải về miễn phí bản đầy đủ luận văn tại địa chỉ:

https://www.file-upload.com/ea38i95m0r5a

Tác giả

ĐÀO ANH HIỂN

Ngành

Công nghệ thông tin

Chuyên ngành

Khoa học máy tính

Mã số

60480101

Người hướng dẫn khoa học

PGS. TS NGUYỄN VIỆT HÀ

Đánh giá

Chưa có đánh giá nào.

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 *