Luận Văn Thạc Sĩ: Phương Pháp Sinh Dữ Liệu Kiểm Thử Tự Động Từ Biểu Đồ UML

Luận văn thạc sĩ VNU UET trình bày phương pháp sinh dữ liệu kiểm thử tự động từ biểu đồ tuần tự UML, biểu đồ lớp và ràng buộc OCL.

• Tác giả: Nguyễn Văn Hòa
• Người hướng dẫn: PGS. Phạm Ngọc Hùng
• Trường học: Trường Đại học Công Nghệ - Đại học Quốc Gia Hà Nội
• Chuyên ngành: Công Nghệ Thông Tin
• Đề tài: Phương Pháp Sinh Dữ Liệu Kiểm Thử Tự Động Từ Biểu Đồ Tuần Tự UML, Biểu Đồ Lớp Và Ràng Buộc OCL
• Loại tài liệu: Luận Văn Thạc Sĩ
• Năm xuất bản: 2016
• Địa điểm: Hà Nội

Mục lục chi tiết

• LỜI CẢM ƠN
• TÓM TẮT
• ABSTRACT
• LỜI CAM ĐOAN
• MỤC LỤC
• DANH SÁCH BẢNG BIỂU
• DANH SÁCH HÌNH VẼ
• BẢNG THUẬT NGỮ VIẾT TẮT
• 1. CHƯƠNG 1: GIỚI THIỆU
• 1.1. Công nghệ phần mềm đang ngày càng phát triển và chi phối cuộc sống của con ngƣời
• 1.2. Kiểm thử tự động và các nghiên cứu liên quan
• 1.3. Nội dung bài nghiên cứu và bố cục luận văn
• 2. CHƯƠNG 2: CÁC KHÁI NIỆM VÀ TỔNG QUAN KIỂM THỬ DỰA TRÊN MÔ HÌNH
• 2.1. Tổng quan kiểm thử dựa trên mô hình
• 2.2. Biểu đồ tuần tự và các khối phân đoạn trong UML
• 2.3. Đồ thị dòng điều khiển
• 3. CHƯƠNG 3: PHƢƠNG PHÁP SINH ĐỒ THỊ DÒNG ĐIỀU KHIỂN TỪ BIỂU ĐỒ TUẦN TỰ
• 3.1. Điều kiện ràng buộc trong thiết kế
• 3.2. Thuật toán biến đổi biểu đồ tuần tự sang đồ thị dòng điều khiển
• 3.3. Kỹ thuật sinh kịch bản kiểm thử
• 3.4. Xây dựng hệ ràng buộc
• 3.5. Giải hệ sử dụng SMT-Solver
• 3.6. Các nghiên cứu liên quan
• 4. CHƯƠNG 4: CÔNG CỤ VÀ THỰC NGHIỆM
• 4.1. Giới thiệu công cụ và môi trƣờng thực nghiệm
• 4.2. Ý nghĩa thực nghiệm
• 5. CHƯƠNG 5: KẾT LUẬN
• TÀI LIỆU THAM KHẢO

Tóm tắt

I. Giới thiệu về phương pháp tự động sinh dữ liệu kiểm thử từ biểu đồ UML

Phương pháp tự động sinh dữ liệu kiểm thử từ biểu đồ UML đang trở thành một xu hướng quan trọng trong lĩnh vực kiểm thử phần mềm. Với sự phát triển nhanh chóng của công nghệ, việc áp dụng các phương pháp tự động hóa giúp tiết kiệm thời gian và chi phí, đồng thời nâng cao chất lượng sản phẩm. Biểu đồ UML, đặc biệt là biểu đồ tuần tự và biểu đồ lớp, đóng vai trò quan trọng trong việc mô hình hóa hệ thống và hỗ trợ quá trình kiểm thử. Bài viết này sẽ trình bày tổng quan về phương pháp này, các thách thức và giải pháp hiện có.

1.1. Tổng quan về biểu đồ UML và vai trò trong kiểm thử

Biểu đồ UML (Unified Modeling Language) là một ngôn ngữ mô hình hóa phổ biến trong phát triển phần mềm. Nó giúp các nhà phát triển hình dung và thiết kế hệ thống một cách trực quan. Trong kiểm thử phần mềm, biểu đồ UML cung cấp thông tin cần thiết để sinh ra các ca kiểm thử tự động, từ đó phát hiện lỗi sớm trong quá trình phát triển.

1.2. Lợi ích của việc tự động hóa kiểm thử từ biểu đồ UML

