Phương Pháp Sinh Dữ Liệu Kiểm Thử Tự Động Từ Mã Nguồn Và Ứng Dụng Trong Hệ Thống Chấm Bài Lập Trình

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ừ mã nguồn và ứng dụng trong hệ thống chấm bài lập trình.

• Tác giả: Nguyễn Thị Khánh Chi
• 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: Kỹ Thuật Phần Mềm
• Đề tài: Phương Pháp Sinh Dữ Liệu Kiểm Thử Tự Động Từ Mã Nguồn Và Ứng Dụng Xây Dựng Hệ Thống Chấm Bài Lập Trình
• Loại tài liệu: Luận văn thạc sĩ
• Năm xuất bản: 2019
• Địa điểm: Hà Nội

Mục lục chi tiết

• LỜI CAM ĐOAN
• 1. CHƯƠNG 1: MỞ ĐẦU
• 2. CHƯƠNG 2: PHƯƠNG PHÁP SINH DỮ LIỆU KIỂM THỬ DÒNG ĐIỀU KHIỂN
• 2.1. Tổng quan về kiểm thử dòng điều khiển
• 2.2. Các tiêu chí kiểm thử
• 2.3. Xây dựng đồ thị dòng điều khiển
• 2.3.1. Xây dựng đồ thị dòng điều khiển ứng với tiêu chí phủ câu lệnh và phủ nhánh
• 2.3.2. Xây dựng CFG ứng với tiêu chí phủ điều kiện con
• 2.3.3. Phương pháp xây dựng CFG từ mã nguồn Java
• 2.4. Sinh đường đi kiểm thử từ đồ thị
• 2.4.1. Sinh đường đi thỏa mãn tiêu chí phủ câu lệnh
• 2.4.2. Sinh đường đi thỏa mãn tiêu chí phủ nhánh
• 2.4.3. Sinh đường đi thỏa mãn tiêu chí phủ điều kiện con
• 2.5. Phương pháp sinh đường đi kiểm thử trên đồ thị
• 2.6. Sinh ca kiểm thử từ đường đi
• 2.7. Sinh dữ liệu kiểm thử
• 2.8. Sinh đầu ra mong muốn
• 2.9. Sinh các ca kiểm thử giá trị biên và vòng lặp
• 2.9.1. Sinh ca kiểm thử giá trị biên
• 2.9.2. Sinh ca kiểm thử vòng lặp
• 3. CHƯƠNG 3: CÔNG CỤ VÀ THỰC NGHIỆM
• 3.1. Đặc tả hệ thống chấm bài lập trình
• 3.2. Danh sách các tác nhân
• 3.3. Mô tả các ca sử dụng của hệ thống
• 3.4. Kiến trúc tổng thể của hệ thống chấm bài lập trình
• 3.5. Kiến trúc của mô-đun sinh ca kiểm thử tự động
• 3.6. Giới thiệu công cụ sinh ca kiểm thử tự động
• 3.6.1. Giao diện công cụ sinh ca kiểm thử tự động
• 3.6.2. Đồ thị dòng điều khiển
• 3.6.3. Tập các đường kiểm thử
• 3.6.4. Tập các ca kiểm thử
• 3.7. Kết quả thực nghiệm
• 3.7.1. Bài toán 1: Bài toán kiểm tra năm nhuận
• 3.7.2. Bài toán 2: Bài toán tính số ngày trong một tháng
• 3.7.3. Bài toán 3: Tìm ước số chung lớn nhất
• 3.7.4. Ý nghĩa của thực nghiệm
• 4. CHƯƠNG 4: KẾT LUẬN
• TÀI LIỆU THAM KHẢO

Tóm tắt

I. Tổng quan về phương pháp tự động sinh dữ liệu kiểm thử từ mã nguồn

Phương pháp tự động sinh dữ liệu kiểm thử từ mã nguồn đang trở thành một xu hướng quan trọng trong lĩnh vực kiểm thử phần mềm. 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ính xác trong việc phát hiện lỗi. Bằng cách phân tích mã nguồn, phương pháp này có thể tạo ra các ca kiểm thử tự động, từ đó hỗ trợ giáo viên trong việc chấm bài lập trình.

1.1. Khái niệm về sinh dữ liệu kiểm thử tự động

Sinh dữ liệu kiểm thử tự động là quá trình tạo ra các ca kiểm thử từ mã nguồn mà không cần sự can thiệp của con người. Điều này giúp giảm thiểu sai sót và tăng cường hiệu quả trong việc kiểm thử phần mềm.

1.2. Lợi ích của phương pháp tự động hóa kiểm thử

Phương pháp tự động hóa kiểm thử mang lại nhiều lợi ích như tiết kiệm thời gian, giảm thiểu lỗi do con người, và đảm bảo tính chính xác trong việc phát hiện lỗi. Điều này đặc biệt quan trọng trong môi trường giáo dục, nơi giáo viên cần chấm bài một cách công bằng và hiệu quả.

II. Vấn đề và thách thức trong kiểm thử phần mềm hiện nay

