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

Quá trình phát triển phần mềm hướng thành phần được biết đến là sự phát triển phần mềm bằng cách ghép nối các phần độc lập. Đây là một trong những kỹ thuật quan trọng nhất trong kỹ nghệ phần mềm. Cách tiếp cận này vẫn đang thu hút sự chú ý trong cộng đồng kỹ nghệ phần mềm và được xem là một cách tiếp cận mở, hiệu quả, giảm thời gian và chi phí phát triển đồng thời tăng chất lượng của phần mềm. Đã có rất nhiều khái niệm, kỹ thuật đề xuất nhằm phát triển cho ý tưởng này.

Tuy nhiên, một trong những hạn chế của phát triển phần mềm hướng thành phần là vấn đề đảm bảo tính đúng đắn của hệ thống khi ghép nối các thành phần với nhau vì các thành phần có thể được phát triển một cách độc lập hoặc được đặt mua từ các công ty thứ 3 (third parties). Hiện tại, các công nghệ hỗ trợ phát triển phần mềm hướng thành phần như CORBA (OMG), COM/DCOM or .NET (Microsoft), Java and JavaBeans (Sun), … vv chỉ hỗ trợ việc ghép nối các thành phần (component plugging). Chúng không có cơ chế kiểm tra liệu các thành phần có thể bị lỗi khi cộng tác với nhau hay không. Điều này có nghĩa là cơ chế “plug-and-play” không được đảm bảo. Một giải pháp phổ biến hiện nay để giải quyết cho vấn đề trên là áp dụng kiểm chứng mô hình (Model Checking – MC). Kiểm chứng mô hình là một cách tiếp cận quan trọng để giải quyết bài toán chứng minh độ tin cậy của phần mềm. Nó cũng tạo ra một không gian trạng thái chi tiết có thể bao phủ được các hệ thống đang được kiểm tra đồng thời đạt được hiệu quả đặc biệt trong quá trình dò các lỗi tổng hợp khá phức tạp mà nguyên nhân chủ yếu do quá trình ghép nối các thành phần gây nên. Tuy nhiên, một trong những hạn chế lớn nhất của kiểm chứng mô hình là “vấn đề bùng nổ không gian trạng thái” khi kiểm chứng các phần mềm có kích thước lớn. Một trong những cách tiếp cận tiềm năng để giải quyết vấn đề này là áp dụng kiểm chứng từng phần (Modular Model Checking – MMC). Thay vì tiến hành kiểm chứng trên toàn bộ hệ thống gồm các thành phần được ghép nối với nhau, cách tiếp cận này tiến hành kiểm chứng trên từng thành phần riêng biệt. Với cách tiếp cận này, vấn đề bùng nổ không gian trạng thái hứa hẹn sẽ được giải quyết. Một trong những phương pháp kiểm chứng hỗ trợ ý tưởng này là phương pháp kiểm chứng đảm bảo giả thiết (Assume- Guarantee Verification – AGV) . Sử dụng tư tưởng của chiến lược “chia để trị”, AGV phân chia bài toán kiểm chứng thành các bài toán con cùng dạng nhưng kích thước nhỏ hơn sao cho chúng ta có thể kiểm chứng các bài toán con một cách riêng biệt. AGV được đánh giá là một phương pháp hứa hẹn để kiểm chứng phần mềm hướng thành phần thông qua phương pháp kiểm chứng mô hình. AGV không những thích hợp cho phần mềm hướng thành phần mà còn có khả năng giải quyết vấn đề bùng nổ không gian trạng thái trong kiểm chứng mô hình. Trong phương pháp này, các giả thiết (assumptions) (có vai trò như là môi trường của các thành phần) sẽ được tạo lập. Việc tạo lập các giả thiết chính là bài toán quan trọng nhất trong phương pháp này. Mục tiêu chính của cách tiếp cận này là nhằm kết hợp tốt nhất giữa lợi thế của hai phần: kiểm chứng mô hình và phát triển hướng thành phần.

