Download miễn phí Khóa luậ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)nlà 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
Để tải bản Đầy Đủ của tài liệu, xin Trả lời bài viết này, Mods sẽ gửi Link download cho bạn sớm nhất qua hòm tin nhắn.
Ai cần download tài liệu gì mà không tìm thấy ở đây, thì đăng yêu cầu down tại đây nhé:
Nhận download tài liệu miễn phí
Tóm tắt nội dung tài liệu:
h (a) biểu diễn các luồng được gửi đi song song (phép AND). Hình (b) baogồm một hộp quyết định xác định xem luồng nào sẽ được gửi đi tiếp (phép OR). Hình
(c) xác định trong một thời điểm chỉ có một luồng được phép gửi đi (phép XOR).
31
3.4.3.3 Mức 3 – biểu diễn xử lý bên trong Agent
Tại mức thấp nhất, đặc tả về một giao thức. Agent yêu cầu giải thích rõ ràng
những xử lý chi tiết bên trong agent để tiến hành giao thức. Các mô hình mức cao hơn
(gọi là holon) bao gồm tập các agent ở mức thấp hơn. Các hành vi bên trong có thể
được biểu diễn bằng việc sử dụng đệ quy các cách biểu diễn ở mức 2.
Ví dụ:
Hình 3.9: Các hành vi bên trong của agent Initiator (a) và Participant(b)
3.5 Java Agent DEvelopment Framework (JADE)
3.5.1 Khái niệm về JADE
“JADE (Java Agent DEvelopment Framework) is a software Framework fully
implemented in Java language. It simplifies the implementation of multi-agent systems
through a middle-ware that complies with the FIPA specifications and through a set of
graphical tools that supports the debugging and deployment phases” [3].
Ta có thể tóm tắt lại định nghĩ trên như sau:
- JADE là phần mềm dạng middle-ware phục vụ cho việc phát triển hệ đa
tác tử. Nó hỗ trợ việc xây dựng từng agent trong hệ đa agent. Cung cấp các
dịch vụ cho từng hoạt động của agent, các công cụ phục vụ cho việc debug
và agent xây dựng dựa trên chuẩn FIFA.
- JADE là một hệ thống mã nguồn mở, được xây dựng trên ngôn ngữ Java.
32
3.5.2 Cấu trúc của JADE platform
Platform JADE là môi trường hỗ trợ agent hoạt động, trao đổi thông tin. Platform
JADE chứa nhiều container, các container có thể hoạt động độc lập trên các host khác
nhau. Có hai loại container chính:
- JADE main-container: Mỗi platform chỉ có một main-container.
Container này được khở tạo và hủy cùng với platform. Nó chứa một số
agent quan trọng của JADE platform như:
o RMA (Remote Management Agent): Hoạt động như màn hình đi ều
khiển, phục vụ việc quản lý platform.
o DF (Directory Facilitator): Là một agent cung cấp dịch vụ trang
vàng (yellow-page) trong platform.
Trang vàng (Yellow-page): Là một dịch vụ cung cấp chức
năng quản lý việc giao tiếp giữa các agent, đối chiếu thông tin
trao đổi.
o AMS (Agent Management System): Là agent theo dõi quản lý sự truy
cập và sử dụng agent platform. Cung cấp dịch vụ trang trắng (white-
page).
Trang trắng (White-page) cung cấp chức năng quản lý việc
đăng ký của agent, quản lý ID của các agent đã đăng ký và
quản lý vòng đời của agent.
- JADE agent-container: Chứa các agent của người sử dụng, nó có thể nằm
trên các host khác nhau.
Hình 3.10: Cấu trúc phân tán của JADE
33
3.5.3 Một số lớp quan trọng trong thư viện JADE
- Gói jade.core: Cài đặt các thành phần cơ bản của hệ thống. Nó chứa lớp
Agent, các agent được tạo ra bắt buộc phải kế thừa từ lớp này. Ngoài ra nó
còn chứa gói jade.core.behavior: cung cấp các hàm cài đặt nhiệm vụ cho
agent.
o Lớp jade.core.Agent: cung cấp các cách đăng ký với
platform, các cách xác định trạng thái của agent, quản lý
trạng thái và các cách hoạt động của agent.
Cách tạo agent:
public class MyAgent extends Agent
{
// some attributes
public void setup()
{
// registry with AMS..
// other activities
addBehaviour(myBehaviour)
}
// other methods
}
o Gói jade.core.behavior: Chứa các lớp cho phép tạo ra các hoạt động
của agent từ đơn giản đến phức tạp. Ta có thể tạo ra các hành động
cho agent bằng việc kế thừa từ các lớp này.
Cách tạo behavior:
public class MyBehaviour extends Behaviour
{
// some attributes
public MyBehaviour(Agent agent){super(agent)}
public void action()
{
// agent action
}
// other methods
}
- Gói jade.lang.acl: cung cấp các cách xử lý giao tiếp giữa các
agent theo chuẩn FIFA.
- Gói jade.domain: mô tả các thực thể quản lý agent theo chuẩn FIFA. Nó
cung cấp một số dịch vụ như: life-cycle, yellow-page, white-page.
Ngoài ra còn một số gói khác như: jade.wrapper, jade.content, jade.tools…
Hoạt động của một agent:
34
Hình 3.11: Hoạt động của agent
3.6 Kết luận
Các kiến thức về UML, XML, XMI, AUML mà tui trình bày trong chương này
không phải quá mới mẻ và cũng không thật sự đầy đủ. Nhưng đó là những nền tảng
kiến thức cơ bản tui sử dụng trong khóa luận để xây dựng công cụ tự động sinh mô-
đun aspect kiểm chứng. Để giải quyết bài toán “kiểm chứng đặc tả UML cho tác tử
phần mềm”, tui chia bài toán ra làm hai bước nhỏ: Bước thứ nhất là xây dựng FSM từ
tài liệu XMI mô tả các biểu đồ UML. Bước thứ hai là xây dựng bộ sinh aspect tự động
từ FSM. Hai bước này sẽ được trình bày cụ thể ở các chương sau.
35
Chương 4. Xây dựng máy trạng thái từ biểu đồ UML
Trong chương 2 và 3 tui đã trình bày các ki ến thức nền tảng cơ bản để xây dựng
công cụ Protocol Verification Generator(PVG). Trong chương này, tui sẽ trình bày
bước thứ nhất trong phương pháp xây dựng công cụ tự động sinh mô-đun aspect, đó là
phân tích tài liệu XMI được xuất ra từ một biểu đồ UML, từ đó xây dựng máy trạng
thái.
Như vậy, trong bước này ta có:
- Input: Một tài liệu XMI mô tả biểu đồ trạng thái hay biểu đồ trình tự
UML.
- Output: Máy trạng thái nếu xây dựng được, nếu không sẽ báo lỗi.
Để xây dựng được máy trạng thái, trước tiên tui sẽ xây dựng các cấu trúc dữ liệu
để đặc tả các thành phần của biểu đồ UML bằng các đối tượng trong Java, cấu trúc dữ
liệu của máy trạng thái mà tui sử dụng. Tiếp theo, tui sẽ trình bày cách thức tạo ra máy
trạng thái từ tài liệu XMI và các cấu trúc dữ liệu đã xây dựng trước đó.
4.1 Biểu đồ trạng thái
4.1.1 Quy tắc biểu diễn giao thức bằng biểu đồ trạng thái
Ngoài cách vẽ biểu đồ trạng thái như trong UML đề cập, tui xin đưa ra thêm một
số quy tắc dùng biểu đồ trạng thái để biểu diễn giao thức. Công cụ PVG mà tui xây
dựng sẽ sử dụng các quy tắc này như là một chuẩn để nó có thể hiểu được giao thức
mà người dùng đặc tả bằng UML. Nếu người dùng không tuân thủ các quy tắc này,
chương trình sẽ không đưa ra được kết quả như ý.
Một số quy tắc:
- Trong một tài liệu UML, chỉ có một biểu đồ trạng thái thể hiện giao thức
cần kiểm tra.
- Biểu đồ trạng thái bắt buộc phải có trạng thái bắt đầu và trạng thái kết
thúc.
- Trạng thái bắt đẩu có tên bắt đầu bằng “Initial”, và chỉ có các cạnh đi ra
chứ không có cạnh đi vào trạng thái này.
- Trạng thái kết thúc có tên bắt đầu bằng “FinalState” và chỉ có cạnh đi vào,
không có cạnh đi ra từ trạng thái này.
36
- Các trạng thái khác phải có ít nhất một cạnh đi vào và một cạnh đi ra. Tên
của các trạng thái này không bắt đầu bằng “Initial” hay “FinalState”.
- Các cạnh là chữ ký (signature) của các hàm, cách sẽ được gọi dùng
để thay đổi trạng thái. Chữ ký này được định nghĩa gi ống như tên hàm
trong mã nguồn của chương trình cần kiểm chứng, bao gồm cả kiểu giá trị
trả về, tên hàm, danh sách các tham số truyền vào. Ví dụ:
o Trong mã nguồn, ta gọi hàm init() không có tham số truyền vào, kiểu
trả về là void thì tên của cạnh trong biểu đồ UML sẽ là: void init().
o Hàm int setAge(int age) đ...