1
ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
Bùi Duy Hải
KIỂM CHỨNG MÔ HÌNH ASPECT-UML BẰNG
ALLOY
KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY
Ngành: Công nghệ thông tin
HÀ NỘI - 2010
ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
Bùi Duy Hải
KIỂM CHỨNG MÔ HÌNH ASPECT-UML BẰNG
ALLOY
KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY
Ngành: Công nghệ thông tin
Cán bộ hướng dẫn: Phạm Thị Kim Dung
HÀ NỘI - 2010
LỜI CÁM ƠN
Đầu tiên tôi xin gửi lời cảm ơn sâu sắc tới cô giáo Ths.Phạm Thị Kim Dung,
bộ môn công nghệ phần mềm, khoa công nghệ thông tin, trường đại học công nghệ,
đại học Quốc Gia Hà Nội – người đã định hướng đề tài và tận tình hướng dẫn chỉ
bảo tôi trong suốt quá trình thực hiện khóa luận tốt nghiệp này.
Tôi cũng xin trân trọng cảm ơn quý thầy cô trong Khoa Công nghệ thông tin
trường Đại học Công nghệ, Đai học Quốc Gia Hà Nội đã tận tình giảng dạy, truyền
đạt những kiến thức quý báu trong suốt bốn năm học làm nền tảng cho tôi thực hiện
khóa luận tốt nghiệp này.
Con xin cảm ơn cha mẹ và gia đình đã sinh ra và nuôi dạy con khôn lớn,
luôn bên cạnh động viên và ủng hộ con trên con đường mà con yêu thích và lựa
chọn.
Cám ơn các bạn sinh viên Khoa công nghệ thông tin khóa 2006-2010. Các

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Ẽ
Figure 1.............................................................................................................................................................16
DANH MỤC BẢNG BIỂU
DANH MỤC NHỨNG TỪ VIẾT TẮT
OOP Object Oriented Programming
UML Unifined Model Language
OCL Object Contraint Language
AOP Aspect Oriented Programming

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

dụng những ưu điểm của các phương pháp của Rumbaugh và Jacobson. Tương tự
Rumbaugh cũng cho đăng một loạt các bài báo được biết đến với tên gọi phương pháp
OMT-2 cũng sử dụng nhiều ưu điểm của phương pháp của Booch. Các phương pháp đã
bắt đầu hợp nhất, nhưng các kí hiệu sử dụng ở các phương pháp vẫn còn nhiều điểm
khác biệt.
Cuộc chiến này chỉ kết thúc khi có sự ra đời của UML – một ngôn ngữ mô hình hóa
hợp nhất. Tại sao lại là hợp nhất? Đó là do có sự hợp nhất các cách kí hiệu của Booch,
OMT và Objectory cũng như các ý tưởng tốt nhất của một số phương pháp khác như
hình vẽ sau:
Hình 1:Hợp nhất các phương pháp thiết kế bằng UML
Bằng cách hợp nhất các kí hiệu sử dụng trong khi phân tích, thiết kế của các phương
pháp đó, UML cung cấp một nền tảng chuẩn trong việc phân tích thiết kế. Có nghĩa là
các nhà phát triển vẫn có thể tiến hành theo phương pháp mà họ đang sử dụng hoặc là
có thể tiến hành theo một phương pháp tổng hợp hơn( do thêm vào những bước ưu
điểm của từng phương pháp). Nhưng điều quan trọng là các ký hiệu giờ đây đã thống
nhất và mỗi ký hiệu chuẩn của tổ chức OMG (Object Management Group) vào tháng
7-1997.
2.1.2 Ứng dụng của mô hình UML
UML là một ngôn ngữ dùng để:
• Trực quan hóa
• Cụ thể hóa
• Sinh mã ở dạng nguyên mẫu
• Lập và cung cấp tài liệu
UML là một ngôn ngữ bao gồm một bảng từ vựng và các quy tắc để kết hợp các từ
vựng đó phục vụ cho mục đích giao tiếp. Một ngôn ngữ dùng cho việc lập mô hình là
ngôn ngữ mà bảng từ vựng( các ký hiệu) và các quy tắc của nó tập trung vào việc thể
hiện về mặt khái niệm cũng như vật lý của một hệ thống.
Mô hình hóa mang lại sự hiểu biết về một hệ thống. Một mô hình không thể giúp
chúng ta hiểu rõ một hệ thống, thường là phải xây dựng một số mô hình xét từ những
góc độ khác nhau. Các mô hình này có quan hệ với nhau.

