Luận Văn đặc tả và kiểm chứng các phần mềm tương tranh

MỤC LỤC
Chương 1: Giới thiệu . 1
1.1 Nhu cầu thực tếvà lý do thực hiện đềtài 1
1.2 Mục tiêu của đềtài 2
1.3 Nội dung của khóa luận 3
Chương 2: Các khái niệm cơ bản . 4
2.1 Phương pháp mô hình hóa 4
2.2 FSP . 5
2.2.1 Khái niệm FSP . 5
2.2.2 Các thành phần cơ bản trongFSP . 6
2.2.3 Quy trình tuần tự 9
2.3 LTS 11
2.3.1 LTS 11
2.3.2 Deadlock 13
2.3.2.1 Khái niệm . 13
2.3.2.2 Phân tích Deadlock 14
2.3.3 Thuộc tính An toàn . 14
2.3.4 Thuộc tính Liveness . 15
2.4 Công cụLTSA 15
2.5 Kết luận 16
Chương 3: Kiểm chứng thiết kế . 17
3.1 Đặc tảthiết kếbằng FSP . 17
3.3. Kiểm chứng thiết kếbằng LTSA . 23
3.3.1 Giao diện của công cụLTSA 23
3.3.2 Check safety . 24
3.3.3 Check Progress . 25
3.3.4 Compile 25
3.3.5 LTS Analiser 27
3.3.6 LTSA Animator 28
3.4 Kết luận 30
Chương 4: Kiểm chứng cài đặt 31
4.1 Phương pháp đểkiểm chứng cài đặt 31
4.2 Cách chuyển từmã nguồn Java sang FSP . 31
4.3 Ứng dụng đểchuyển mã nguồn bài toán “SingleLandBridge” 34
4.5 Kiểm chứng cài đặt . 36
4.6 Kết luận 41
Chương 5: Kết luận 42
Tài liệu tham khảo . 43