Mặc dù phương pháp tự động sinh dữ liệu kiểm thử mang lại nhiều lợi ích, nhưng vẫn tồn tại một số thách thức cần được giải quyết. Các vấn đề như độ phức tạp của mã nguồn, sự đa dạng của ngôn ngữ lập trình, và khả năng phát hiện lỗi vẫn là những thách thức lớn.

2.1. Độ phức tạp của mã nguồn

Mã nguồn ngày càng trở nên phức tạp với nhiều cấu trúc điều khiển khác nhau. Điều này làm cho việc sinh dữ liệu kiểm thử trở nên khó khăn hơn, đòi hỏi các phương pháp phân tích mã nguồn phải chính xác và hiệu quả.

2.2. Sự đa dạng của ngôn ngữ lập trình

Mỗi ngôn ngữ lập trình có những đặc điểm riêng, điều này tạo ra thách thức trong việc phát triển các công cụ sinh dữ liệu kiểm thử có thể áp dụng cho nhiều ngôn ngữ khác nhau.

III. Phương pháp sinh dữ liệu kiểm thử từ mã nguồn Java

Phương pháp sinh dữ liệu kiểm thử từ mã nguồn Java được xây dựng dựa trên việc phân tích đồ thị dòng điều khiển (Control Flow Graph - CFG). Phương pháp này cho phép sinh ra các ca kiểm thử đáp ứng các tiêu chí kiểm thử khác nhau.

3.1. Xây dựng đồ thị dòng điều khiển

Đồ thị dòng điều khiển là một công cụ quan trọng trong việc phân tích mã nguồn. Nó giúp xác định các đường đi kiểm thử và từ đó sinh ra dữ liệu kiểm thử tương ứng.

3.2. Sinh ca kiểm thử từ đồ thị

Từ đồ thị dòng điều khiển, các ca kiểm thử sẽ được sinh ra dựa trên các tiêu chí như phủ câu lệnh, phủ nhánh và phủ điều kiện con. Điều này đảm bảo rằng tất cả các nhánh của mã nguồn đều được kiểm tra.

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ừ mã nguồn đã được áp dụng thành công trong việc chấm bài lập trình tại các trường học. Điều này không chỉ giúp giáo viên tiết kiệm thời gian mà còn nâng cao chất lượng chấm bài.

4.1. Kết quả thực nghiệm với các bài tập lập trình

Các kết quả thực nghiệm cho thấy phương pháp này có khả năng phát hiện lỗi hiệu quả, từ đó giúp giáo viên có thể chấm bài một cách chính xác hơn.

4.2. Phản hồi từ giáo viên và học sinh

Phản hồi từ giáo viên và học sinh cho thấy rằng việc sử dụng phương pháp này đã cải thiện đáng kể quá trình học tập và giảng dạy, giúp học sinh tự tin hơn trong việc lập trình.

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 sinh dữ liệu kiểm thử từ mã nguồn đang mở ra nhiều cơ hội mới trong lĩnh vực kiểm thử phần mềm. Tương lai của phương pháp này hứa hẹn sẽ tiếp tục phát triển và hoàn thiện hơn nữa.

5.1. Hướng phát triển công cụ hỗ trợ

Cần phát triển thêm các công cụ hỗ trợ để tự động hóa quá trình sinh dữ liệu kiểm thử, giúp giáo viên dễ dàng hơn trong việc chấm bài.

5.2. Nghiên cứu mở rộng cho các ngôn ngữ khác

Nghiên cứu mở rộng phương pháp này cho các ngôn ngữ lập trình khác sẽ giúp tăng cường khả năng áp dụng và hiệu quả của phương pháp trong giáo dục.

Nội dung chính

Tổng quan nghiên cứu

Trong bối cảnh chuyển đổi số giáo dục và triển khai chương trình giáo dục phổ thông mới, môn Tin học tại các trường trung học cơ sở và trung học phổ thông đang chuyển dịch mạnh mẽ từ ngôn ngữ Pascal sang các ngôn ngữ hiện đại như Java và C/C++. Tuy nhiên, theo khảo sát thực tế tại nhiều cơ sở giáo dục, hơn 85% giáo viên vẫn phải chấm bài lập trình của học sinh bằng phương pháp thủ công. Công việc này chiếm từ 10 đến 15 giờ mỗi tuần của mỗi giáo viên, đồng thời tiềm ẩn nhiều sai sót do áp lực thời gian khiến các lỗi giải thuật phức tạp dễ bị bỏ sót, dẫn đến đánh giá thiếu chính xác và chưa đảm bảo tính công bằng.

Vấn đề cốt lõi của việc chấm bài lập trình không chỉ dừng lại ở kiểm tra lỗi cú pháp vốn đã được trình biên dịch xử lý, mà nằm ở việc đánh giá tính đúng đắn của mã nguồn so với đặc tả yêu cầu của bài toán. Luận văn thạc sĩ chuyên ngành Kỹ thuật Phần mềm thực hiện năm 2019 tại Trường Đại học Công nghệ, Đại học Quốc gia Hà Nội đã tập trung giải quyết bài toán cấp thiết này.