Hiện nay, đã có nhiều nghiên cứu về kiểm chứng mô hình từng phần cho phần mềm hướng thành phần. Mỗi khi thêm một thành phần nào đó vào hệ thống, thì toàn bộ hệ thống gồm các thành phần đang tồn tại và thành phần mới phải được kiểm chứng lại. Vì thế, đối với những phần mềm phức tạp, vấn đề “bùng nổ không gian trạng thái” có thể xảy ra khi áp dụng các phương pháp trong các nghiên cứu này. Cách tiếp cận trong đề xuất phương pháp kiểm chứng đảm bảo giả thiết như đã trình bày ở trên. Xét một hệ thống đơn giản gồm hai thành phần M1 và M2. Mục đích của cách tiếp cận này là kiểm chứng hệ thống này thoả mãn một thuộc tính p mà không cần đến việc ghép nối giữa các thành phần với nhau. Dựa trên tư tưởng này, AGV tìm ra một giả thiết A sao cho nó đủ mạnh cho M1 thoả mãn p và đủ yếu để nó được thỏa mãn bởi M2 (tức là A M1 p và true M2 A gọi là các luật đảm bảo giả thiết – AGR). Nếu tìm được một giả thiết A thỏa mãn các điều kiện trên thì hệ thống khi ghép nối M1 || M2 sẽ thoả mãn thuộc tính p.

Như chúng ta đã biết, vấn đề quan trọng và cũng hết sức khó khăn của cách tiếp cận đảm bảo giả thiết là làm sao để xác định được giả thiết A. Bên cạnh đó, kích thước của giả thiết cũng đóng vai trò quyết định đến chi phí cho quá trình kiểm chứng hệ thống hướng thành phần. Phương pháp đề xuất tạo giả thiết bằng cách sử dụng giải thuật học có tên là L*. Giải thuật này gồm nhiều bước lặp, bắt đầu từ giả thiết rỗng để đạt được giả thiết thoả mãn yêu cầu của AGR. Tại mỗi bước lặp, giải thuật sẽ sinh ra một giả thiết ứng cử viên. Sau đó, giải thuật sẽ kiểm tra xem ứng cử viên đó có thoả mãn các yêu cầu của AGR hay không? Nếu thoả mãn, giải thuật sẽ dừng và ứng cử viên đó chính là giả thiết cần tìm. Nếu yêu cầu của AGR không được thoả mãn, quá trình kiểm tra sẽ đưa ra một phản ví dụ giúp cho giải thuật sẽ xác định các ứng cử viên tiếp theo tốt hơn. Quá trình trên sẽ được lặp đi lặp lại cho đến khi tìm được giả thiết hoặc chỉ ra một phản ví dụ chứng tỏ hệ thống không thỏa mãn thuộc tính p. Tuy nhiên phương pháp này chỉ tập trung vào việc sinh giả thiết thỏa mãn các luật đảo bảo giả thiết và kích thước của giả thiết không được đề cập tới trong phương pháp này. Một cách tiếp cận để tối ưu cho việc kiểm chứng bảo bảo giả thiết sử dụng giải thuật học L* được Chaki và đồng nghiệp đề xuất trong [3]. Các tác giả đề xuất 3 cách tối ưu cho phương pháp sinh giả thiết dựa trên giải thuật học L* nhưng cũng không đề cập tới việc tối ưu kích thước của giả thiết được sinh ra. Phương pháp sinh giả thiết tối thiểu cho kiểm chứng phần mềm dựa trên thành phần đề xuất trong [9, 10] tập trung vào việc sinh giả thiết có kích thước nhỏ nhất nhưng độ phức tạp của phương pháp này là rất lớn bởi phương pháp này tìm giả thiết tối thiểu trên cây tìm kiếm bao gồm tất cả các giả thiết ứng cử viên có thể bằng chiến lược tìm kiếm theo chiều rộng. Để lưu trữ các bảng quan sát sinh giả thiết ứng cử viên phương pháp sử dụng cấu trúc dữ liệu hàng đợi và kích thước hằng đợi này có thể sẽ tăng theo hàm số mũ bảng quan sát.

Điều này có nghĩa là chúng ta phải trả một chi phí cao cho việc sinh giả thiết tối thiểu. Kết quả là phương pháp khó được áp dụng vào trong thực tế. Hơn nữa phương pháp kiểm chứng đảo bảo giả thiết chỉ hiệu quả khi kích thước của giả thiết A luôn nhỏ hơn hoặc bằng kích thước của thành phần M2. Vì lý do này, trong luận văn này chúng tôi đề xuất một phương pháp cải tiến cho việc tối ưu phương pháp sinh giả thiết tổi thiểu nhằm giảm độ phức tạp của phương pháp. Trong phương pháp cải tiến này thay vì việc sử dụng chiến lược tìm kiếm theo chiều rộng trên toàn bộ không gian tìm kiếm là cây chứa toàn bộ các giả thiết ứng cử viên bằng việc sử dụng chiến lược tìm kiếm theo chiều sâu lặp (Iterative Deepening Depth-First Search – IDDFS) để tìm kiếm giả thiết tối thiểu trên cây con của cây tìm kiếm bao gồm các gia thiết với kích thước nhỏ hơn hoặc bằng kích thước của thành phần M2.

