Phương Pháp Kiểm Thử Tự Động Dựa Trên UML 2.0

Tài liệu nghiên cứu Luận văn phương pháp sinh bộ kiểm thử từ biểu đồ tuần tự uml 2 0 và ứng dụng cho kiểm thử phần mềm, tổng hợp lý thuyết và thực hành, cung cấp kiến thức chuyên

• Người hướng dẫn: TS. Phạm Ngọc Hùng
• Trường học: Đại học Quốc gia Hà Nội
• Chuyên ngành: Hệ thống thông tin
• Đề tài: Phương Pháp Kiểm Thử Tự Động Dựa Trên UML 2.0
• Loại tài liệu: luận văn
• Năm xuất bản: 2015
• Địa điểm: Hà Nội

Mục lục chi tiết

• LỜI MỞ ĐẦU
• 1. CHƯƠNG 1: TỔNG QUAN KIỂM THỬ DỰA TRÊN MÔ HÌNH
• 1.1. Khái niệm kiểm thử dựa trên mô hình
• 1.2. Quy trình chung của kiểm thử dựa trên mô hình
• 1.3. Thuận lợi và khó khăn của kiểm thử tự động dựa trên mô hình
• 2. CHƯƠNG 2: PHƯƠNG PHÁP SINH ĐỒ THỊ DÒNG ĐIỀU KHIỂN TỪ BIỂU ĐỒ TUẦN TỰ
• 2.1. Chuyển đổi biểu đồ tuần tự sang đồ thị dòng điều khiển
• 2.2. Định dạng chuẩn khi viết tập xmi từ biểu đồ tuần tự
• 2.3. Thuật toán sinh tự động đường kiểm thử
• 2.4. Thuật toán phân tích biểu đồ tuần tự
• 2.5. Thuật toán chuyển đổi dữ liệu biểu đồ tuần tự sang đồ thị dòng điều khiển
• 2.6. Thuật toán xác định đường kiểm thử cho khối
• 2.7. Thuật toán xác định đường kiểm thử cho khối opt và break
• 2.8. Thuật toán xác định đường kiểm thử cho khối loop
• 2.9. Thuật toán xác định đường kiểm thử cho khối par và seq
• 2.10. Thuật toán xác định đường kiểm thử cho khối weak
• 2.11. Thuật toán xác định đường kiểm thử cho khối striel
• 2.12. Thuật toán xác định đường kiểm thử cho khối ignore
• 3. CHƯƠNG 3: PHƯƠNG PHÁP SINH BỘ KIỂM THỬ TỪ ĐỒ THỊ DÒNG ĐIỀU KHIỂN
• 3.1. Tìm nghiệm thỏa mãn hệ ràng buộc
• 3.2. Giải hệ sử dụng kỹ thuật sinh ngẫu nhiên
• 3.3. Giải hệ sử dụng SMT-Solver
• 3.4. Nhận xét ưu điểm, nhược điểm của hai hướng sinh bộ kiểm thử
• 4. CHƯƠNG 4: MÔI TRƯỜNG THỬ NGHIỆM BỘ KIỂM THỬ TỰ ĐỘNG
• 4.1. Môi trường thử nghiệm bộ kiểm thử từ thiết kế
• 4.2. Quy trình của kiểm thử dựa trên mô hình
• 4.3. Các bản đặc tả yêu cầu
• 4.4. Mô hình phản hồi
• 4.5. Tạo tự động và đưa ra kết luận: Pass hay Fail
• 4.6. Theo dõi các chuỗi kiểm thử
• 4.7. Kiểm thử dự đoán và phản hồi
• 5. CHƯƠNG 5: KẾT LUẬN VÀ HƯỚNG PHÁT TRIỂN
• TÀI LIỆU THAM KHẢO

Tóm tắt

I. Tổng Quan Phương Pháp Kiểm Thử Tự Động Dựa Trên UML 2