Mục tiêu chính của đề tài là nghiên cứu phương pháp tự động sinh dữ liệu kiểm thử từ mã nguồn chuẩn viết bằng ngôn ngữ Java và ứng dụng vào việc xây dựng mô hình hệ thống chấm bài lập trình tự động. Phạm vi nghiên cứu tập trung vào các cấu trúc điều khiển cơ bản trong chương trình giảng dạy phổ thông, thử nghiệm thực tế trên các bài tập của học sinh khối 11 tại Trường Trung học phổ thông Ngô Gia Tự, thị xã Từ Sơn, tỉnh Bắc Ninh. Nghiên cứu mang lại ý nghĩa thực tiễn to lớn khi giúp giảm thiểu hơn 75% thời gian chấm bài của giáo viên, đồng thời nâng cao độ chính xác trong phát hiện lỗi logic lên mức tuyệt đối thông qua việc đạt 100% độ bao phủ các đường thực thi của mã nguồn mẫu.

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

Khung lý thuyết áp dụng

Nghiên cứu được xây dựng dựa trên nền tảng vững chắc của lý thuyết kiểm thử phần mềm hộp trắng, kết hợp với các kỹ thuật phân tích tĩnh và giải hệ ràng buộc tự động. Hai lý thuyết cốt lõi được áp dụng bao gồm lý thuyết kiểm thử dòng điều khiển và lý thuyết đồ thị ứng dụng trong cấu trúc chương trình.

Trong khung lý thuyết này, luận văn làm rõ 4 khái niệm chuyên ngành nền tảng:

• Đồ thị dòng điều khiển: Mô hình toán học biểu diễn toàn bộ các luồng thực thi có thể có của mã nguồn thông qua tập các đỉnh biểu diễn câu lệnh và các cạnh có hướng biểu diễn luồng điều khiển giữa các lệnh.
• Cây cú pháp trừu tượng: Cấu trúc dữ liệu cây thể hiện cấu trúc ngữ pháp trừu tượng của mã nguồn Java, được trích xuất thông qua bộ công cụ phát triển phần mềm Eclipse Java Development Tooling.
• Độ phủ kiểm thử: Thước đo định lượng mức độ kiểm tra mã nguồn, bao gồm 3 cấp độ tiêu chí: phủ câu lệnh, phủ nhánh và phủ điều kiện con.
• Bộ giải thỏa mãn lý thuyết modulo: Công cụ toán học hỗ trợ tìm nghiệm thỏa mãn hệ các điều kiện logic và số học trên từng đường thực thi.

Mô hình nghiên cứu kết hợp việc phân tích mã nguồn chuẩn không có lỗi do giáo viên cung cấp thành cây cú pháp trừu tượng, từ đó tự động chuyển đổi sang đồ thị dòng điều khiển. Trên đồ thị này, thuật toán duyệt đồ thị độc lập của tác giả Thomas McCabe được triển khai để tìm tập đường đi ngắn nhất bao phủ 100% các nhánh và điều kiện logic. Hệ điều kiện dọc theo mỗi đường đi được trích xuất thành hệ ràng buộc và giải tự động bằng công cụ Z3 SMT-Solver nhằm sinh ra các giá trị đầu vào hợp lệ. Giá trị đầu ra mong đợi được xác định tự động bằng cách thực thi trực tiếp mã nguồn chuẩn với dữ liệu đầu vào vừa tạo. Để khắc phục triệt để hạn chế của kiểm thử hộp trắng đối với các hành vi không được lập trình, mô hình tích hợp thêm kỹ thuật kiểm thử hộp đen gồm phân tích giá trị biên với 5 giá trị cơ bản cùng kỹ thuật kiểm thử chu trình lặp từ 0 đến n cộng 1 lần lặp.

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

Nghiên cứu sử dụng nguồn dữ liệu thực nghiệm gồm mã nguồn chuẩn của giáo viên và 6 bộ mã nguồn bài tập do học sinh khối 11 nộp trong các giờ thực hành Tin học. Các bài toán được lựa chọn đại diện cho các cấu trúc giải thuật điển hình trong chương trình giáo dục phổ thông, bao gồm bài toán kiểm tra năm nhuận, bài toán tính số ngày trong tháng và bài toán tìm ước số chung lớn nhất.

Phương pháp chọn mẫu là phương pháp chọn mẫu có chủ đích với cỡ mẫu gồm 3 dạng bài toán bao quát toàn bộ các cấu trúc điều khiển cơ bản: rẽ nhánh lồng nhau if-else, rẽ nhánh đa trường hợp switch-case và cấu trúc lặp while/for. Lý do lựa chọn phương pháp chọn mẫu này là nhằm đánh giá toàn diện khả năng phân tích cây cú pháp trừu tượng và hiệu quả giải hệ ràng buộc của công cụ trên mọi loại hình luồng điều khiển phổ biến trong lập trình hướng cấu trúc.

Phương pháp phân tích được tiến hành theo quy trình định lượng và đối sánh thực nghiệm. Mã nguồn của học sinh được đưa vào hệ thống để chạy kiểm thử với 2 bộ dữ liệu: bộ ca kiểm thử sinh tự động từ đồ thị dòng điều khiển và bộ ca kiểm thử giá trị biên mở rộng. Toàn bộ quá trình nghiên cứu, xây dựng thuật toán, phát triển công cụ phần mềm và thu thập dữ liệu thực nghiệm được hoàn thành trọn vẹn trong năm 2019.

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 công cụ trên các bài toán mẫu đã mang lại 4 phát hiện khoa học và kỹ thuật nổi bật:

Thứ nhất, công cụ sinh ca kiểm thử tự động đạt độ phủ tuyệt đối 100% đối với tiêu chí phủ điều kiện con trên mã nguồn Java chuẩn. Đối với bài toán kiểm tra năm nhuận, công cụ đã tự động xây dựng đồ thị dòng điều khiển gồm 4 đỉnh quyết định và sinh ra đúng 5 ca kiểm thử độc lập bao quát mọi nhánh đúng và sai của biểu thức điều kiện phức hợp.

Thứ hai, việc sử dụng bộ ca kiểm thử sinh từ đồ thị dòng điều khiển cho phép phát hiện chính xác các lỗi rẽ nhánh trên bài làm của học sinh. Khi kiểm thử bài làm của 2 học sinh với 5 ca kiểm thử phủ điều kiện con của hàm kiểm tra năm nhuận, hệ thống phát hiện 1 lỗi trên bài làm của học sinh thứ nhất tương ứng tỷ lệ sai sót 20% và phát hiện 2 lỗi trên bài làm của học sinh thứ hai tương ứng tỷ lệ sai sót 40%.

Thứ ba, sự kết hợp giữa kiểm thử dòng điều khiển và kiểm thử giá trị biên giúp tăng vọt khả năng phát hiện lỗi tiềm ẩn lên hơn 100%. Trong bài toán kiểm tra năm nhuận, bộ 13 ca kiểm thử giá trị biên đã phát hiện thêm 2 lỗi trên bài làm của học sinh thứ nhất gồm lỗi không kiểm tra năm âm và vượt ngưỡng trên, đồng thời phát hiện tới 4 lỗi trên bài làm của học sinh thứ hai.

Thứ tư, phương pháp tự động bắt giá trị đầu ra mong đợi từ việc thực thi mã nguồn chuẩn đã rút ngắn thời gian thiết lập bộ kiểm thử mẫu từ trung bình 45 phút cho mỗi bài tập xuống còn dưới 3 giây, đạt độ chính xác 100% mà không đòi hỏi giáo viên phải tính toán thủ công.

Thảo luận kết quả

Nguyên nhân chính dẫn đến các lỗi trên bài làm của học sinh bắt nguồn từ 2 yếu tố: học sinh thường bỏ qua việc kiểm tra tính hợp lệ của miền giá trị đầu vào ở các giá trị biên như số âm hoặc giá trị vượt ngưỡng, và học sinh thường nhầm lẫn giữa các toán tử logic trong các biểu thức điều kiện phức hợp. Chẳng hạn, trong bài toán năm nhuận, học sinh thứ hai đã bỏ sót nhánh kiểm tra năm chia hết cho 400 khiến thuật toán cho kết quả sai tại các năm thế kỷ.

Dữ liệu kết quả kiểm thử có thể được trình bày trực quan và hiệu quả thông qua một bảng tổng hợp đối sánh hoặc biểu đồ cột biểu diễn số lượng lỗi phát hiện được. Cụ thể, biểu đồ cột so sánh giữa phương pháp kiểm thử dòng điều khiển đơn thuần và phương pháp kiểm thử kết hợp giá trị biên sẽ phản ánh rõ nét sự chênh lệch: từ 1 lỗi tăng lên 2 lỗi đối với học sinh thứ nhất và từ 2 lỗi tăng lên 4 lỗi đối với học sinh thứ hai.

So với các nghiên cứu trước đây vốn chỉ dừng lại ở việc sinh dữ liệu đầu vào cho ngôn ngữ C/C++ mà chưa thể sinh tự động đầu ra mong đợi, hoặc các nghiên cứu sinh test cho Java hướng đối tượng chưa tối ưu cho cấu trúc bài tập phổ thông, giải pháp trong luận văn này đã hoàn thiện chu trình khép kín: phân tích mã nguồn, sinh đồ thị, giải hệ ràng buộc bằng Z3, sinh đầu vào và tự động kết xuất đầu ra chuẩn xác. Điều này mang lại giá trị ứng dụng to lớn cho việc tự động hóa khâu đánh giá chất lượng bài tập.

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

Nhằm phát huy tối đa hiệu quả nghiên cứu và sớm đưa hệ thống vào ứng dụng rộng rãi tại các cơ sở giáo dục, luận văn đưa ra 4 khuyến nghị hành động cụ thể:

Thứ nhất, hoàn thiện tích hợp 3 phân hệ chức năng gồm phân hệ Quản lý bài tập, phân hệ Sinh ca kiểm thử tự động và phân hệ Chấm bài trực tuyến trên nền tảng web ứng dụng điện toán đám mây. Nhóm phát triển phần mềm giáo dục cần triển khai nhiệm vụ này trong thời gian 6 đến 12 tháng tới, hướng tới mục tiêu phục vụ đồng thời trên 10.000 lượt chấm bài mỗi ngày với độ trễ phản hồi dưới 2 giây.

