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

DANH MỤC HÌNH VẼ

Hình 1: Các bước thực hiện kiểm thử mô hình. . 4

Hình 2: Mô hình chuyển đổi trạng thái của kitchen timer. 7

Hình 3: Màn hình cửa sổ chính của XSpin. 13

Hình 4: Cửa sổ chức năng Run Slicing algorithm. 14

Hình 5: Cửa sổ chính chức năng Set Simulation Parameters. 15

Hình 6: Cửa sổ khi chạy chức năng Run Simulation. 16

Hình 7: Cửa sổ chính chức năng Set Verification Parameters. 17

Hình 8: Cửa sổ khi chạy chức năng Run Verification. 18

Hình 9: Cửa sổ khi chạy chức năng LTL Property Manager. 19

Hình 10: Cửa sổ khi chạy chức năng View Spin Automaton. 20

Hình 11: Kiến trúc hệ thống kitchen timer. 23

Hình 12: Mô hình máy hữu hạn trạng thái kitchen timer. 24