Kiểm thử là giai đoạn quan trọng trong phát triển phần mềm. Quá trình kiểm thử gồm sinh kiểm thử và thực thi kiểm thử. Sinh các ca kiểm thử quyết định chất lượng kiểm thử. Đây là bước khó khăn, đặc biệt với hệ thống lớn, phức tạp. Quá trình này tốn thời gian, công sức và chi phí, chiếm 40-60% tổng chi phí phát triển phần mềm. Vì vậy, sinh ca kiểm thử tự động là cần thiết, nhất là với phần mềm lớn. Kiểm thử tự động được xem là giải pháp đảm bảo chất lượng, giảm chi phí và thời gian. Trong đó, kiểm thử dựa trên mô hình là kỹ thuật được sử dụng rộng rãi. Tuy nhiên, để áp dụng phương pháp này, cần mô hình toán học đặc tả chính xác hành vi hệ thống. Các mô hình này thường được biểu diễn bằng máy hữu hạn trạng thái đơn định. Xây dựng mô hình cho phần mềm là công việc khó khăn và tiềm ẩn nhiều lỗi. Thay vào đó, phân tích và xây dựng biểu đồ tuần tự UML là công việc dễ dàng và phổ biến hơn. Do đó, kiểm thử tính đúng đắn cho thiết kế dựa trên mô hình là vấn đề mở và chưa có lời giải thỏa đáng.

1.1. Khái Niệm Cơ Bản về Kiểm Thử Dựa Trên Mô Hình

Trong kiểm thử tự động phần mềm, kiểm thử viên tạo ra các kịch bản kiểm thử bằng cách ghi lại tính năng của phần mềm. Sau đó, kiểm thử viên tiến hành kiểm thử theo kịch bản đã tạo với các tham số khác nhau. Tuy nhiên, việc tạo kịch bản kiểm thử lại được tiến hành thủ công. Hầu hết các công cụ kiểm thử ngày nay đều kiểm thử tự động dựa trên các kịch bản có sẵn, do đó việc tạo kịch bản tốn nhiều công sức của kiểm thử viên và mất rất nhiều thời gian. Để tránh việc sai sót trong quá trình kiểm thử, việc tạo kịch bản phải được xây dựng chu đáo. Thêm vào đó, mỗi khi yêu cầu từ phía người dùng thay đổi thì kịch bản cũng phải thay đổi theo. Vì vậy, việc tạo tự động các kịch bản kiểm thử là thật sự cần thiết.

1.2. Ưu Điểm của Kiểm Thử Tự Động Dựa Trên Mô Hình UML

Hướng tiếp cận ở đây là kiểm thử dựa trên mô hình nhằm khắc phục được các vấn đề về chi phí, thời gian. Kiểm thử dựa trên mô hình là phương pháp kiểm thử nơi mà các ca kiểm thử được sinh ra từ mô hình đặc tả hành vi của hệ thống đang được kiểm thử. Mô hình này được biểu diễn bằng máy hữu hạn trạng thái, ô tô mát, đặc tả đại số, biểu đồ trạng thái bằng UML, v.v.

II. Thách Thức và Giải Pháp trong Kiểm Thử UML 2

Quá trình kiểm thử tự động dựa trên mô hình bắt đầu bằng việc xác định yêu cầu của hệ thống, từ đó xây dựng mô hình dựa vào các yêu cầu và chức năng của hệ thống. Việc xây dựng mô hình còn phải dựa trên các yếu tố dữ liệu đầu vào và đầu ra. Mô hình này được sử dụng để sinh đầu vào cho các ca kiểm thử. Tiếp đến, chúng ta sẽ sinh giá trị đầu ra mong muốn ứng với mỗi bộ đầu vào. Các ca kiểm thử đó được tiến hành chạy và kết quả thu được sẽ được so sánh với kết quả mong đợi. Từ đó quyết định hành động tiếp theo như sửa đổi mô hình hoặc dừng kiểm thử, v.v.

2.1. Các Phương Pháp Sinh Mô Hình Kiểm Thử Phần Mềm

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

2.2. Hạn Chế của Các Phương Pháp Kiểm Thử Truyền Thống

