I. Tổng Quan Hệ Thống Kiểm Thử Phần Mềm Tại UTT Hà Nội
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, 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 phần mềm 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 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.
1.1. Giới thiệu chung về kiểm thử phần mềm tại UTT
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).
1.2. Vấn đề đảm bảo chất lượng phần mềm tại Đại học GTVT
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.
II. Thách Thức Trong Kiểm Thử Phần Mềm Tại Khoa CNTT UTT
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 thử mô hình (Model Checking). 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 verification - MV). 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.
2.1. Bùng nổ không gian trạng thái trong kiểm thử mô hình
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.
2.2. Hạn chế của kiểm thử toàn bộ hệ thống tại UTT
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.
III. Phương Pháp Kiểm Thử Đảm Bảo Giả Định AGV Tối Ưu
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. 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).
3.1. Ưu điểm của phương pháp AGV trong kiểm thử phần mềm
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.
3.2. Tạo lập giả định trong phương pháp kiểm thử AGV
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.
3.3. Ứng dụng AGV trong kiểm thử phần mềm hướng thành phần
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.
IV. Giải Thuật Tạo Giả Định Tối Thiểu Cho Hệ Thống Kiểm Thử
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.
4.1. Mục tiêu của giải thuật tạo giả định tối thiểu
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).
4.2. Ưu điểm của giả định tối thiểu trong kiểm thử
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.
V. Ứng Dụng Thực Tiễn Hệ Thống Kiểm Thử Tại UTT Hà Nội
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.
5.1. Giới thiệu các chương trong luận văn nghiên cứu
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.
5.2. Phân tích 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.
VI. Kết Luận Và Hướng Phát Triển Hệ Thống Kiểm Thử Tối Ư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.
6.1. So sánh hiệu quả của giải pháp kiểm thử mới
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.
6.2. Tổng kết và hướng nghiên cứu tiếp theo tại UTT
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.
