Luận Văn Kiểm chứng các giao thức bằng aop

MỤC LỤC
Chương 1. Mở Đầu 8
1.1. Đặt vấn đề . 8
1.2.Bài toán 8
1.3. Tổng quan về phương pháp giải quyết bài toán 9
1.4. Cấu trúc khóa luận . 9
Chương 2. Ngôn ngữ UML và biểu diễn biểu đồ trong UML bằng XMI. . 11
2.1. Giới thiệu chung về UML: . 11
2.2. Các loại biểu đồ UML . 12
2.2.1. Nhóm biểu đồ về cấu trúc 12
2.2.2. Nhóm biểu đồ hành vi 12
2.3. Biểu đồ tuần tự trong UML2.0(Sequence diagram) . 12
2.4. Một số thành phần chính trong biểu đồ tuần tự 14
2.4.1. Đường đời (lifeLine) 14
2.4.2. Thông điệp (Message) 15
2.4.3. Đoạn gộp (Combind Fragment) 16
2.5. Biểu diễn biểu đồ tuần tự : . 19
2.5.1. Biểu diễn Đường đời (LifeLine ): . 19
2.5.2. Biểudiễn Thông điệp: 19
2.5.3. Lời chú giải (Comment) . 19
2.5.4. Các đoạn gộp (CombindedFragment) . 19
2.6. Sơ lược về XML 20
2.7.Biểu diễn tài liệu XML 21
2.8. TƯƠNG TÁC VỚI TÀI LIỆU XML . 23
2.8.1 DOM 23
2.8.2 XML DOM : . 23
2.8.3 XMI: . 25
2.9. Máy trạng thái FSM. . 25
2.9.1. Tổng quan về các thành phần trong máy trạng thái FSM 25
2.9.2. Xây dựng máy hữu hạn trạng thái từ các thành phần của biểu đồ . 26
CHƯƠNG 3 Aspect và lập trình hướng khía cạnh 30
3.1 Tổng quan về lập trình hướng khía cạnh. 30
3.2 Biên dịch AOP: 31
3.3 LỢI ÍCH CỦA AOP : . 32
3.4 AspectJ . 32
3.4.1. Đặc tả ngôn ngữ: 32
3.4.2. Phần thực thi: . 33
3.5. Một số khái niệm cơ bản trong AspectJ: 33
3.5.1. Join point . 33
3.5.2. Pointcut 33
3.5.3. Advice . 33
3.5.4. Aspect 34
3.6. Cơ chế họa động của AspectJ 35
3.6.1. Compile –time: . 35
3.6.2. Link –time: . 35
3.6.3. Load –time: . 35
3.7. 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 . 36
CHƯƠNG 4 38
PHƯƠNG PHÁP KIỂM CHỨNG CÁC GIAO THỨC BẰNG AOP 38
4.1 Biểu diễn giao thức . 38
4.2. Tiền điều kiện và hậu điều kiện : . 39
4.2.1. Tiền điều kiện : 39
4.2.2. Hậu điều kiện : . 39
4.2.3 Biểu diễn tiền điều kiện và hậu điều kiện trong biểu đồ trình tự : 39
4.3 Kiểm chứng giao thức: . 40
Chương 5 Xây dựng công cụ sinh mã từ máy trạng thái 42
5.1 Tổng quan về xây dựng công cụ sinh mã từ máy trạng thái . 42
5.1.1 Lấy các thành phần trong tài liệu XMI. . 42
5.1.2. Sinh mã Aspect từ biểu đồ tuần tự UML 45
5.2. Sinh mã kiểm chứng giao thức AnBm . 46
Chương 6 Kết luận . 49
6.1 Kết luận về khóa luận . 49
6.2 Hướng phát triển trong tương lai : 50