Đồ Án Kiểm chứng các giao thức bằng AOP

TÓM TẮT NỘI DUNG

Kiểm chứng phần mềm có một vai trò quan trọng trong việc đảm bảo tính đúng đắn của hệ thống phần mềm trong suốt quá trình thực thi,kiểm chứng giúp phát hiện, tìm ra lỗi và thông báo lỗi cho nhà phát triển. Phương pháp lập trình hướng khía cạnh (AOP) cùng với công nghệ AspectJ ra đời đã tạo ra một hướng phát triển mới cho kiểm chứng phần mềm, giúp nâng cao khả năng dò tìm lỗi, thông báo lỗi mà không ảnh hưởng tới mã nguồn hệ thống. Trong thực tế, biểu đồ UML là sự lựa chọn rất phổ biến cho việc mô hình hóa hệ thống phần mềm ở giai đoạn thiết kế hiện nay. Trong đó, biểu đồ tuần tự (sequence diagram) là một biểu đồ quan trọng, nó miêu tả các cách thức đối tượng tương tác và giao tiếp với nhau. Việc kiểm chứng thiết kế và kiểm chứng các giao thức ràng buộc trong biểu đồ trình tự là rất cần quan trọng vì nếu thiết kế biểu đồ tuần tự sai kéo theo các hoạt động của hệ thống hoặc trình tự hệ thống cần thực hiện sẽ bị sai dẫn tới toàn bộ hệ thống thiết kế sai. Trong phạm vi khóa luận, tôi xin trình bày phương pháp sinh mã aspect phục vụ cho mục đích kiểm chứng phần mềm từ biểu đồ tuần tự kết hợp với máy trạng thái và công cụ tự động sinh mã aspect dựa trên phương pháp này. Mã aspect tạo ra từ công cụ có thể dùng đan vào chương trình để thực hiện nhiệm vụ kiểm chứng các ràng buộc giữa các đối tượng và tính đúng đắn của hệ thống nhằm giảm thiểu tối đa lỗi khi viết mã cài đặt cho hệ thống.


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ểu diễ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 30 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