Luận án tiến sĩ công nghệ thông tin kiểm thử dựa trên mô hình với cách tiếp cận mô hình hóa chuyên biệt miền

Luận án tiến sĩ nghiên cứu phương pháp kiểm thử dựa trên mô hình với tiếp cận mô hình hóa chuyên biệt miền, ứng dụng hiệu quả trong công nghệ phần mềm.

• Người hướng dẫn: PGS. Nguyễn Ngọc Bình
• Trường học: Đại học Công nghệ
• Chuyên ngành: Công nghệ phần mềm
• Đề tài: Kiểm thử dựa trên mô hình với tiếp cận mô hình hóa chuyên biệt miền
• Loại tài liệu: luận án tiến sĩ
• Địa điểm: Hà Nội

Mục lục chi tiết

• LỜI CAM ĐOAN
• LỜI CẢM ƠN
• TÓM TẮT
• MỤC LỤC
• DANH MỤC CÁC TỪ VIẾT TẮT
• DANH MỤC CÁC BẢNG
• DANH MỤC CÁC HÌNH VẼ
• DANH MỤC CÁC THUẬT TOÁN
• DANH MỤC CÁC ĐẶC TẢ
• 1. CHƯƠNG 1: MỞ ĐẦU
• 1.1. Đặt vấn đề
• 2. CHƯƠNG 2: KIẾN THỨC CƠ SỞ
• 2.1. Kiểm thử dựa trên ca sử dụng
• 2.1.1. Kiểm thử phần mềm
• 2.1.2. Ca sử dụng
• 2.1.3. Xây dựng các ca kiểm thử từ ca sử dụng
• 2.2. Mô hình hóa chuyên biệt miền
• 2.2.1. Một số khái niệm cơ bản
• 2.2.2. Phương pháp xây dựng DSML
• 2.2.3. Xây dựng DSML trong Eclipse
• 2.3. Chuyển đổi mô hình
• 2.3.1. Chuyển đổi mô hình sang mô hình
• 2.3.2. Chuyển đổi mô hình sang văn bản
• 2.3.3. Ngôn ngữ ràng buộc đối tượng OCL
• 2.3.3.1. Cơ bản về OCL
• 2.3.3.2. Công cụ hỗ trợ OCL
• 2.4. Tổng kết chương
• 3. CHƯƠNG 3: ĐẶC TẢ CA SỬ DỤNG THEO HƯỚNG MÔ HÌNH HÓA CHUYÊN BIỆT MIỀN
• 3.1. Các nghiên cứu liên quan
• 3.2. Xác định miền cho ngữ cảnh đặc tả ca sử dụng
• 3.3. Cú pháp của USL
• 3.3.1. Cú pháp trừu tượng của USL
• 3.3.2. Các luật hợp lệ trên siêu mô hình của USL
• 3.3.3. Cú pháp cụ thể của USL
• 3.4. Ngữ nghĩa hình thức của mô hình USL
• 3.5. Chuyển đổi mô hình USL
• 3.5.1. Sinh các ca kiểm thử
• 3.5.2. Sinh các mô hình cấu trúc và mô hình hành vi
• 3.6. Tổng kết chương
• 4. CHƯƠNG 4: PHƯƠNG PHÁP SINH TỰ ĐỘNG CÁC CA KIỂM THỬ TỪ MÔ HÌNH CA SỬ DỤNG VÀ MÔ HÌNH KHÁI NIỆM MIỀN CỦA HỆ THỐNG
• 4.1. Các nghiên cứu liên quan
• 4.2. Tổng quan phương pháp đề xuất
• 4.3. Ngôn ngữ đặc tả các ca kiểm thử TCSL
• 4.3.1. Xác định miền cho ngữ cảnh đặc tả ca kiểm thử chức năng
• 4.3.2. Định nghĩa siêu mô hình TCSL
• 4.4. Chuyển đổi mô hình từ USL sang TCSL
• 4.4.1. Xác định tiêu chí phủ
• 4.4.2. Sinh các kịch bản ca sử dụng và các ràng buộc
• 4.4.3. Sinh các bộ dữ liệu đầu vào kiểm thử
• 4.4.4. Sinh mô hình TCSL
• 4.5. Tổng kết chương
• 5. CHƯƠNG 5: THỰC NGHIỆM VÀ ĐÁNH GIÁ
• 5.1. Công cụ hỗ trợ USL
• 5.2. Ví dụ minh họa
• 5.2.1. Đánh giá ngôn ngữ USL
• 5.2.2. Đánh giá phương pháp sinh các ca kiểm thử USLTG
• 5.3. Tổng kết chương
• 6. CHƯƠNG 6: KẾT LUẬN VÀ HƯỚNG PHÁT TRIỂN
• 6.1. Các đóng góp của luận án
• 6.2. Hướng phát triển
• DANH MỤC CÁC CÔNG TRÌNH KHOA HỌC
• TÀI LIỆU THAM KHẢO

Tóm tắt

I. Giới thiệu và bối cảnh nghiên cứu

Luận án tiến sĩ này tập trung vào kiểm thử dựa trên mô hình với tiếp cận mô hình hóa chuyên biệt miền. Mục tiêu chính là sinh tự động các ca kiểm thử chức năng từ các ca sử dụng, áp dụng các kỹ thuật kiểm thử dựa trên mô hình và mô hình hóa chuyên biệt miền. Luận án đề xuất các phương pháp đặc tả rõ ràng các ca sử dụng và ca kiểm thử bằng các ngôn ngữ mô hình hóa chuyên biệt, đồng thời chuyển đổi tự động các mô hình ca sử dụng sang mô hình ca kiểm thử. Các đóng góp chính bao gồm việc xây dựng ngôn ngữ USL và TCSL, cùng với phương pháp USLTG để sinh tự động ca kiểm thử.

1.1. Bối cảnh và thách thức

Trong bối cảnh phát triển phần mềm hiện đại, kiểm thử phần mềm đóng vai trò quan trọng trong việc đảm bảo chất lượng. Tuy nhiên, việc sinh và thực thi các ca kiểm thử thường tốn nhiều thời gian và chi phí. Kiểm thử dựa trên mô hình (MBT) được xem là giải pháp tối ưu để tăng tính tự động hóa, giảm chi phí và nâng cao chất lượng. Thách thức chính là việc sinh tự động các ca kiểm thử từ các mô hình ca sử dụng, đặc biệt khi các yêu cầu thay đổi liên tục.

1.2. Mục tiêu nghiên cứu

Luận án hướng đến việc giải quyết các thách thức trong kiểm thử dựa trên mô hình bằng cách đề xuất các phương pháp mô hình hóa chuyên biệt miền để đặc tả ca sử dụng và ca kiểm thử. Mục tiêu cụ thể là xây dựng các ngôn ngữ USL và TCSL, cùng với phương pháp USLTG để sinh tự động ca kiểm thử từ ca sử dụng.

II. Phương pháp và công cụ đề xuất

Luận án đề xuất các phương pháp và công cụ để thực hiện kiểm thử dựa trên mô hình với tiếp cận mô hình hóa chuyên biệt miền. Cụ thể, ngôn ngữ USL được xây dựng để đặc tả rõ ràng các ca sử dụng, trong khi TCSL được sử dụng để đặc tả các ca kiểm thử. Phương pháp USLTG được đề xuất để chuyển đổi tự động các mô hình USL sang TCSL, từ đó sinh ra các ca kiểm thử tự động. Bộ công cụ hỗ trợ USL được xây dựng để tích hợp các phương pháp này vào quy trình phát triển phần mềm.

2.1. Ngôn ngữ USL và TCSL

