Luận án về kiểm thử dựa trên mô hình và phương pháp mô hình hóa chuyên biệt miền

Kiểm thử phần mềm là một hoạt động thiết yếu trong quy trình phát triển phần mềm, nhằm đảm bảo chất lượng sản phẩm. 147 trang.

• Trường học: Trường Đại Học
• Chuyên ngành: Kiểm Thử Phần Mềm
• Đề tài: Kiểm Thử Dựa Trên Mô Hình Với Phương Pháp Mô Hình Hóa Chuyên Biệt
• Loại tài liệu: Luận Án

Mục lục chi tiết

• 1. CHƯƠNG 1: MỞ ĐẦU
• 1.1. Đặt vấn đề
• 1.2. Mục tiêu nghiên cứu và các đóng góp chính của luận án
• 1.3. Cấu trúc luận án
• 2. CHƯƠNG 2: KIẾN THỨC NỀN
• 3. CHƯƠNG 3: NGÔN NGỮ ĐẶC TẢ CHUYÊN BIỆT MIỀN CHO CA SỬ DỤNG
• 4. CHƯƠNG 4: PHƯƠNG PHÁP SINH TỰ ĐỘNG CÁC CA KIỂM THỬ CHỨC NĂNG
• 5. CHƯƠNG 5: CÔNG CỤ HỖ TRỢ VÀ ĐÁNH GIÁ PHƯƠNG PHÁP

Tóm tắt

I. Giới thiệu về kiểm thử dựa trên mô hình

Kiểm thử phần mềm là một hoạt động thiết yếu trong quy trình phát triển phần mềm, nhằm đảm bảo chất lượng sản phẩm. Kiểm thử dựa trên mô hình (Model-Based Testing - MBT) đã nổi lên như một phương pháp hiệu quả, giúp tự động hóa không chỉ trong thực thi kiểm thử mà còn trong việc sinh các ca kiểm thử. MBT cho phép cập nhật tự động bộ kiểm thử khi có sự thay đổi trong yêu cầu phần mềm, từ đó giảm thiểu thời gian và công sức cho các kiểm thử viên. Theo nghiên cứu, MBT có thể giảm chi phí kiểm thử từ 30-60%, đồng thời nâng cao chất lượng sản phẩm. Việc áp dụng MBT trong thực tế đã cho thấy những lợi ích rõ rệt, đặc biệt trong việc duy trì và mở rộng bộ kiểm thử. Điều này cho thấy tầm quan trọng của việc phát triển các phương pháp và công cụ hỗ trợ cho MBT.

1.1. Lợi ích của kiểm thử dựa trên mô hình

MBT mang lại nhiều lợi ích cho quy trình phát triển phần mềm. Đầu tiên, nó giúp tăng cường tính tự động hóa trong việc sinh và thực thi các ca kiểm thử. Thứ hai, MBT cho phép các kiểm thử viên dễ dàng duy trì và cập nhật bộ kiểm thử khi có sự thay đổi trong yêu cầu phần mềm. Cuối cùng, MBT giúp giảm thiểu số lượng lỗi và sai sót trong quá trình kiểm thử, từ đó nâng cao chất lượng sản phẩm. Các nghiên cứu đã chỉ ra rằng việc áp dụng MBT có thể cải thiện hiệu suất kiểm thử lên đến 50%. Điều này chứng tỏ rằng MBT không chỉ là một phương pháp lý thuyết mà còn có giá trị thực tiễn cao trong ngành công nghiệp phần mềm.

II. Mô hình hóa trong kiểm thử phần mềm

Mô hình hóa là một bước quan trọng trong quy trình kiểm thử dựa trên mô hình. Mô hình hóa hóa phần mềm giúp xác định các yêu cầu chức năng và phi chức năng của hệ thống. Các mô hình này thường được biểu diễn dưới dạng biểu đồ hoặc tài liệu mô tả, giúp các bên liên quan dễ dàng hiểu và sử dụng. Việc sử dụng các ngôn ngữ mô hình hóa chuyên biệt như UML (Unified Modeling Language) cho phép tạo ra các mô hình rõ ràng và chính xác. Tuy nhiên, việc chuyển đổi từ mô hình sang ca kiểm thử vẫn còn nhiều thách thức. Các nghiên cứu đã chỉ ra rằng việc sử dụng ngôn ngữ mô hình hóa chuyên biệt có thể giúp cải thiện khả năng sinh ca kiểm thử tự động, từ đó nâng cao hiệu quả của quy trình kiểm thử.