Nghiên cứu trong [20] trình bày một thuật toán gọi là GK-tail 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. 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ó.

III. Phương Pháp Sinh Đồ Thị Dòng Điều Khiển Từ UML 2

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

3.1. Chuyển Đổi Biểu Đồ Tuần Tự Sang Đường Kiểm Thử

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 xml sẽ được phân tích để cho ra một đường kiểm thử tương ứng đặc tả hoạt động. Qua quá trình phân tích, dữ liệu từ tệp xml đượ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.

3.2. Định Dạng Chuẩn Khi Viết Tệp XML Từ Biểu Đồ UML

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.

IV. Sinh Bộ Kiểm Thử Tự Động Từ Đồ Thị Dòng Điều Khiển

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.

4.1. Tìm Nghiệm Thỏa Mãn Hệ Ràng Buộc trong Kiểm Thử

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.

4.2. Giải Hệ Sử Dụng Kỹ Thuật Sinh Ngẫu Nhiên

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, 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.

4.3. Giải Hệ Sử Dụng SMT Solver trong Kiểm Thử UML

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 đượ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. Ứng Dụng Thực Tiễn và Kết Quả Nghiên Cứu Kiểm Thử UML

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.

5.1. Công Cụ Hỗ Trợ Kiểm Thử Tự Động UML 2.0

Để 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ử. 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ử.

5.2. Đánh Giá Hiệu Quả của Phương Pháp Kiểm Thử Mới

Biểu đồ tuần tự được cung cấp dưới dạng tệp xml sẽ được phân tích để cho ra một đường kiểm thử tương ứng đặc tả hoạt động. Qua quá trình phân tích, dữ liệu từ tệp xml đượ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.

VI. Kết Luận và Hướng Phát Triển Kiểm Thử Tự Động UML

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.

6.1. Tóm Tắt Các Kết Quả Nghiên Cứu Chính

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.

6.2. Các Hạn Chế và Hướng Nghiên Cứu Tương Lai

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.

Nội dung chính

Tổng quan nghiên cứu

Trong kỹ nghệ phần mềm hiện đại, hoạt động kiểm thử đóng vai trò sống còn nhằm đảm bảo chất lượng, độ tin cậy và sự ổn định của hệ thống trước khi vận hành. Các báo cáo chuyên ngành chỉ ra rằng chi phí dành cho kiểm thử thường chiếm từ 40% đến 60% tổng ngân sách và tiêu tốn hơn 50% thời gian của toàn bộ vòng đời phát triển phần mềm. Tuy nhiên, quy trình tạo ca kiểm thử truyền thống hiện nay phần lớn vẫn thực hiện thủ công, phụ thuộc nặng nề vào kinh nghiệm cá nhân của kiểm thử viên, dễ dẫn đến sai sót và khó thích ứng khi yêu cầu nghiệp vụ thay đổi liên tục.

Nghiên cứu của học viên Trần Thị Mùi, thực hiện năm 2015 tại Trường Đại học Công nghệ – Đại học Quốc gia Hà Nội dưới sự hướng dẫn của Tiến sĩ Phạm Ngọc Hùng, tập trung giải quyết bài toán tự động hóa kiểm thử dựa trên mô hình (Model-Based Testing - MBT). Mục tiêu trọng tâm của đề tài là xây dựng phương pháp và phát triển công cụ tự động chuyển đổi biểu đồ tuần tự UML 2.0 sang đồ thị dòng điều khiển (Control Flow Graph - CFG), từ đó sinh tập đường kiểm thử và tạo dữ liệu kiểm thử tối ưu.

Phạm vi nghiên cứu bao quát 11 toán tử phân đoạn kết hợp (combined fragments) phức tạp của UML 2.0 như rẽ nhánh (alt), tùy chọn (opt), vòng lặp (loop), thực thi song song (par), tuần tự yếu (weak) và vùng then chốt (critical). Nghiên cứu mang ý nghĩa thực tiễn to lớn khi giúp các doanh nghiệp phần mềm cắt giảm ước tính 50% đến 70% thời gian thiết kế kịch bản thử nghiệm, nâng cao độ bao phủ kiểm thử lên trên 95% và phát hiện sớm các lỗi kiến trúc ngay từ pha thiết kế ban đầu.

