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

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 ATM60
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