TÓM TẮT

Quá trình sinh các ca kiểm thử tự động dựa trên mô hình gồm các công đoạn chính: Xây dựng mô hình, nhúng mã C, áp dụng công cụ Spin để sinh các ca kiểm thử. Trong đó xây dựng mô hình là công đoạn đầu tiên, nhiệm vụ chính ở đây là từ mô tả các yêu cầu của hệ thống và chức năng xác định cùng với dữ liệu đầu vào và ra phải xây dựng được mô hình của hệ thống. Xây dựng mô hình có vai trò hết sức quan trọng, nếu việc xây dựng mô hình không chính xác thì các công đoạn về sau trong hệ thống kiểm thử dựa trên mô hình không thể chính xác được. Do tầm quan trọng đó của việc xây dựng mô hình, khóa luận này đề cập tới các lý thuyết cơ bản về xây dựng mô hình của hệ thống bằng ngôn ngữ mô hình promela.

Trong khóa luận này tôi trình bày phương pháp nhúng mã nguồn C vào trong mô tả promela để lọc các trạng thái và sinh các ca kiểm thử một cách tự động bằng công cụ hỗ trợ kiểm thử Spin. Từ đó áp dụng các kỹ thuật trên vào bài toán cụ thể kitchen timer.

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

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 .

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ên mô hình và ứng dụng công cụ Spin vào việc tự động sinh các ca kiểm thử: Xây dựng mô hình hệ 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à hai nộ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 C và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ác bướ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