2.1. Các phương pháp mô hình hóa

Có nhiều phương pháp mô hình hóa khác nhau được áp dụng trong kiểm thử phần mềm. Một trong những phương pháp phổ biến là sử dụng biểu đồ ca sử dụng để mô tả các yêu cầu chức năng. Các biểu đồ này giúp xác định các tác nhân và hành động trong hệ thống, từ đó tạo điều kiện thuận lợi cho việc sinh ca kiểm thử. Ngoài ra, việc sử dụng các ngôn ngữ mô hình hóa chuyên biệt như DSL (Domain-Specific Language) cũng đã được đề xuất để cải thiện khả năng mô hình hóa. Các nghiên cứu cho thấy rằng việc áp dụng các phương pháp mô hình hóa này có thể giúp giảm thiểu sai sót trong quá trình kiểm thử và nâng cao chất lượng sản phẩm.

III. Quy trình kiểm thử dựa trên mô hình

Quy trình kiểm thử dựa trên mô hình bao gồm năm bước chính: (1) mô hình hóa, (2) sinh các ca kiểm thử, (3) sinh các tập lệnh thực thi kiểm thử, (4) thực thi kiểm thử, và (5) phân tích các ca kiểm thử. Mỗi bước trong quy trình này đều có vai trò quan trọng trong việc đảm bảo chất lượng phần mềm. Việc mô hình hóa chính xác các yêu cầu phần mềm là điều kiện tiên quyết để sinh ra các ca kiểm thử hiệu quả. Các công cụ hỗ trợ kiểm thử tự động hiện nay đã giải quyết tốt các bước cuối cùng trong quy trình, tuy nhiên, hai bước đầu tiên vẫn còn nhiều thách thức cần được nghiên cứu và cải tiến.

3.1. Các bước trong quy trình kiểm thử

Mỗi bước trong quy trình kiểm thử dựa trên mô hình đều có những yêu cầu và thách thức riêng. Bước mô hình hóa yêu cầu chức năng cần phải được thực hiện một cách chính xác để đảm bảo rằng các ca kiểm thử được sinh ra sẽ phản ánh đúng các yêu cầu của phần mềm. Bước sinh ca kiểm thử là bước quan trọng nhất, vì nó quyết định đến chất lượng của quá trình kiểm thử. Các nghiên cứu đã chỉ ra rằng việc áp dụng các ngôn ngữ mô hình hóa chuyên biệt có thể giúp cải thiện khả năng sinh ca kiểm thử tự động, từ đó nâng cao hiệu quả của quy trình kiểm thử.

Nội dung chính

Tổng quan luận án

Hoạt động kiểm thử phần mềm (software testing) là khâu quan trọng nhằm bảo đảm chất lượng hệ thống nhưng thường chiếm từ 30% đến 60% tổng thời gian và chi phí phát triển [71]. Trong thực tế, các yêu cầu phần mềm thường xuyên biến động trong suốt vòng đời phát triển, kéo theo nhu cầu kiểm thử hồi quy lớn cùng chi phí bảo trì và tái thực thi bộ kiểm thử rất cao. Mặc dù tự động hóa kiểm thử đã được ứng dụng rộng rãi, thực tế công nghiệp mới chỉ tập trung vào tự động hóa khâu thực thi kiểm thử (test execution), trong khi vấn đề sinh ca kiểm thử tự động (automated test case generation) vẫn chưa được giải quyết triệt để.

