ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
Đoàn Trung Kiên
KIỂM THỬ DỰA TRÊN MÔ HÌNH
KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY

Ngành: Công nghệ thông tin
HÀ NỘI - 2010

ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
Đoàn Trung Kiên
KIỂM THỬ DỰA TRÊN MÔ HÌNH
KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY

Ngành: Công nghệ thông tin
Cán bộ hướng dẫn: TS. Phạm Ngọc Hùng
Cán bộ đồng hướng dẫn: ThS. Đặng Việt Dũng
HÀ NỘI - 2010

Kiểm thử dựa trên mô hình Đoàn Trung Kiên
LỜI CẢM ƠN
Lời đầu tiên em xin bày tỏ lòng biết ơn sâu sắc tới TS. Phạm Ngọc Hùng và ThS.
Đặng Việt Dũng, các thầy đã hướng dẫn em tận tình trong suốt năm học vừa qua.
Em xin bày tỏ lòng biết ơn tới các thầy, cô giáo trong Khoa Công nghệ thông
tin - Trường Đại học Công nghệ - ĐHQGHN. Các thầy cô đã dạy bảo, chỉ dẫn em và
luôn tạo điều kiện tốt nhất cho em học tập trong suốt quá trình học đại học đặc biệt là
trong thời gian làm khoá luận tốt nghiệp.
Con xin chân thành cảm ơn Ông Bà, Cha Mẹ đã luôn động viên, ủng hộ vật
chất lẫn tinh thần trong suốt thời gian qua.
Tôi xin cảm ơn sự quan tâm, giúp đỡ và ủng hộ của anh chị, bạn bè, đặc biệt

LỜI CẢM ƠN.............................................................................................................i
TÓM TẮT.................................................................................................................ii
1.1 Đặt vấn đề........................................................................................................1
1.2 Nội dung nghiên cứu của khóa luận..................................................................1
1.3 Cấu trúc khóa luận............................................................................................1
2.1 Khái niệm kiểm thử dựa trên mô hình ..............................................................3
2.2 Các bước thực hiện...........................................................................................3
2.3 Thuận lợi và khó khăn của kiểm thử dựa trên mô hình......................................4
Thuận lợi................................................................................................................4
Khó khăn................................................................................................................5
Mặc dù có nhiều thuận lợi nhưng bên cạnh đó cũng có những trở ngại nhất định
của kiểm thử dựa trên mô hình:..............................................................................5
Do phải xây dựng mô hình của hệ thống vì vậy người kiểm thử phần mềm phải yêu
cầu là những người có khả năng phân tích và thiết kế hệ thống..............................5
Trong kiểm thử dựa trên mô hình công việc quan trọng nhất là xây dựng mô hình.
Người kiểm thử phải đầu tư đáng kể cả về thời gian, trí tuệ và tiền bạc cho việc
xây dựng mô hình hệ thống....................................................................................5
Giống như các phương pháp kiểm thử khác, việc kiểm thử dựa trên mô hình chỉ
phát hiện được lỗi của hệ thống mà không thể phát hiện được hệ thống còn lỗi hay
không. 5
2.4 Máy hữu hạn trạng thái ( Finite State Machines )..............................................5
Trong kiểm thử phần mềm có nhiều kiểu mô hình được sử dụng như : Finite State
Machines, UML, Grammars, ... Trong nghiên cứu này trình bày về mô hình máy
hữu hạn trạng thái: Finite State Machines...............................................................5
Một máy trạng thái mô tả cho hệ thống phần mềm được định nghĩa dựa vào ( I,
S, T, F, L), trong do:...............................................................................................5
I : Tập hợp các yếu tố đầu vào của hệ thống.........................................................6
iii
Kiểm thử dựa trên mô hình Đoàn Trung Kiên
S : Tập các trạng thái của hệ thống.......................................................................6

