ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƢỜNG ĐẠI HỌC CÔNG NGHỆ

NGUYỄN THỊ KHÁNH CHI

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

LUẬN VĂN THẠC SĨ
Ngành: Kỹ Thuật Phần Mềm

HÀ NỘI – 2019


ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƢỜNG ĐẠI HỌC CÔNG NGHỆ

NGUYỄN THỊ KHÁNH CHI

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

Ngành: Kỹ Thuật Phần Mềm
Chuyên ngành: Kỹ Thuật Phần Mềm
Mã số: 848 01 03.01

LUẬN VĂN THẠC SĨ
Ngành: Kỹ Thuật Phần Mềm


LỜI CAM ĐOAN ........................................................................................................... vi
DANH MỤC THUẬT NGỮ VIẾT TẮT ......................................................................vii
DANH MỤC HÌNH VẼ .............................................................................................. viii
DANH MỤC BẢNG ....................................................................................................... x
Chương 1: Mở đầu ........................................................................................................... 1
Chương 2: Phương pháp sinh dữ liệu kiểm thử dòng điều khiển .................................... 3
2.1 Tổng quan về kiểm thử dòng điều khiển ..................................................................... 3
2.2 Các tiêu chí kiểm thử .................................................................................................. 4
2.3 Xây dựng đồ thị dòng điều khiển ................................................................................ 6
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 ..... 8
2.3.2. Xây dựng CFG ứng với tiêu chí phủ điều kiện con ............................................... 9
2.3.3. Phương pháp xây dựng CFG từ mã nguồn Java .................................................. 10
2.4. Sinh đường đi kiểm thử từ đồ thị............................................................................. 12
2.4.1. Sinh đường đi thỏa mãn tiêu chí phủ câu lệnh..................................................... 12
2.4.2. Sinh đường đi thỏa mãn tiêu chí phủ nhánh ........................................................ 13
2.4.3. Sinh đường đi thỏa mãn tiêu chí phủ điều kiện con ............................................ 13
2.4.4. Phương pháp sinh đường đi kiểm thử trên đồ thị ................................................ 14
2.5.

Sinh ca kiểm thử từ đường đi ............................................................................. 15

2.5.1. Sinh dữ liệu kiểm thử .......................................................................................... 15
2.5.2. Sinh đầu ra mong muốn ....................................................................................... 17
2.6 . Sinh các ca kiểm thử giá trị biên và vòng lặp.......................................................... 17
2.6.1.Sinh ca kiểm thử giá trị biên ................................................................................. 18
2.6.2. Sinh ca kiểm thử vòng lặp ................................................................................... 19
Chương 3: Công cụ và thực nghiệm .............................................................................. 22


ii

những kiến thức quý báu trong suốt quá trình tôi học tập và nghiên cứu tại trường.
Tôi xin chân thành cảm ơn những người thân trong gia đình, các bạn bè, đồng
nghiệp luôn tạo điều kiện, giúp đỡ động viên tôi trong công tác nghiên cứu khoa học.
Cuối cùng, tôi xin cảm ơn ban giám hiệu trường THPT Ngô Gia Tự - Từ Sơn Bắc Ninh nơi tôi công tác, các đồng nghiệp và các em học sinh khối 11 đã tạo điều
kiện tối đa, đóng góp những nhận xét khách quan cho đề tài nghiên cứu để tôi có thể
hoàn thành luận văn Thạc sỹ tại trường Đại học Công nghệ - Đại học Quốc Gia Hà
Nội.


iv