rang và duy nhất, một nhà phát triển có thể đọc được mô hình xây dựng bằng UML do
một người khác viết.Những cấu trúc mà việc nắm bắt thông qua đọc mã lệnh là khó
khăn nay đã được thực hiện trực quan.Một mô hình rõ ràng, sáng sủa làm tăng khả năng
giao tiếp, trao đổi giữa các nhà phát triển.
2.1.2.2 UML là ngôn ngữ để chi tiết hóa
Có nghĩa là xây dựng các mô hình một các tỉ mỉ, rõ ràng, đầy đủ ở các mức độ chi
tiết khác nhau. Đặc biệt là UML thực hiện việc chi tiết hoá tất cả các quyết định quan
trọng trong phân tích, thiết kế và thực thi một hệ thống phần mềm.
2.1.2.3 UML là ngôn ngữ dùng để sinh ra mã ở dạng nguyên mẫu
Các mô hình xây dựng bởi UML có thể ánh xạ tới một ngôn ngữ lập trình cụ thể như
: Java, C++… thậm chí cả các bảng trong một CSDL quan hệ hay CSDL hướng đối
tượng.
Việc các yêu cầu có khả năng thường xuyên thay đổi trong quá trình phát triển hệ
thống dẫn đến việc các cấu trúc và hành vi của hệ thống được xây dựng có thể khác mô
hình mà ta đã xây dựng. Điều này có thể làm cho một mô hình tốt trở nên vô nghĩa vì nó
không còn phản ánh đúng hệ thống nữa. Cho nên phải có một cơ chế để đồng bộ xhóa
giữa mô hình và mã lệnh.
UML cho phép cập nhật một mô hình từ các mã thực thi ( ánh xạ ngược). Điều này
tạo ra sự nhất quán giữa mô hình của hệ thống và các đoạn mã thực thi mà ta xây dựng
cho hệ thống đó.
2.1.2.4 UML là ngôn ngữ dùng để lập và cung cấp tài liệu
Một tổ chức phần mềm ngoài việc tạo ra các đoạn mã lệnh( thực thi) thì còn tạo ra
các tài liệu sau:
• Ghi chép về các yêu cầu của hệ thống
• Kiến trúc của hệ thống
• Thiết kế
• Mã nguồn
• Kế hoạch dự án
• Test
• Các nguyên mẫu

ứng(reactive).
2.1.3.7 Biểu đồ hoạt động(Activity)
Là một dạng đặc biệt của biểu đồ chuyển trạng. Nó chỉ ra luồng đi từ hoạt động này
sang hoạt động khác trong một hệ thống. Nó đặc biệt quan trọng trong việc xây dựng
mô hình chức năng của hệ thống và nhấn mạnh tới việc chuyển đổi quyền kiểm soát
giữa các đối tượng.
2.1.3.8 Biểu đồ thành phần (Component)
Chỉ ra cách tổ chức và sự phụ thuộc của các thành phần(component). Nó liên quan
tới biểu đồ lớp, trong đó một thành phần thường ánh xạ tới một hay nhiều lớp, giao diện
, collaboration.
2.2 Ngôn ngữ ràng buộc đối tượng (OCL)
OCL (Object constraint language) là ngôn ngữ xây dựng mô hình phần mềm được
định nghĩa như một chuẩn thêm vào UML cho phân tích và thiết kế hướng đối tượng .
Các biểu thức viết trong OCL phụ thuộc vào các kiểu lớp, giao diện, …) được định
nghĩa trong các biểu đồ UML.
Các biểu thức viết trong OCL thêm các thông tin quan trọng cho các mô hình hướng
đối tượng. Các thông tin này thường khôn thể biểu diễn trong biểu đồ. Trong UML
phiên bản 1.1 các thông tin này được giới hạn bởi các ràng buộc, mỗi ràng buộc được
định nghĩa như một hạn chế về giá trị nhận được( một hay nhiều) của mộ hệ thống hay
mô hình hướng đối tượng. Trong UML phiên bản 2, một mô hình có thể chứa nhiều
thông tin thêm hơn là chỉ có ràng buộc. Tất cả các công việc như định nghĩa truy vấn,
các giá trị tham chiếu, các quy tăc nghiệp vụ hay các điều kiện trạng thái được viết bằng
biểu thức trong một mô hình. OCL là ngôn ngữ chuẩn trong đó các biểu thức được viết
một cách rõ ràng dễ hiểu.
Một mô hình thường có những thiếu sót do những hạn chế của các biểu đồ. Một biểu
đồ đơn giản không thể biểu diễn hết các phát biểu đặc tả.
Hình 2: Mô hình UML không biểu diễn hết đặc tả
Trong mô hình, quan hệ giữa lớp Flight và lớp Person , phía lớp Person có bản số là
0…* tức là số khách hang là không giới hạn. Trong thực thế số khách hàng bị giới hạn
bởi số ghế mà máy bay có, và giới hạn này không thể biểu diễn trong biểu đồ. Trong ví

Dưới đây là sơ đồ lớp của bài toán
Figure 1
Hình 4: Sơ đồ lớp của bài toán vẽ hình
Mô hình hóa thành các lớp như vậy ta thấy bài toán đã tương đối ổn. Bây giờ vấn đề
đặt ra là mỗi khi ta thay đổi tọa độ của một điểm hay co giãn hình, di chuyển hình ta lại
phải vẽ lại hình ở vị trí mới – tức là phải update lại Display.