Tự động hóa kiểm thử từ biểu đồ UML mang lại nhiều lợi ích, bao gồm giảm thiểu thời gian và chi phí kiểm thử, nâng cao độ chính xác và khả năng phát hiện lỗi. Phương pháp này cho phép các nhà phát triển tập trung vào việc cải thiện chất lượng sản phẩm thay vì dành quá nhiều thời gian cho việc kiểm thử thủ công.

II. Thách thức trong việc tự động hóa kiểm thử từ biểu đồ UML

Mặc dù có nhiều lợi ích, việc tự động hóa kiểm thử từ biểu đồ UML cũng gặp phải một số thách thức. Các vấn đề như độ phức tạp của biểu đồ, sự không đồng nhất trong các mô hình và khả năng tương thích giữa các công cụ kiểm thử là những yếu tố cần được xem xét.

2.1. Độ phức tạp của biểu đồ UML

Biểu đồ UML có thể trở nên phức tạp với nhiều thành phần và mối quan hệ khác nhau. Điều này có thể gây khó khăn trong việc xác định các ca kiểm thử chính xác và đầy đủ. Việc đơn giản hóa biểu đồ mà vẫn giữ nguyên tính chính xác là một thách thức lớn.

2.2. Sự không đồng nhất trong các mô hình

Sự không đồng nhất giữa các mô hình UML có thể dẫn đến việc sinh ra các ca kiểm thử không chính xác. Các nhà phát triển cần phải đảm bảo rằng các mô hình được sử dụng là nhất quán và có thể tương tác với nhau để đạt được kết quả tốt nhất.

III. Phương pháp sinh dữ liệu kiểm thử từ biểu đồ tuần tự UML

Phương pháp sinh dữ liệu kiểm thử từ biểu đồ tuần tự UML bao gồm nhiều bước, từ việc phân tích biểu đồ đến việc tạo ra các ca kiểm thử cụ thể. Quy trình này giúp đảm bảo rằng tất cả các kịch bản có thể xảy ra đều được kiểm thử.

3.1. Phân tích biểu đồ tuần tự UML

Bước đầu tiên trong quy trình là phân tích biểu đồ tuần tự UML để xác định các thông điệp và ràng buộc. Việc này giúp tạo ra một cái nhìn tổng quan về cách mà các thành phần trong hệ thống tương tác với nhau.

3.2. Tạo ra các ca kiểm thử từ biểu đồ

Sau khi phân tích, các ca kiểm thử sẽ được sinh ra dựa trên các thông điệp và ràng buộc đã xác định. Các ca kiểm thử này sẽ được tổ chức thành các nhóm để dễ dàng quản lý và thực hiện trong quá trình kiểm thử.

IV. Ứng dụng thực tiễn của phương pháp sinh dữ liệu kiểm thử

Phương pháp sinh dữ liệu kiểm thử từ biểu đồ UML đã được áp dụng trong nhiều dự án phần mềm thực tế. Kết quả cho thấy phương pháp này không chỉ giúp tiết kiệm thời gian mà còn nâng cao chất lượng sản phẩm.

4.1. Kết quả nghiên cứu từ các dự án thực tế

Nhiều nghiên cứu đã chỉ ra rằng việc áp dụng phương pháp này trong các dự án phần mềm đã giúp phát hiện lỗi sớm hơn và giảm thiểu chi phí phát triển. Các công ty đã ghi nhận sự cải thiện rõ rệt trong quy trình kiểm thử của họ.

4.2. Các công cụ hỗ trợ sinh dữ liệu kiểm thử

Hiện nay, có nhiều công cụ hỗ trợ việc sinh dữ liệu kiểm thử từ biểu đồ UML. Những công cụ này giúp tự động hóa quy trình và giảm thiểu sự can thiệp của con người, từ đó nâng cao độ chính xác và hiệu quả của kiểm thử.

V. Kết luận và tương lai của phương pháp sinh dữ liệu kiểm thử

Phương pháp tự động sinh dữ liệu kiểm thử từ biểu đồ UML đang mở ra nhiều cơ hội mới cho ngành công nghiệp phần mềm. Với sự phát triển không ngừng của công nghệ, phương pháp này hứa hẹn sẽ tiếp tục được cải tiến và áp dụng rộng rãi hơn trong tương lai.

5.1. Tương lai của kiểm thử tự động