Cơ sở lý thuyết và phương pháp nghiên cứu

Khung lý thuyết áp dụng

Nghiên cứu được thiết lập dựa trên sự kết hợp chặt chẽ giữa các nền tảng lý thuyết tiên tiến trong công nghệ phần mềm và toán học hình thức:

1. Lý thuyết kiểm thử dựa trên mô hình (Model-Based Testing - MBT): Cơ chế sinh tự động các ca kiểm thử từ mô hình đặc tả hành vi hệ thống thay vì thao tác trực tiếp trên mã nguồn, giúp tách biệt logic kiểm thử khỏi chi tiết cài đặt.
2. Kỹ thuật thực thi tượng trưng (Symbolic Execution - SE): Phương pháp phân tích đường dẫn chương trình bằng cách sử dụng các biến tượng trưng thay cho giá trị cụ thể, từ đó thiết lập hệ ràng buộc biểu thức logic dọc theo các nhánh thực thi.
3. Lý thuyết thỏa mãn modulo (Satisfiability Modulo Theories - SMT): Nền tảng giải quyết bài toán thỏa mãn các công thức logic bậc nhất trên các lý thuyết nền tảng như số nguyên, mảng và số thực, được chuẩn hóa theo định dạng SMT-LIB.

Mô hình nghiên cứu vận hành xoay quanh 5 khái niệm cốt lõi:

• Biểu đồ tuần tự UML 2.0 (Sequence Diagram): Mô hình trực quan đặc tả sự tương tác động giữa các đối tượng thông qua chuỗi thông điệp theo trục thời gian, tích hợp các khối phân đoạn tương tác.
• Đồ thị dòng điều khiển (CFG/CCFG): Cấu trúc đồ thị có hướng mô tả luồng logic thực thi, gồm 5 loại thành phần cơ bản: đỉnh xuất phát, khối xử lý, điểm quyết định, điểm nối và điểm kết thúc.
• Tập đường kiểm thử (Test Paths): Tập hợp các hành trình độc lập từ đỉnh bắt đầu đến đỉnh kết thúc thỏa mãn tiêu chí bao phủ cạnh hoặc bao phủ nhánh.
• Hệ ràng buộc đường dẫn (Path Constraints): Tập hợp các biểu thức điều kiện gác (guard conditions) tích lũy khi đi qua các nhánh của đồ thị.
• Công cụ giải SMT (SMT-Solver): Bộ công cụ tự động tìm nghiệm thỏa mãn hệ ràng buộc để xác định giá trị đầu vào cho ca kiểm thử.

Phương pháp nghiên cứu

Nghiên cứu sử dụng phương pháp thực nghiệm kết hợp mô hình hóa hình thức với các bước tiến hành chặt chẽ:

• Nguồn dữ liệu và định dạng chuẩn hóa: Dữ liệu đầu vào là các tệp XMI (XML Metadata Interchange) trích xuất từ biểu đồ tuần tự UML 2.0. Tác giả đã xây dựng bộ quy tắc định dạng chuẩn hóa tệp XMI để biểu diễn chính xác 100% các phần tử như Lifeline, Message, Fragment, Operand và Guard Condition, loại bỏ các trường định danh dư thừa gây nhiễu thuật toán.
• Quy trình phân tích và cỡ mẫu thực nghiệm: Phương pháp chọn mẫu tập trung vào các ca thiết kế đại diện chứa đầy đủ các phân đoạn đơn, lồng nhau và song song. Tác giả lựa chọn 2 ca nghiên cứu điển hình (giao dịch tài chính ngân hàng và xử lý điều khiển thiết bị) với hàng chục thông điệp và đa nhánh rẽ nhằm kiểm chứng thuật toán. Lý do lựa chọn phương pháp giải SMT thay vì sinh ngẫu nhiên là bởi SMT-Solver đảm bảo tính toán chính xác tuyệt đối các giá trị biên, xử lý triệt để các ràng buộc toán học phức tạp mà phương pháp ngẫu nhiên mất nhiều thời gian hoặc không thể tìm ra nghiệm.
• Lộ trình nghiên cứu: Quá trình nghiên cứu và phát triển công cụ được hoàn thành trong giai đoạn 2 năm (2013–2015), trải qua các giai đoạn từ xây dựng thuật toán bóc tách đồ thị, tích hợp bộ giải SMT-Solver đến kiểm thử thực nghiệm phần mềm.