Quy trình 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ả quá trình sinh và thực thi ca kiểm thử thông qua năm bước chính: (1) Mô hình hóa, (2) Sinh các ca kiểm thử, (3) Sinh các tập lệnh thực thi kiểm thử (test scripts), (4) Thực thi kiểm thử, và (5) Phân tích các ca kiểm thử [9]. Ba bước cuối đã có nhiều công cụ tự động hóa thương mại và mã nguồn mở giải quyết tốt, nhưng hai bước đầu tiên (mô hình hóa yêu cầu và sinh ca kiểm thử) vẫn là thách thức lớn đối với cộng đồng nghiên cứu. Yêu cầu chức năng thường được đặc tả bằng mô hình ca sử dụng (use case) dưới dạng biểu đồ ca sử dụng và các mô tả văn bản có cấu trúc theo mẫu trong ngôn ngữ tự nhiên [53]. Tuy nhiên, dạng mô tả ngôn ngữ tự nhiên gây khó khăn cho việc nhận dạng và xử lý thông tin tự động, cản trở việc tự động sinh ca kiểm thử và tích hợp vào quy trình phát triển hướng mô hình (Model-Driven Development - MDD).

Luận án xác định bốn thách thức nghiên cứu cụ thể:

1. Thách thức thứ nhất: Cần một ngôn ngữ đặc tả chuyên biệt miền cho phép biểu diễn các thông tin trong ca sử dụng rõ ràng và đủ chi tiết để tích hợp mô hình ca sử dụng vào phương pháp phát triển hướng mô hình, phục vụ sinh tự động ca kiểm thử, mô hình cấu trúc, mô hình hành vi và tài liệu hóa.
2. Thách thức thứ hai: Cần một phương pháp sinh tự động các ca kiểm thử chứa đầy đủ các thông tin cần thiết để làm đầu vào cho việc sinh và thực thi tự động các tập lệnh kiểm thử bằng các công cụ thực thi kiểm thử tự động.
3. Thách thức thứ ba: Cần một ngôn ngữ đặc tả chuyên biệt miền để biểu diễn rõ ràng và đầy đủ thông tin của các ca kiểm thử được sinh.
4. Thách thức thứ tư: Cần một công cụ hỗ trợ hoàn chỉnh cho phép tích hợp ca sử dụng vào phương pháp MDD nhằm sinh tự động các chế tác phần mềm khác nhau từ mô hình ca sử dụng, trọng tâm là sinh tự động ca kiểm thử chức năng.

Mục tiêu nghiên cứu của luận án là đặt ca sử dụng vào trong ngữ cảnh của quy trình kiểm thử dựa trên mô hình (MBT) và phát triển hướng mô hình (MDD), cho phép tự động hóa hoạt động kiểm thử chức năng từ các yêu cầu phần mềm đầu vào, tập trung vào hai bước: mô hình hóa yêu cầu và sinh ca kiểm thử tự động có kèm dữ liệu cụ thể.

Đối tượng và phạm vi nghiên cứu:

• Đối tượng nghiên cứu: Các mô hình ca sử dụng, các ca kiểm thử chức năng, phương pháp xác định ca kiểm thử chức năng từ ca sử dụng và phương pháp tự động hóa trong kiểm thử phần mềm áp dụng cho kiểm thử chức năng.
• Phạm vi nghiên cứu: Kiểm thử mức hệ thống (system testing), kỹ thuật kiểm thử hộp đen dựa trên yêu cầu chức năng; tiếp cận kiểm thử dựa trên mô hình (MBT) kết hợp phương pháp mô hình hóa chuyên biệt miền (Domain-Specific Modeling - DSM).

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

Các hướng nghiên cứu trước đây được luận án điểm lại và phân loại theo các nhóm tiếp cận:

• Hướng tiếp cận xử lý ngôn ngữ tự nhiên (NLP) trên mô tả ca sử dụng theo mẫu: T. Yue và các cộng sự [75] đề xuất ngôn ngữ RUCM (Restricted Use Case Modeling) sử dụng khuôn mẫu văn bản, từ khóa và các luật rút gọn để giảm sự mơ hồ. Wang và các cộng sự [73] sử dụng đặc tả RUCM kết hợp kỹ thuật NLP và OCL để sinh mô hình kiểm thử trung gian UCTM (Use Case Test Model) làm đầu vào sinh ca kiểm thử. Các nghiên cứu khác trong [58] cũng trích xuất mô hình trung gian bằng NLP. Hạn chế của nhóm này là ngôn ngữ đặc tả mang tính bán hình thức hoặc phi hình thức (informal), thiếu cú pháp trừu tượng, việc xử lý phụ thuộc vào ngôn ngữ tự nhiên cụ thể và khó sinh dữ liệu kiểm thử cụ thể từ các ràng buộc văn bản.
• Hướng tiếp cận sử dụng biểu đồ chuẩn UML: Tiwari và Gupta [67], cùng các nghiên cứu [24, 51], đề xuất sử dụng biểu đồ hoạt động và biểu đồ tuần tự hướng tác nhân trong UML để đặc tả các tương tác và phân biệt hành động giữa tác nhân với hệ thống. Nhược điểm chính là phương pháp chỉ tập trung sinh các ca kiểm thử trừu tượng (kịch bản kiểm thử) mà không đề cập đến việc sinh tự động dữ liệu cụ thể cho ca kiểm thử.
• Hướng tiếp cận sử dụng ngôn ngữ chuyên biệt miền (DSL): Escalona và các cộng sự [16, 23] đề xuất ngôn ngữ NDT (Navigational Development Techniques) để đặc tả ca sử dụng nhưng không đề cập phương pháp xác định giá trị kiểm thử cho kịch bản. Śmiałek và các cộng sự [63, 65] giới thiệu 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ử trong TSL mới dừng lại ở các mô tả điều kiện chứ chưa có giá trị cụ thể. Ngôn ngữ SelabReq [59] chỉ hỗ trợ sinh mô hình cấu trúc và hành vi, không hỗ trợ sinh ca kiểm thử. Misbhauddin và các cộng sự [47] mở rộng siêu mô hình UML nhưng chưa hình thức hóa toàn diện. Murali và các cộng sự [48] xây dựng plug-in UC-B trên nền Rodin để hình thức hóa điều kiện ca sử dụng phục vụ kiểm chứng mô hình Event-B nhưng bỏ qua các thông tin tương tác khác.

Khoảng trống nghiên cứu luận án lựa chọn giải quyết là: Thiếu một giải pháp hình thức hoàn chỉnh cho phép đặc tả đầy đủ cả cấu trúc, hành vi và các ràng buộc của ca sử dụng để tích hợp vào MDD; đồng thời thiếu một phương pháp và ngôn ngữ đặc tả ca kiểm thử có khả năng xác định tự động các bước kiểm thử, kiểu bước, đối tượng, hành động, loại điểm kiểm tra, trạng thái bên trong hệ thống trước kiểm thử và dữ liệu kiểm thử cụ thể.

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

Lý thuyết, khái niệm và khung phân tích được tác giả sử dụng bao gồm:

• Quy trình kiểm thử dựa trên mô hình (MBT): Áp dụng quy trình 5 bước theo Utting và Legeard [9], tập trung vào mô hình hóa hệ thống cần kiểm thử (SUT) và sinh ca kiểm thử tự động.
• Kỹ thuật kiểm thử phần mềm: Sử dụng các định nghĩa chuẩn trong [5, 49] về lỗi phần mềm, kiểm thử tĩnh, kiểm thử động, ca kiểm thử (test case gồm test data, pre-condition, test steps, expected output), kịch bản kiểm thử (test scenario) và oracle. Áp dụng kỹ thuật kiểm thử hộp đen ở mức kiểm thử hệ thống (system testing) trong mô hình chữ V [50, 64].
• Mô hình lỗi và tiêu chí bao phủ kiểm thử trên biểu đồ hoạt động: Luận án dựa trên ba loại lỗi: lỗi điểm quyết định, lỗi vòng lặp (cấu trúc while-do và do-while) và lỗi đồng bộ hóa các luồng song song. Luận án áp dụng tiêu chí phủ đường hoạt động (activity path coverage) của [39] (mở rộng từ tiêu chí phủ đường cơ bản - basic path coverage [41, 46]) bao gồm đường hoạt động không đồng thời và đường hoạt động đồng thời, kết hợp công thức độ phức tạp Cyclomatic $V(G) = E - N + 2 = P + 1$ của McCabe [8, 31, 33] để xác định giới hạn số ca kiểm thử.
• Mô hình hóa chuyên biệt miền (DSM / MDE): Áp dụng quy trình 4 bước xây dựng DSML [9, 35, 62] gồm: khảo sát miền, xây dựng cú pháp trừu tượng (bằng siêu mô hình - metamodel), xây dựng cú pháp cụ thể và thao tác mô hình. Ngữ nghĩa hình thức của ngôn ngữ được ánh xạ sang hệ thống chuyển trạng thái được gán nhãn (Labelled Transition System - LTS [34, 70]).
• Ngôn ngữ ràng buộc đối tượng (OCL): Sử dụng OCL [10, 54, 74] ở hai cấp độ: cấp độ siêu mô hình (đặc tả các luật ràng buộc hợp lệ - well-formed rules) và cấp độ mô hình (đặc tả bất biến invariants, khởi tạo init, luật dẫn xuất derive, truy vấn query, cùng tiền điều kiện pre và hậu điều kiện post của thao tác).
• Kỹ thuật chuyển đổi mô hình: Chuyển đổi mô hình sang mô hình (M2M) ngoại sinh bằng ngôn ngữ ATL [32] và chuyển đổi mô hình sang văn bản (M2T) dựa trên mẫu bằng ngôn ngữ Acceleo [9, 22, 30] với các thẻ file, for, if, query, biểu thức và vùng bảo vệ protected.
• Công cụ giải ràng buộc OCL trong USE: Sử dụng hệ thống USE (UML-based Specification Environment) [18, 19] tích hợp công cụ giải logic quan hệ Kodkod [69], khai thác hai chức năng chính là kiểm tra tính nhất quán mô hình (model consistency) và hoàn thiện giải pháp cục bộ (partial solution completion) để giải các bất biến OCL và sinh biểu đồ đối tượng.

Phương pháp nghiên cứu thực tế:

• Phương pháp hình thức hóa cú pháp và ngữ nghĩa trên nền tảng Eclipse Modeling Framework (EMF) và Graphical Modeling Framework (GMF).
• Phương pháp sinh dữ liệu kiểm thử và trạng thái hệ thống: Tự động trích xuất các ràng buộc OCL từ mô hình ca sử dụng và mô hình lớp khái niệm miền, đưa vào công cụ USE/Kodkod để giải và trích xuất giá trị cụ thể.
• Nguồn tư liệu/dữ liệu: Mô hình đặc tả ca sử dụng mẫu (như ca sử dụng Đăng nhập trên website trung tâm X, ca sử dụng Hủy đăng ký) và mô hình lớp thực thể miền ứng dụng (như hệ thống rút tiền ATM với các lớp EV, Customer, ATMCard, Permission).

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

Chương 1: Mở đầu

Chương này trình bày lý do chọn đề tài, tính cấp thiết của việc tự động hóa kiểm thử phần mềm và ứng dụng quy trình MBT trong công nghiệp. Tác giả phân tích những hạn chế của các phương pháp đặc tả ca sử dụng hiện hành, xác định 4 thách thức nghiên cứu, thiết lập mục tiêu khoa học, đối tượng, phạm vi nghiên cứu, tóm lược 4 đóng góp chính và giới thiệu cấu trúc tổng thể 6 chương của luận án.

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

Chương 2 hệ thống hóa các nền tảng lý thuyết được sử dụng xuyên suốt luận án. Tác giả làm rõ các khái niệm kiểm thử phần mềm, kỹ thuật kiểm thử hộp đen/hộp trắng, các mức kiểm thử trong mô hình chữ V, quy trình MBT 5 bước, tiêu chí bao phủ đường hoạt động và độ phức tạp Cyclomatic. Tác giả trình bày cấu trúc ca sử dụng theo mẫu chuẩn (luồng chính, luồng thay thế) và phương pháp xác định ca kiểm thử truyền thống qua 3 bước (xác định kịch bản, xác định ca kiểm thử, gán giá trị cụ thể). Phần tiếp theo giới thiệu mô hình hóa chuyên biệt miền, siêu mô hình, phương pháp xây dựng DSML trên Eclipse (EMF, GMF), kỹ thuật chuyển đổi mô hình M2M (ATL), M2T (Acceleo), ngôn ngữ OCL và cơ chế giải ràng buộc trong công cụ USE/Kodkod.