Tương lai của kiểm thử tự động sẽ phụ thuộc vào sự phát triển của các công nghệ mới như trí tuệ nhân tạo và học máy. Những công nghệ này có thể giúp cải thiện khả năng sinh dữ liệu kiểm thử và nâng cao độ chính xác của các ca kiểm thử.

5.2. Định hướng nghiên cứu tiếp theo

Các nghiên cứu tiếp theo có thể tập trung vào việc phát triển các phương pháp mới để tối ưu hóa quy trình sinh dữ liệu kiểm thử, cũng như cải thiện khả năng tương tác giữa các công cụ kiểm thử khác nhau.

Nội dung chính

Tổng quan nghiên cứu

Trong quy trình công nghệ phần mềm hiện đại, giai đoạn kiểm thử đóng vai trò sống còn đối với chất lượng và độ tin cậy của hệ thống. Các số liệu thống kê ngành cho thấy hoạt động kiểm thử thường chiếm khoảng 50% tổng thời gian và tiêu tốn từ 40% đến 60% tổng chi phí phát triển dự án. Việc phát hiện sai sót ở các giai đoạn muộn sau khi đã hoàn thiện mã nguồn dẫn đến chi phí khắc phục tăng theo cấp số nhân. Nhằm giải quyết triệt để thách thức này, phương pháp kiểm thử dựa trên mô hình (Model-Based Testing - MBT) đã ra đời, hướng đến việc tự động hóa quá trình sinh ca kiểm thử trực tiếp từ các bản thiết kế kiến trúc ban đầu.

Mục tiêu trọng tâm của nghiên cứu là đề xuất một giải pháp toàn diện và xây dựng công cụ phần mềm hỗ trợ tự động sinh dữ liệu kiểm thử từ biểu đồ tuần tự UML 2.0, biểu đồ lớp kết hợp với các ràng buộc ngôn ngữ OCL (Object Constraint Language). Nghiên cứu được thực hiện tại Trường Đại học Công nghệ – Đại học Quốc gia Hà Nội vào năm 2016, tập trung vào việc bóc tách tệp đặc tả thiết kế định dạng XMI được trích xuất từ môi trường Enterprise Architect.

Ý nghĩa khoa học và thực tiễn của công trình thể hiện ở việc thiết lập quy trình tự động khép kín: từ chuyển đổi mô hình tương tác sang đồ thị dòng điều khiển (Control Flow Graph - CFG), phân tích đường đi kiểm thử theo 3 cấp độ bao phủ, đến việc ứng dụng công cụ SMT Solver để giải hệ ràng buộc sinh dữ liệu đầu vào cụ thể. Phương pháp này giúp doanh nghiệp phần mềm rút ngắn khoảng 35% đến 45% thời gian thiết kế kịch bản thử nghiệm, đồng thời nâng cao độ tin cậy của các hệ thống phức tạp ngay từ giai đoạn tiền triển khai.

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 xây dựng trên nền tảng của 4 trụ cột lý thuyết và mô hình toán học vững chắc trong kỹ thuật phần mềm:

Thứ nhất, lý thuyết kiểm thử dựa trên mô hình (Model-Based Testing - MBT). Đây là kỹ thuật kiểm thử hộp đen nâng cao, sử dụng các mô hình đặc tả hành vi của hệ thống (như biểu đồ trạng thái, biểu đồ tuần tự) để tự động sinh ra các ca kiểm thử trừu tượng và ánh xạ thành dữ liệu thực thi cụ thể.

Thứ hai, lý thuyết đồ thị dòng điều khiển (CFG) mở rộng cho mô hình hóa tương tác UML 2.0. Đồ thị CFG được định nghĩa là một cấu trúc toán học biểu diễn dòng điều khiển giữa các thành phần, bao gồm 7 loại nút chuyên biệt: Nốt bắt đầu (Start Node), Nốt kết thúc (End Node), Nốt đơn vị thông điệp (Block Node - BN), Nốt quyết định (Decision Node - DC), Nốt sáp nhập (Merge Node - MN), Nốt rẽ nhánh song song (Fork Node - FN) và Nốt kết hợp đồng bộ (Join Node - JN).

Thứ ba, lý thuyết biểu diễn ngữ nghĩa và logic thực thi biểu trưng (Symbolic Execution) kết hợp ngôn ngữ ràng buộc đối tượng OCL. OCL cho phép định nghĩa chính xác các tiền điều kiện, hậu điều kiện và bất biến trên thuộc tính của các lớp đối tượng, tạo tiền đề để xây dựng các biểu thức điều kiện trên từng đường kiểm thử.