Ngôn ngữ USL (Use Case Specification Language) được thiết kế để đặc tả rõ ràng các ca sử dụng, hướng đến khả năng sinh tự động các chế tác phần mềm khác nhau. TCSL (Test Case Specification Language) được sử dụng để đặc tả các ca kiểm thử, đảm bảo tính rõ ràng và đầy đủ thông tin cần thiết cho việc thực thi kiểm thử tự động.

2.2. Phương pháp USLTG

Phương pháp USLTG (USL-based Test Generation) được đề xuất để sinh tự động các ca kiểm thử từ ca sử dụng. Phương pháp này chuyển đổi tự động các mô hình USL sang TCSL, từ đó sinh ra các ca kiểm thử chức năng. Quá trình này bao gồm việc xác định các kịch bản ca sử dụng, sinh dữ liệu đầu vào kiểm thử, và tạo mô hình TCSL.

III. Thực nghiệm và đánh giá

Luận án tiến hành các thực nghiệm để đánh giá hiệu quả của các phương pháp và công cụ đề xuất. Các ví dụ nghiên cứu được áp dụng để minh họa quy trình sinh tự động ca kiểm thử từ ca sử dụng. Kết quả thực nghiệm cho thấy khả năng tích hợp kiểm thử dựa trên mô hình vào quy trình phát triển phần mềm, đồng thời đánh giá tính hiệu quả của ngôn ngữ USL và phương pháp USLTG.

3.1. Ví dụ minh họa

Các ví dụ nghiên cứu được sử dụng để minh họa quy trình sinh tự động ca kiểm thử từ ca sử dụng. Các mô hình USL được tạo ra để đặc tả ca sử dụng, sau đó chuyển đổi sang TCSL để sinh ca kiểm thử. Kết quả cho thấy tính khả thi và hiệu quả của phương pháp đề xuất.

3.2. Đánh giá kết quả

Kết quả thực nghiệm được đánh giá dựa trên khả năng sinh tự động ca kiểm thử và tính chính xác của các ca kiểm thử được sinh. So sánh với các phương pháp khác, phương pháp USLTG cho thấy ưu điểm trong việc tích hợp mô hình hóa chuyên biệt miền vào quy trình kiểm thử dựa trên mô hình.

IV. Kết luận và hướng phát triển

Luận án đã đề xuất các phương pháp và công cụ để thực hiện kiểm thử dựa trên mô hình với tiếp cận mô hình hóa chuyên biệt miền. Các kết quả thực nghiệm cho thấy tính khả thi và hiệu quả của các phương pháp đề xuất. Hướng phát triển trong tương lai bao gồm việc mở rộng ứng dụng của các phương pháp này trong các lĩnh vực khác nhau, cải tiến các công cụ hỗ trợ, và tích hợp sâu hơn vào quy trình phát triển phần mềm.

4.1. Đóng góp chính

Luận án đã đóng góp vào lĩnh vực kiểm thử phần mềm bằng cách đề xuất các phương pháp mô hình hóa chuyên biệt miền và kiểm thử dựa trên mô hình. Các ngôn ngữ USL và TCSL, cùng với phương pháp USLTG, đã được xây dựng và thử nghiệm thành công.

4.2. Hướng phát triển

Hướng phát triển trong tương lai bao gồm việc mở rộng ứng dụng của các phương pháp này trong các lĩnh vực khác nhau, cải tiến các công cụ hỗ trợ, và tích hợp sâu hơn vào quy trình phát triển phần mềm. Ngoài ra, việc nghiên cứu thêm về khả năng sinh tự động các mô hình cấu trúc và hành vi từ ca sử dụng cũng là một hướng đi tiềm năng.

Nội dung chính

Tổng quan luận án

Hoạt động kiểm thử phần mềm chiếm vị trí trọng yếu trong việc bảo đảm chất lượng hệ thống, chiếm từ 30% đến 60% tổng thời gian và chi phí của quy trình phát triển phần mềm [71]. Trong thực tế, các yêu cầu phần mềm thường xuyên thay đổi dẫn đến nhu cầu thực hiện kiểm thử hồi quy lớn, đòi hỏi nỗ lực cao trong việc xác định, duy trì và thực thi các ca kiểm thử. Mặc dù tự động hóa thực thi kiểm thử đã đạt được nhiều giải pháp thương mại và mã nguồn mở, việc sinh tự động các ca kiểm thử từ giai đoạn đặc tả yêu cầu vẫn đối mặt với nhiều thách thức. Phương pháp kiểm thử dựa trên mô hình (Model-Based Testing - MBT) cung cấp khả năng tự động hóa cả khâu sinh ca kiểm thử lẫn khâu thực thi, giúp duy trì bộ kiểm thử và độ bao phủ khi hệ thống tiến hóa [9, 71]. Tuy nhiên, hai bước đầu của quy trình MBT là mô hình hóa yêu cầu và sinh ca kiểm thử tự động từ ca sử dụng còn gặp nhiều rào cản do các mô tả ngôn ngữ tự nhiên thiếu tính hình thức, trong khi các biểu đồ UML chuẩn chưa tích hợp đầy đủ dữ liệu kiểm thử cụ thể và trạng thái bên trong của hệ thống.

Mục tiêu tổng quát của luận án là tích hợp ca sử dụng vào ngữ cảnh của quy trình kiểm thử dựa trên mô hình và kỹ nghệ phát triển hướng mô hình (Model-Driven Development - MDD), qua đó tự động hóa hoạt động kiểm thử chức năng mức hệ thống từ các yêu cầu chức năng. Các mục tiêu cụ thể được triển khai nhằm giải quyết bốn thách thức chính:

1. Xây dựng một ngôn ngữ mô hình hóa chuyên biệt miền (DSML) cho phép đặc tả ca sử dụng rõ ràng, đủ chi tiết về cấu trúc và hành vi để tích hợp vào MDD và MBT.
2. Xây dựng một ngôn ngữ chuyên biệt miền để đặc tả đầy đủ, chi tiết các thông tin của ca kiểm thử chức năng, bao gồm các bước kiểm thử, hành động, đối tượng tác động, loại điểm kiểm tra, trạng thái hệ thống và dữ liệu kiểm thử cụ thể.
3. Đề xuất phương pháp chuyển đổi tự động từ mô hình ca sử dụng và mô hình khái niệm miền của hệ thống sang mô hình ca kiểm thử nhằm sinh đầy đủ kịch bản, dữ liệu đầu vào và trạng thái bên trong hệ thống.
4. Xây dựng bộ công cụ phần mềm hỗ trợ mô hình hóa trực quan và thực thi các chuyển đổi mô hình tự động, phục vụ sinh ca kiểm thử và sinh tài liệu đặc tả yêu cầu.

Đối tượng nghiên cứu của luận án bao gồm: mô hình ca sử dụng, ca kiểm thử chức năng mức hệ thống, phương pháp sinh ca kiểm thử từ ca sử dụng, cùng các kỹ thuật mô hình hóa chuyên biệt miền (DSM), chuyển đổi mô hình và kiểm thử dựa trên mô hình. Phạm vi nghiên cứu tập trung vào kiểm thử chức năng phần mềm ở mức hệ thống (System Testing), áp dụng cho các ca sử dụng biểu diễn yêu cầu chức năng và mô hình lớp khái niệm miền, không mở rộng sang các loại kiểm thử phi chức năng hay kiểm thử mã nguồn mức đơn vị.

---

Tổng quan tài liệu và vị trí của luận án

Luận án tiến hành phân loại và đánh giá các công trình nghiên cứu trước đây về sinh ca kiểm thử từ ca sử dụng theo ba hướng tiếp cận chính:

• Hướng tiếp cận dựa trên xử lý ngôn ngữ tự nhiên (NLP): Các nghiên cứu tiêu biểu như của Wang và cộng sự (RUCM) [73], Sinha và cộng sự [58] sử dụng ngôn ngữ tự nhiên có cấu trúc theo mẫu, kết hợp các từ khóa và quy tắc hạn chế (Restricted-form of Natural Language - RNL). Kỹ thuật NLP được áp dụng để trích xuất các mô hình trung gian trước khi sinh ca kiểm thử. Hạn chế của hướng này là các ngôn ngữ đặc tả không có cú pháp trừu tượng hình thức (informal), việc phân tích ngữ pháp phụ thuộc ngôn ngữ tự nhiên cụ thể và khó trích xuất chính xác các ràng buộc logic phức tạp để sinh dữ liệu kiểm thử.
• Hướng tiếp cận dựa trên biểu đồ UML chuẩn: Các nghiên cứu của Briand và cộng sự [7], Hartmann và cộng sự [24], Shen và cộng sự [51], Sharma và cộng sự [67] sử dụng biểu đồ hoạt động (Activity Diagram) hoặc biểu đồ tuần tự (Sequence Diagram) để nắm bắt luồng điều khiển và phân biệt hành động giữa tác nhân với hệ thống. Hạn chế cốt lõi là các mô hình này chủ yếu sinh ra các kịch bản kiểm thử trừu tượng (chuỗi bước thực hiện) mà không tự động xác định được dữ liệu kiểm thử cụ thể cũng như trạng thái bên trong của cơ sở dữ liệu.
• Hướng tiếp cận dựa trên ngôn ngữ chuyên biệt miền (DSL): Nghiên cứu của Escalona và cộng sự [16, 23] phát triển kỹ thuật NDT (Navigational Development Techniques) cho ứng dụng web nhưng không giải quyết việc xác định giá trị dữ liệu cụ thể. Nghiên cứu của Smialek và cộng sự [63, 65] đề xuất ngôn ngữ RSL (Requirements Specification Language) và ngôn ngữ đặc tả kiểm thử TSL (Test Specification Language), tuy nhiên dữ liệu kiểm thử sinh ra chỉ dừng lại ở các mệnh đề mô tả điều kiện. Nghiên cứu của Soeken và cộng sự [59] với ngôn ngữ SelabReq hỗ trợ sinh mô hình cấu trúc và hành vi trong MDD nhưng không hỗ trợ sinh ca kiểm thử.

+----------------------------------------------------------------------------------------------------+
|                                    CÁC HƯỚNG TIẾP CẬN TRƯỚC ĐÂY                                    |
+------------------------------------+----------------------------------+----------------------------+
| Hướng NLP (RUCM, Sinha)           | Hướng UML (Briand, Hartmann)     | Hướng DSL (NDT, RSL/TSL)   |
| - Dựa trên văn bản bán cấu trúc   | - Biểu đồ hoạt động/tuần tự      | - Ngôn ngữ chuyên biệt     |
| - Thiếu cú pháp trừu tượng        | - Sinh kịch bản trừu tượng       | - Dữ liệu dừng ở mô tả     |
| - Khó sinh dữ liệu cụ thể         | - Thiếu dữ liệu cụ thể & State   | - Chưa tích hợp trọn vẹn   |
+------------------------------------+----------------------------------+----------------------------+
                                                  |
                                                  v
+----------------------------------------------------------------------------------------------------+
|                                   KHOẢNG TRỐNG NGHIÊN CỨU ĐÃ CHỌN                                  |
| - Thiếu ngôn ngữ đặc tả ca sử dụng hình thức (USL) đủ chi tiết cho MDD và MBT                      |
| - Thiếu ngôn ngữ đặc tả ca kiểm thử (TCSL) chứa đầy đủ đối tượng, hành động, checkpoint và state  |
| - Thiếu phương pháp giải ràng buộc OCL tự động sinh dữ liệu kiểm thử cụ thể và trạng thái hệ thống |
+----------------------------------------------------------------------------------------------------+

Khoảng trống nghiên cứu mà luận án lựa chọn giải quyết là: thiết lập một quy trình hình thức hoàn chỉnh, sử dụng kỹ thuật mô hình hóa chuyên biệt miền để đặc tả cả ca sử dụng và ca kiểm thử, kết hợp giải các ràng buộc logic OCL trên mô hình miền nhằm sinh tự động các ca kiểm thử chứa đầy đủ dữ liệu cụ thể, trạng thái bên trong hệ thống và các điểm kiểm tra phục vụ tự động hóa thực thi kiểm thử.

---

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

Khung lý thuyết và các khái niệm nền tảng

Luận án xây dựng trên nền tảng kỹ nghệ hướng mô hình (MDE), phát triển hướng mô hình (MDD) và kiểm thử dựa trên mô hình (MBT) theo mô hình chữ V [50]. Quy trình MBT tiêu chuẩn gồm 5 bước [9]: (1) Mô hình hóa, (2) Sinh ca kiểm thử, (3) Sinh tập lệnh thực thi kiểm thử, (4) Thực thi kiểm thử trên SUT (System Under Testing), và (5) Phân tích kết quả kiểm thử. Luận án tập trung giải quyết Bước 1 và Bước 2.

              Quy trình Kiểm thử Dựa trên Mô hình (MBT) 5 Bước

Về mặt kiểm thử phần mềm, luận án áp dụng các nguyên lý kiểm thử hộp đen ở mức hệ thống [5, 49]. Để bảo đảm tính đầy đủ của tập kiểm thử, luận án áp dụng:

• Tiêu chí phủ đường cơ bản (Basic Path Coverage Criterion) [41, 46]: duyệt đồ thị theo chiều sâu, giới hạn mỗi vòng lặp thực hiện nhiều nhất một lần.
• Tiêu chí phủ đường hoạt động (Activity Path Coverage Criterion) của Chen và cộng sự [39]: mở rộng phủ đường cơ bản để bao phủ các mô hình lỗi trong điểm quyết định, lỗi vòng lặp (kiểm tra 0 và 1 lần với vòng lặp while-do, 1 và 2 lần với vòng lặp do-while), và lỗi đồng bộ hóa trong các hành động đồng thời thông qua duyệt theo chiều rộng.
• Độ phức tạp Cyclomatic $V(G)$ của McCabe [33] được sử dụng để xác định chặn trên của số ca kiểm thử phủ nhánh và chặn dưới của tổng số đường thực thi có thể có: $V(G) = E - N + 2$ hoặc $V(G) = P + 1$ (trong đó $E$ là số cạnh, $N$ là số nút, $P$ là số điểm quyết định nhị phân) [8, 31].

Về kỹ thuật mô hình hóa chuyên biệt miền (DSM) [9, 35, 62], ngôn ngữ được cấu thành từ: cú pháp trừu tượng (định nghĩa bằng siêu mô hình - Metamodel), cú pháp cụ thể (ký pháp đồ họa), tập luật hợp lệ (Well-formedness rules) và ngữ nghĩa hình thức. Ngữ nghĩa thực thi của mô hình được biểu diễn thông qua Hệ thống chuyển trạng thái được gán nhãn (Labelled Transition System - LTS).

Về kỹ thuật chuyển đổi mô hình và ràng buộc:

• Chuyển đổi mô hình sang mô hình (Model-to-Model - M2M): sử dụng ngôn ngữ dựa trên luật ATL (ATLAS Transformation Language) [9, 32].
• Chuyển đổi mô hình sang văn bản (Model-to-Text - M2T): sử dụng ngôn ngữ dựa trên mẫu Acceleo (chuẩn MOF Model-to-Text của OMG) [22, 30].
• Ngôn ngữ ràng buộc đối tượng OCL (Object Constraint Language) [10, 54, 74]: biểu diễn các bất biến, tiền điều kiện, hậu điều kiện và điều kiện gác trên mô hình.
• Công cụ USE (UML-based Specification Environment): đóng vai trò bộ giải ràng buộc (solver) trung gian để tìm kiếm các thể hiện đối tượng (snapshots) thỏa mãn hệ ràng buộc OCL.