Thứ hai, mở rộng bộ phân tích cú pháp để hỗ trợ đa ngôn ngữ lập trình. Các viện nghiên cứu công nghệ thông tin và trường đại học cần nâng cấp mô-đun trích xuất cây cú pháp trừu tượng để xử lý thêm ngôn ngữ Python và C++ trong lộ trình 18 tháng, đáp ứng đầy đủ định hướng chọn lựa ngôn ngữ của chương trình giáo dục phổ thông mới.

Thứ ba, chuẩn hóa quy trình biên soạn mã nguồn mẫu và tập huấn kỹ năng cho giáo viên. Sở Giáo dục và Đào tạo cùng tổ chuyên môn Tin học các trường trung học phổ thông cần tổ chức các khóa tập huấn ngắn hạn trong 3 tháng đầu năm học cho 100% giáo viên bộ môn, hướng dẫn cách viết mã nguồn chuẩn tối ưu và cách xác định miền giá trị biên nhằm tối đa hóa độ bao phủ của bộ dữ liệu kiểm thử.

Thứ tư, triển khai cơ chế phản hồi học tập tự động cho học sinh. Ban giám hiệu các nhà trường cần đưa tính năng xem lại chi tiết ca kiểm thử bị lỗi vào quy chế thực hành trực tuyến, giúp hơn 85% học sinh có thể tự đối chiếu, phân tích nguyên nhân sai sót giải thuật và tự sửa lỗi ngay sau mỗi buổi học.

Đố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ị học thuật và ứng dụng thiết thực cho 4 nhóm đối tượng chính:

1. Giáo viên giảng dạy môn Tin học tại các trường trung học cơ sở và trung học phổ thông: Khai thác tài liệu để nắm vững quy trình tạo lập bộ ca kiểm thử chuẩn, ứng dụng công cụ tự động sinh dữ liệu kiểm tra giúp tiết kiệm hơn 75% thời gian chấm bài thực hành và nâng cao tính khách quan trong đánh giá học sinh.

2. Sinh viên và học viên cao học chuyên ngành Kỹ thuật Phần mềm và Khoa học Máy tính: Sử dụng luận văn như tài liệu tham khảo chuyên sâu về kỹ thuật kiểm thử hộp trắng, phương pháp phân tích cây cú pháp trừu tượng bằng Eclipse JDT, thuật toán duyệt đồ thị dòng điều khiển và kỹ thuật ứng dụng SMT-Solver Z3 để giải hệ ràng buộc.

3. Các nhà phát triển nền tảng giáo dục trực tuyến và hệ thống chấm thi tự động: Tham khảo kiến trúc tổng thể 3 phân hệ và thiết kế mô-đun sinh dữ liệu kiểm thử tự động để tích hợp vào các hệ thống quản lý học tập, nền tảng thi lập trình trực tuyến quy mô lớn.

4. Kỹ sư kiểm thử và đảm bảo chất lượng phần mềm: Áp dụng phương pháp kết hợp giữa kiểm thử dòng điều khiển, kiểm thử giá trị biên và kiểm thử vòng lặp để nâng cao độ bao phủ kiểm thử đơn vị cho các dự án phát triển phần mềm thương mại.

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

Phương pháp sinh dữ liệu kiểm thử trong luận văn khác biệt như thế nào so với kỹ thuật sinh ngẫu nhiên truyền thống?

Kỹ thuật sinh ngẫu nhiên tạo dữ liệu ngẫu nhiên không định hướng nên tỷ lệ rơi vào các nhánh điều kiện phức tạp rất thấp, thường chỉ đạt dưới 40% độ bao phủ. Ngược lại, phương pháp trong luận văn phân tích cấu trúc mã nguồn để trích xuất hệ ràng buộc trên từng đường đi cụ thể, sau đó sử dụng công cụ Z3 SMT-Solver để giải chính xác nghiệm số, đảm bảo đạt 100% độ bao phủ nhánh và điều kiện con.

Tại sao kiểm thử dòng điều khiển đạt độ phủ 100% vẫn cần bổ sung kiểm thử giá trị biên?

Kiểm thử dòng điều khiển là phương pháp hộp trắng chỉ kiểm tra những cấu trúc đã được viết trong mã nguồn. Nếu học sinh quên không viết câu lệnh kiểm tra điều kiện đầu vào hợp lệ, ví dụ bỏ sót điều kiện năm phải lớn hơn 0, kiểm thử dòng điều khiển sẽ không thể phát hiện. Kiểm thử giá trị biên là kỹ thuật hộp đen giúp bổ sung các ca kiểm thử tại các điểm cực trị, đảm bảo phát hiện triệt để các lỗi thiếu sót này.

Hệ thống tự động xác định giá trị đầu ra mong đợi của ca kiểm thử bằng cách nào?

Thay vì yêu cầu giáo viên phải tính toán thủ công từng kết quả đầu ra, hệ thống tận dụng mã nguồn chuẩn không có lỗi do giáo viên cung cấp. Khi một giá trị đầu vào được bộ giải ràng buộc sinh ra, hệ thống tự động nạp giá trị này vào mã nguồn chuẩn và thực thi để ghi nhận kết quả trả về làm giá trị đầu ra mong đợi chuẩn xác 100%.

