Hệ Thống Kiểm Thử Phần Mềm Tối Ưu Tại Đại Học Giao Thông Vận Tải Hà Nội

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 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ầm 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 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 thử mô hình (model checking - MC) [5]. Kiểm thử 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 thử đồ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 thử mô hình là “vấn đề bùng nổ không gian trạng thái” khi kiểm thử 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 thử từng phần (modular model checking - MMC) [10, 11]. Thay vì tiến hành kiểm thử 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 thử 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 thử hỗ trợ ý tưởng này là phương pháp kiểm thử đảm bảo giả định (Assume-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 thử 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 thử 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 thử phần mềm hướng thành phần thông qua phương pháp kiểm thử 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 thử 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 thử mô hình và phát triển hướng thành phần.

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 thử 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.

Hiện nay, đã có nhiều nghiên cứu về kiểm thử 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 thử 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.

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 thử đả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 thử 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.

Luận văn trình bày các chương 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 thử 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 họa 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 họa cho thuật toán tạo giả định tối thiểu.

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.