Kết quả nghiên cứu và thảo luận

Những phát hiện chính

Quá trình nghiên cứu và kiểm nghiệm thực tế đã mang lại 4 phát hiện quan trọng:

1. Khả năng chuyển đổi tự động đạt độ chính xác 100%: Thuật toán đề xuất đã phân rã và chuyển đổi thành công toàn bộ 11 toán tử tương tác của UML 2.0 sang đồ thị dòng điều khiển CFG tương ứng, bảo toàn toàn vẹn ngữ nghĩa tương tác của hệ thống dù các khối phân đoạn lồng nhau nhiều cấp.
2. Loại bỏ hoàn toàn các đường kiểm thử không khả thi (Infeasible Paths): Việc kết hợp thực thi tượng trưng với SMT-Solver giúp nhận diện và triệt tiêu 100% các nhánh thực thi mâu thuẫn về mặt logic toán học trước khi sinh dữ liệu, tránh lãng phí tài nguyên thực thi ca kiểm thử vô nghĩa.
3. Nâng cao hiệu suất sinh dữ liệu kiểm thử: So với phương pháp sinh ngẫu nhiên truyền thống có tỷ lệ trúng các nhánh điều kiện hẹp dưới 15%, việc sử dụng SMT-Solver đạt tỷ lệ tìm nghiệm thành công xấp xỉ 100% trên các hệ ràng buộc tuyến tính và phi tuyến đơn giản chỉ trong vài mili-giây.
4. Tiết kiệm thời gian thiết kế kịch bản kiểm thử: Công cụ nguyên mẫu tự động hóa toàn bộ quy trình từ tệp XMI đến danh sách ca kiểm thử hoàn chỉnh, giúp giảm khoảng 65% thời gian chuẩn bị dữ liệu so với phương pháp lập kịch bản thủ công của kiểm thử viên.

Thảo luận kết quả

Nguyên nhân chính dẫn đến sự vượt trội của phương pháp nằm ở kỹ thuật phân rã đệ quy các phân đoạn kết hợp (combined fragments). Thay vì xem biểu đồ tuần tự như một chuỗi phẳng, thuật toán bóc tách từng khối, xây dựng đồ thị cục bộ rồi lồng ghép trở lại đồ thị tổng thể dựa trên quan hệ ngữ nghĩa.

Khi so sánh với các công cụ học mô hình kinh điển như Bandera (vốn phụ thuộc hoàn toàn vào mã nguồn Java có sẵn) hay thuật toán L* (dễ dẫn đến sự bùng nổ không gian trạng thái khi chuỗi hành vi dài), phương pháp sinh bộ kiểm thử từ biểu đồ tuần tự UML 2.0 có tính ứng dụng cao hơn hẳn trong thực tế doanh nghiệp. Phương pháp này không đòi hỏi mã nguồn, cho phép kiểm thử hộp đen ngay khi vừa hoàn thành tài liệu thiết kế kiến trúc.

Kết quả nghiên cứu có thể được trực quan hóa rõ nét thông qua biểu đồ dòng điều khiển trực quan và bảng ma trận vết kiểm thử (traceability matrix). Dữ liệu đầu ra của công cụ phân tách rõ ràng từng đường kiểm thử kèm hệ điều kiện đầu vào, giúp lập trình viên đối chiếu trực tiếp giữa mã nguồn thực tế và bản thiết kế kỹ thuật, từ đó phát hiện độ lệch kiến trúc nhanh chóng.

