Thạc Sĩ Kiểm tra mô hình phần mềm sử dụng lý thuyết Ôtômat Buchi và Logic thời gian tuyến tính

MỤC LỤC
LỜI CẢM ƠN . 1
LỜI CAM ĐOAN . 2
MỤC LỤC . 3
DANH MỤC CÁC TỪVIẾT TẮT 6
DANH MỤC CÁC HÌNH VẼ, ĐỒTHỊ . 7
LỜI MỞ ĐẦU . 8
CHƯƠNG I: TỔNG QUAN VỀKIỂM TRA MÔ HÌNH PHẦN MỀM . 12
1.1 Lịch sửphát triển 12
1.2 Kiểm tra mô hình phần mềm . 15
1.2.1 Khái niệm kiểm tra mô hình 15
1.2.2 Kiểm tra mô hình phần mềm . 15
1.3 Phân loại hướng tiếp cận kiểm tra mô hình phần mềm 19
1.3.1 Cách tiếp cận động . 19
1.3.2 Cách tiếp cận tĩnh . 19
1.3.4 Kết hợp giữa hai cách tiếp cận tĩnh và động 19
1.4 Kiểm tra mô hình phần mềm cổ điển và hiện đại . 20
1.5 Kết luận chương 22
CHƯƠNG 2: CÁC KỸTHUẬT KIỂM TRA MÔ HÌNH PHẦN MỀM . 23
2.1 Giới thiệu . 23
2.2 Phương pháp ký hiệu biểu diễn 25
2.3 Phương pháp duyệt nhanh . 28
2.4 Phương pháp rút gọn . 30
2.4.1 Rút gọn bậc từng phần . 30
2.4.2 Tối thiểu hoá kết cấu 32
2.4.3 Trừu tượng hoá . 33
2.5 Kỹthuật xác thực kết cấu 35
2.6 Kết luận chương 36
CHƯƠNG 3: KỸTHUẬT KIỂM TRA MÔ HÌNH PHẦN MỀM SỬDỤNG
LÝ THUYẾT LOGIC THỜI GIAN TUYẾN TÍNH VÀ ÔTÔMAT BUCHI 37
3.1 Bài toán kiểm tra mô hình phần mềm . 37
3.2 Mô hình hoá hệthống phần mềm 38
3.2.1 Vấn đề đặt ra 38
3.2.2. Hệthống đánh nhãn dịch chuyển 39
3.2.2.1 Các định nghĩa . 39
3.2.2.2 Áp dụng mô hình hoá chương trình 40
3.3 Đặc tảhình thức các thuộc tính của hệthống . 43
3.3.1. Vấn đề đặt ra . 43
3.3.2. Logic thời gian 44
3.3.3. Logic thời gian tuyến tính (Linear TemporalLogic - LTL) . 44
3.3.3.1 Thuộc tính trạng thái . 45
3.3.3.2. Cú pháp LTL 46
3.3.3.3. Ngữnghĩa của LTL 46
3.3.4 Logic thời gian nhánh (Branching Temporal Logic - BTL) 50
3.4 Ôtômat đoán nhận các xâu vô hạn . 51
3.4.1 Một sốkhái niệm ôtômat cổ điển: 51
3.4.2 Ôtômat Buchi . 53
3.5 Chuyển đổi từLTL sang Ôtômat Buchi . 55
3.5.1 Tổng quan . 55
3.5.2 Chuẩn hoá vềdạng LTL chuẩn 56
3.5.3 Biểu thức con . 56
3.5.4 Chuyển đổi từLTL sang Ôtômat Buchi 57
3.5.4.1 Giải thuật chuyển đổi từLTL sang Ôtômat Buchi . 57
3.5.4.2. Ví dụ . 60
3.6 Chuyển từhệthống chuyển trạng thái sang Ôtômat Buchi 64
3.7 Tích chập của hai Ôtômat Buchi . 66
3.7.1 Ôtômat Buchi dẫn xuất 66
3.7.2 Nguyên tắc thực hiện . 66
3.8 Kiểm tra tính rỗng của ngôn ngữ được đoán nhận bởi Ôtômat Buchi 68
3.9 Kết luận chương 70
CHƯƠNG 4: XÂY DỰNG HỆTHỐNG ĐỂKIỂM TRA MÔ HÌNH PHẦN
MỀM . 72
4.1 Giới thiệu vềmô hình SPIN 72
4.2 Cấu trúc SPIN . 73
4.3 Ngôn ngữPROMELA . 76
4.3.1 Giới thiệu chung vềPromela 76
4.3.2 Mô hình một chương trình Promela . 77
4.3.5 Tiến trình khởi tạo 78
4.3.6 Khai báo biến và kiểu . 78
4.3.7 Câu lệnh trong Promela 79
4.3.8 Cấu trúc atomic 81
4.3.9 Các cấu trúc điều khiển thường gặp . 81
4.3.9.1 Câu lệnh điều kiện IF 81
4.3.9.2 Câu lệnh lặp DO 82
4.3.10 Giao tiếp giữa các tiến trình . 83
4.3.10.1 Mô hình chung 83
4.3.10.2 Giao tiếp giữa các tiến trình kiểu bắt tay 85
4.4 Cú pháp của LTL trong SPIN . 86
4.5 Minh hoạkiểm tra mô hình phần mềm với SPIN . 86
KẾT LUẬN . 95
TÀI LIỆU THAM KHẢO . 98