Bảng tổng hợp các kịch bản kiểm thử của ca sử dụng Đăng nhập (trích xuất từ Chương 2):

Mã kịch bản (SID)	Tên kịch bản	Luồng bắt đầu	Luồng phụ
SC1	Đăng nhập thành công	Luồng chính	Không
SC2	Nhập UserName không hợp lệ	Luồng chính	4a
SC3	Nhập Password không hợp lệ	Luồng chính	6a
SC4	Tài khoản đăng nhập không có trong hệ thống	Luồng chính	8a

Bảng tổng hợp các ca kiểm thử với giá trị cụ thể của ca sử dụng Đăng nhập (trích xuất từ Chương 2):

Mã kiểm thử (TID)	Mã kịch bản (SID)	Giá trị UserName	Giá trị PassWord	Trạng thái tài khoản trong hệ thống	Kết quả mong đợi
T01	SC1	"user name 1"	"12345678"	True	Hiển thị các chức năng sinh viên được thực hiện
T02	SC2	"name 1"	N/A	N/A	Thông báo "UserName phải từ 8 đến 16 ký tự, yêu cầu nhập lại"
T03	SC3	"user name 1"	"123"	N/A	Thông báo "PassWord phải là 8 ký tự, yêu cầu nhập lại"
T04	SC4	"user name 2"	"12345678"	False	Thông báo "Tài khoản không tồn tại, đăng nhập lại"

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 này đề xuất ngôn ngữ đặc tả chuyên biệt miền USL (Use case Specification Language) nhằm mô hình hóa hình thức các thông tin trong ca sử dụng. Cấu trúc USL bao gồm cú pháp trừu tượng được định nghĩa bằng siêu mô hình, cú pháp cụ thể dạng đồ họa, tập luật ràng buộc hợp lệ viết bằng OCL và ngữ nghĩa hình thức được ánh xạ sang hệ thống chuyển trạng thái được gán nhãn (LTS). Siêu mô hình USL hỗ trợ biểu diễn đầy đủ: thông tin tổng quan của ca sử dụng, các loại luồng sự kiện (tuần tự, rẽ nhánh, lặp, đồng thời), phân loại hành động theo đối tượng tác nhân/hệ thống, các quan hệ cấu trúc («include», «extend») và các biểu thức ràng buộc tiền/hậu điều kiện.

Chương 4: Phương pháp sinh tự động các ca kiểm thử chức năng 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 đề xuất ngôn ngữ đặc tả ca kiểm thử chuyên biệt miền TCSL (Test Case Specification Language) và phương pháp sinh ca kiểm thử tự động USLTG (USL-based Test Generation). Phương pháp sử dụng đầu vào gồm mô hình ca sử dụng USL và mô hình lớp khái niệm miền của hệ thống. Dựa trên tiêu chí phủ đường hoạt động, thuật toán xác định các kịch bản kiểm thử, sau đó tích hợp công cụ USE để giải các bất biến OCL nhằm xác định trạng thái bên trong hệ thống trước kiểm thử cùng bộ dữ liệu kiểm thử cụ thể, cuối cùng chuyển toàn bộ thông tin vào mô hình TCSL.

Chương 5: Công cụ hỗ trợ và các đánh giá của phương pháp đã đề xuất

Chương này trình bày việc hiện thực hóa các đề xuất thành bộ công cụ hỗ trợ USL trong môi trường Eclipse. Công cụ bao gồm trình soạn thảo mô hình USL, bộ sinh tài liệu ca sử dụng dạng văn bản tự nhiên theo mẫu USL2TUCD và bộ sinh ca kiểm thử tự động sang mô hình TCSL bằng Acceleo. Tác giả thực nghiệm công cụ trên các ca sử dụng cụ thể, tiến hành so sánh, đối sánh phương pháp đặc tả và phương pháp sinh kiểm thử với các nghiên cứu liên quan.

Chương 6: Kết luận và hướng nghiên cứu trong tương lai

