Luận Văn Kiểm chứng mô hình aspect-uml bằng alloy

Mục Lục
1 Chương 1 : MỞ ĐẦU 6
1.1 Đặt vấn đề .6
1.2 Cấu trúc khóa luận 6
2 Chương 2: Giới thiệu về mô hình UML và lập trình hướng Aspect .7
2.1 Mô hình UML (Unifined Model Language) 7
2.1.1 Lịch sử phát triển của UML 7
2.1.2 Ứng dụng của mô hình UML 9
2.1.3 Các loại biểu đồ UML .12
2.2 Ngôn ngữ ràng buộc đối tượng (OCL) 13
2.3 Lập trình hướng khía cạnh (Aspect Oriented Programming) .15
2.3.1 Phương pháp lập trình hướng khía cạnh 15
2.3.2 Các khái niệm trong Aspect 21
3 Chương 3: Kiểm chứng mô hình Aspect-UML .23
3.1 Giới thiệu về Alloy .23
3.1.1 Alloy là gì? .23
3.1.2 Tính chất của ngôn ngữ alloy 23
3.1.3 Cấu trúc một chương trình Alloy 24
3.1.4 Khai báo trong alloy 24
3.2 Đặc tả mô hình Aspect-UML trong Alloy .28
3.2.1 Mô hình Aspect UML .28
3.2.2 Mô hình viễn thông .30
3.2.3 Đặc tả mô hình Aspect UML bằng Alloy 32
3.2.4 Kiểm chứng mô hình Aspect UML sử dụng Alloy 37
4 Chương 4 : Kết luận 40
DANH MỤC HÌNH VẼ
Hình 1: Hợp nhất các phương pháp thiết kế bằng UML Error! Bookmark not defined.
Hình 2: Mô hình UML không biểu diễn hết đặc tả Error! Bookmark not defined.
Hình 3:OPP Error! Bookmark not defined.
Hình 4: Sơ đồ lớp của bài toán vẽ hình .16
Hình 5: Dùng AOP giải quyết bài toán vẽ hình .Error! Bookmark not defined.
Hình 6: Mô hình class cho hệ thống viễn thông .Error! Bookmark not defined

1 Chương 1 : MỞ ĐẦU
1.1 Đặt vấn đề
Ngày nay, công nghệ thông tin ngày càng phát triển và được ứng dụng vào tất cả
các lĩnh vực của cuộc sống xã hội. Nó tạo ra một diện mạo mới cho xã hội và nhờ đó
nền văn minh nhân loại được nâng lên một tầm cao mới. Công nghệ phần mềm là một
phần không thể tách rời trong công nghệ thông tin. Hiện nay ngành công nghệ phần
mềm trên thế giới đã và đang phát triển như vũ bão. Những tiến bộ của khoa học kĩ thuật
phần cứng đã tạo điều kiện thuận lợi cho công nghệ phần mềm ngày càng phát triển
không ngừng.
Phần mềm được coi là sản phẩm chính của công nghệ phần mềm.Quá trình phát
triển phần mềm gồm nhiều giai đoạn: thu thập yêu cầu, phân tích, thiết kế,xây dựng,
kiểm chứng , triển khai và bảo trì. Trong đó việc kiểm chứng phần mềm là hết sức quan
trọng để đảm bảo chất lượng của một phần mềm.
Kiểm chứng mô hình UML cũng đóng góp vào việc kiểm chứng phần mềm.Việc
kiểm chứng mô hình UML + OCL đã được giải quyết [2]. Vấn đề đặt ra bây giờ là
kiểm chứng mô hình Aspect-UML(là một mô hình UML đơn giản được mở rộng với
việc sử dụng Aspect). Nhờ Aspect và các ràng buộc của nó mà mô hình Aspect UML
được cung cấp thêm thông tin. Mô hình Aspect UML có thể được kiểm chứng từ các
xung đột tương tác Aspect, để làm tự động công việc kiểm chứng mô hình Aspect
UML là chuyển đổi mô hình Aspect UML sang ngôn ngữ đặc tả Alloy. Alloy cung cấp
một ngôn ngữ đặc tả mô hình đơn giản dựa trên logic cũng như công cụ mô phỏng[].
Trong phạm vi khóa luận này tôi sẽ chỉ ra quy tắc chuyển đổi một mô hình Aspect
UML sang ngôn ngữ Alloy.
1.2 Cấu trúc khóa luận
Chương 1: Phần mở đầu.
Chương 2: Giới thiệu về mô hình UML và lập trình hướng Aspect.
Chương 3: Kiểm chứng mô hình Aspect- UML bằng Alloy
Chương 4: Kết luận và hướng nghiên cứu trong tương lai.