Luận Văn Kiểm thử dựa trên mô hình

MỤC LỤC
CHƯƠNG 1 GIỚI THIỆU .1
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
CHƯƠNG 2 CƠ SỞLÝ THUYẾT CHO KIỂM THỬMÔ HÌNH .3
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
2.4 Máy hữu hạn trạng thái ( Finite State Machines ) 5
2.5 Bài toán Kitchen Timer .6
2.5.1 Miêu tảbài toán .6
2.5.2 Xây dựng mô hình .6
CHƯƠNG 3 GIỚI THIỆU PROMELA VÀ SPIN 8
3.1 Ngôn ngữPromela 8
3.1.1 Khái niệm cơ bản .8
3.1.2 Biến và Kiểu 9
3.1.3 Định danh, Hằng sốvà Biểu thức . 10
3.1.4 Tiến trình . 11
3.2 Công cụSpin 12
3.2.1 Sơ lược vềSpin 12
3.2.2 Công cụXSpin . 12
CHƯƠNG 4 SINH CA KIỂM THỬTỰĐỘNG VÀ THỰC NGHIỆM . 21
4.1 Phương pháp sinh các ca kiểm thửtựđộng . 21
4.2 Ví dụáp dụng 22
4.2.1 Mô tảbài toán 23
4.2.2 Máy hữu hạn trạng thái của Kitchen Timer 23
4.2.3 Đặc tảkitchen timer bằng promela có nhúng mã C 24
4.2.4 Kết quả 30
CHƯƠNG 5 KẾT LUẬN 32
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
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
traquá nhiều mà các kiểm thửviênkhô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ềmliê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ềmcó 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ênmô hình choquá trìnhsinh các cakiểm thửtựđộng .
Do đó, khoá luận này tập trung trình bày vềviệc nghiên cứu kiểm thửdựa
trênmô hình và ứng dụng công cụSpinvào việc tựđộng sinh các ca kiểm thử: Xây
dựng mô hìnhhệthống và thực nghiệm.
1.2 Nội dung nghiên cứu của khóa luận
Bài toán thực hiện trong khóa luận này là bài toán kiểm thửdựa trên mô hình
để sinh ra các ca kiểm thử một cách tự động. Thiết kế hệ thống bằng ngôn ngữ
Promela và nhúng mã C vào thiết kếPromela là hainội dung quan trong nhất của
quátrình sinh ca kiểm thửtựđộng. Tôi nghiên cứu phương pháp được sửdụng để
thực hiện các nội dung đó, và áp dụng nó vào bài toán sinh ca kiểm thửtựđộng của
hệthống máy hẹn giờkitchen timer.
Quá trình thực nghiệm sẽ bao gồm các thực nghiệm về thiết kế hệ thống
kitchen timer bằng Promela, nhúng mã nguồn Cvào thiết kếPromela của hệthống
và sửdụng Spin sinh các ca kiểm thửmột cách tựđộng.
1.3 Cấu trúc khóa luận
Các phần còn lại của khóa luận có cấu trúc như sau:
Chương 2 trình bày cơ sởlý thuyết của kiểm thửmô hình, bao gồm các khái
niệm cơ bản, cácbước thực hiện, lợi ích của kiểm thửmô hình và cách thức xây
dựng mô hình (máy hữu hạn trạng thái).
Chương 3 trình bày các khái niệm vềngôn ngữmô hình promela, bao gồm
các định nghĩa cơ bản vềkhai báo biến và kiểu, định danh, hằng số, biểu thức,
tiến trình.
Chương 4 trình bày vềcác kết quảthực nghiệm của quá trình mô tảmáy hẹn
giờ kitchen timer, thiết kế mô hình hệ thống kitchen timer bằng Promela, và quá
trình sinh ca kiểm thửtựđộng.
Chương 5 tóm tắt các kết quảđã đạt được, kết luận, những hạn chếvà hướng
nghiên cứu phát triển trong tương lai.