TÓM TẮT
Luận văn tập trung nghiên cứu phương pháp sinh các ca kiểm thử từ mã nguồn
và ứng dụng trong việc tự động chấm các bài tập lập trình của học sinh viết bằng ngôn
ngữ Java nhằm hỗ trợ các giáo viên Tin học tại các Trường Trung học phổ
thông/Trung học cơ sở trong việc sinh các ca kiểm thử và chấm các bài tập lập trình
của học sinh. Với mỗi bài tập, giáo viên sẽ cung cấp mã nguồn mẫu (mã nguồn không
có lỗi). Dựa vào mã nguồn này, chúng ta sẽ tiến hành phân tích nhằm xây dựng đồ thị
dòng điều khiển của mã nguồn. Tiếp đến, các đường đi của đồ thị ứng với các dòng
điều khiển có thể có của chương trình sẽ được sinh. Từ các đường đi này, chúng ta sẽ
xây dựng hệ ràng buộc chứa các điều kiện của các tham số. Việc sinh dữ liệu kiểm thử
trên đường thực thi chính là việc giải hệ ràng buộc trên đường đi tương ứng. Khi có dữ
liệu kiểm thử, chúng ta sẽ sử dụng đầu ra của mã nguồn chuẩn để sinh giá trị đầu ra
mong muốn tương ứng. Cùng với các ca kiểm thử đã được sinh ra, luận văn còn
nghiên cứu các giải pháp để sinh các ca kiểm thử cho các vòng lặp và sinh các ca kiểm
thử tại các biên của từng tham số ứng với miền giá trị và đặc tả của bài toán.
Luận văn cũng đã tiến hành xây dựng công cụ hỗ trợ và áp dụng thử nghiệm với
các chương trình đơn giản nhằm minh chứng cho tính đúng đắn và tính hiệu quả của
phương pháp đề xuất. Tuy nhiên, công cụ cài đặt chưa được hoàn thiện và cần được
tiếp tục phát triển nhằm có một công cụ hỗ trợ giáo viên như đã nêu ở trên.



vi

LỜI CAM ĐOAN
Tôi xin cam đoan luận văn Thạc sỹ Công nghệ thông tin "Phương pháp sinh dữ
liệu kiểm thử từ mã nguồn và ứng dụng xây dựng hệ thống chấm bài tập lập trình" là
công trình nghiên cứu của tôi dưới sự hướng dẫn của Thầy hướng dẫn, không sao chép
lại của người khác. Trong toàn bộ nội dung luận văn, những điều được trình bày là của
cá nhân tôi hoặc là được tổng hợp từ các nguồn tài liệu khác. Tất cả các nguồn tài liệu
tham khảo đều có trích dẫn cụ thể và hợp pháp.
Tôi xin hoàn toàn chịu trách nhiệm và chịu mọi hình thức kỷ luật theo quy định
của trường Đại học Công Nghệ - Đại học Quốc Gia Hà Nội cho lời cam đoan này.
Hà Nội, ngày 26 tháng 03 năm 2019

Nguyễn Thị Khánh Chi


vii

DANH MỤC THUẬT NGỮ VIẾT TẮT
STT

Từ viết tắt

Từ đầy đủ

Ý nghĩa

1


RO

Real Output

Giá trị đầu ra thực tế

6

SE

Symbolic Excecution

Thực thi tượng trưng

7

SMT-Solver

Satisfiability Modulo Theories
Solver

8

TC

Test Case

Ca kiểm thử


Hình 3.18. Mã nguồn chuẩn của hàm timuscln ............................................................. 40
Hình 3.19. Chi tiết các ca kiểm thử cho tiêu chí phủ nhánh hàm timuscln ...................40


ix
Hình 3.20. Chi tiết các ca kiểm thử phủ tất cả các nhánh hàm timuscln .......................41
Hình 3.21. Mã nguồn hàm timuscnl_1 của học sinh thứ nhất .......................................41
Hình 3.22. Mã nguồn hàm timuscln_2 của học sinh thứ hai .........................................41


x