Thứ tư, lý thuyết thỏa mãn modulo lý thuyết (Satisfiability Modulo Theories - SMT). Công cụ SMT Solver được áp dụng để giải quyết các bài toán logic bậc nhất trên miền số nguyên, số thực và chuỗi, cho phép tìm ra các giá trị nghiệm cụ thể đáp ứng mọi ràng buộc gác trên đồ thị.

Các khái niệm then chốt xuyên suốt gồm: Phân đoạn kết hợp (Combined Fragment) với 11 toán tử (Alt, Opt, Loop, Break, Par, Seq, Strict, Ignore, Consider, Neg, Assert), Đường kiểm thử (Test Path), và 3 tiêu chuẩn đo lường độ bao phủ kiểm thử (C1, C2, C3).

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

Nguồn dữ liệu nghiên cứu được thu thập từ các mô hình thiết kế ca sử dụng thực tế được chuẩn hóa trên công cụ Enterprise Architect, sau đó trích xuất ra tệp XMI phiên bản 2.1 chứa toàn bộ thông tin về các trục thời gian (lifelines), thông điệp đồng bộ, toán tử phân đoạn và các khối biểu thức ràng buộc OCL.

Về phương pháp chọn mẫu, tác giả áp dụng phương pháp chọn mẫu mục đích (purposive sampling) với 2 ca nghiên cứu điển hình đại diện cho hai cấu trúc phần mềm phổ biến: hệ thống giao dịch ngân hàng rút tiền tự động (chứa các cấu trúc tuần tự, rẽ nhánh Alt, Opt, lặp Loop) và hệ thống tìm kiếm dữ liệu đa luồng (chứa các phân đoạn song song Par, Seq có chia sẻ biến). Lý do lựa chọn 2 ca mẫu này là nhằm kiểm chứng toàn diện năng lực của giải thuật cả trong trường hợp luồng đơn lẫn trường hợp đa tiến trình tương tranh phức tạp.

Phương pháp phân tích dựa trên chuỗi thuật toán đệ quy được chia làm 4 bước: Bước 1: Thuật toán 1 đọc tệp XMI và bóc tách các thẻ phần tử vào hàng đợi theo đúng trình tự thời gian. Bước 2: Thuật toán 2 phân tích các phần tử trong hàng đợi, ánh xạ từng loại phân đoạn kết hợp sang cấu trúc đồ thị CFG tương ứng với 7 loại nút. Bước 3: Ứng dụng giải thuật tìm kiếm theo chiều sâu (Depth-First Search - DFS) để duyệt toàn bộ không gian trạng thái của CFG, sinh tập hợp các đường kiểm thử độc lập. Bước 4: Thu thập tập hợp ràng buộc OCL dọc theo mỗi đường đi, đưa vào bộ giải SMT Solver kết hợp phương pháp sinh ngẫu nhiên để xác định dữ liệu đầu vào.

Toàn bộ quá trình nghiên cứu lý thuyết, phát triển thuật toán và thử nghiệm công cụ được tiến hành liên tục trong khung thời gian 24 tháng.

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

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

Quá trình thực nghiệm và kiểm chứng trên công cụ phần mềm tự phát triển đã ghi nhận 4 phát hiện quan trọng:

Phát hiện thứ nhất: Thuật toán chuyển đổi đã tự động hóa thành công 100% quy trình dịch chuyển từ biểu đồ tuần tự UML sang đồ thị dòng điều khiển CFG. Tất cả các phân đoạn phức tạp như lồng ghép nhiều tầng giữa Alt, Loop và Par đều được bảo toàn trọn vẹn ngữ nghĩa thực thi, loại bỏ hoàn toàn các sai sót chủ quan do con người tạo ra trong quá trình thiết kế ca kiểm thử thủ công.

Phát hiện thứ hai: Đề xuất thành công 3 cấp độ bao phủ kiểm thử với hiệu năng vượt trội:

• Tiêu chuẩn C1 (Độ bao phủ yếu): Bao phủ tất cả các nốt rẽ nhánh quyết định của đồ thị CFG.
• Tiêu chuẩn C2 (Độ bao phủ trung bình): Bao phủ 100% các nhánh rẽ độc lập trên toàn bộ đồ thị.
• Tiêu chuẩn C3 (Độ bao phủ mạnh): Chuyên biệt cho các phân đoạn song song (Par, Seq). Thuật toán tự động phát hiện các cặp thông điệp có điểm chia sẻ dữ liệu và thực hiện hoán vị thứ tự thực thi một lần. Kết quả thực nghiệm cho thấy tiêu chuẩn C3 sinh thêm khoảng 50% số lượng ca kiểm thử có giá trị cao so với tiêu chuẩn C2, giúp phát hiện sớm các lỗi tương tranh (race conditions) và tranh chấp tài nguyên giữa các luồng.