Phương pháp nghiên cứu thực tế và nguồn dữ liệu

Phương pháp nghiên cứu là tiếp cận kỹ thuật - thực nghiệm trong kỹ nghệ phần mềm. Tác giả tiến hành phân tích miền đặc tả yêu cầu và miền kiểm thử chức năng, thiết kế siêu mô hình, định nghĩa quy tắc biến đổi hình thức, phát triển thuật toán và tích hợp thành bộ công cụ trên nền tảng Eclipse (sử dụng Eclipse Modeling Framework - EMF và Graphical Modeling Framework - GMF) [21].

Dữ liệu thực nghiệm được thu thập và thẩm định qua các hệ thống ca sử dụng mẫu: ca sử dụng "Đăng nhập" trong hệ thống Website trung tâm X, ca sử dụng "Lend book" trong hệ thống quản lý thư viện (Library System), và ca sử dụng "Withdraw" trong hệ thống máy rút tiền tự động (ATM System).

---

Nội dung chính theo từng chương

Chương 1: Mở đầu

Chương 1 thiết lập bối cảnh nghiên cứu về thực trạng phát triển phần mềm và tầm quan trọng của hoạt động kiểm thử (chiếm 30-60% chi phí dự án). Tác giả phân tích những hạn chế của các công cụ kiểm thử hiện nay khi chỉ tập trung vào khâu thực thi, trong khi khâu sinh ca kiểm thử tự động từ đặc tả yêu cầu chưa được giải quyết triệt để. Chương này làm rõ 4 thách thức nghiên cứu chính, xác định mục tiêu đưa mô hình ca sử dụng trở thành chế tác trung tâm trong quy trình phát triển hướng mô hình (MDD) và kiểm thử dựa trên mô hình (MBT), đồng thời tóm lược 4 đóng góp khoa học và bố cục 6 chương của luận án.

Chương 2: Kiến thức cơ sở

Chương 2 tổng hợp hệ thống lý thuyết nền tảng cho toàn bộ luận án, bao gồm:

• Các khái niệm kiểm thử phần mềm: lỗi phần mềm, kiểm thử động, kiểm thử tĩnh, oracle, ca kiểm thử, kịch bản kiểm thử, dữ liệu kiểm thử, kết quả mong đợi [5, 49]. Phân tích các mức kiểm thử trong mô hình chữ V [50, 64] và 5 bước của quy trình MBT [9].
• Tiêu chí phủ kiểm thử và mô hình lỗi: phân tích chi tiết lỗi điểm quyết định, lỗi vòng lặp và lỗi đồng bộ hóa. Trình bày chi tiết tiêu chí phủ đường cơ bản [41] và tiêu chí phủ đường hoạt động [39], cùng phương pháp tính độ phức tạp Cyclomatic $V(G)$ [33].
• Đặc tả ca sử dụng truyền thống: cấu trúc mẫu đặc tả ca sử dụng (Bảng 2.1), quy trình 3 bước xác định ca kiểm thử thủ công từ ca sử dụng thông qua ví dụ ca sử dụng Đăng nhập (Bảng 2.2 đến 2.4).
• Kỹ thuật mô hình hóa chuyên biệt miền (DSM): các bước xây dựng DSML, vai trò của siêu mô hình, khung phát triển EMF và GMF trong môi trường Eclipse [21, 35, 62].
• Ngôn ngữ chuyển đổi mô hình và OCL: nguyên lý chuyển đổi M2M qua ngôn ngữ ATL [32], chuyển đổi M2T dựa trên mẫu qua ngôn ngữ Acceleo [22, 30], và cú pháp, ngữ nghĩa của ngôn ngữ ràng buộc OCL [10, 74].

Tiêu chí so sánh	Phủ đường cơ bản (Basic Path Coverage) [41]	Phủ đường hoạt động (Activity Path Coverage) [39]
Xử lý vòng lặp	Thực hiện vòng lặp tối đa 1 lần	Kiểm tra 0 và 1 lần (while-do); 1 và 2 lần (do-while)
Hành động đồng thời	Không định nghĩa thứ tự đồng bộ cụ thể	Đóng gói theo chiều rộng (BFS), bảo đảm thứ tự ưu tiên
Mô hình lỗi bao phủ	Lỗi nhánh cơ bản	Lỗi điểm quyết định, lỗi vòng lặp, lỗi đồng bộ hóa
Ứng dụng trong luận án	Nền tảng so sánh ban đầu	Tiêu chí chính để sinh kịch bản trong USLTG

Chương 3: Đặc tả ca sử dụng theo hướng mô hình hóa chuyên biệt miền

Chương 3 đề xuất ngôn ngữ đặc tả ca sử dụng chuyên biệt miền USL (Use Case Specification Language):

• Phân tích miền: xác định các khái niệm cốt lõi trong ngữ cảnh đặc tả ca sử dụng, bao gồm tác nhân (Actor), ca sử dụng (UseCase), luồng sự kiện (Flow of Events), bước thực hiện (Step), bước người dùng (UserStep), bước hệ thống (SystemStep), điểm quyết định (Decision), điểm ghép (Merge), điểm phân nhánh (Fork), điểm nối (Join), điều kiện gác (GuardCondition), và biến đầu vào/đầu ra.
• Cú pháp USL: Cú pháp trừu tượng được định nghĩa bằng một siêu mô hình (USL metamodel). Tập luật hợp lệ được đặc tả bằng OCL để bảo đảm tính đúng đắn của mô hình (như tính liên tục của luồng điều khiển, tính duy nhất của tên bước, tính hợp lệ của điểm kết thúc). Cú pháp cụ thể cung cấp các ký pháp đồ họa trực quan (Bảng 3.2).
• Ngữ nghĩa hình thức: Ánh xạ các khái niệm của mô hình USL sang Hệ thống chuyển trạng thái được gán nhãn (LTS) thông qua danh sách các hàm toán học trong miền $D$ (Bảng 3.3 và 3.4), cung cấp ngữ nghĩa thực thi chính xác cho mô hình.
• Khả năng chuyển đổi: Trình bày tiềm năng chuyển đổi mô hình USL sang các chế tác khác trong MDD, bao gồm mô hình kiểm thử, mô hình cấu trúc (biểu đồ lớp), mô hình hành vi (biểu đồ tuần tự), và sinh tự động tài liệu đặc tả ca sử dụng dạng văn bản theo mẫu TUCD thông qua bộ chuyển USL2TUCD.

Chương 4: Phương pháp sinh tự động các ca kiểm thử từ mô hình ca sử dụng và mô hình khái niệm miền của hệ thống

Chương 4 trình bày giải pháp cốt lõi của luận án:

• Đề xuất ngôn ngữ TCSL (Test Case Specification Language): Xây dựng siêu mô hình TCSL để đặc tả ca kiểm thử chức năng mức hệ thống. Siêu mô hình TCSL bao gồm các phần tử: bộ kiểm thử (TestSuite), ca kiểm thử (TestCase), bước kiểm thử (TestStep), hành động (Action), đối tượng tác động (TargetObject), kiểu điểm kiểm tra (CheckpointType: UI, Data, Message), dữ liệu đầu vào (InputData), dữ liệu đầu ra mong đợi (ExpectedOutput), tiền điều kiện (PreCondition), hậu điều kiện (PostCondition), và trạng thái bên trong hệ thống (InternalState).
• Quy trình phương pháp USLTG: Chuyển đổi từ mô hình USL và biểu đồ lớp khái niệm miền sang mô hình TCSL qua 4 giai đoạn:
  1. Xác định tiêu chí phủ: Áp dụng tiêu chí phủ đường hoạt động để xác định không gian các đường thực thi.
  2. Sinh kịch bản và ràng buộc: Sử dụng thủ tục GenerateScenarios để duyệt mô hình USL, trích xuất danh sách các kịch bản kiểm thử kèm theo tập hợp các điều kiện gác và ràng buộc OCL tương ứng.
  3. Sinh bộ dữ liệu đầu vào kiểm thử: Áp dụng thuật toán GenTestInputData, kết hợp mô hình lớp khái niệm miền, biểu diễn các ràng buộc dưới dạng tệp đặc tả USE (CONF, INVS, OMpartial). Sử dụng công cụ USE để giải ràng buộc, tìm snapshot thỏa mãn nhằm sinh ra dữ liệu cụ thể và trạng thái hệ thống ban đầu (EV objects).
  4. Sinh mô hình TCSL: Sử dụng thuật toán GenTCSLModel để tổng hợp các bước kiểm thử, dữ liệu đầu vào, kết quả mong đợi và trạng thái hệ thống thành mô hình TCSL hoàn chỉnh, lưu trữ dưới định dạng XML.

                    Quy trình Phương pháp USLTG (Chương 4)
+----------------+      +-------------------+
| Mô hình USL    |      | Domain Class Model|
+--------+-------+      +---------+---------+
         v                        v
+---------------------------------------------------+
| 1. Thủ tục GenerateScenarios                      |
|    - Trích xuất kịch bản (Activity Path Coverage) |
|    - Thu thập điều kiện gác & ràng buộc OCL       |
+-------------------------+-------------------------+
                          v
+---------------------------------------------------+
| 2. Thuật toán GenTestInputData                    |
|    - Chuyển ràng buộc sang tệp cấu hình USE       |
|    - Bộ giải USE tìm Snapshots                    |
|    - Xác định dữ liệu cụ thể & Trạng thái (EV)    |
+-------------------------+-------------------------+
                          v
+---------------------------------------------------+
| 3. Thuật toán GenTCSLModel                        |
|    - Ghép bước kiểm thử, Checkpoints, Data, State |
|    - Xuất mô hình ca kiểm thử TCSL (XML)          |
+---------------------------------------------------+

Chương 5: Thực nghiệm và đánh giá

Chương 5 trình bày việc hiện thực hóa và đánh giá thực nghiệm:

• Bộ công cụ hỗ trợ USL: Phát triển trên nền tảng Eclipse dưới dạng các plugin, gồm trình soạn thảo đồ họa USL (xây dựng bằng GMF) và bộ sinh USLTG (xây dựng bằng Acceleo và Java tích hợp USE).
• Ví dụ minh họa: Áp dụng công cụ trên hai ca sử dụng thực tế là "Withdraw" trong hệ thống ATM (Bảng 5.1, 5.2, 5.3 và tệp XML mô hình TCSL) và "Lend book" trong hệ thống Library (Bảng 5.4). Kết quả minh chứng công cụ sinh đầy đủ các kịch bản, dữ liệu đầu vào hợp lệ/không hợp lệ và trạng thái đối tượng liên kết trong cơ sở dữ liệu.
• Đánh giá và so sánh ngôn ngữ USL: So sánh khả năng diễn đạt của USL với các ngôn ngữ đặc tả khác (Bảng 5.5) trên các tiêu chí: cú pháp trừu tượng, cú pháp cụ thể, luật hợp lệ, ngữ nghĩa hình thức, khả năng tích hợp MDD.
• Đánh giá và so sánh phương pháp USLTG: So sánh số lượng kịch bản sinh ra (Bảng 5.6) và mức độ chi tiết của thông tin kiểm thử được xác định (Bảng 5.7) giữa USLTG với các công trình của Wang và cộng sự [73], Sinha và cộng sự [58], Smialek và cộng sự [65], Hartmann và cộng sự [24].

Tiêu chí so sánh	Phương pháp NLP (RUCM [73], Sinha [58])	Phương pháp UML (Hartmann [24], Shen [51])	Phương pháp DSL (RSL/TSL [65])	Phương pháp USLTG (Luận án đề xuất)
Ngôn ngữ nguồn	Văn bản có cấu trúc hạn chế (RNL)	Biểu đồ hoạt động / Biểu đồ tuần tự	Ngôn ngữ yêu cầu RSL	Ngôn ngữ mô hình hóa USL
Cú pháp hình thức	Không (Informal)	Có (Chuẩn UML)	Có (DSML)	Có (DSML với luật OCL & ngữ nghĩa LTS)
Ngôn ngữ đích	Bảng kịch bản / Test cases văn bản	Kịch bản kiểm thử trừu tượng	Ngôn ngữ đặc tả TSL	Ngôn ngữ ca kiểm thử TCSL
Dữ liệu kiểm thử	Mô tả văn bản hoặc phân lớp	Trừu tượng (không có giá trị cụ thể)	Biểu thức mô tả điều kiện	Giá trị dữ liệu cụ thể (sinh từ USE Solver)
Trạng thái hệ thống	Không xác định	Không xác định	Không xác định	Có (Xác định các đối tượng trạng thái EV)
Chi tiết bước kiểm	Bước thực hiện chung	Bước hành động	Bước kiểm thử	Bước, kiểu bước, đối tượng, hành động, checkpoint

Chương 6: Kết luận và hướng phát triển

Chương 6 tổng kết các kết quả đạt được về mặt lý thuyết, phương pháp luận và công cụ cài đặt; khẳng định luận án đã hoàn thành mục tiêu đề ra về tự động hóa sinh ca kiểm thử chức năng từ ca sử dụng; đồng thời chỉ ra các định hướng nghiên cứu tiếp theo.

---

Kết quả và những đóng góp mới

Luận án đã đạt được bốn đóng góp khoa học và thực tiễn chính:

1. Đề xuất ngôn ngữ đặc tả ca sử dụng USL (Use Case Specification Language): Ngôn ngữ được xây dựng theo phương pháp mô hình hóa chuyên biệt miền, sở hữu cú pháp trừu tượng (siêu mô hình EMF), cú pháp cụ thể dạng đồ họa, hệ thống luật ràng buộc hợp lệ bằng OCL và ngữ nghĩa hình thức ánh xạ sang hệ thống chuyển trạng thái được gán nhãn (LTS). USL cho phép đặc tả đầy đủ thông tin cấu trúc, hành vi và các ràng buộc dữ liệu của ca sử dụng, đóng vai trò chế tác trung tâm trong phát triển phần mềm hướng mô hình.
2. Đề xuất ngôn ngữ đặc tả ca kiểm thử TCSL (Test Case Specification Language): Cung cấp một ngôn ngữ chuyên biệt miền với siêu mô hình hoàn chỉnh để đặc tả ca kiểm thử chức năng mức hệ thống. TCSL mô tả chi tiết các thành phần: bước kiểm thử, kiểu bước, đối tượng đích, hành động, loại điểm kiểm tra (UI, Data, Message), dữ liệu đầu vào cụ thể, kết quả mong đợi, cùng trạng thái bên trong của hệ thống trước khi thực thi.
3. Đề xuất phương pháp sinh ca kiểm thử tự động USLTG (USL-based Test Generation): Thiết lập quy trình chuyển đổi tự động từ mô hình USL và mô hình lớp khái niệm miền sang mô hình TCSL. Phương pháp tích hợp tiêu chí phủ đường hoạt động (xử lý vòng lặp và hành động đồng thời), thuật toán trích xuất kịch bản (GenerateScenarios), thuật toán sinh dữ liệu kiểm thử cụ thể và trạng thái hệ thống bằng cách giải ràng buộc OCL qua công cụ USE (GenTestInputData), và thuật toán tổng hợp mô hình TCSL (GenTCSLModel).
4. Xây dựng bộ công cụ hỗ trợ USL và đánh giá thực nghiệm: Cài đặt hoàn chỉnh bộ công cụ trên nền tảng Eclipse, bao gồm trình soạn thảo đồ họa cho USL và các bộ sinh tự động (USL2TUCD sinh tài liệu đặc tả ca sử dụng theo mẫu, USLTG sinh mô hình ca kiểm thử TCSL). Các thực nghiệm trên các hệ thống mẫu (ATM, Library) và các phân tích so sánh đã chứng minh tính khả thi, tính đúng đắn và ưu thế của phương pháp.