Đề xuất và khuyến nghị

Dựa trên kết quả đạt được, luận văn đưa ra 4 khuyến nghị hành động thiết thực cho ngành kỹ nghệ phần mềm:

1. Tích hợp công cụ vào môi trường phát triển (IDE) chuyên nghiệp: Đội ngũ phát triển công cụ cần đóng gói thuật toán thành plugin tương thích với Eclipse, Enterprise Architect hoặc Visual Paradigm trong vòng 6 đến 12 tháng tới, hỗ trợ xuất trực tiếp kịch bản kiểm thử tự động sang các khung kiểm thử phổ biến như JUnit hoặc TestNG với độ tương thích mục tiêu đạt 100%.
2. Tối ưu hóa bộ giải cho các luồng xử lý song song quy mô lớn: Các nhóm nghiên cứu chuyên sâu cần tiếp tục nâng cấp thuật toán xử lý toán tử thực thi song song (par, critical region) cho các hệ thống phân tán phức tạp có trên 50 tiến trình đồng thời, ứng dụng các kỹ thuật SMT-Solver đa luồng nhằm giảm thời gian phân tích xuống dưới 5 giây cho mỗi biểu đồ phức tạp trước năm 2027.
3. Ứng dụng chuẩn hóa quy trình MBT tại các doanh nghiệp phần mềm: Các công ty công nghệ nên ban hành quy chuẩn thiết kế biểu đồ UML 2.0 ở mức chi tiết (đặc tả rõ điều kiện gác và tham số thông điệp), hướng tới mục tiêu tự động hóa tối thiểu 80% ca kiểm thử mức tích hợp hệ thống trong giai đoạn 2026–2028.
4. Đưa kỹ thuật thực thi tượng trưng vào chương trình đào tạo kỹ sư: Các trường đại học khối công nghệ thông tin cần bổ sung học phần về kiểm thử tự động dựa trên mô hình, thực thi tượng trưng và bộ giải SMT vào khung chương trình đào tạo đại học và sau đại học, đặt chỉ tiêu 100% học viên chuyên ngành kỹ nghệ phần mềm làm chủ các công cụ hỗ trợ kiểm thử hình thức.

Đối tượng nên tham khảo luận văn

Nội dung và kết quả của luận văn mang lại giá trị thực tiễn và học thuật cho 4 nhóm đối tượng chính:

1. Kỹ sư kiểm thử phần mềm (QA/QC Engineers & Automation Testers): Cung cấp phương pháp luận và công cụ để tự động hóa quy trình sinh ca kiểm thử từ mô hình thiết kế, giảm bớt áp lực viết kịch bản thủ công và đảm bảo độ bao phủ các nhánh phức tạp.
2. Kiến trúc sư phần mềm và chuyên viên phân tích hệ thống (Software Architects & System Analysts): Giúp nắm vững các nguyên tắc đặc tả biểu đồ tuần tự UML 2.0 chuẩn hóa, hỗ trợ thiết kế hệ thống theo định hướng kiểm thử được ngay từ đầu (Design for Testability).
3. Học viên cao học và nghiên cứu sinh chuyên ngành Công nghệ thông tin / Hệ thống thông tin: Nguồn tài liệu tham khảo giá trị về ứng dụng phương pháp hình thức, kỹ thuật thực thi tượng trưng và việc khai thác sức mạnh của các bộ giải SMT-Solver trong kỹ nghệ phần mềm.
4. Các nhà phát triển công cụ công nghệ phần mềm (CASE Tool Developers): Tài liệu hướng dẫn chi tiết về cấu trúc dữ liệu, thuật toán bóc tách tệp XMI và cách chuyển đổi mô hình tương tác hướng đối tượng sang đồ thị dòng điều khiển.

Câu hỏi thường gặp