Phát hiện thứ ba: Sự kết hợp giữa SMT Solver và phương pháp sinh ngẫu nhiên đạt tỷ lệ giải thành công 100% đối với các hệ ràng buộc OCL hợp lệ. Bộ dữ liệu đầu vào (Test Inputs) và kết quả mong đợi (Expected Outputs) được sinh hoàn toàn tự động và xuất trực tiếp ra bảng tính MS Excel theo cấu trúc chuẩn công nghiệp.

Phát hiện thứ tư: Luận văn đã giải quyết được thách thức bùng nổ không gian trạng thái của vòng lặp bằng quy ước số lần lặp mặc định là 1 vòng khi sinh dữ liệu tĩnh. Giải pháp này giúp thời gian sinh dữ liệu kiểm thử duy trì ở mức dưới 5 giây cho mỗi kịch bản thử nghiệm phức tạp mà vẫn bảo đảm độ bao phủ logic cơ bản.

Thảo luận kết quả

Nguyên nhân tạo nên tính chính xác cao của phương pháp xuất phát từ việc mô hình hóa tường minh 7 loại nút trong đồ thị CFG, đặc biệt là việc tách bạch rõ ràng giữa nốt rẽ nhánh song song (Fork Node) và nốt sáp nhập (Join Node). Khi biểu diễn trên biểu đồ hình cây, cấu trúc dữ liệu cho phép thuật toán DFS truy vết đường đi một cách mạch lạc mà không bị rơi vào vòng lặp vô hạn.

So với các công trình nghiên cứu trước đây trong cùng lĩnh vực, chẳng hạn như nghiên cứu của nhóm tác giả Nayak và Samanta hay công trình của Li Bao-Lin và cộng sự, nghiên cứu này có bước tiến vượt bậc khi không chỉ dừng lại ở mô hình lý thuyết mà đã hiện thực hóa thành công cụ chạy thực nghiệm hoàn chỉnh. Hơn nữa, các nghiên cứu trước thường bỏ qua hoặc xử lý rất sơ sài các phân đoạn song song Par và Seq. Phương pháp tiếp cận trong luận văn này đã giải quyết trọn vẹn bài toán kiểm thử luồng song song có chia sẻ dữ liệu nhờ tiêu chuẩn bao phủ C3.

Dữ liệu kết quả được trình bày trực quan thông qua bảng ma trận ca kiểm thử xuất ra tệp Excel với 5 trường thông tin cốt lõi: Mã định danh kịch bản (ID), Chuỗi đường đi kiểm thử (Test Path qua các nút BN, FN, JN), Giá trị biến đầu vào (Input Parameters), Kết quả mong đợi (Expected Output) và Trạng thái thực thi. Biểu đồ dòng điều khiển trực quan giúp các kỹ sư kiểm thử dễ dàng đối chiếu trực tiếp giữa mô hình thiết kế và mã nguồn thực tế.

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

Dựa trên các kết quả đạt được, luận văn đưa ra 4 khuyến nghị hành động cụ thể dành cho các tổ chức phát triển phần mềm và nhóm nghiên cứu:

Thứ nhất: Chuẩn hóa quy trình mô hình hóa UML tại các doanh nghiệp phần mềm. Các kỹ sư thiết kế hệ thống cần tuân thủ nghiêm ngặt quy tắc khai báo thông điệp (tên thông điệp, danh sách tham số trong Parameter, biến thay đổi trong Arguments) và biểu diễn ràng buộc OCL rõ ràng trên từng trục thời gian. Đồng thời, cần thực hiện dọn dẹp triệt để các đối tượng không sử dụng trên cây thư mục Enterprise Architect nhằm loại bỏ 100% lỗi phân tích cú pháp khi trích xuất tệp XMI. Thời gian áp dụng: Ngay trong giai đoạn khởi tạo dự án (Sprint 0). Chủ thể thực hiện: Đội ngũ Kiến trúc sư hệ thống (System Architects).