Phần còn lại của luận văn được tổ chức như sau: Chương 2 trình bày các kiến thức cơ bản được sử dụng trong luận văn gồm: Hệ thống chuyển trạng thái có gán nhãn (LTSs), dẫn xuất, phép toán ghép nối song song, LTS an toàn, thuộc tính an toán, sự thảo mãn, automat đơn định hữu hạn trạng thái, vấn đề đảm bảo giả thiết. Giải thuật học L* và phương pháp sinh giả thiết bằng giải thuật học L* sẽ được trình bày trong chương 3. Chương 4 trình bày phương pháp sinh giả thiết tối thiểu cho việc kiểm chứng phần mềm hướng thành phần. Trong chương này cũng sẽ trình bày chi tiết một cải tiến cho phương pháp sinh giải thiết tối thiểu. Phương pháp này giúp giảm thời gian và cả chi phí cho việc sinh giả thiết bằng cách áp dụng giải thuật tìm kiếm theo chiều sâu lặp. Việc xây dựng một công cụ hỗ trợ được trình bày trong chương 5. Trong chương này cũng trình bày kết quả thực nghiệm chứng minh cho tính đúng đắn và hiệu quả của phương pháp cải tiến. Cuối cùng chúng tôi trình bày kết luận của luận văn, thảo luận các nghiên cứu liên quan và những cải tiến trong tương lai trong chương 6.

Link tải tài liệu: https://tii.la/ZoQ4pl40

Lưu ý: Link tải có chứa quảng cáo được rút gọn bằng Shrinkearn.com

Mật khẩu mở tệp PDF: sharetailieu.net

Nghiên cứu chế tạo và khảo sát tính chất vật liệu Polyme Nanocompozit trên cơ sở Polyaniline và Graphit

Nghiên cứu công nghệ chế tạo và tính chất của giả vật liệu Metamaterial

Nghiên cứu chế tạo vật liệu sắt điện BaTiO3 và tổ hợp BaTiO3/Fe3O4 có cấu trúc micro-nano bằng phương pháp thủy phân nhiệt

Tiếp cận các ứng dụng giao thức truyền thông không dây MiWi PRO

Nghiên cứu chế tạo và khảo sát tính chất vật liệu Polyme Nanocompozit trên cơ sở Polyaniline và Graphit

Nghiên cứu công nghệ chế tạo và tính chất của giả vật liệu Metamaterial

Nghiên cứu chế tạo vật liệu sắt điện BaTiO3 và tổ hợp BaTiO3/Fe3O4 có cấu trúc micro-nano bằng phương pháp thủy phân nhiệt

Tiếp cận các ứng dụng giao thức truyền thông không dây MiWi PRO

LEAVE A REPLY Cancel reply

Mới Nhất

Nghiên cứu chế tạo và khảo sát tính chất vật liệu Polyme Nanocompozit trên cơ sở Polyaniline và Graphit

Nghiên cứu công nghệ chế tạo và tính chất của giả vật liệu Metamaterial

Nghiên cứu chế tạo vật liệu sắt điện BaTiO3 và tổ hợp BaTiO3/Fe3O4 có cấu trúc micro-nano bằng phương pháp thủy phân nhiệt

Tiếp cận các ứng dụng giao thức truyền thông không dây MiWi PRO

Nâng cao độ chính xác định vị robot bằng phương pháp tổng hợp dữ liệu cảm biến lập mã quang với bộ lọc Kalman...

Cùng Chuyên Mục

Đọc Nhiều Nhất

Áp dụng OSGi trong việc xây dựng hệ thống dựa thành...

Kiến trúc hướng dịch vụ và ứng dụng điện toán đám...

Nghiên cứu tính khả kiểm thử của ứng dụng trên nền...

Kiểm thử đơn vị cho hệ thống

Phát triền phần mềm cho người học tại Đại học Quốc...

Các kỹ thuật phân cụm trong khai phá dữ liệu sử...