Mục Lục

1 Chương 1 : MỞ ĐẦU 5

1.1 Đặt vấn đề 5

1.2 Cấu trúc khóa luận 5

2 Chương 2: Giới thiệu về mô hình UML và lập trình hướng Aspect 6

2.1 Mô hình UML (Unifined Model Language) 6

2.1.1 Lịch sử phát triển của UML 6

2.1.2 Ứng dụng của mô hình UML 8

2.1.3 Các loại biểu đồ UML 11

2.2 Ngôn ngữ ràng buộc đối tượng (OCL) 12

2.3 Lập trình hướng khía cạnh (Aspect Oriented Programming) 14

2.3.1 Phương pháp lập trình hướng khía cạnh 14

2.3.2 Các khái niệm trong Aspect 20

3 Chương 3: Kiểm chứng mô hình Aspect-UML 22

3.1 Giới thiệu về Alloy 22

3.1.1 Alloy là gì? 22

3.1.2 Tính chất của ngôn ngữ alloy 22

3.1.3 Cấu trúc một chương trình Alloy 23

3.1.4 Khai báo trong alloy 23

3.2 Đặc tả mô hình Aspect-UML trong Alloy 27

3.2.1 Mô hình Aspect UML 27

3.2.2 Mô hình viễn thông 29

3.2.3 Đặc tả mô hình Aspect UML bằng Alloy 31

3.2.4 Kiểm chứng mô hình Aspect UML sử dụng Alloy 36

4 Chương 4 : Kết luận 39

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