Công cụ Z3 SMT-Solver đóng vai trò gì trong mô hình nghiên cứu?

Z3 SMT-Solver là bộ công cụ toán học mạnh mẽ do Microsoft Research phát triển. Trong luận văn, Z3 đóng vai trò giải các biểu thức logic và phương trình số học thu thập được dọc theo từng đường đi của đồ thị dòng điều khiển. Nhờ đó, hệ thống tìm ra chính xác các giá trị biến đầu vào thỏa mãn đồng thời toàn bộ các điều kiện rẽ nhánh để kích hoạt đường thực thi tương ứng.

Hệ thống này có thể áp dụng ngay cho các ngôn ngữ lập trình khác ngoài Java hay không?

Về mặt lý thuyết, quy trình kiểm thử dòng điều khiển và giải hệ ràng buộc hoàn toàn có thể áp dụng cho mọi ngôn ngữ lập trình. Tuy nhiên, mô-đun phân tích cú pháp hiện tại được xây dựng dựa trên thư viện Eclipse JDT chuyên biệt cho Java. Để áp dụng cho các ngôn ngữ khác như Python hay C++, hệ thống cần được tích hợp thêm các bộ phân tích cây cú pháp trừu tượng tương ứng của từng ngôn ngữ đó.

Kết luận

• Luận văn đã xây dựng thành công quy trình tự động hóa toàn diện từ phân tích mã nguồn Java, trích xuất cây cú pháp trừu tượng đến thiết lập đồ thị dòng điều khiển trực quan.
• Ứng dụng xuất sắc công cụ Z3 SMT-Solver kết hợp kỹ thuật sinh ngẫu nhiên để giải hệ ràng buộc, giúp sinh tự động bộ dữ liệu kiểm thử đạt 100% độ bao phủ điều kiện con.
• Đề xuất giải pháp đột phá trong việc tự động sinh giá trị đầu ra mong đợi từ mã nguồn chuẩn, loại bỏ hoàn toàn các thao tác tính toán thủ công phức tạp của giáo viên.
• Kết hợp hoàn hảo kỹ thuật kiểm thử dòng điều khiển với kiểm thử giá trị biên và kiểm thử vòng lặp, nâng cao hiệu quả phát hiện lỗi logic giải thuật trong bài làm học sinh lên hơn 80%.
• Thiết kế hoàn chỉnh kiến trúc hệ thống chấm bài lập trình 3 phân hệ, tạo tiền đề vững chắc cho việc phát triển các nền tảng giáo dục thông minh.

Đóng góp chính của luận văn không chỉ nằm ở giải pháp kỹ thuật sinh ca kiểm thử tự động cho ngôn ngữ Java mà còn mở ra hướng tiếp cận mới trong việc ứng dụng công nghệ phần mềm vào đổi mới phương pháp giảng dạy Tin học. Trong giai đoạn 6 đến 12 tháng tới, nhóm nghiên cứu dự kiến sẽ hoàn thiện giao diện người dùng web và mở rộng hỗ trợ ngôn ngữ Python. Các đơn vị giáo dục và quý thầy cô quan tâm có thể liên hệ hợp tác thử nghiệm hệ thống để nâng cao chất lượng giảng dạy và tối ưu hóa công tác chấm thi lập trình ngay hôm nay.

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

Mở đầu Hiện nay, môn học lập trình đã được đưa vào giảng dạy ở các trường Trung học phổ thông (THPT) trên toàn quốc, giúp các em học sinh làm quen với công việc lập trình và làm quen dần với tư duy thiết kế các thuật toán. Ngôn ngữ lập trình được sử dụng để giảng dạy trong hầu hết các trường THPT là Pascal. Tuy nhiên, theo chương trình giáo dục THPT mới, trên cơ sở định hướng lập trình và tùy chọn ngôn ngữ, nhiều trường THPT đã bước đầu đưa các ngôn ngữ lập trình phổ biến như C, Java, v. vào giảng dạy.

Trong quá trình giảng dạy, công việc chấm bài tập lập trình đối với người giáo viên thường diễn ra thủ công và tiềm ẩn nhiều sai sót. Do thời gian chấm bài có hạn nên việc không phát hiện ra các lỗi trong bài lập trình là không tránh khỏi. Điều này dẫn đến điểm chấm chưa thực sự chính xác và công bằng. Làm thế nào để công việc chấp bài lập trình được dễ dàng hơn với các giáo viên, cũng như đảm bảo tính chính xác, rút ngắn thời gian chấm bài là mục tiêu cần hướng tới.

Đối với các bài tập lập trình, việc chấm bài chính là rà soát để phát hiện các lỗi có thể có trên mã nguồn của bài tập học sinh. Khi chương trình xuất hiện lỗi cú pháp, các lỗi sẽ được trình biên dịch phát hiện để người lập trình sửa lỗi. Tuy nhiên, ngay cả khi một chương trình không có lỗi cú pháp thì chương trình vẫn chưa chắc đã đúng vì lỗi có thể xảy ra trong quá trình thiết kế giải thuật. Làm thế nào để hỗ trợ giáo viên kiểm tra xem chương trình có thực hiện đúng với đặc tả yêu cầu của bài toán hay không, hoặc đúng bao nhiêu phần so với đặc tả của bài toán chính là mục tiêu của quá trình chấm bài.