DANH MỤC BẢNG
Bảng 2.1. Các ca kiểm thử cho tiêu chí phủ câu lệnh của hàm laNamNhuan.................5
Bảng 2.2. Các trường hợp cần kiểm thử với tiêu chí phủ nhánh cho hàm laNamNhuan 5
Bảng 2.3. Các trường hợp cần kiểm thử với tiêu chí phủ điều kiện con của hàm
laNamNhuan ....................................................................................................................6
Bảng 2.4. Các ca kiểm thử cho tiêu chí phủ điều kiện con hàm laNamNhuan ...............6
Bảng 2.5. Dữ liệu kiểm thử cho tiêu chí phủ điều kiện con hàm laNamNhuan ............16
Bảng 2.6. Các ca kiểm thử cho tiêu chí phủ câu lệnh hàm laNamNhuan .....................17
Bảng 2.7. Các ca kiểm thử giá trị biên cho hàm laNamNhuan .....................................18
Bảng 2.8. Các ca kiểm thử cho tiêu chí phủ nhánh hàm giaithua .................................20
Bảng 2.9. Các ca kiểm thử vòng lặp for hàm giaithua ..................................................21
Bảng 3.1. Danh sách tác nhân của hệ thống chấm bài lập trình. ...................................22
Bảng 3.2. Danh sách các ca sử dụng của hệ thống chấm bài lập trình. ......................... 23
Bảng 3.3. Kết quả kiểm thử bài tập kiểm tra năm nhuận của hai học sinh ...................34
Bảng 3.4. Các ca kiểm thử giá trị biên cho hàm laNamNhuan .....................................35
Bảng 3.5. Kết quả kiểm thử giá trị biên bài tập kiểm tra năm nhuận của hai học sinh .35
Bảng 3.6. Kết quả kiểm thử bài tập tính số ngày trong tháng của hai học sinh ............38
Bảng 3.7. Các ca kiểm thử giá trị biên cho hàm songay ...............................................39

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


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.

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.

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


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].
Có rất nhiều tiêu chí kiểm thử được áp dụng trong thực tế, dưới đây là ba tiêu chí
kiếm thử đang được sử dụng rộng rãi [1, 2]:
-

Phủ câu lệnh: Sau khi thực hiện các ca kiểm thử, mỗi dòng lệnh trên mã nguồn
phải được duyệt qua ít nhất một lần. Giả sử, ta cần sinh các ca kiểm thử cho hàm
laNamNhuan có mã nguồn được hiển thị ở Hình 2.2. Để đạt được 100% tiêu chí
phủ câu lệnh cho hàm, ta cần thực hiện ba ca kiểm thử như Bảng 2.1. Giá trị EO
(Expected Output) trên bảng là giá trị đầu ra mong muốn khi chạy ca kiểm thử,
RO (Real Output) là giá trị đầu ra thực tế (giá trị này sẽ được điền khi chạy các ca
kiểm thử trong môi trường thực).