Về mặt kiến nghị và giải pháp ứng dụng, luận án đề xuất tích hợp ngôn ngữ USL và phương pháp USLTG vào quy trình phát triển phần mềm hướng mô hình tại các tổ chức công nghệ, nhằm giảm chi phí thiết kế kiểm thử thủ công, nâng cao độ tin cậy và tạo điều kiện tự động hóa hoàn toàn từ khâu đặc tả yêu cầu đến khâu sinh kịch bản thực thi kiểm thử.

---

Hạn chế và hướng nghiên cứu tiếp

Căn cứ theo các nội dung được trình bày trong luận án, các hạn chế và định hướng phát triển được xác định như sau:

• Hạn chế:
  • Phạm vi kiểm thử tập trung vào kiểm thử chức năng mức hệ thống từ ca sử dụng, chưa bao quát các thuộc tính phi chức năng (hiệu năng, độ tin cậy, an toàn bảo mật).
  • Khâu sinh dữ liệu kiểm thử cụ thể phụ thuộc vào hiệu năng và khả năng tìm kiếm snapshot của công cụ giải ràng buộc USE đối với các hệ thống có miền dữ liệu và ràng buộc OCL quy mô lớn.
• Hướng nghiên cứu tiếp:
  • Nghiên cứu mở rộng các bộ sinh chuyển đổi từ mô hình USL sang các mô hình cấu trúc (biểu đồ lớp chi tiết) và mô hình hành vi khác (biểu đồ tuần tự, biểu đồ hoạt động UML) nhằm hoàn thiện quy trình phát triển hướng mô hình (MDD).
  • Phát triển các bộ sinh chuyển đổi từ mô hình ca kiểm thử TCSL sang các tập lệnh thực thi kiểm thử tự động (Test Scripts) tương thích với các khung kiểm thử tự động phổ biến (như Keyword-Driven Testing Framework - KDTF, Selenium, JUnit).
  • Cải tiến và tối ưu hóa thuật toán giải ràng buộc dữ liệu để nâng cao khả năng mở rộng trên các hệ thống phần mềm công nghiệp có độ phức tạp cao.

---

Giá trị tham khảo

Luận án là tài liệu tham khảo chuyên sâu cho các đối tượng sau:

• Nghiên cứu sinh, học viên cao học và giảng viên ngành Công nghệ phần mềm / Khoa học máy tính: Tham khảo phương pháp luận xây dựng ngôn ngữ chuyên biệt miền (DSML), kỹ thuật định nghĩa siêu mô hình trên Eclipse EMF/GMF, cách thiết lập ngữ nghĩa hình thức LTS cho ngôn ngữ mô hình hóa, và kỹ thuật giải ràng buộc OCL trong kiểm thử phần mềm.
• Kỹ sư kiểm thử phần mềm (QA/QC Engineers) và Chuyên viên tự động hóa kiểm thử: Tham khảo cấu trúc mô hình ca kiểm thử hình thức trong TCSL, nguyên lý bao phủ đường hoạt động (Activity Path Coverage) để bao phủ lỗi vòng lặp và lỗi đồng bộ hóa, cùng cơ chế tự động xác định trạng thái hệ thống trước kiểm thử.
• Chuyên viên phân tích nghiệp vụ (Business Analysts) và Kiến trúc sư phần mềm (Software Architects): Tham khảo cách tiếp cận của ngôn ngữ USL để chuẩn hóa tài liệu đặc tả yêu cầu chức năng, kết nối tài liệu ca sử dụng với quy trình phát triển hướng mô hình (MDD) nhằm tự động sinh các chế tác phần mềm liên quan.

Các phần đáng tham khảo nhất trong luận án gồm: Siêu mô hình và tập luật OCL của USL (Chương 3), Siêu mô hình TCSL và các thuật toán chuyển đổi mô hình GenerateScenarios, GenTestInputData, GenTCSLModel (Chương 4), cùng cấu trúc bộ công cụ hỗ trợ trên Eclipse (Chương 5).

---

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

1. Ngôn ngữ USL giải quyết hạn chế gì của các phương pháp đặc tả ca sử dụng bằng ngôn ngữ tự nhiên và biểu đồ UML chuẩn?

Đặc tả ca sử dụng bằng ngôn ngữ tự nhiên (dù có cấu trúc hạn chế như RUCM) thiếu cú pháp trừu tượng hình thức, phụ thuộc vào kỹ thuật NLP vốn phức tạp và khó trích xuất chính xác các ràng buộc logic. Trong khi đó, các biểu đồ UML chuẩn (Activity, Sequence Diagram) chỉ phân biệt được luồng hành động giữa tác nhân và hệ thống để tạo kịch bản trừu tượng, không chứa đủ thông tin để sinh dữ liệu kiểm thử cụ thể. USL khắc phục điều này bằng cách cung cấp một DSML có siêu mô hình chặt chẽ, ràng buộc OCL đầy đủ, ký pháp đồ họa trực quan và ngữ nghĩa hình thức dựa trên LTS, cho phép biểu diễn đầy đủ thông tin cấu trúc, hành vi và ràng buộc phục vụ sinh tự động cả kịch bản lẫn dữ liệu kiểm thử.

2. Ngôn ngữ đặc tả ca kiểm thử TCSL có điểm gì khác biệt so với ngôn ngữ TSL và các đặc tả kiểm thử trước đây?

Các ngôn ngữ đặc tả kiểm thử trước đây (như TSL trong nghiên cứu của Smialek) chỉ đặc tả chuỗi bước kiểm thử và mô tả dữ liệu dưới dạng các biểu thức điều kiện trừu tượng. TCSL mở rộng và chi tiết hóa mô hình ca kiểm thử bằng cách bổ sung: kiểu bước kiểm thử, hành động cụ thể, đối tượng kiểm thử mục tiêu, loại điểm kiểm tra (Checkpoint Type: UI, Data, Message), dữ liệu đầu vào cụ thể, kết quả mong đợi xác định và đặc biệt là trạng thái bên trong của hệ thống (Internal State) trước khi thực thi ca kiểm thử.

3. Phương pháp USLTG sử dụng tiêu chí bao phủ nào và cơ chế sinh dữ liệu kiểm thử cụ thể hoạt động ra sao?

Phương pháp USLTG áp dụng Tiêu chí phủ đường hoạt động (Activity Path Coverage Criterion) của Chen và cộng sự [39] để bao phủ lỗi điểm quyết định, lỗi vòng lặp (kiểm tra 0 và 1 lần với while-do, 1 và 2 lần với do-while) và lỗi đồng bộ hóa trong các nhánh đồng thời. Cơ chế sinh dữ liệu cụ thể được thực hiện qua thuật toán GenTestInputData: hệ thống chuyển đổi các điều kiện gác và ràng buộc OCL từ kịch bản ca sử dụng cùng mô hình lớp khái niệm miền sang tệp cấu hình của công cụ USE; công cụ USE đóng vai trò solver để tìm kiếm các snapshot đối tượng thỏa mãn, từ đó trích xuất các giá trị dữ liệu cụ thể và trạng thái đối tượng hệ thống ban đầu.