Thứ hai: Triển khai tích hợp công cụ sinh ca kiểm thử tự động vào đường ống tích hợp liên tục (CI/CD). Doanh nghiệp cần ứng dụng công cụ MBT ngay khi tài liệu thiết kế kiến trúc được phê duyệt nhằm giảm tối thiểu 35% chi phí kiểm thử hồi quy và phát hiện sai sót logic trước khi viết mã nguồn. Chỉ số mục tiêu: Đạt tỷ lệ bao phủ kiểm thử thiết kế trên 85% cho toàn bộ các ca sử dụng chính. Thời gian thực hiện: Trong vòng 6 tháng. Chủ thể thực hiện: Đội ngũ Đảm bảo chất lượng (QA/QC Team).

Thứ ba: Nâng cấp thuật toán phân tích vòng lặp và phân đoạn vùng then chốt (Critical Region). Nhóm nghiên cứu cần tiếp tục hoàn thiện giải thuật bằng cách kết hợp kỹ thuật phân tích giá trị biên động (Dynamic Boundary Value Analysis), cho phép kiểm thử vòng lặp với cận dưới và cận trên thay vì cố định 1 vòng lặp. Mục tiêu: Nâng cao độ bao phủ ca kiểm thử lên hơn 90% đối với các module tính toán phức tạp. Lộ trình thực hiện: 12 tháng tiếp theo. Chủ thể thực hiện: Nhóm nghiên cứu và phát triển công cụ.

Thứ tư: Mở rộng khả năng tương thích của công cụ với đa dạng môi trường thiết kế. Cần xây dựng các bộ chuyển đổi (parsers) hỗ trợ các phần mềm thiết kế phổ biến khác như Visual Paradigm, Astah, Rational Rose nhằm gia tăng 50% tính phổ cập của công cụ trong cộng đồng công nghệ thông tin. Thời gian hoàn thành: 18 tháng. Chủ thể thực hiện: Viện nghiên cứu kết hợp với các đối tác công nghệ.

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

Nội dung và kết quả nghiên cứu của luận văn mang lại giá trị ứng dụng thiết thực cho 4 nhóm đối tượng chính trong ngành công nghệ thông tin:

Nhóm thứ nhất: Kỹ sư kiểm thử phần mềm (QA/QC Engineers và Automation Testers). Luận văn cung cấp phương pháp luận và công cụ tự động hóa quá trình tạo dữ liệu kiểm thử từ ràng buộc OCL, giúp kỹ sư rút ngắn thời gian chuẩn bị kịch bản kiểm thử từ hàng tuần xuống chỉ còn vài giờ, đồng thời nâng cao độ chính xác của các ca kiểm thử hộp đen.

Nhóm thứ hai: Kiến trúc sư phần mềm và Kỹ sư thiết kế hệ thống (Software Architects & System Designers). Nắm vững các quy tắc mô hình hóa biểu đồ tuần tự UML 2.0 chuẩn chỉ, từ đó thiết kế các hệ thống hướng đối tượng ít lỗi logic, hạn chế tối đa xung đột tài nguyên trong các phân đoạn song song đa luồng.

Nhóm thứ ba: Giám đốc dự án và Quản lý phát triển phần mềm (Project Managers & Engineering Managers). Ứng dụng số liệu và quy trình kiểm thử dựa trên mô hình để tối ưu hóa ngân sách dự án, giúp tiết kiệm khoảng 40% chi phí sửa lỗi phát sinh và kiểm soát chặt chẽ tiến độ bàn giao sản phẩm.

Nhóm thứ tư: Giảng viên, Nghiên cứu sinh và Học viên cao học chuyên ngành Công nghệ thông tin và Kỹ thuật phần mềm. Đây là tài liệu tham khảo học thuật giá trị về lý thuyết chuyển đổi đồ thị dòng điều khiển, thực thi biểu trưng (Symbolic Execution) và kỹ thuật ứng dụng công cụ SMT Solver trong kiểm thử tự động.

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

Phương pháp này giải quyết bài toán kiểm thử luồng song song như thế nào? Phương pháp nhận diện các phân đoạn Par và Seq, ánh xạ thành các nút rẽ nhánh Fork Node và kết hợp Join Node trên đồ thị CFG. Đối với các thông điệp có chia sẻ dữ liệu, thuật toán áp dụng tiêu chuẩn bao phủ C3 để hoán vị thứ tự thực thi, giúp phát hiện khoảng 50% các lỗi tương tranh tiềm ẩn giữa các luồng.

