Ứng dụng công cụ SOAP UI cho kiểm thử tự động các ứng dụng Web.

Luận văn này tập trung nghiên cứu phương pháp sinh bộ kiểm thử từ biểu đồ tuần tự UML 2.0 dựa trên lý thuyết kiểm thử mô hình nhằm tự động hóa quá trình kiểm thử, nâng cao hiệu quả, tiết kiệm chi phí và thời gian. Phương pháp này được thực hiện thông qua các bước chính sau. Đầu tiên, để có được mô hình làm đầu vào cho kiểm thử, phương pháp thực hiện chuyển đổi biểu đồ tuần tự về đồ thị dòng điều khiển bằng cách tiến hành bóc, tách từng khối (fragment) trong biểu đồ tuần tự. Các khối này có thể tuần tự hoặc lồng nhau, dựa vào quan hệ của chúng, tiến hành xây dựng đồ thị cho mỗi khối, sau đó lồng chúng lại nhằm sinh ra đồ thị dòng điều khiển tương ứng với biểu đồ tuần tự. Kế tiếp, đồ thị dòng điều khiển được phân tích để xây dựng tập đường kiểm thử. Vận dụng kỹ thuật SE (Symbolic Execution) nhằm xây dựng hệ ràng buộc tương ứng cho tập đường kiểm thử. Cuối cùng, sử dụng công cụ SMT solver để giải hệ các ràng buộc nhằm tìm kiếm nghiệm và từ đó sinh ca kiểm thử.
Kiểm thử là giai đoạn quan trọng và không thể thiếu trong quá trình phát triển phần mềm. Quá trình kiểm thử trải qua hai giai đoạn: sinh ca kiểm thử và thực thi ca kiểm thử. Trong quá trình kiểm thử, việc sinh các ca kiểm thử đóng vai trò quyết định đến chất lượng kiểm thử. Tuy nhiên, đây là bước khó khăn và thách thức nhất, đặc biệt đối với các hệ thống lớn không những phức tạp để kiểm thử mà còn đòi hỏi một số lượng lớn các ca kiểm thử được tạo ra. Quá trình này tốn thời gian, công sức và chi phí có thể chiếm 40% – 60% tổng chi phí trong toàn bộ quá trình phát triển phần mềm [9]. Vì vậy, quá trình sinh các ca kiểm thử tự động trở nên thực sự cần thiết, nhất là đối với những phần mềm lớn và phức tạp. Kiểm thử tự động đang được xem là giải pháp chính nhằm đảm bảo chất lượng mà vẫn giảm chi phí và thời gian trong quá trình phát triển các sản phẩm phần mềm.
Trong đó, kiểm thử dựa trên mô hình là một trong những kỹ thuật kiểm thử đang được sử dụng ngày càng rộng rãi trong việc kiểm thử các sản phẩm phần mềm. Tuy nhiên, để áp dụng phương pháp này, ta cần phải có các mô hình toán học đặc tả chính xác hành vi của hệ thống và có sẵn trong thực tế. Các mô hình này thường được biểu diễn bằng các máy hữu hạn trạng thái đơn định. Xây dựng mô hình cho các phần mềm là một công việc khó khăn và tiềm ẩn nhiều lỗi đối với các công ty. Thay vào đó, việc phân tích và xây dựng nên các biểu đồ tuần tự UML là một công việc dễ dàng và phổ biến. Do đó, việc kiểm thử tính đúng đắn cho thiết kế dựa trên mô hình là một vấn đề mở và chưa có lời giải thỏa đáng.
Hiện nay, có nhiều hướng nghiên cứu liên quan đến việc sinh mô hình cho phần mềm đã được đề xuất bởi nhiều tác giả. Một hướng là tập trung vào nghiên cứu các phương pháp sinh mô hình cho phần mềm. Với cách tiếp cận này, ta có thể kể đến các phương pháp sinh mô hình được đề cập trong [19], [20], [21], và [22]. Trong [19], các tác giả đã đặt ngữ cảnh là xây dựng mô hình cho phần mềm được cho dưới dạng một hộp đen và ta có thể thử nghiệm thực thi các hành động trên nó để có thể xây dựng được một tập các chuỗi hành động của phần mềm. Sau đó, tập 2 các chuỗi hành động của phần mềm thu được có thể được coi là một biểu thức chính quy đặc tả hành vi của phần mềm, các tác giả sau đó đã sử dụng thuật toán Thompson để sinh mô hình cho phần mềm được cho bởi biểu thức chính quy đó. Phương pháp này bị giới hạn bởi độ dài tối đa của chuỗi các hành động có thể thử nghiệm trên phần mềm. Nghiên cứu trong [20] trình bày một thuật toán gọi là GKtail mà tự động sinh mô hình cho phần mềm dưới dạng các EFSM (Extended Finite State Machine) từ các chuỗi tương tác của nó. EFSM mô hình hóa sự tương tác giữa các giá trị dữ liệu và phần mềm bằng cách ghi chú lên các cạnh của ôtômát hữu hạn đó với các điều kiện trên các giá trị dữ liệu. Trong nghiên cứu này, các tác giả đã đề cập một khía cạnh rất quan trọng của phần mềm. Đó là mô hình hóa các lời gọi hàm trong quan hệ với các tham số của nó. Phương pháp này dựa vào một phần mềm gọi là phần mềm giám sát để có thể sinh ra được các chuỗi tương tác mà được dùng như là đầu vào của nó. Nghiên cứu [21] giới thiệu một tập tích hợp các chương trình phân tích, chuyển đổi thành phần gọi là Bandera mà tự động trích xuất mô hình cho chương trình phần mềm dựa trên mã nguồn. Trong nghiên cứu này, Bandera lấy mã nguồn Java như là đầu vào để sinh mô hình dưới dạng đầu vào cho một số công cụ khác. Ngoài ra, Bandera cũng tham chiếu trở lại mã nguồn ban đầu với mô hình đã được sinh ra. Phương pháp này rõ ràng là phụ thuộc vào mã nguồn của phần mềm cần phân tích. Do đó, đối với các phần mềm hướng thành phần không có mã nguồn của một số thành phần mua từ bên phát triển thứ ba thì phương pháp này rất khó khả thi. Nghiên cứu [22] giới thiệu một công cụ gọi là Bandera Environment Generator (BEG). Công cụ này tự động hóa việc sinh mô hình môi trường để cung cấp một dạng hạn chế của việc kiểm chứng mô hình các mô đun của chương trình Java. Công cụ này sinh mô hình cho đơn vị chương trình Java dựa trên một số giả định về môi trường được cung cấp bởi người dùng. Mô hình đã được sinh ra có thể được dùng trong việc phân tích ảnh hưởng của môi trường lên đơn vị trong phương pháp kiểm chứng mô hình. Đây là một vấn đề rất thách thức trong thực tế phát triển phần mềm vì hệ thống phần mềm luôn phải chạy trên một sự kết hợp của rất nhiều hệ thống khác như hệ điều hành, các hệ thống khác,v.v. Người dùng, thậm chí cả 3 người thiết kế phần mềm cũng khó có thể nhận biết được những thông tin đầy đủ về môi trường trong thời gian làm thiết kế hệ thống
Một hướng tiếp cận khác là sinh mô hình trong khi thực hiện kiểm chứng mô hình hay trong khi thực hiện kiểm thử dựa trên mô hình [23], [24], và [25]. Trong [23], các tác giả đã sử dụng thuật toán học L* để học đặc tả của một thành phần phần mềm thông qua một biểu thức chính quy để sinh ra mô hình cho thành phần đó. Biểu thức chính quy đó là kết quả của khâu thiết kế, có thể được sinh ra từ từ biểu đồ tuần tự theo phương pháp được đề cập trong [23]. Tuy phương pháp này sinh được mô hình cho phần mềm, nhưng sử dụng nhiều thời gian và bộ nhớ. Đặc biệt là phương pháp này bị giới hạn bởi độ dài tối đa của một chuỗi hành vi của phần mềm. Do đó, phương pháp này rất khó áp dụng được trong thực tế. Nghiên cứu [24] đặt vấn đề cho việc kiểm thử hộp đen. Trong nghiên cứu này, nhiều chiến lược được trình bày để kiểm chứng phần mềm từ khi chúng ta chưa có mô hình. Mô hình được sinh ra trong các lần lặp kiểm chứng phần mềm. Nghiên cứu [25] trình bày một phương pháp sinh mô hình thành phần phần mềm trong quá trình thành phần đó tiến hóa. Những mô hình này được sinh ra sử dụng các mô hình chưa đúng hiện có dựa vào các kỹ thuật kiểm thử hộp đen và học máy. Tuy nhiên, phương pháp này sinh mô hình cho toàn bộ phần mềm. Với những phần mềm lớn thì phương pháp này có thể dẫn đến sự bùng nổ trạng thái của mô hình. Với cách tiếp cận này, những mô hình được sinh ra như là một phần của quá trình khác như kiểm thử hộp đen, kiểm chứng mô hình. Luận văn này tập trung vào việc chỉ sinh mô hình cho thành phần phần mềm. Bằng cách này, chúng ta tập trung vào việc có được mô hình bằng một cách thực tế hơn như từ biểu đồ tuần tự [23]. Những mô hình này sau đó có thể được dùng như là đầu vào cho các phương pháp khác như kiểm chứng mô hình, kiểm thử dựa trên mô hình.
Để giải quyết vấn đề trên, trong luận văn này, tôi nghiên cứu về phương pháp nhằm xây dựng một công cụ hỗ trợ phân tích biểu đồ dòng điểu khiển dựa trên biểu đồ tuần tự UML 2.0 và ứng dụng để sinh bộ kiểm thử. 4 Phương pháp nghiên cứu gồm hai quá trình chính là chuyển đồi biểu đồ tuần tự về đồ thị dòng điều khiển và từ đồ thị dòng điều khiển sinh bộ kiểm thử. Biểu đồ tuần tự được cung cấp dưới dạng tệp xmi sẽ được phân tích để cho ra một đường kiểm thử tương ứng đặc tả hoạt động. Đây chính là giá trị đầu vào. Qua quá trình phân tích, dữ liệu từ tệp xmi được chuyển đổi thành cấu trúc dữ liệu biểu đồ tuần tự tương ứng. Ứng với mỗi khối trong biểu đồ tuần tự, tiến hành bóc, tách từng khối và dự a vào quan hệ giữa các khối để lồng các khối nhằm sinh ra đồ thị dòng điều khiển. Kế tiếp, một đường kiểm thử tương ứng được trả về đặc tả chính xác hoạt động của đồ thị dòng điều khiển. Kỹ thuật được sử dụng để xây dựng hệ ràng buộc tương ứng cho tập đường kiểm thử ở đây là thực thi tượng trưng (symbolic execution - SE). Cuối cùng, bằng cách kết hợp kỹ thuật sinh ngẫu nhiên và tận dụng thế mạnh các công cụ giải các hệ ràng buộc (SMT-Solver), hệ ràng buộc được giải để sinh ca kiểm thử. Bộ kiểm thử này sẽ được sử dụng để kiểm tra xem việc lập trình có đúng với thiết kế hay không.
Phần còn lại của luận văn được cấu trúc như sau: Chương 2 trình bày cơ sở lý thuyết của kiểm thử mô hình, bao gồm các khái niệm cơ bản, quy trình thực hiện, phương pháp đặc tả mô hình bằng máy trạng thái UML, thuận lợi và khó khăn của kiểm thử dựa trên mô hình và áp dụng cho kiểm thử phần mềm. Phương pháp sinh đồ thị dòng điều khiển từ biểu đồ tuần tự bao gồm tổng quan về đồ thị dòng điều khiển, cách đặc tả biểu đồ tuần tự, phương pháp sinh đồ thị dòng điều khiển được trình bày trong chương 3. Chương 4 trình bày về phương pháp sinh ca kiểm thử từ đồ thị dòng điều khiển bao gồm bước xây dựng hệ ràng buộc và bước tìm nghiệm thỏa mãn hệ ràng buộc dựa trên SMT - Solver. Chương 5 trình bày kết quả đã đạt được. Cuối cùng, chương 6 tóm tắt lại nội dung nghiên cứu, đưa ra những hạn chế và hướng nghiên cứu phát triển trong tương lai.
Ứng dụng công cụ SOAP UI cho kiểm thử tự động các ứng dụng Web.: Tải về