Hơn nữa, việc giáo viên cung cấp các cơ chế cho phép học sinh tự làm bài và tương tác qua các ứng dụng nhằm nâng cao khả năng tự học và tăng cường chất lượng là một xu hướng tất yếu trong hệ thống giáo dục thời gian tới. Vì vậy, nhu cầu về bài toán này càng cấp thiết hơn. Để giải quyết vấn đề này, ứng với mỗi bài toán, giáo viên phải sinh ra một bộ ca kiểm thử đủ tốt (có khả năng phát hiện tất cả các lỗi có thể có của bài lập trình của học sinh). Bộ ca kiểm thử này sau đó sẽ được sử dụng để chấm các chương trình cho học sinh nộp (tự động hoặc thủ công tùy thuộc vào phương pháp và công cụ mà giáo viên sử dụng).

Hiện tại, việc sinh ra các bộ ca kiểm thử như vậy là vượt ngoài khả năng của các giáo viên Trung học phổ thông. Vì vậy, có một công cụ tự động hỗ trợ giáo viên giải quyết bài toán này là một vấn đề cấp thiết, có ý nghĩa thực tiễn cao. Một trong những giải pháp để giải quyết vấn đề này là sinh dữ liệu kiểm thử từ mã nguồn sử dụng phương pháp kiểm thử dòng dữ liệu [2, 3, 4, 8, 9, 11]. Trong phương pháp này, ứng với đặc tả của mỗi bài toán, thay vì yêu cầu giáo viên phải sinh bộ ca kiểm thử, họ sẽ phải cung cấp mã nguồn mẫu (mã nguồn của bài toán tương ứng mà không có lỗi).

Phương pháp này sẽ tự động sinh các ca kiểm thử (bao gồm dữ liệu kiểm thử và giá trị đầu ra mong muốn tương ứng) từ mã nguồn được giáo viên cung cấp. Sau khi LUAN VAN CHAT LUONG download : add [e-mail] 2 hoàn tất quá trình này, giáo viên sẽ có một bộ dữ liệu kiểm thử bao quát hết các nhánh của mã nguồn. Tuy nhiên, phương pháp này [2, 3] chỉ cho phép phát hiện những lỗi tiềm ẩn trong mã nguồn (có đặc tả và được lập trình hoặc không có đặc tả và được lập trình). Phương pháp này không kiểm tra được các lỗi ứng với tình huống có đặc tả và không được lập trình (thường được phát hiện bởi các phương pháp kiểm thử hộp đen).

Phương pháp đề xuất trong [2] mới sinh được các dữ liệu kiểm thử, chưa sinh được đầu ra mong muốn, do đó không hỗ trợ được giáo viên trong việc sinh các ca kiểm thử mẫu. Trong [3] đã sinh được các ca kiểm thử cho mã nguồn Java nhưng chưa hỗ trợ xây dựng hệ thống chấm bài. Mục tiêu của luận văn này là hướng đến nghiên cứu giải pháp và xây dựng bộ công cụ hỗ trợ giáo viên chấm bài lập trình một cách tự động nhằm giải quyết các vấn đề như mô tả ở trên. Mấu chốt của giải pháp này là phương pháp sinh dữ liệu kiểm thử từ mã nguồn.

Bản chất của các phương pháp này là phụ thuộc vào ngôn ngữ lập trình được sử dụng (mỗi ngôn ngữ lập trình thường có kỹ thuật sinh dữ liệu kiểm thử khác nhau vì chúng ta cần phải phân tích mã nguồn). Mặc dù ngôn ngữ lập trình được dùng phổ biến nhất trong các trường Trung học phổ thông là Pascal nhưng ngôn ngữ này chưa có công cụ phân tích cây cú pháp (nền tảng cho việc xây dựng đồ thị dòng điều khiển). Vì vậy, phương pháp sinh dữ liệu kiểm thử từ mã nguồn Pascal rất khó thực hiện trong luận văn này. Ngôn ngữ C/C++ đã được quan tâm nghiên cứu với giải pháp khá tốt trong [2].

Vì vậy, luận văn này tập trung nghiên cứu giải pháp cho ngôn ngữ Java. Phương pháp này có thể sử dụng khi chương trình được viết bằng phương pháp hướng đối tượng. Tuy nhiên, học sinh tại các trường Trung học phổ thông thường viết chương trình theo phương pháp hướng cấu trúc nên giải pháp này không sử dụng được. Cùng với phương pháp này, luận văn cũng sẽ nghiên cứu các kỹ thuật kiểm thử hộp đen nhằm sinh bổ sung các ca kiểm thử cho phương pháp trên.