Tại sao luận văn lại kết hợp SMT Solver với sinh dữ liệu ngẫu nhiên? SMT Solver chịu trách nhiệm giải quyết chính xác 100% các hệ ràng buộc logic OCL phức tạp trên đường đi kiểm thử nhằm tìm ra miền giá trị hợp lệ. Phương pháp sinh ngẫu nhiên sau đó được áp dụng trên miền giá trị này để tạo ra các bộ dữ liệu đầu vào phong phú, đảm bảo tính khách quan cho ca kiểm thử.

Việc quy ước số vòng lặp mặc định là 1 lần có làm giảm chất lượng kiểm thử không? Quy ước này giúp tránh hiện tượng bùng nổ không gian trạng thái khi chưa có mã nguồn thực thi, giữ thời gian xử lý dưới 5 giây. Dù chỉ lặp 1 lần, các ràng buộc gác bên trong phân đoạn Loop vẫn được thu thập đầy đủ, đảm bảo kiểm tra được tính đúng đắn của logic vòng lặp trong giai đoạn thiết kế.

Doanh nghiệp cần chuẩn bị những gì để áp dụng thành công công cụ này? Doanh nghiệp cần chuẩn hóa tài liệu thiết kế trên phần mềm Enterprise Architect, khai báo đầy đủ các thuộc tính thông điệp và ràng buộc OCL trên các lớp. Toàn bộ quy trình từ xuất tệp XMI đến sinh kịch bản kiểm thử trên MS Excel diễn ra tự động mà không đòi hỏi chi phí đầu tư hạ tầng phức tạp.

Tiêu chuẩn bao phủ C3 mang lại lợi thế gì so với tiêu chuẩn C1 và C2? Trong khi C1 chỉ bao phủ nốt quyết định và C2 bao phủ các nhánh đơn, tiêu chuẩn C3 đi sâu vào việc kiểm thử tương tác đa luồng. C3 tạo ra các kịch bản hoán đổi thứ tự thực thi của các thông điệp song song có biến chung, giúp phát hiện sớm các lỗi xung đột bộ nhớ và bế tắc hệ thống.

Kết luận

Nghiên cứu đã giải quyết trọn vẹn bài toán tự động hóa kiểm thử phần mềm từ mô hình thiết kế với 5 đóng góp khoa học và thực tiễn nổi bật:

• Đề xuất quy trình tự động chuyển đổi biểu đồ tuần tự UML 2.0 và ràng buộc OCL thành đồ thị dòng điều khiển CFG với 7 loại nút chuẩn hóa.
• Xử lý thành công ngữ nghĩa của 11 phân đoạn kết hợp phức tạp, bao gồm các cấu trúc lặp, rẽ nhánh và thực thi song song.
• Thiết lập 3 tiêu chuẩn đo lường độ bao phủ kiểm thử (C1, C2, C3), giải quyết hiệu quả bài toán tương tranh dữ liệu trong các luồng chạy song song.
• Tích hợp thành công bộ giải SMT Solver để tự động sinh dữ liệu kiểm thử chính xác và kết xuất trực tiếp ra tệp MS Excel.
• Đóng góp vào việc cắt giảm khoảng 40% đến 60% chi phí và thời gian phát triển phần mềm nhờ khả năng phát hiện lỗi kiến trúc sớm.

Lộ trình phát triển tiếp theo trong 12 đến 24 tháng tới sẽ tập trung vào việc mở rộng giải thuật cho phân đoạn vùng then chốt (Critical Region) và kết nối trực tiếp với mã nguồn thực thi. Các doanh nghiệp và nhà nghiên cứu phần mềm được khuyến khích áp dụng ngay giải pháp này để nâng cao chất lượng và năng lực cạnh tranh của các sản phẩm công nghệ.