5
public int laNamNhuan(int year) {
if(year

Điều kiện

Đúng

Sai

Year
Tc2
?
?
?

Tc2
Tc3
?
?
?

year%400==0
(Year%4==0)&&(year%100!=0)
year%4==0
year%100!=0

Rõ ràng, các ca kiểm thử ứng với tiêu chí phủ nhánh chỉ kiểm thử được 3/6 ca
kiểm thử (tương ứng với độ phủ đạt 50%) của tiêu chí phủ điều kiện con. Để kiểm tra
tất cả các điểm quyết định cho hàm laNamNhuan, ta cần thực hiện sáu ca kiểm thử
như Bảng 2.4.
Bảng 2.4. Các ca kiểm thử cho tiêu chí phủ điều kiện con của hàm laNamNhuan

STT

Input

EO

Tc1
Tc2


7
lệnh i thì sẽ tồn tại một đường đi từ đỉnh i đến đỉnh j. Mỗi tiêu chí kiểm thử, chúng ta
xây dựng được một CFG tương ứng [1].
Một CFG được xây dựng từ đỉnh bắt đầu (ứng lời khai báo hàm), đi qua các đỉnh
(các câu lệnh khai báo, câu lệnh gán, câu lệnh điều kiện, câu lệnh lặp, các khối xử lý...)
theo thứ tự thực hiện trên mã nguồn và đi đến đỉnh kết thúc (ứng với điểm kết thúc
hàm). Các thành phần để xây dựng CFG được mô tả ở Hình 2.3. [1]

Đỉnh bắt đầu

Đỉnh xử
lý

Đỉnh quyết
định

Đỉnh kết
thúc

Đỉnh
nối

Hình 2.3. Các thành phần cơ bản của đồ thị dòng điều khiển

Ngoài đỉnh bắt đầu và đỉnh kết thúc, mỗi đỉnh là duy nhất trong đồ thị, các đỉnh
khác trong đồ thị tương ứng với một câu lệnh của mã nguồn, được đặt tên theo chức
năng của câu lệnh. Đỉnh xử lý ứng với câu lệnh khai báo, gán giá trị hoặc các câu lệnh
tính toán. Đỉnh quyết định ứng với câu lệnh rẽ nhánh hoặc biểu thức điều kiện trong
câu lệnh lặp. Đỉnh nối là đỉnh tiếp theo được thực hiện ngay sau khi câu lệnh rẽ nhánh

switch…case

Hình 2.4. Các cấu trúc điều khiển cơ bản của đồ thị dòng điều khiển


8

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
Chúng ta sẽ thực hiện xây dựng CFG từ mã nguồn theo các bước như sau: Đầu
tiên, ta đánh số thứ tự cho các câu lệnh trên mã nguồn. Từ đỉnh bắt đầu ứng với lời gọi
hàm ta lần lượt nối các đỉnh theo thứ tự thực hiện câu lệnh trên mã nguồn. [1, 2]. Do
tiêu chí phủ câu lệnh và phủ nhánh có các đường đi phủ toàn bộ các câu lệnh trên mã
nguồn, nên CFG của hai tiêu chí này có hình dạng giống nhau. CFG của tiêu chí phủ
điều kiện con có cấu trúc phức tạp hơn do các đường đi trên đồ thị này phủ đến cả hai
nhánh của các điều kiện con cơ bản.
public int laNamNhuan(int year) {
1. if(year
2.5b. Đây chính là CFG cho tiêu chí phủ câu lệnh và cũng là CFG cho tiêu chí phủ
nhánh.


9

2.3.2 Xây dựng CFG ứng với tiêu chí phủ điều kiện con
Trên các mã nguồn có chứa câu lệnh mang điều kiện phức hợp, chúng ta cần xây
dựng CFG ứng với tiêu chí phủ điều kiện con. Các điều kiện con thuộc điều kiện phức
hợp sẽ được tách các đỉnh con tương ứng trên CFG. Cách xây dựng CFG với tiêu chí
phủ điều kiện con cũng tương tự như xây dựng CFG ứng với tiêu chí phủ câu lệnh.
public int laNamNhuan(int year) {
1.
if(year
(return -1) rồi nối đến đỉnh kết thúc. Nếu điều kiện tại đỉnh 1 (year
2.3.3.2 Xây dựng CFG từ cây cấu trúc trừu tƣợng.
Từ cấu trúc cây AST, chúng ta sử dụng một thuật toán để biến đổi cây AST sang
dạng đồ thị dòng điều khiển, được mô tả ở Thuật toán 2.1.
Thuật toán 2.1: Sinh_G(AST, t)
Đầu vào: AST: cây AST môt tả cấu trúc của hàm cần kiểm thử;
t: tiêu chí kiểm thử
Đầu ra: G: đồ thị dòng điều khiển ứng với độ phủ t,

G là biến toàn cục được khởi tạo là rỗng
1:

for (mỗi nút c trên cây AST)

2:

if (c là đỉnh quyết định)

3:

node := đỉnh đại diện cho c

4:

Cập nhật node vào G

5:

Liên kết node với các đỉnh của G

6:


14:

c_AST :=cây AST của nhóm lệnh c

15:

Sinh_G(c, t)

16:

else

17:

node := đỉnh đại diện cho c

18:

cập nhật node vào G

19:

Liên kết node với các đỉnh của G

20:

endif

21:

nó được tính bằng số đỉnh quyết định của CFG tương ứng cộng 1 hoặc bằng số cạnh
trừ số đỉnh của CFG tương ứng cộng 2.

2.4.1 Sinh đƣờng đi thỏa mãn tiêu chí phủ câu lệnh
Để sinh các đường kiểm thử thỏa mãn tiêu chí phủ câu lệnh từ CFG tương ứng,
chúng ta tìm các đường đi sao cho mỗi đỉnh được "ghé thăm" ít nhất một lần (đồng
nghĩa với mỗi câu lệnh được duyệt qua ít nhất một lần).
Ví dụ, ta cần sinh đường kiểm thử thỏa mãn tiêu chí phủ câu lệnh cho hàm
laNamNhuan có CFG được hiển thị ở Hình 2.7. Trên đồ thị, ta xác định được ba
đường đi để mỗi đỉnh của đồ thị được đi qua ít nhất một lần, các đường được liệt kê
như sau:
p1: 1(T), 2
p2: 1(F), 3(T), 4
p3: 1(F), 3(F), 5