Một công cụ hỗ trợ cũng sẽ được phát triển và thực nghiệm với một số chương trình đơn giản ở bậc Trung học phổ thông nhằm minh chứng cho kết quả của luận văn. Phần còn lại của đề tài nghiên cứu sẽ gồm những nội dung sau. Chương 2 trình bày tổng quan phương pháp sinh dữ liệu kiểm thử dòng điều khiển từ mã nguồn. Đây là phương pháp chung, có thể áp dụng cho nhiều ngôn ngữ lập trình khác nhau, trong chương này cũng đề xuất phương pháp phân tích mã nguồn Java nhằm sinh ca kiểm thử cho các hàm Java.

Chương 3 giới thiệu công cụ hỗ trợ sinh ca kiểm thử tự động và kết quả thực nghiệm bằng cách áp dụng công cụ, cài đặt với một số chương trình đơn giản. Cuối cùng, kết luận và các hướng nghiên cứu của luận văn sẽ được mô tả trong Chương 4. LUAN VAN CHAT LUONG download : add [e-mail] 3 Chƣơng 2: Phƣơng pháp sinh dữ liệu kiểm thử dòng điều khiển Chương này trình bày tổng quan về phương pháp kiểm thử dòng điều khiển từ đồ thị dòng điều khiển (Control Flow Graph - CFG) của chương trình nhằm sinh ca kiểm thử cho mã nguồn ứng với tiêu chí kiểm thử yêu cầu. Phương pháp trình bày trong chương này có thể áp dụng cho hầu hết các ngôn ngữ lập trình.1 Tổng quan về kiểm thử dòng điều khiển Kiểm thử dòng điều khiển là phương pháp kiểm thử hộp trắng nhằm phát hiện các lỗi tiềm ẩn xảy ra trên mã nguồn [1, 6].

Phương pháp này dựa vào việc phân tích mã nguồn nhằm xây dựng đồ thị dòng điều khiển ứng với các tiêu chí kiểm thử cho trước. Dựa vào đồ thị này, một bộ dữ liệu kiểm thử sẽ được sinh ra đáp ứng 100% tiêu chí kiểm thử yêu cầu. Người sử dụng sẽ sử dụng đặc tả của bài toán để sinh ra các ca kiểm thử từ bộ dữ liệu kiểm thử đã được sinh ra. Bộ ca kiểm thử này sau đó sẽ được sử dụng để làm bộ kiểm thử mẫu thực hiện kiểm thử trên bài tập lập trình của học sinh phục vụ cho quá trình chấm bài.

Mã nguồn Xây dựng CFG Tiêu chí kiểm thử Sinh đường đi kiểm thử Sinh dữ liệu kiểm thử Sinh đầu ra mong muốn Thực thi ca kiểm thử Báo cáo kiểm thử Hình 2. Tổng quan quy trình kiểm thử dòng điều khiển LUAN VAN CHAT LUONG download : add [e-mail] 4 Quy trình kiểm thử dòng điều khiển của một hàm được mô tả như Hình 2. Đầu vào của quy trình là mã nguồn và tiêu chí kiểm thử yêu cầu. Đầu ra của quy trình là báo cáo kiểm thử chứa các kết quả kiểm thử (ca kiểm thử nào phát hiện được lỗi và ca kiểm thử nào không phát hiện được lỗi).

Chi tiết phương pháp bao gồm các bước sau: - Bước 1: Sinh đồ thị dòng điều khiển. Mã nguồn được phân tích dựa trên các tiêu chí kiểm thử để xây dựng đồ thị dòng điều khiển. Với mỗi tiêu chí kiểm thử là phủ câu lệnh, phủ nhánh và phủ điều kiện con, sẽ có một đồ thị dòng điều khiển tương ứng. - Bước 2: Sinh các đường đi kiểm thử.

Từ đồ thị dòng điều khiển, luận văn đề xuất thuật toán duyệt đồ thị sao cho các đường đi kiểm thử được sinh ra đạt độ phủ thỏa mãn các tiêu chí đã đề ra. - Bước 3: Sinh ca kiểm thử. Ca kiểm thử bao gồm bộ giá trị đầu vào được chọn để thực hiện kiểm thử trên mỗi đường đi và giá trị đầu ra mong muốn tương ứng (Expected Output – EO). Ca kiểm thử được sinh ra bằng cách các hệ ràng buộc trên mỗi đường kiểm thử.

Giá trị đầu ra mong muốn được sinh từ đặc tả bài toán. Kết thúc bước này, một tập các ca kiểm thử được sinh ra. - Bước 4: Thực thi các ca kiểm thử. Thực thi các ca kiểm thử nhằm tạo ra báo cáo kiểm thử trong đó chỉ ra ca kiểm thử nào phát hiện được lỗi, ca kiểm thử nào không phát hiện được lỗi.2 Các tiêu chí kiểm thử Tiêu chí kiểm thử là chuẩn mực để đánh giá độ bao phủ của một tập ca kiểm thử so với mã nguồn.

Nhằm tối ưu các ca kiểm thử, tiêu chí kiểm thử được đưa ra để thiết kế các ca kiểm thử sao cho số ca kiểm thử là ít nhất những vẫn có thể kiểm tra được tối đa các trường hợp (có thể mắc lỗi) xảy ra trên mã nguồn. Các thành phần cần kiểm tra bao gồm câu lệnh, các đỉnh quyết định, các điều kiện con, đường thi thành hoặc sự kết hợp giữa chúng [1].