4. Bộ công cụ hỗ trợ USL được phát triển trên nền tảng công nghệ nào và gồm những thành phần chức năng nào?

Bộ công cụ hỗ trợ USL được phát triển trên nền tảng Eclipse, sử dụng Eclipse Modeling Framework (EMF) để quản lý siêu mô hình, Graphical Modeling Framework (GMF) để xây dựng trình soạn thảo mô hình USL trực quan, và Acceleo kết hợp Java để cài đặt các bộ chuyển đổi mô hình. Bộ công cụ gồm hai thành phần chính: (1) Trình soạn thảo đồ họa cho phép người dùng xây dựng và kiểm tra tính hợp lệ của mô hình USL; (2) Các bộ sinh tự động, gồm bộ sinh USL2TUCD (chuyển mô hình USL sang tài liệu ca sử dụng theo mẫu trong ngôn ngữ tự nhiên) và bộ sinh USLTG (chuyển mô hình USL và mô hình miền sang mô hình ca kiểm thử TCSL dưới dạng tệp XML).

5. Độ phức tạp Cyclomatic $V(G)$ có vai trò gì trong việc kiểm soát số lượng ca kiểm thử sinh ra?

Độ phức tạp Cyclomatic $V(G)$ của McCabe được tính theo công thức $V(G) = E - N + 2$ hoặc $V(G) = P + 1$ (với $E$ là số cạnh, $N$ là số nút, $P$ là số điểm quyết định nhị phân trong đồ thị hoạt động). Độ đo này cung cấp cơ sở toán học để xác định cận trên của số lượng ca kiểm thử cần thiết nhằm đạt độ bao phủ nhánh, đồng thời là cận dưới cho tổng số đường thực thi có thể có trong mô hình. Nhờ đó, phương pháp bảo đảm số lượng ca kiểm thử sinh ra là tối thiểu nhưng vẫn bảo đảm khả năng phát hiện lỗi tối đa theo tiêu chí phủ.

---

Kết luận

Luận án "Kiểm thử dựa trên mô hình với cách tiếp cận mô hình hóa chuyên biệt miền" đã giải quyết bài toán sinh tự động ca kiểm thử chức năng mức hệ thống từ đặc tả yêu cầu ca sử dụng. Bằng việc đề xuất ngôn ngữ đặc tả ca sử dụng USL, ngôn ngữ đặc tả ca kiểm thử TCSL, phương pháp chuyển đổi USLTG dựa trên giải ràng buộc OCL và tiêu chí phủ đường hoạt động, nghiên cứu đã khắc phục các hạn chế về thiếu dữ liệu cụ thể và thiếu trạng thái hệ thống của các hướng tiếp cận trước. Bộ công cụ hỗ trợ được cài đặt trên nền tảng Eclipse đã chứng minh tính khả thi và hiệu quả thực nghiệm của phương pháp, mở ra khả năng tích hợp ca sử dụng làm chế tác trung tâm trong quy trình kỹ nghệ phát triển phần mềm hướng mô hình.

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

Mở đầu, Mục 2.1 sẽ làm rõ các khái niệm trong kiểm thử phần mềm, ca sử dụng, và phương pháp xác định các ca kiểm thử từ các ca sử dụng. Các mục tiếp theo, luận án sẽ lần lượt mô tả về mô hình hóa chuyên biệt miền (Domain-Specific Modeling - DSM ), ngôn ngữ chuyển mô hình (model transformation language), và ngôn ngữ ràng buộc đối tượng OCL.1 Kiểm thử dựa trên ca sử dụng Phần này, luận án sẽ trình bày các kiến thức nền trong kiểm thử phần mềm, ca sử dụng, và kiểm thử dựa trên ca sử dụng. Các kiến thức này được luận án tìm hiểu khi nghiên cứu bài toán kiểm thử chức năng từ ca sử dụng.1 Kiểm thử phần mềm 2.1 Các khái niệm cơ bản Lỗi phần mềm là một khiếm khuyết trong một thành phần hoặc hệ thống mà nó có thể làm cho thành phần hoặc hệ thống này không thực hiện đúng chức năng yêu cầu của nó, ví dụ như thông báo sai hoặc định nghĩa dữ liệu không đúng [5]. Kiến thức cơ sở 12 Kiểm thử (Testing) là một quy trình thực hiện một chương trình với ý định tìm kiếm các lỗi.

Kiểm thử phần mềm bao gồm việc kiểm chứng động các hành vi của một chương trình trên một tập hữu hạn các ca kiểm thử (test case). Các ca kiểm thử được lựa chọn phù hợp từ các miền thực thi thường là vô hạn để có được hành vi được mong đợi [49]. Kiểm thử tĩnh (Static Testing) là hoạt động kiểm tra mà không thực hiện chương trình. Hoạt động này bao gồm kiểm tra phần mềm và một số dạng của phân tích [5].

Kiểm thử động (Dynamic Testing) là thực hiện chương trình với các giá trị đầu vào xác định để tìm các lỗi trong các hành vi của chương trình [5]. Hầu hết các tài liệu sử dụng thuật ngữ kiểm thử để chỉ kiểm thử động và kiểm thử tĩnh được gọi là hoạt động xác minh. Khi thực thi kiểm thử, việc kiểm thử toàn diện chương trình thực tế là không thể thực hiện được. Bởi vì, mỗi hoạt động trong chương trình thường có một số lượng lớn các dữ liệu đầu vào thỏa mãn.

Vì vậy khi kiểm thử, kiểm thử viên cần chọn một số lượng các ca kiểm thử đủ nhỏ để có thể thực thi các kiểm thử trong thời gian giới hạn. Vậy làm thế nào để chọn được các ca kiểm thử có nhiều khả năng để lộ thất bại trong hệ thống. Khi đó, một số chiến lược sẽ được áp dụng để xác định tập các đầu vào cho ca kiểm thử như phân lớp tương đương, kiểm thử giá trị biên. Sau mỗi lần thực hiện kiểm thử, chúng ta phải quyết định hành vi được quan sát của hệ thống là một thất bại hay không.

Vấn đề này được gọi là một lời tiên tri (oracle). Vấn đề oracle thường được giải quyết thông qua kiểm tra thủ công đầu ra thực tế. Nhưng để kiểm thử lặp lại và hiệu quả, oracle cần được tự động hóa. Ca kiểm thử (Test case) là tập của các dữ liệu kiểm thử (test data), các điều kiện thực hiện (pre-condition), các bước kiểm thử (test steps), và các kết quả đầu ra mong đợi (expected output) được phát triển cho một kịch bản kiểm thử (test scenario) cụ thể để kiểm chứng sự tuân thủ một yêu cầu kiểm thử xác định.

Một ca kiểm thử định nghĩa một thử nghiệm đơn lẻ sẽ được thực hiện để đạt được mục tiêu kiểm thử phần mềm cụ thể, chẳng hạn như đi qua một đường thực thi của chương trình cụ thể hoặc kiểm chứng tuân thủ một yêu cầu cụ thể [5]. Dữ liệu kiểm thử là tập các giá trị thực (thỏa mãn tiêu chí bao phủ dữ Chương 2. Kiến thức cơ sở 13 liệu đã chọn) được xác định chỉ rõ là đầu vào để thực hiện các ca kiểm thử trong quá trình kiểm thử [5]. Đầu ra mong đợi là các kết quả dự kiến sẽ được tạo ra khi thực hiện kiểm thử.