Chương cuối cùng tổng kết các kết quả nghiên cứu chính đã đạt được, phân tích mức độ đáp ứng các mục tiêu khoa học đề ra và thảo luận các định hướng mở rộng nghiên cứu trong tương lai từ các kết quả ban đầu.

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

Luận án tự xác định bốn đóng góp mới chính:

1. Đề xuất ngôn ngữ mô hình hóa chuyên biệt miền USL (Use case Specification Language): Định nghĩa đầy đủ cú pháp trừu tượng, cú pháp cụ thể, tập luật ràng buộc OCL và ngữ nghĩa thực thi hình thức LTS. USL giải quyết hạn chế thiếu chi tiết của các mô hình ca sử dụng truyền thống, hỗ trợ tích hợp ca sử dụng vào quy trình MDD và bảo đảm tính trực quan cho các bên liên quan phi kỹ thuật.
2. Đề xuất ngôn ngữ đặc tả ca kiểm thử chuyên biệt miền TCSL (Test Case Specification Language): Cung cấp siêu mô hình và tập luật ràng buộc để đặc tả toàn diện ca kiểm thử hệ thống. TCSL mô tả chi tiết: bước kiểm thử, đối tượng, hành động, loại điểm kiểm tra (checkpoint type), dữ liệu đầu vào, dữ liệu đầu ra mong đợi, tiền/hậu điều kiện và đặc biệt là trạng thái bên trong của hệ thống trước khi thực thi ca sử dụng.
3. Đề xuất phương pháp sinh ca kiểm thử tự động USLTG (USL-based Test Generation): 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 thuật toán sinh kịch bản theo tiêu chí phủ đường hoạt động và cơ chế giải ràng buộc OCL bằng công cụ USE/Kodkod để sinh dữ liệu kiểm thử cụ thể và trạng thái hệ thống.
4. Xây dựng bộ công cụ hỗ trợ USL trên nền tảng Eclipse: Hiện thực hóa trình soạn thảo mô hình USL, bộ sinh tài liệu ca sử dụng USL2TUCD và bộ sinh ca kiểm thử TCSL, chứng minh tính khả thi và tính ứng dụng của phương pháp.

Kiến nghị và giải pháp: Luận án kiến nghị sử dụng USL và TCSL làm công cụ trung gian chuẩn hóa để kết nối khâu nắm bắt yêu cầu với khâu kiểm thử tự động trong các dự án phát triển phần mềm theo hướng mô hình.

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

• Hạn chế: Luận án tập trung vào kiểm thử chức năng hộp đen ở mức kiểm thử hệ thống, chưa giải quyết các loại kiểm thử phi chức năng (hiệu năng, độ tin cậy, bảo mật) và các mức kiểm thử khác (kiểm thử đơn vị, kiểm thử tích hợp). Phương pháp đòi hỏi mô hình đầu vào phải được xây dựng chính xác bằng USL và biểu đồ lớp có ràng buộc OCL, yêu cầu nỗ lực ban đầu từ chuyên gia miền.
• Hướng nghiên cứu tiếp: Mở rộng các bộ sinh tự động từ mô hình USL sang các chế tác khác trong MDD (sinh biểu đồ lớp, biểu đồ tuần tự, mã nguồn); phát triển bộ sinh tập lệnh thực thi kiểm thử (test scripts) cho các công cụ kiểm thử tự động từ mô hình TCSL; tiến hành thực nghiệm trên các hệ thống phần mềm có quy mô lớn hơn.

Giá trị tham khảo

Luận án có giá trị tham khảo chuyên môn cho các đối tượng:

• Nghiên cứu sinh, học viên cao học và giảng viên ngành Kỹ thuật 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), định nghĩa siêu mô hình EMF/GMF, ngữ nghĩa LTS, kỹ thuật giải ràng buộc OCL bằng USE/Kodkod và kỹ thuật chuyển đổi mô hình (ATL, Acceleo).
• Kỹ sư phân tích yêu cầu (BA), kỹ sư phát triển phần mềm và kiểm thử viên (QA/QC): Tham khảo phương pháp hình thức hóa ca sử dụng bằng USL, cấu trúc hóa dữ liệu kiểm thử bằng TCSL và quy trình tự động hóa kiểm thử chức năng mức hệ thống.

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

