Luận Văn Kiểm chứng đặt tả uml cho tác tử phần mềm

Mục lục
Chương 1. Mở đầu 1
1.1 Đặt vấn đề 1
1.2 Nội dung bài toán . 2
1.3 Tổng quan phương pháp “Kiểm chứng đặc tả UML cho tác tử phần
mềm” . 3
1.4 Cấu trúc khóa luận . 4
Chương 2. Giới thiệu lập trình hướng khía cạnh (Aspect-Oriented Programming)
và AspectJ . 6
2.1 Phương pháp lập trình hướng khía cạnh 6
2.1.1 Sự hạn chế của lập trình hướng đối tượng (OOP) . 6
2.1.2 Lập trình hướng khía cạnh (AOP) . 9
2.2 AspectJ . 12
2.2.1 Join point . 12
2.2.2 Pointcut 12
2.2.3 Advice . 13
2.2.4 Aspect 14
2.2.5 Cơ chế họa động của AspectJ 15
2.3 Sử dụng AOP Phát triển ứng dụng và phương pháp kiểm chứng dựa
trên AOP . 15
2.4 Kết luận 17
Chương 3. Agent UML và JADE framework . 18
3.1 Ngôn ngữ mô hình hóa UML 18
3.1.1 Khái niệm 18
3.1.2 Biểu đồ trạng thái (State Diagram) . 18
3.1.3 Biểu đồ trình tự (Sequence Diagram) . 19
3.2 XML (eXtensible Markup Language) . 20
3.2.1 Cơ bản về XML . 20
3.2.2 XML DOM 22
3.3 XMI (XML Metadata Interchange) . 24
3.4 AUML (Agent UML) 25
3.4.1 Tác tử phần mềm là gì? . 25
3.4.2 Phần mềm hướng Agent 26
3.4.3 AUML (Agent Unified Modeling Language) . 28
3.5 Java Agent DEvelopment Framework (JADE) . 31
3.5.1 Khái niệm về JADE . 31
3.5.2 Cấu trúc của JADE platform . 32
3.5.3 Một số lớp quan trọng trong thư viện JADE . 33
3.6 Kết luận 34
Chương 4. Xây dựng máy trạng thái từ biểu đồ UML . 35
4.1 Biểu đồ trạng thái . 35
4.1.1 Quy tắc biểu diễn giao thức bằng biểu đồ trạng thái . 35
4.1.2 Xây dựng cấu trúc dữ liệu mô tả biểu đồ trạng thái UML 36
4.1.3 Xây dựng FSM mô tả biểu đồ trạng thái UML . 40
4.2 Biểu đồ trình tự UML 42
4.2.1 Cách biểu diễn giao thức giữa nhiều đối tượng bằng biểu đồ trình tự
UML . 42
4.2.2 Xây dựng cấu trúc dữ liệu mô tả biểu đồ trình tự UML . 43
4.2.3 Xây dựng FSM mô tả biểu đồ trình tự UML 46
4.3 Kết luận 47
Chương 5. Xây dựng công cụ tự động sinh aspect từ máy trạng thái . 48
5.1 Đặt vấn đề 48
5.2 Sinh aspect từ FSM mô tả biểu đồ trạng thái UML . 49
5.3 Sinh aspect từ FSM mô tả biểu đồ trình tự UML 50
5.4 Mở rộng . 51
5.5 Sinh mã aspect kiểm chứng giao thức (AB)n . 52
5.5.1 Giao thức (AB)n là gì? . 52
5.5.2 Thuật toán kiểm chứng giao thức (AB)n . 53
5.5.3 Sinh mã aspect kiểm chứng giao thức (AB)n 54
5.6 Kết luận 54
Chương 6. Thực nghiệm . 55
6.1 Xây dựng công cụ PVG . 55
6.2 Kiểm chứng một số giao thức thực tế 56
6.2.1 Giao thức của các ứng dụng Applet 56
6.2.2 Kiểm chứng giao thức biểu diễn giao thức ghi nợ ở một máy ATM 60
6.2.3 Kiểm chứng giao thức [A*B] n 64
6.2.4 Kiểm chứng giao thức tương tác tác tử . 66
6.3 Kết luận 70
Chương 7. Kết luận . 71
7.1 Kết luận về khóa luận 71
7.2 Hướng phát triển trong tương lai . 72
Phụ lục 73
Phụ lục A: Tài liệu XMI mô tả biểu đồ trạng thái UML 73
Phụ lục B: Tài liệu XMI mô tả biểu đồ trình tự UML 75
Phụ lục C: Agent Customer (Customer.java) . 78
Phụ lục D: Agent ShoppingCart (ShoppingCart.java) 81
Phụ lục E: Aspect Template . 83