Chương trình thỏa mãn khi và chỉ khi đầu ra thực tế thỏa mãn đầu ra mong đợi của kiểm thử [5]. Các bước kiểm thử mô tả các bước thực hiện và kiểm tra kết quả đầu ra của hệ thống [5]. Các điều kiện thực hiện là các điều kiện cần thỏa mãn để ca kiểm thử được thực hiện [5]. Kịch bản kiểm thử (Test scenario) là một ca kiểm thử trừu tượng và nó thường bao gồm nhiều ca kiểm thử liên quan nhau.

Một kịch bản kiểm thử mô tả một thủ tục thực hiện kiểm thử bao gồm một tập các bước kiểm thử (test step). Mục đích của kịch bản kiểm thử là kiểm tra việc thực hiện chức năng từ đầu đến cuối của một chức năng phần mềm và đảm bảo luồng logic đang hoạt động là đúng. Với mỗi kịch bản kiểm thử, kiểm thử viên có thể xác định được một hoặc nhiều bộ dữ liệu kiểm thử thỏa mãn kịch bản kiểm thử. Một ca kiểm thử là sự kết hợp của một kịch bản kiểm thử với một bộ dữ liệu kiểm thử thỏa mãn kịch bản [5].2 Kỹ thuật kiểm thử Một hoạt động quan trọng trong kiểm thử phần mềm là thiết kế các ca kiểm thử.

Một quy trình phát triển phần mềm tạo ra một lượng lớn thông tin như đặc tả yêu cầu, tài liệu thiết kế và mã nguồn. Để tạo các ca kiểm thử hiệu quả với chi phí thấp, các nhà thiết kế kiểm thử sẽ phân tích một số nguồn thông tin như các đặc tả yêu cầu và đặc tả chức năng (requirements and functional specifications), mã nguồn, các miền đầu vào và đầu ra (input and output domains), hồ sơ hoạt động (operational profile), và mô hình lỗi. Tất cả các nguồn thông tin này cung cấp các thông tin bổ sung cho các nhà thiết kế kiểm thử. Dựa trên nguồn thông tin cho thiết kế kiểm thử, kỹ thuật kiểm thử được chia thành hai kỹ thuật chính là kiểm thử hộp trắng (white box testing) và kiểm thử hộp đen (black box testing) như được định nghĩa trong [5].

Kiến thức cơ sở 14 Kiểm thử hộp đen là kỹ thuật kiểm thử mà các ca kiểm thử được xác định từ các mô tả bên ngoài của phần mềm, bao gồm các đặc tả, các yêu cầu, và thiết kế. Kiểm thử hộp trắng là kỹ thuật kiểm thử mà các ca kiểm thử được xác định từ mã nguồn bên trong của phần mềm, đặc biệt bao gồm các nhánh, các điều kiện riêng, và các câu lệnh.3 Các mức trong kiểm thử phần mềm Kiểm thử được thực hiện tại các mức khác nhau liên quan tới các hoạt động phát triển phần mềm.1 là mô hình chữ V (V model), mô hình minh họa các mức kiểm thử và các hoạt động phát triển phần mềm. Các mức kiểm thử được trình bày trong [50, 64] gồm có kiểm thử đơn vị, kiểm thử tích hợp, kiểm thử hệ thống, và kiểm thử chấp nhận. Các ca kiểm thử của các mức kiểm thử này sẽ được thiết kế dựa vào các chế tác tương ứng trong các quy trình khác nhau trong phát triển phần mềm.

Sau khi có mã chương trình, các mức kiểm thử khác nhau sẽ lần lượt được thực hiện. Trong kiểm thử đơn vị (Unit testing), các lập trình viên kiểm thử riêng lẻ các đơn vị chương trình như các hàm, thủ tục, phương thức, hoặc lớp một cách độc lập. Sau khi chắc chắn các đơn vị riêng lẻ làm việc thỏa mãn, các mô-đun được lắp ráp để xây dựng các hệ thống con lớn hơn bằng cách thực hiện các kỹ thuật kiểm tra tích hợp.1: Các pha kiểm thử và phát triển trong mô hình chữ V [50]. Kiến thức cơ sở 15 Kiểm thử tích hợp (Integration testing) được thực hiện bởi các nhà phát triển phần mềm và các kỹ sư kiểm thử tích hợp.

Mục tiêu của kiểm thử tích hợp là để xây dựng một hệ thống thỏa mãn ổn định có thể chịu được sự nghiêm ngặt của việc kiểm thử mức hệ thống. Kiểm thử mức hệ thống (System testing) gồm một phổ rộng các kiểm thử như kiểm thử chức năng (functionality testing), kiểm thử độ bền (ro- buntness), kiểm thử bảo mật (security testing), kiểm thử tải (load testing), kiểm thử hiệu năng (performamce testing), kiểm thử độ tin cậy (reliability testing), kiểm thử ổn đinh (stability), kiểm thử quá tải (stress testing). Kiểm thử mức hệ thống là một pha quan trọng trong quy trình phát triển phần mềm vì cần phải đáp ứng một kế hoạch chặt chẽ gần ngày chuyển giao, để khám phá hầu hết các lỗi, và kiểm chứng sản phẩm đang làm việc và không dẫn đến các lỗi mới. Kiểm thử hệ thống gồm các hoạt động phân biệt như tạo một kế hoạch kiểm thử (test plan), thiết kế một bộ kiểm thử (test suite), chuẩn bị môi trường kiểm thử, thực hiện các kiểm thử theo một chiến lược rõ ràng và giám sát quy trình thực hiện kiểm thử.

Sau khi hoàn thành việc kiểm thử mức hệ thống, sản phẩm sẽ được chuyển giao đến khách hàng. Khách hàng sẽ thực hiện một loạt các kiểm thử của họ, thường biết đến như là kiểm thử chấp nhận (acceptance testing).4 Kiểm thử dựa trên mô hình Kiểm thử dựa trên mô hình (Model-Based Testing - MBT) là một kỹ thuật kiểm thử với mục đích để sinh các ca kiểm thử tự động từ mô hình đặc tả các khía cạnh liên quan của hành vi hệ thống cần kiểm thử (System Under Testing - SUT ). Mô hình mô tả hệ thống cần kiểm thử từ góc nhìn của những vấn đề cần được kiểm thử. Ví dụ, một mô hình luồng điều khiển (control flow) của một phương thức sẽ mô hình khía cạnh luồng điều khiển đi qua các câu lệnh thực hiện của phương thức [56].

Cụ thể, thay vì thiết kế hàng trăm ca kiểm thử thủ công thì người thiết kế kiểm thử xây dựng mô hình trừu tượng của SUT, sau đó công cụ kiểm thử dựa trên mô hình sinh ra một tập các ca kiểm thử từ mô hình đó. Toàn bộ thời gian thiết kế kiểm thử được giảm xuống, và ưu điểm nữa là có thể sinh ra một loạt các tập ca kiểm thử khác nhau từ cùng một mô hình bằng việc sử dụng các tiêu Chương 2. Kiến thức cơ sở 16 chí lựa chọn kiểm thử khác nhau [9].2 thể hiện năm bước chính của quy trình kiểm thử dựa trên mô hình.2: Quy trình kiểm thử dựa trên mô hình [9]. Bước 1 Mô hình hóa: Người tạo mô hình sẽ tạo ra các mô hình cho hệ thống cần kiểm thử hoặc môi trường của hệ thống cần kiểm thử.

Sau khi mô hình được tạo ra, các mô hình cần được kiểm tra để đảm bảo tính nhất quán và có được các hành vi mong muốn.