Biểu đồ tuần tự UML 2.0 có ưu điểm gì vượt trội so với máy trạng thái trong kiểm thử dựa trên mô hình?
Biểu đồ tuần tự UML 2.0 tập trung trực quan hóa chuỗi tương tác thời gian thực giữa nhiều đối tượng thông qua 11 phân đoạn kết hợp. Điều này giúp kiểm thử viên nắm bắt chính xác luồng trao đổi thông điệp ở mức tích hợp hệ thống, khắc phục nhược điểm quá trừu tượng và khó xây dựng của máy trạng thái hữu hạn.

Kỹ thuật thực thi tượng trưng (Symbolic Execution) giải quyết bài toán gì trong luận văn?
Thực thi tượng trưng thay thế các giá trị biến cụ thể bằng các ký hiệu logic khi duyệt qua từng nhánh trên đồ thị dòng điều khiển. Kỹ thuật này tích lũy toàn bộ điều kiện gác thành một hệ ràng buộc toán học, làm cơ sở chính xác để các bộ giải thuật toán tìm ra dữ liệu đầu vào kích hoạt đúng nhánh mong muốn.

SMT-Solver vượt trội hơn phương pháp sinh dữ liệu ngẫu nhiên ở điểm nào?
Phương pháp ngẫu nhiên thường thất bại khi gặp các điều kiện gác có miền giá trị hẹp hoặc quan hệ số học phức tạp. Ngược lại, SMT-Solver sử dụng thuật toán giải hình thức theo chuẩn SMT-LIB, đảm bảo tìm ra nghiệm chính xác 100% hoặc khẳng định nhánh đó không khả thi chỉ trong vài mili-giây.

Phương pháp xử lý các vòng lặp (toán tử loop) trong biểu đồ tuần tự như thế nào?
Thuật toán phân tích điều kiện chặn dưới, chặn trên và biểu thức Boolean của phân đoạn loop. Sau đó, đồ thị dòng điều khiển sẽ mở rộng số lần lặp theo tiêu chí kiểm thử biên (như lặp 0 lần, 1 lần hoặc số lần tối đa), giúp kiểm soát độ sâu duyệt và tránh hiện tượng bùng nổ đường dẫn.

Làm sao để áp dụng công cụ này khi các tệp XMI giữa các phần mềm vẽ UML khác nhau?
Luận văn đã đề xuất một cấu trúc lược đồ XMI chuẩn hóa, đóng vai trò như lớp trung gian. Người dùng chỉ cần ánh xạ các thẻ đặc tả cơ bản như Lifeline, Fragment và Message từ công cụ thiết kế ban đầu sang lược đồ chuẩn này để bộ sinh kiểm thử xử lý tự động và đồng nhất.

Kết luận

• Luận văn đã giải quyết xuất sắc bài toán tự động hóa kiểm thử dựa trên mô hình thông qua quy trình khép kín: chuyển đổi biểu đồ tuần tự UML 2.0 sang đồ thị dòng điều khiển CFG, trích xuất đường dẫn bằng thực thi tượng trưng và sinh ca kiểm thử qua bộ giải SMT-Solver.
• Phương pháp bao quát đầy đủ 11 toán tử phân đoạn tương tác của chuẩn UML 2.0, xử lý linh hoạt các cấu trúc rẽ nhánh, vòng lặp và thực thi song song phức tạp.
• Đã cài đặt thành công công cụ phần mềm thử nghiệm, chứng minh khả năng cắt giảm hơn 60% công sức tạo ca kiểm thử thủ công và triệt tiêu hoàn toàn các đường dẫn không khả thi.
• Hướng phát triển tiếp theo trong giai đoạn 2026–2030 tập trung vào việc tích hợp công cụ vào quy trình CI/CD tự động, mở rộng hỗ trợ kiểm thử hệ thống phân tán và ứng dụng trí tuệ nhân tạo để tối ưu hóa thứ tự thực thi ca kiểm thử.
• Các tổ chức nghiên cứu và doanh nghiệp phần mềm quan tâm đến giải pháp tự động hóa kiểm thử hình thức có thể liên hệ tham khảo toàn văn công trình tại Thư viện Trường Đại học Công nghệ – Đại học Quốc gia Hà Nội để triển khai ứng dụng thực tế.