Luận Văn NGHIÊN CỨU ĐẶC TẢ VÀ KIỂM CHỨNG PHẦN MỀM SỬ DỤNG CafeO

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 . 2
Chương 2. Phương pháp hình thức 3
2.1 Phân loại . 3
2.2 Sửdụng . 4
2.2.1 Đặc tảhình thức 4
2.2.2 Phát triển 5
2.2.3 Kiểm chứng 5
2.2.3.1 Chứng minh của con người . 5
2.2.3.1 Chứng minh tựđộng . 6
Chương 3. Ngôn ngữCafeOBJ . 7
3.1 Giới thiệu 7
3.2 Đặc tảvà kiểm chứng trong CafeOBJ 9
3.2.1 Ví dụ . 9
3.2.2 Đặc tảsốtựnhiên . 10
3.2.3 Đặc tảthuộc tính . 10
3.2.4 Kiểm chứng thuộc tính 10
Chương 4. Khái quát vềOTS và bài toán QLOCK 13
4.1 Giới thiệu vềOTS . 13
4.2 OTS (Observation transition system) . 14
4.3 Mô tảbài toán QLOCK . 17
4.4 Đặc tảQLOCK với OTS . 17
4.5 Đặc tảthuộc tính và kiểm chứng đặc tả . 21
Chương 5. Đặc tảvà kiểm chứng hệthống lò vi sóng . 24
5.1 Hệthống lò vi sóng . 24
5.1.1 Mô tảhệthống 24
5.1.2 Mô tảcác thuộc tính 26
5.2 Mô hình hóa hệthống trong OTS/CafeObj 26
5.2.1 Mô hình hóa và mô tảhệthống trong OTS 26
5.2.2 Đặc tảhình thức hệthống trong CafeObj 28
5.2.3 Không gian trạng thái của hệthống đặc tảhình thức . 29
5.2.4 Các thuộc tính được mô tả 29
5.3 Kiểm chứng bằng phươngpháp quy nạp 33
5.3.1 Các bước quy nạp . 33
5.3.2 Kiểm chứng bằng phương pháp quy nạp trong CafeOBJ . 33
5.4. Kiểm chứng bằng phương pháp tìm kiếm trạng thái . 33
Chương 6. Kết luận . 36