1. Quy trình kiểm thử dựa trên mô hình (MBT) gồm những bước nào và luận án tập trung giải quyết những bước nào?
   Trả lời: Quy trình MBT gồm năm bước: (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ử, và (5) Phân tích ca kiểm thử. Luận án tập trung giải quyết hai bước đầu tiên còn nhiều thách thức là Bước (1) Mô hình hóa các yêu cầu và Bước (2) Sinh các ca kiểm thử tự động.

2. Ngôn ngữ USL có cấu tạo như thế nào và khắc phục hạn chế gì của mô tả ca sử dụng truyền thống?
   Trả lời: USL gồm cú pháp trừu tượng (siêu mô hình), cú pháp cụ thể (đồ họa), tập luật ràng buộc hợp lệ OCL và ngữ nghĩa hình thức LTS. USL khắc phục tình trạng thiếu hình thức, mơ hồ và thiếu chi tiết của văn bản ngôn ngữ tự nhiên, cho phép mô hình hóa rõ ràng các luồng điều khiển (tuần tự, rẽ nhánh, lặp, đồng thời), phân loại hành động của tác nhân/hệ thống và các ràng buộc tiền/hậu điều kiện.

3. Ngôn ngữ đặc tả ca kiểm thử TCSL có điểm khác biệt gì so với các ngôn ngữ đặc tả kiểm thử trước đây?
   Trả lời: Khác với các ngôn ngữ trước đây chỉ mô tả bước kiểm thử và dữ liệu kiểm thử ở dạng điều kiện trừu tượng, TCSL đặc tả chi tiết các bước kiểm thử, kiểu bước, đối tượng, hành động, loại điểm kiểm tra, dữ liệu đầu vào cụ thể, dữ liệu đầu ra mong đợi, tiền/hậu điều kiện và trạng thái bên trong của hệ thống trước khi thực thi ca sử dụng.

4. Phương pháp USLTG sử dụng tiêu chí bao phủ nào để sinh ca kiểm thử?
   Trả lời: USLTG áp dụng tiêu chí phủ đường hoạt động (activity path coverage), mở rộng từ tiêu chí phủ đường cơ bản. Tiêu chí này bao gồm kiểm thử đường hoạt động không đồng thời (xét vòng lặp tối đa hai lần để phát hiện lỗi điều kiện nhánh và vòng lặp) và đường hoạt động đồng thời (bảo toàn thứ tự ưu tiên giữa các hành động song song và tuần tự), kết hợp hàm độ phức tạp Cyclomatic $V(G) = P + 1$ để xác định giới hạn số ca kiểm thử.

5. Công cụ USE và Kodkod đóng vai trò gì trong phương pháp của luận án?
   Trả lời: USE tích hợp bộ giải logic quan hệ Kodkod đóng vai trò là công cụ trung gian giải các bất biến OCL. Luận án sử dụng hai chức năng là kiểm tra tính nhất quán (model consistency) và hoàn thiện giải pháp cục bộ (partial solution completion) để tìm kiếm và sinh ra biểu đồ đối tượng thỏa mãn ràng buộc, từ đó xác định dữ liệu kiểm thử cụ thể và trạng thái hệ thống trước kiểm thử.

Kết luận

Luận án đã xây dựng phương pháp hoàn chỉnh để tự động hóa hoạt động kiểm thử chức năng mức hệ thống từ mô hình ca sử dụng theo hướng tiếp cận kiểm thử dựa trên mô hình kết hợp mô hình hóa chuyên biệt miền. Thông qua việc đề xuất hai ngôn ngữ chuyên biệt miền USL và TCSL, quy trình chuyển đổi tự động USLTG tích hợp cơ chế giải ràng buộc OCL và bộ công cụ hỗ trợ trên nền tảng Eclipse, luận án đã giải quyết bài toán sinh kịch bản kèm dữ liệu kiểm thử cụ thể và trạng thái hệ thống. Các kết quả đạt được tạo cơ sở để tích hợp mô hình ca sử dụng vào quy trình 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.