Một mảng có cấu trúc như sau:............................................................................10
int table[max].......................................................................................................10
iv
Kiểm thử dựa trên mô hình Đoàn Trung Kiên
Lưu ý rằng điều này tạo ra một mảng max-1 số nguyên: .....................................10
table[0], table[1], ... table[max-1]........................................................................10
Kiểu liệt kê...........................................................................................................10
3.1.3 Định danh, Hằng số và Biểu thức.................................................................10
Định danh.............................................................................................................10
Định danh có thể là một chữ cái, một ký tự.........................................................10
Hằng số 10
Hằng số là một chuỗi ký tự đại diện cho một số nguyên thập phân. Hằng số tượng
trưng có thể được định nghĩa như sau:..................................................................10
#define MAX 999...............................................................................................10
Biểu thức..............................................................................................................10
3.1.4 Tiến trình.....................................................................................................10
3.2 Công cụ Spin..................................................................................................11
3.2.1 Sơ lược về Spin...........................................................................................11
3.2.2 Công cụ XSpin............................................................................................12
4.1 Phương pháp sinh các ca kiểm thử tự động.....................................................21
char tempLable[256] ="FIRST";................................................................21
char tempInput[256] = "";.....................................................................................21
char tempOutput[256] = "";..........................................................................21
Node tempNode = {"FIRST","",""};............................................................21
void setNode(char* cur_label, char* cur_input, char* cur_output) {............21
strcpy(tempNode.label,cur_label);........................................................................22
strcpy(tempNode.input, cur_input);......................................................................22
strcpy(tempNode.output, cur_output);..................................................................22
} 22
void printNode(Node n) {.....................................................................................22

Từ những thông số kỹ thuật được mô tả ở trên chúng ta xây dựng được mô hình
máy trạng thái của Kitchen Timer như hình vẽ sau...............................................23
24
Hình 12: Mô hình máy hữu hạn trạng thái kitchen timer.......................................24
Bộ 24
Yếu tố 24
Ý nghĩa 24
Nhãn 24
NUMINPUT.........................................................................................................24
COUNTDOWN....................................................................................................24
PAUSE 24
vi
Kiểm thử dựa trên mô hình Đoàn Trung Kiên
ALARM24
ALARMOFF........................................................................................................24
Thiết lập thời gian................................................................................................24
Đếm ngược...........................................................................................................24
Tạm dừng.............................................................................................................24
Báo giờ 24
Ngừng báo giờ......................................................................................................24
Biến 24
in_t 24
t 24
alarm_t 24
bTimeClk.............................................................................................................24
Biến đại diện cho thời gian thiết lập.....................................................................24
Biến đại diện cho thời gian đếm ngược................................................................24
Biến đại diện cho thời gian báo chuông................................................................24
Biến đại diện cho hoạt động chu kỳ......................................................................24
Đặt biểu tượng đầu vào........................................................................................25

proctype Timer() {................................................................................................25
mtype evt;.............................................................................................................25
/*-------------------------------------------------------------------*/.................................25
/* Thiet lap thoi gian */........................................................................................25
NUMINPUT_ST:.................................................................................................25
printf("TIMER: ST NUMINPUT\n");.................................................................25
NUMINPUT:.......................................................................................................25
c_code{ 25
strcpy(tempLabel,"NUMINPUT");......................................................................26
setNode(tempLabel,now.in_time,now.time,now.alm_time,now.bTimeClk,tempInp
ut,tempOutput);....................................................................................................26
printNode(tempNode);.........................................................................................26
}; 26
GetEvtTimer(evt);................................................................................................26
if 26
::evt==TIMER_CLK ->........................................................................................26
atomic{ 26
MUSI; 26
c_code{..............................................................................................................26
strcpy(tempInput,"TIME_CLK");......................................................................26
strcpy(tempOutput, "");.....................................................................................26
viii
Kiểm thử dựa trên mô hình Đoàn Trung Kiên
} 26
} 26
::evt==xTIME_SET -> ........................................................................................26
IncInTime(); .......................................................................................................26
atomic {26
printf("NumDsp.\n");..........................................................................................26
c_code{..............................................................................................................26

Đoạn mã mô tả tiến trình Environment.................................................................28
/* Tien trinh Environment */................................................................................28
proctype Environment(){......................................................................................28
do 28
::true -> SetEvtTimer(xTIME_SET);....................................................................28
::true -> SetEvtTimer(xSTART);..........................................................................28
::true -> 28
if 28
::bTimeClk==1 -> SetEvtTimer(TIMER_CLK);..................................................28
::bTimeClk==0 -> ;..............................................................................................28
fi 28
od 28
} 28
Bởi vì kiểu dữ liệu mới này được tham chiếu tới các khai báo khác, vì vậy chúng
ta phải chắc chắn rằng định nghĩa của nó được đặt đầu đoạn mã mô hình Promela.
Đoạn mã c_decl chỉ để định nghĩa kiểu dữ liệu mới C trong Promela...................28
Đoạn mã định nghĩa dữ liệu Node......................................................................28
Đoạn mã sau có nhiệm vụ thiết lập các thông số cho dữ liệu kiểu Node và in ra
input, output và các trạng thái cùng các thông số của nó.......................................29
Đoạn mã lưu các trạng thái vào Node và in ra Node...........................................29
c_code{ 29
char tempLabel[256] = "NUMINPUT";................................................................29
char tempInput[256] = "";.....................................................................................29
char tempOutput[256] = "";..................................................................................29
Node tempNode = {"NUMINPUT",0,0,0,0,"",""};...............................................29
void setNode(char* cur_label, int cur_in_time, int cur_time, int cur_alm_time,
unsigned cur_bTimeClk, char* cur_input, char* cur_output) {.............................29
strcpy(tempNode.label,cur_label);........................................................................29
tempNode.in_time = cur_in_time;........................................................................29
tempNode.time = cur_time;..................................................................................29

Phụ lục B: Một số ca kiểm thử.................................................................................42
TÀI LIỆU THAM KHẢO........................................................................................44
DANH MỤC HÌNH VẼ
Đoàn Trung Kiên ....................................................................................................... 1
xi
Kiểm thử dựa trên mô hình Đoàn Trung Kiên
Đoàn Trung Kiên ........................................................................................................ i
LỜI CẢM ƠN.............................................................................................................i
TÓM TẮT.................................................................................................................ii
Phụ lục A: Đặc tả của kitchen timer bằng promela có nhúng mã C ..........................33
Phụ lục B: Một số ca kiểm thử.................................................................................42
TÀI LIỆU THAM KHẢO........................................................................................44
xii
Kiểm thử dựa trên mô hình Đoàn Trung Kiên
CHƯƠNG 1
GIỚI THIỆU
1.1 Đặt vấn đề
Trong các công ty phát triển phần mềm hầu hết công việc kiểm thử của kiểm
thử viên được thực hiện thủ công bằng tay. Trong khi đó số lượng tình huống kiểm
tra quá nhiều mà các kiểm thử viên không thể hoàn tất bằng tay trong thời gian cụ thể
nào đó. Hoặc khi nhóm lập trình đưa ra nhiều phiên bản phần mềm liên tiếp để kiểm
tra. Thực tế cho thấy việc đưa ra các phiên bản phần mềm có thể là hàng ngày, mỗi
phiên bản bao gồm những tính năng mới, hoặc tính năng cũ được sửa lỗi hay nâng
cấp. Việc bổ sung hoặc sửa lỗi code cho những tính năng ở phiên bản mới có thể làm
cho những tính năng khác đã kiểm tra tốt chạy sai mặc dù phần code của nó không hề
chỉnh sửa. Để khắc phục điều này, đối với từng phiên bản, kiểm thử viên không chỉ
kiểm tra chức năng mới hoặc được sửa, mà phải kiểm tra lại tất cả những tính năng
đã kiểm tra tốt trước đó. Điều này khó khả thi về mặt thời gian nếu kiểm tra thông
thường. Để giải quyết vấn đề này chúng ta áp dụng kỹ thuật kiểm thử dựa trên mô
hình cho quá trình sinh các ca kiểm thử tự động .

CHƯƠNG 2
CƠ SỞ LÝ THUYẾT CHO KIỂM THỬ MÔ HÌNH
Quá trình thiết kế mô hình của hệ thống bằng ngôn ngữ mô hình Promela làm
việc dựa trên các khái niệm về kiểm thử mô hình. Chương này sẽ lần lượt trình bày
những khái niệm cơ bản về kiểm thử mô hình.
2.1 Khái niệm kiểm thử dựa trên mô hình
Theo Colin Campbell, kiểm thử dựa trên mô hình là một kỹ thuật kiểm thử mà
các hoạt động của hệ thống được chạy thử trong một thời gian sẽ được dự đoán
trước, nó được thực hiện bởi một đặc tả hình thức hoặc một mô hình của hệ thống.
Các mẫu thiết kế hay mô hình là mô tả đơn giản của hệ thống dựa trên yêu cầu
hệ thống và chức năng xác định, giúp chúng ta có thể hiểu và dự đoán được hành vi
của hệ thống.
2.2 Các bước thực hiện
Quá trình kiểm thử dựa trên mô hình được bắt đầu bằng việc xác định yêu cầu
của hệ thống từ đó xây dựng mô hình dựa vào các yêu cầu và chức năng của hệ
thống. Việc xây dựng mô hình còn phải dựa trên các yếu tố dữ liệu đầu vào và đầu ra.
Mô hình này được sử dụng để sinh ra các ca kiểm thử. Chúng ta có thể biết kết quả
đầu ra mong đợi từ mô hình hoặc từ quy định chuẩn ( oracle ). Khi chạy kịch bản và
kết quả thu được sẽ được so sánh với kết quả mong đợi. Từ đó quyết định hành động
tiếp theo như sửa đổi mô hình hoặc dừng kiểm thử,…
Các bước để thực hiện kiểm thử dựa trên mô hình:
• Xây dựng mô hình dựa trên các yêu cầu và chức năng của hệ thống.
• Tạo đầu ra dự kiến từ mô tả bài toán.
• Chạy kịch bản kiểm thử.
• So sánh kết quả đầu ra thực tế với kết quả đầu ra dự kiến.
• Quyết định hành động tiếp theo (Sửa đổi mô hình, tạo thêm ca kiểm thử,
dừng kiểm thử, đánh giá chất lượng của phần mềm )
Các bước thực hiện kiểm thử dựa trên mô hình được minh họa bằng sơ
đồ sau:
3

trên mô hình. Việc thay đổi các ca kiểm thử chỉ việc thay đổi mô
hình của hệ thống.
 Có khả năng đánh giá chất lượng phần mềm.
•Khó khăn
Mặc dù có nhiều thuận lợi nhưng bên cạnh đó cũng có những trở ngại
nhất định của kiểm thử dựa trên mô hình:
 Do phải xây dựng mô hình của hệ thống vì vậy người kiểm thử
phần mềm phải yêu cầu là những người có khả năng phân tích và
thiết kế hệ thống.
 Trong kiểm thử dựa trên mô hình công việc quan trọng nhất là xây
dựng mô hình. Người kiểm thử phải đầu tư đáng kể cả về thời gian,
trí tuệ và tiền bạc cho việc xây dựng mô hình hệ thống.
 Giống như các phương pháp kiểm thử khác, việc kiểm thử dựa trên
mô hình chỉ phát hiện được lỗi của hệ thống mà không thể phát hiện
được hệ thống còn lỗi hay không.
2.4 Máy hữu hạn trạng thái ( Finite State Machines )
Trong kiểm thử phần mềm có nhiều kiểu mô hình được sử dụng như : Finite
State Machines, UML, Grammars, ... Trong nghiên cứu này trình bày về mô hình
máy hữu hạn trạng thái: Finite State Machines.
Một máy trạng thái mô tả cho hệ thống phần mềm được định nghĩa dựa vào
( I, S, T, F, L), trong do:
5
Kiểm thử dựa trên mô hình Đoàn Trung Kiên
I : Tập hợp các yếu tố đầu vào của hệ thống.
S : Tập các trạng thái của hệ thống.
T : Tập hợp hàm chuyển đổi trạng thái khi đầu vào là một trạng thái cụ thể.
F : Tập hợp các trạng thái kết thúc.
L : Trạng thái ban đầu của hệ thống.
2.5 Bài toán Kitchen Timer
Chúng ta sẽ dựa vào các khái niệm của máy hữu hạn trạng thái để xây dựng

Thiết
lập
Đếm
ngược
Chờ
Thiết lập
thời gian
Đếm ngược
Tạm dừng
Tiếp tục
Tạm
dừng
Đếm ngược kết
thúc
Kiểm thử dựa trên mô hình Đoàn Trung Kiên
CHƯƠNG 3
GIỚI THIỆU PROMELA VÀ SPIN
Chương này chúng ta sẽ biết cách sinh các ca kiểm thử một cách tự động bằng
công cụ Spin. Để có thể làm việc được với Spin chúng ta phải xây dựng mô hình của
hệ thống bằng ngôn ngữ Promela. Chương này sẽ lần lượt trình bày những khái niệm
cơ bản về ngôn ngữ mô hình Promela, công cụ Spin, và giao diện người dùng XSpin.
3.1 Ngôn ngữ Promela
Xây dựng mô hình hệ thống bằng ngôn ngữ Promela là một công đoạn quan
trọng trong kiểm thử dựa trên mô hình, để từ đó có thể dùng công cụ Spin sinh ra các
ca kiểm thử. Ngôn ngữ mô hình Promela có nhiều nét tương đồng với ngôn ngữ C.
3.1.1 Khái niệm cơ bản
•Định nghĩa Promela (Process meta language )
Promela là ngôn ngữ mô hình dùng để mô tả hệ thống đồng thời [The Spin
Model Checker: Primer and Reference Manual].
Ví dụ: Giao thức mạng, hệ thống điện thoại, các chương trình giao tiếp đa

ngôn ngữ lập trình C. Theo mặc định tất cả các biến của các loại biến cơ bản được
bắt đầu từ 0. Cũng như trong C thì 0 được coi như sai và khác 0 được coi là đúng.
Một biến có thể là biến toàn cục hoặc là biến địa phương của mỗi tiến trình.
•Kiểu dữ liệu
Type Domain
bit or bool { 0, 1}
byte 0…255
short -2
15
… 2
15
- 1
int -2
31
… 2
31
– 1
•Kiểu khai báo
int ii;
bit bb;
bb = 1;
ii = 2;
•Kiểu cấu trúc
Records (structs): Có thể tìm ra xung đột khi chạy
Typedef record{
short f1;
byte f2;
}
Truy cập như C
Record rr;