MỞ ĐẦU Phát triển phần mềm hƣớng thành phần (Component-Based Software Development - CBSD) là một trong những công nghệ quan trọng nhất trong kỹ nghệ phần mềm. Hệ thống phần mềm hƣớng thành phần đƣợc xây dựng dựa trên quá trình lựa chọn và ghép nối các thành phần riêng biệt thành một hệ thống hoàn chỉnh. Với cách tiếp cận này, phát triển phần mềm hƣớng thành phần đã góp phần rút ngắn thời gian thực hiện dự án, nâng cao chất lƣợng và độ tin cậy của sản phầm. Vì những ƣu điểm này mà công nghệ này đã đƣợc áp dụng rộng rãi trong quá trình phát triển các dự án phần mềm hiện nay.
Tuy nhiên, một trong những hạn chế của CBSD 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 trong những giải pháp phổ biến để giải quyết vấn đề nêu trên là sử dụng các phƣơng pháp kiểm chứng mô hình (Model checking). 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 verification - MV). 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ả định (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. AVG đƣợ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.
AVG không những thích hợp cho phần mềm hƣớng thành phần mà còn có khả LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 5 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ả định (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ả định chính là bài toán quan trọng nhất trong phƣơng pháp này. Kích thƣớc của các giả định này (số lƣợng trạng thái) nên đƣợc cực tiểu hóa bởi vì chi phí cho quá trình kiểm chứng mô hình của phƣơng pháp này phụ thuộc chính vào thông số này.
Đây chính là mục tiêu nghiên cứu của luận văn này. Với mục tiêu này, chúng tôi đề xuất một phƣơng pháp tạo giả định tối thiểu (có kích thƣớc nhỏ nhất) nhƣ là một cải tiến của phƣơng pháp kiểm chứng đảm bảo giả định nhƣ đã trình bày ở trên. Ý tƣởng chính của phƣơng pháp đề xuất là tìm kiếm giả định tối thiểu trên toàn bộ không gian tìm kiếm của các ứng cử viên giả định (candidate assumptions). Giả định tối thiểu sau khi tạo lập bằng phƣơng pháp đề xuất sẽ đƣợc sử dụng để kiểm chứng lại hệ thống với chi phí thấp hơn.
Một số ví dụ minh họa và kết quả thực nghiệm cũng đƣợc trình bày trong luận văn này. Bố cục của luận văn đƣợc trình bày nhƣ sau: Chƣơng 1: Giới thiệu tổng quan phần mềm hƣớng thành phần, các khái niệm cơ bản, cách tiếp cận để kiểm chứng phần mềm hƣớng thành phần. Chƣơng 2: Trình bày chi tiết thuật toán học L*, giải thuật tạo giả định sử dụng thuật toán học L*. Chƣơng 3: Chƣơng này trình bày giải thuật tạo giả định tối thiểu.
Trong chƣơng này chúng tôi sẽ đƣa ra một phản ví dụ để minh hoạ rằng: giả định đƣợc tạo ra bởi giải thuật sử dụng thuật toán học L* chƣa phải là giả định tối thiểu. Chúng tôi cũng sẽ trình bày một ví dụ cụ thể để minh hoạ cho thuật toán tạo giả định tối thiểu. Chƣơng 4: Thực nghiệm. Chúng tôi sử dụng bộ công cụ LTSA để xác minh một số hệ thống đơn giản nhằm so sánh về thời gian cũng nhƣ bộ nhớ sử dụng của giải pháp cũ và giải pháp đƣợc đƣa ra trong luận văn.
Phần kết luận của luận văn tổng kết các kết quả đã đạt đƣợc, kết luận và đƣa ra một số hƣớng nghiên cứu tiếp theo. LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 6 CHƢƠNG 1: TỔNG QUAN VỀ KIỂM CHỨNG PHẦN MỀM HƢỚNG THÀNH PHẦN 1.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) [10, 11]. 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ả định (Assume- LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 7 Guarantee Verification - AGV) [2, 4, 7, 8]. 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. AVG đƣợ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. AVG 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ả định (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ả định 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 (modular verification of component based software) [2, 4, 7, 8, 10, 11, 22].
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, 7, 8] đề xuất phƣơng pháp kiểm chứng đảm bảo giả định nhƣ đã trình bày ở trên. Xét một hệ thống đơn giản gồm hai 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ả định 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ả định 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. Tuy nhiên, cách tiếp cận này không đề cập đến việc kiếm chứng hệ thống trong ngữ cảnh của tiến hóa thành phần phền mềm.
Nếu một thành phần bị tiến hóa sau khi thực hiện một vài thay đổi, khi đó giải pháp này sẽ phải thực hiện kiểm chứng hệ thống nhƣ một hệ thống mới. Trong khi đó việc thay đổi chỉ xảy ra ở một vài thành phần nên việc chạy lại trên toàn bộ hệ thống là không cần thiết. Để giải quyết hạn chế này, giải pháp trong [25] đã đề xuất một cách tiếp nhằm tạo lại giả định nhanh hơn trong ngữ cảnh các thành phần bị tiến hóa (thay đổi). Giả sử tồn tại một thành phần M1 có trƣớc (thành phần này không đƣợc phép thay đổi) và một phần mở rộng M2 (thành phần này đƣợc phép thay đổi).
Phần mở rộng M2 đƣợc ghép nối với LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 8 thành phần M1 bởi một vài cơ chế nào đó.