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 trong FSP 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 26

3.3.6 LTSA Animator 28

3.4 Kết luận 29

Chương 4: Kiểm chứng cài đặt 30

4.1 Phương pháp để kiểm chứng cài đặt 30

4.2 Cách chuyển từ mã nguồn Java sang FSP 30

4.3 Ứng dụng để chuyển mã nguồn bài toán “SingleLandBridge” 33

4.5 Kiểm chứng cài đặt 35

4.6 Kết luận 40

Chương 5: Kết luận 41

Tài liệu tham khảo 42