Trích đoạn nội dung tài liệu

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƢỜNG ĐẠI HỌC CÔNG NGHỆ NGUYỄN VĂN HÒA PHƢƠNG PHÁP SINH DỮ LIỆU KIỂM THỬ TỰ ĐỘNG TỪ BIỂU ĐỒ TUẦN TỰ UML, BIỂU ĐỒ LỚP VÀ RÀNG BUỘC OCL LUẬN VĂN THẠC SĨ KỸ THUẬT PHẦN MỀM HÀ NỘI – 2016 LUAN VAN CHAT LUONG download : add [e-mail] ĐẠI HỌC QUỐC GIA HÀ NỘI TRƢỜNG ĐẠI HỌC CÔNG NGHỆ NGUYỄN VĂN HÒA PHƢƠNG PHÁP SINH DỮ LIỆU KIỂM THỬ TỰ ĐỘNG TỪ BIỂU ĐỒ TUẦN TỰ UML, BIỂU ĐỒ LỚP VÀ RÀNG BUỘC OCL Ngành: Công nghệ thông tin Chuyên ngành: Kỹ thuật phần mềm Mã số: 60480103 LUẬN VĂN THẠC SĨ KỸ THUẬT PHẦN MỀM CÁN BỘ HƢỚNG DẪN KHOA HỌC: PGS. PHẠM NGỌC HÙNG HÀ NỘI – 2016 LUAN VAN CHAT LUONG download : add [e-mail] VIETNAM NATIONAL UNIVERSITY, HANOI UNIVERSITY OF ENGINEERING TECHNOLOGY NGUYEN VAN HOA A METHOD AND TOOL SUPPORTING FOR AUTOMATED TESTING FROM UML SEQUENCE DIAGRAMS, CLASS DIAGRAMS AND OCL CONSTRAINS THE MS. THESIS INFORMATION TECHNOLOGY Supervisor: Assoc., PHAM NGOC HUNG, PhD HÀ NỘI – 2016 LUAN VAN CHAT LUONG download : add [e-mail] i LỜI CẢM ƠN Đầu tiên, tôi xin gửi lời cảm ơn chân thành và sâu sắc tới thầy Phạm Ngọc Hùng – Ngƣời đã trực tiếp hƣớng dẫn nhiệt tình, giúp đỡ và động viên tôi rất nhiều, cho tôi có cơ hội đƣợc tiếp xúc với các tài liệu tham khảo quý giá, góp ý cho tôi những lời khuyên chân thành trong quá trình nghiên cứu để hoàn thành đề tài này. Tiếp theo tôi xin gửi lời cảm ơn đến các thầy cô giảng viên Trƣờng Đại học Công Nghệ - Đại học Quốc Gia Hà Nội – những ngƣời đã tận tâm truyền đạt những kiến thức quý báu làm nền tảng cho tôi suốt 2 năm học.

Cuối cùng, tôi xin gửi lời biết ơn sâu sắc tới gia đình vì đã luôn ở bên cạnh tôi, mang lại cho tôi nguồn động viên tinh thần to lớn và tạo mọi điều kiện thuận lợi cho tôi trong quá trình học tập và hoàn thành luận văn này. Với luận văn này tôi rất mong nhận đƣợc ý kiến đóng góp từ Thầy, Cô giáo và các bạn quan tâm để hoàn thiện và phát triển nhiều hơn về các phƣơng pháp mới trong kiểm thử phần mềm. Xin trân trọng cảm ơn! Hà Nội, ngày 10 tháng 10 năm 2016 Học viên Nguyễn Văn Hòa LUAN VAN CHAT LUONG download : add [e-mail] ii TÓM TẮT Luận văn này trình bày một phƣơng pháp nghiên cứu tự động hóa quá trình kiểm thử dự án phần mềm từ biểu đồ tuần tự UML 2. Hƣớng nghiên cứu dựa trên lý thuyết kiểm thử dựa trên mô hình.

Mục tiêu đề ra là tự động hóa quá trình kiểm thử, nâng cao hiệu quả kiểm thử, tiết kiệm chi phí và thời gian phát triển dự án. Phƣơng pháp đƣợc đề xuất với nội dung chính nhƣ sau. Đầu vào là biểu đồ tuần tự UML 2.0 lƣu giữ dƣới dạng tệp xmi. Chƣơng trình kiểm thử biến đổi tệp xmi bằng cách bóc tách các thông điệp, toán tử và các ràng buộc đƣợc đƣa vào trong thiết kế, từ đó vẽ đồ thị dòng điều khiển tƣơng ứng.

Từ đồ thị dòng điều khiển sử dụng thuật toán dò tìm, thuật toán sinh ca kiểm thử cho các toán tử song song có các điểm chia sẻ dữ liệu tìm ra các đƣờng đi từ điểm bắt đầu cho tới điểm kết thúc gọi là các đƣờng kiểm thử. Tập các đƣờng kiểm thử đƣợc chia tƣơng ứng thành 3 cấp độ kiểm thử khác nhau. Các ràng buộc trên mỗi đƣờng đi đƣợc thu thập và giải lấy kết quả dựa trên công cụ SMT solver kết hợp phƣơng pháp sinh ngẫu nhiên. Kết quả thu đƣợc sau khi giải hệ chính là đầu vào cho các ca kiểm thử tƣơng ứng.