Khóa luận Chuyển đổi đặc tả UML với OCL sang đặc tả alloy
ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
Chử Kim Cường
CHUYỂN ĐỔI ĐẶC TẢ UML VỚI OCL SANG ĐẶC TẢ
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Ệ
Chử Kim Cường
CHUYỂN ĐỔI ĐẶC TẢ UML VỚI OCL SANG ĐẶC TẢ
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: ThS. Vũ Diệu Hương
Cán bộ đồng hướng dẫn:TS. Đặng Văn Hưng
HÀ NỘI - 2010
LỜI CẢM ƠN
Lời đầu tiên em xin gửi lời cảm ơn chân thành, và lòng biết ơn sâu sắc tới cô giáo
Vũ Diệu Hương cùng thầy Đặng Văn Hưng đã hướng dẫn tận tình cho em trong suốt quá
trình làm khóa luận tốt nghiệp.
Em cũng xin gửi lời cám ơn tới các thầy, cô trong khoa Công nghệ thông tin-Trường
Đại Học Công Nghệ - ĐHQGHN. Các thầy, cô đã dạy bảo và luôn luôn tạo điều kiện cho
chúng em học tập trong quá trình học và đặc biệt trong thời gian làm khóa luận tốt nghiệp.
Cuối cùng, xin gửi lời cảm ơn tới tập thể sinh viên lớp K51CC trường Đại Học
Công Nghệ, những người bạn luôn chia sẻ và giúp đỡ tôi trong suốt quá trình học tập.
Hà Nội, ngày ....tháng....năm 2010
Sinh Viên
Chử Kim Cường
TÓM TẮT NỘI DUNG
UML là ngôn ngữ mô hình hóa thống nhất, biểu diễn các đối tượng thực bằng các ký
hiệu trực quan. Một mô hình UML gồm nhiều biểu đồ thể hiện các khía cạnh khác nhau
của hệ thống. OCL được sử dụng để mô tả các ràng buộc cho các đối tượng của mô hình
UML.
Một cách để kiểm tra sự đúng đắn của mô hình UML là chuyển đổi mô hình UML
sang đặc tả Alloy và sử dụng công cụ Alloy Analyzer để phân tích tự động.
Khóa luận này giới thiệu về UML, OCL, Alloy và tập trung trình bày cách thức
chuyển đổi mô hình UML sang Alloy để thực hiện phân tích các yếu tố mô hình. Hệ
thống quản lý các tài khoản và giao dịch ATM được sử dụng để minh họa phương pháp
đã trình bày.
Mục lục
LỜI CẢM ƠN........................................................................................................................................... i
TÓM TẮT NỘI DUNG ........................................................................................................................... ii
DANH MỤC BẢNG BIỂU...................................................................................................................... v
DANH MỤC HÌNH VẼ.......................................................................................................................... vi
Mở Đầu ................................................................................................................................................... 1
Chương 1 . Tổng quan UML và OCL.................................................................................................... 2
1.1
Ngôn ngữ mô hình hóa thống nhất - UML................................................................................. 2
Mục đích của UML........................................................................................................... 2
Miền ứng dụng của UML.................................................................................................. 2
Hệ thống biểu đồ trong UML ............................................................................................ 3
Biểu đồ lớp ....................................................................................................................... 3
OCL – Object Constraint Language .......................................................................................... 5
Biểu diễn đặc tả OCL........................................................................................................ 6
Đặc tả OCL trên biểu đồ lớp.............................................................................................. 7
Kiểu tập hợp và các phép toán trên tập hợp..................................................................... 10
Biểu thức lặp trên tập hợp ............................................................................................... 12
Kết luận.................................................................................................................................. 13
1.1.1
1.1.2
1.1.3
1.1.4
1.2
1.2.1
1.2.2
1.2.3
1.2.4
1.3
Chương 2 . Giới thiệu Alloy và công cụ Alloy Analyzer...................................................................... 13
2.1
2.2
Khái quát về Alloy.................................................................................................................. 14
Mô hình Alloy ........................................................................................................................ 14
Khai báo ký hiệu - signature............................................................................................ 14
Khai báo sự kiện - fact .................................................................................................... 15
Khai báo mệnh đề và chức năng – predicate & fuction..................................................... 16
Khai báo khẳng định - assertion ...................................................................................... 16
Lệnh trong Alloy............................................................................................................. 16
Khai báo mô đun............................................................................................................. 17
Thực thi mô hình Alloy................................................................................................... 17
Công cụ Alloy Analyzer ......................................................................................................... 17
Ví dụ đặc tả Alloy................................................................................................................... 18
2.2.1
2.2.2
2.2.3
2.2.4
2.2.5
2.2.6
2.2.7
2.3
2.4
Chương 3 . Chuyển đổi biểu đồ lớp với đặc tả OCL sang mô hình Alloy ............................................. 20
3.1 Chuyển biểu đồ lớp UML với các liên kết phức tạp sang biểu đồ lớp UML với các liên kết đơn
giản 22
3.1.1
3.1.2
3.1.3
3.1.4
3.1.5
Quan hệ nhị phân với các lượng từ .................................................................................. 23
Chuyển quan hệ tổng quát hóa sang quan hệ nhị phân ..................................................... 25
Chuyển quan hệ kết tập và tạo thành sang quan hệ nhị phân ............................................ 28
Chuyển các thành phần của lớp sang Alloy...................................................................... 29
Chuyển các ràng buộc bất biến, tiền điều kiện hậu điều kiện OCL ................................... 32
Những vấn đề khi chuyển đổi.................................................................................................. 35
Kết luận.................................................................................................................................. 36
3.2
3.3
Chương 4 . Kiểm tra đặc tả hệ thống quản lý các tài khoản và các giao dịch trên máy ATM................ 37
4.1
4.1.1
4.1.2
4.2
Yêu cầu của hệ thống.............................................................................................................. 37
Yêu cầu chức năng.......................................................................................................... 37
Ràng buộc cho hệ thống.................................................................................................. 37
Thiết kế cơ sở dữ liệu ............................................................................................................. 38
Biểu đồ lớp ..................................................................................................................... 38
Các ràng buộc được mô tả bằng OCL.............................................................................. 38
Chuyển đổi mô hình thiết kế sang Alloy.................................................................................. 39
4.2.1
4.2.2
4.3
Kết luận................................................................................................................................................. 42
TÀI LIỆU THAM KHẢO...................................................................................................................... 43
DANH MỤC BẢNG BIỂU
Bảng 1. Kiểu dữ liệu tập hợp trong OCL ................................................................................................ 11
Bảng 2. Phép toán trên tập hợp OCL...................................................................................................... 11
Bảng 3. Biểu thức lặp trên tập hợp OCL................................................................................................. 12
Bảng 4. Chuyển đặc tả OCL của lớp Student sang Alloy ........................................................................ 24
Bảng 5. Quy tắc chuyển quan hệ tổng quát hóa sang quan hệ nhị phân ................................................... 26
Bảng 6. Quy tắc chuyển OCL sang Alloy – [4]....................................................................................... 33
DANH MỤC HÌNH VẼ
Hình 1. Biểu diễn đặc tả OCL trên biểu đồ lớp[5]..................................................................................... 6
Hình 2. Công cụ Alloy Analyzer ............................................................................................................ 18
Hình 3. Kết quả thực thi mô hình Alloy.................................................................................................. 20
Hình 4. Kết quả thực thi mệnh đề "thêm” ............................................................................................... 20
Hình 5. Mô hình chuyển đổi biểu đồ lớp với đặc tả OCL sang mô hình Alloy......................................... 22
Hình 6. Chuyển quan hệ nhị phân với lượng từ[3] .................................................................................. 23
Hình 7. Ví dụ chuyển quan hệ nhị phân với lượng từ.............................................................................. 24
Hình 8. Đặc tả Alloy lớp Student............................................................................................................ 25
Hình 9. Chuyển quan hệ tổng quát hóa sang quan hệ nhị phân[3] ........................................................... 25
Hình 10. Ví dụ mô hình chuyển đổi OCL sang Alloy.............................................................................. 26
Hình 11. Chuyển lớp sang ký hiệu .......................................................................................................... 29
Hình 12. Lớp với thuộc tính, phương thức và đặc tả OCL....................................................................... 32
Hình 13. Biểu đồ lớp hệ thống ATM[8].................................................................................................. 38
Hình 14. Ràng buộc OCL của hệ thống .................................................................................................. 38
Hình 15. Đặc tả Alloy của lớp ATM....................................................................................................... 39
Hình 16. Đặc tả Alloy của lớp Account .................................................................................................. 40
Hình 17. Ràng buộc cho hệ thống ATM ................................................................................................. 41
Mở Đầu
UML[1] là ngôn ngữ được sử dụng phổ biến nhất trong ngành công nghiệp phần
mềm vì tính dễ hiểu, trực quan và dễ thể hiện bằng công cụ. Trong những năm gần đây,
OCL[5] được phát triển với mục đích là ngôn ngữ mô tả các ràng buộc cho các yếu tố mô
hình UML[1] để mô hình UML[1] có ngữ nghĩa chặt chẽ hơn.
Cho đến nay, để kiểm tra các ràng buộc của mô hình UML[1], chúng ta phải chuyển
đặc tả UML[1] sang đặc tả bằng các ngôn ngữ có tính hình thức hóa cao hơn như là Z, B,
OWL, Alloy[2]...Alloy[2] đã được phát triển khá hoàn thiện cả về ngôn ngữ và công cụ
phân tích tự động. Chúng ta có thể chuyển đổi mô hình UML[1] với đặc tả OCL[5] sang
mô hình Alloy[2] và sử dụng công cụ phân tích Alloy Analyzer để phân tích các yếu tố
mô hình.
Hiện nay, đã có nhiều nhóm tham gia nghiên cứu lý thuyết chuyển đổi đặc tả
UML[1] và OCL[5] sang đặc tả Alloy[2] và xây dựng công cụ chuyển đổi tự động. Có thể
kể đến công cụ UML2ALLOY[7]. Tuy nhiên, vẫn còn nhiều hạn chế trong việc nghiên
cứu lý thuyết chuyển đổi đặc tả UML[1] với OCL[5] sang đặc tả Alloy[2] ví dụ như việc
chuyển đổi quan hệ tam phân (hoặc lớn hơn quan hệ tam phân) giữa các lớp trong biểu đồ
lớp sang đặc tả Alloy[2].
Khóa luận này tập trung vào tìm hiểu các quy tắc chuyển đổi các yếu tố mô hình
UML[1] sang mô hình Alloy[2] đã được đề xuất trong các nghiên cứu khác và có đề xuất
một số quy tắc chuyển đổi mới cho một số trường hợp đặc biệt. Khóa luận cũng thực hiện
một ví dụ minh họa là “hệ thống quản lý các tài khoản và các giao dịch trên máy ATM”.
Kết cấu của khóa luận như sau:
Chương 1: Tổng quan UML và OCL
Chương 2: Giới thiệu Alloy và công cụ phân tích Alloy Analyzer
Chương 3: Chuyển đổi biểu đồ lớp UML với đặc tả OCL sang Alloy
Chương4: Bài toán minh họa
1
Chương 1. Tổng quan UML và OCL
1.1 Ngôn ngữ mô hình hóa thống nhất - UML
UML[1] là ngôn ngữ mô hình hóa thống nhất với các ký hiệu trực quan, được các
phương pháp hướng đối tượng sử dụng để thể hiện và miêu tả các thiết kế của hệ thống.
Nó là một ngôn ngữ để đặc tả, trực quan hóa, xây dựng và làm tài liệu cho nhiều đối
tượng khác nhau. UML[1] có thể làm công cụ giao tiếp giữa người dùng, nhà phân tích,
nhà thiết kế và nhà phát triển phần mềm.
1.1.1 Mục đích của UML
Mô hình hóa hệ thống sử dụng các khái niệm hướng đối tượng.
Thiết lập một kết nối từ nhận thức của con người đến các sự việc cần mô hình hóa.
Giải quyết vấn đề về mức độ thừa kế trong các hệ thống phức tạp, có nhiều ràng
buộc khác nhau.
Tạo một ngôn ngữ mô hình hóa có thể sử dụng được bởi người và máy.
1.1.2 Miền ứng dụng của UML
UML[1] có thể được sử dụng trong nhiều giai đoạn từ phát triển, thiết kế, thực hiện
và bảo trì .
Hệ thống thông tin (Infomation system) : Cất giữ, lấy, biến đổi thông tin cho người
sử dụng. Xử lý những khoảng dữ liệu lớn có quan hệ phức tạp, mà chúng được lưu
trữ trong các cơ sở dữ liệu quan hệ hay hướng đối tượng.
Hệ thống kỹ thuật (Technical system): Xử lý và điều khiển các thiết bị viễn thông,
hệ thống quân sự hay quá trình công nghiệp. Đây là loại thiết bị phải xử lý các giao
tiếp đặc biệt, không có giao giao diện chuẩn và thường là các hệ thống thời gian
thực.
Hệ thống nhúng (Embeded system): Thực hiện trên các thiết bị phần cứng trên ô tô,
thiết bị di động...Điều này được thực hiện với lập trình mức thấp với hỗ trợ thời
gian thực.
Hệ thống phân bố (Distributed system): Được phân bố trên một số máy cho phép
truyền dữ liệu từ nơi này đến nơi khác một cách dễ dàng. Chúng đòi hỏi các cơ chế
liên lạc đồng bộ để bảo đảm toàn vẹn dữ liệu. Thường được xây dựng trên một số
kỹ thuật hướng đối tượng như CORBA, COM/DCOM.
Hệ thống giao dịch (Bussiness system): Mô tả mục đích, tài nguyên, các quy tắc và
công việc kinh doanh.
Phần mềm hệ thống (System software): Định nghĩa cơ sở hạ tầng kỹ thuật cho phần
mềm khác sử dụng chẳng hạn như hệ điều hành, cơ sở dữ liệu,...
2
1.1.3 Hệ thống biểu đồ trong UML
Biểu đồ Use case (Use case Diagram)
Biểu đồ lớp (Class Diagram)
Biểu đồ đối tượng (Object Diagram)
Biểu đồ trạng thái (State Diagram)
Biểu đồ trình tự (Sequence Diagram)
Biểu đồ cộng tác (Collaboration Diagram)
Biểu đồ hoạt động (Activity Diagram)
Biểu đồ thành phần (Component Diagram)
Biểu đồ triển khai (Deployment Diagram)
1.1.4 Biểu đồ lớp
Một biểu đồ lớp[1] là một dạng mô hình tĩnh. Một biểu đồ lớp mô tả hướng nhìn
tĩnh của hệ thống bằng các khái niệm lớp và mối quan hệ của chúng với nhau. Mặc dù
biểu đồ lớp có những nét tương đồng với mô hình dữ liệu nhưng các lớp không chỉ thể
hiện cấu trúc thông tin mà còn miêu tả hành vi. Một trong những mục đích của biểu đồ
lớp chính là tạo nền tảng cho các biểu đồ khác, thể hiện các khía cạnh khác của hệ thống.
Biểu đồ lớp được coi là biểu đồ quan trọng nhất trong một mô hình UML[1]. Mô tả chính
xác biểu đồ lớp là tiền đề cho việc xây dựng hệ thống chính xác.
Các phần tử của biểu đồ lớp
Lớp
Thuộc tính
Phương thức
Quan hệ giữa các lớp
. Liên kết – associations
. Tổng quát hóa – generalization
. Phụ thuộc – dependency
. Nâng cấp – refinment
Các luật ràng buộc và các ghi chú
Lớp.
Một lớp là một mô tả một tập các đối tượng có chung thuộc tính, chung phương thức
(ứng xử), chung các mối quan hệ với đối tượng khác và chung ngữ nghĩa. Điều đó cũng
có nghĩa là lớp chính là một khuôn mẫu để tạo ra đối tượng. Mỗi đối tượng sẽ là một thực
thể của lớp nào đó và một đối tượng không thể là kết quả thực thể hóa của nhiều hơn một
lớp. UML thể hiện lớp bằng hình chữ nhật có 3 phần. Phần thứ nhất chứa tên lớp, tên lớp
thường là các danh từ, được in đậm, căn giữa. Phần thứ hai là các thuộc tính và thành
phần dữ liệu của lớp và trong phần thứ ba là các phương thức hay các hàm thành phần của
lớp.
3
Thuộc tính.
Lớp có các thuộc tính miêu tả những đặc điểm của đối tượng. Thuộc tính có thể có
nhiều mức độ trông thấy khác nhau, miêu tả liệu thuộc tính có thể được truy xuất từ lớp
khác hay không. Có 3 mức độ nhìn thấy của thuộc tính : public, private, protected. Mọi
đặc điểm của một thực thể là những thông tin cần lưu trữ có thể chuyển thành thuộc tính
của lớp miêu tả thực thể đó.
Phương thức.
Phương thức định nghĩa các hoạt động mà lớp có thể thực hiện. Tất cả các đối tượng
được tạo ra từ một lớp sẽ có chung thuộc tính và phương thức. Phương thức được sử dụng
để xử lý thay đổi các thuộc tính cũng như thực hiện các công việc khác. Phương thức
thường được gọi là các hàm, chúng nằm trong một lớp và chỉ được áp dụng cho các đối
tượng của lớp. Giống như thuộc tính, phương thức cũng có tính trông thấy được là :
public, private, proteted.
Liên kết – Association
Một liên kết là một sự nối kết giữa các lớp, mối liên quan về ngữ nghĩa giữa các đối
tượng của các lớp tham gia liên kết. Liên kết thường mang tính 2 chiều, có nghĩa khi một
đối tượng này liên kết với đối tượng khác thì cả 2 đối tượng đều nhìn thấy nhau. Một mối
liên kết thể hiện bằng số lượng các đối tượng của 2 lớp có thể tham gia liên kết.
Mối liên kết có thể có các vai trò - role. Các vai trò được nối với mỗi lớp bao chứa
quan hệ. Vai trò của một lớp là chức năng mà nó đảm nhận từ góc nhìn của lớp kia. Tên
vai trò được ghi kèm với mũi tên chỉ từ hướng lớp chủ nhân ra, thể hiện lớp này có vai trò
như thế nào đó với lớp hướng mũi tên chỉ tới.
Ta có thể sử dụng mối liên hệ một chiều bằng cách thêm mũi tên vào một đầu của
liên kết. Mũi tên chỉ ra rằng quan hệ chỉ có thể sử dụng theo chiều mũi tên.
Một liên kết được hạn định liên kết hai lớp và một yếu tố hạn định – qualifier với
nhau. Yếu tố hạn định là một thuộc tính hạn chế số lượng thành phần tham gia trong một
mối liên kết. Có thể hạn định các mối quan hệ một – nhiều hoặc nhiều – nhiều.
Bên cạnh những liên kết thông thường, UML[1] còn đưa ra 1 số liên kết : Liên kết
VÀ, Liên kết HOẶC, Liên kết ĐỆ QUY, Liên kết ĐƯỢC SẮP XẾP, Liên kết TAM
NGUYÊN.
Quan hệ kết tập - Aggregation
Kết tập là một trường hợp đặc biệt của liên kết. Kết tập biểu thị rằng quan hệ giữa
các lớp dựa trên nền tảng nguyên tắc “một tổng thể được tạo bởi các bộ phận”. Nó được
sử dụng khi chúng ta muốn tạo ra một thực thể mới bằng cách tập hợp tất cả thực thể tồn
tại với nhau. Quá trình ghép các bộ phận lại với nhau để tạo nên thực thể gọi là sự kết tập.
Ký hiệu UML cho kết tập là đường thẳng hình thoi đặt sát lớp kết tập. Mỗi thành phần tạo
nên tổng thể gọi là một bộ phận . Mỗi bộ phận có thể là sự kết tập khác.
4
Khái quát hóa và chuyên biệt hóa - Generalization & Specialization
Chuyên biệt hóa là quá trình tinh chế một lớp thành một lớp chuyên biệt hơn.
Chuyên biệt hóa bổ sung các chi tiết. Đơn giản thì chúng ta coi khái quát hóa và chuyên
biệt hóa chính là mối liên hệ giữa lớp cha và lớp con trong kế thừa.
Phụ thuộc và nâng cấp - Dependency & Refinment
Quan hệ phụ thuộc là một sự liên quan ngữ nghĩa giữa 2 phần tử mô hình, một mang
tính chất độc lập, một mang tính chất phụ thuộc. Mọi sự thay đổi từ phần tử độc lập đều
ảnh hưởng tới phần tử phụ thuộc. Phần tử mô hình có thể là một lớp, một gói,..Quan hệ
phụ thuộc được biểu diễn bằng một đường gạch rời - dash line với mũi tên giữa các phần
tử mô hình.
Nâng cấp là một quan hệ giữa hai lời miêu tả của cùng một sự việc, nhưng ở mức
độ trừu tượng hóa khác nhau. Nâng cấp cũng có thể là mối quan hệ giữa một loại đối
tượng và lớp thực hiện nó. Quan hệ nâng cấp được biểu diễn bằng đường gạch rời với mũi
tên rỗng.
Biểu đồ lớp là biểu đồ quan trọng trong mô hình UML[1], biểu đồ lớp là cơ sở cho
hàng loạt các biểu đồ khác. Tuy nhiên, làm sao chúng ta có thể biết được biểu đồ vừa
được tạo ra là tốt hay không tốt ? UML[1] với đặc tả OCL[5] có thể cung cấp ngữ pháp và
ngữ nghĩa cho ta làm việc nhưng nó không cho chúng ta biết biểu đồ được tạo ra có tốt
hay không. Mặt khác, điều chủ chốt khi chúng ta thiết kế biểu đồ là thứ chúng ta muốn
nói về hiện thực hệ thống. Câu hỏi đặt ra là có cách nào thể hiện hiện thực hệ thống ứng
với đặc tả UML[1] với OCL[5] ? Trong phần sau chúng ta đi xem xét ngôn ngữ ràng
buộc đối tượng OCL[5] đặc tả những ràng buộc cho một mô hình UML[1] và cụ thể sẽ
tập trung vào vấn đề đặc tả ràng buộc cho biểu đồ lớp.
1.2 OCL – Object Constraint Language
Trong quá trình phát triển phần mềm người ta nhận ra rằng, chỉ với hệ thống ký hiệu
trực quan trong UML[1] không thể đặc tả được hết các khía cạnh thực tế của hệ thống
phần mềm. Chính vì thế, OCL[5] được xây dựng và phát triển với mục đích bổ sung cho
các đặc tả UML[1] trở nên rõ ràng và chính xác hơn. Và OCL[5] trở thành chuẩn ngôn
ngữ đặc tả cho các biểu đồ trong UML[1] trong thực tế. Trong phần này chúng ta quan
tâm chủ yếu tới cách thức biểu diễn đặc tả OCL[5] trên biểu đồ lớp, tập trung vào biểu
diễn các ngữ cảnh, các bất biến, tiền điều kiện, hậu điều kiện cho phương thức.
OCL được sử dụng
Giống như một ngôn ngữ truy vấn
Các biểu thức OCL[5] có thể được sử dụng trong mọi mô hình UML[1] để biểu diễn
giá trị. Giá trị biểu diễn của nó có thể là một giá trị kiểu cơ sở hay tham chiếu tới đối
tượng.
Mô tả sự bất biến trong các lớp và các kiểu bên trong các mô hình lớp
5
Một bất biến trong lớp và các kiểu bên trong lớp là một ràng buộc luôn luôn đúng.
Mô tả sự bất biến cho lớp và các kiểu bên trong lớp chính là xác định những ràng buộc
tổng quát cho lớp và các kiểu bên trong mô hình lớp.
Đặc tả bất biến kiểu cho mẫu – stereotypes.
Mô tả tiền điều kiện và hậu điều kiện trong các phương thức.
Đặc tả các ràng buộc của thuộc tính lớp, các phương thức.
1.2.1 Biểu diễn đặc tả OCL
Cách thức thứ nhất : Biểu diễn các biểu thức OCL[5] ngay trên biểu đồ UML[1]. Hình 1
là một ví dụ cho cách biểu diễn này.
Cách thức thứ hai : Biểu diễn các biểu thức đặc tả OCL[5] bằng tài liệu. Lúc này, các
biểu thức OCL[5] được viết trên các tài liệu. Người xem có thể tham chiếu từ các biểu đồ
UML[1] đến tài liệu này. Trong thực tế thì cả 2 cách trên được sử dụng đồng thời với
nhau.
Hình 1. Biểu diễn đặc tả OCL trên biểu đồ lớp[5]
6
1.2.2 Đặc tả OCL trên biểu đồ lớp
1.2.2.1 Khai báo ngữ cảnh
OCL[5] là một ngôn ngữ hình thức, chúng được biểu diễn dưới dạng biểu thức.Biểu
thức OCL[5] dùng để đặc tả cho UML[1] luôn luôn phải gắn liền với một đối tượng trong
mô hình UML[1]. Do vậy trước khi tiến hành biểu diễn biểu thức OCL[5] chúng ta phải
khai báo ngữ cảnh mà biểu thức OCL[5] tham gia.
Cú pháp khai báo một ngữ cảnh :
Khai báo một ngữ cảnh bắt đầu bằng từ khóa context và tiếp đến là tên ngữ cảnh.
Ví dụ khai báo ngữ cảnh có tên là Bank: context Bank
Sử dụng “--” để viết chú thích cho biểu thức OCL[5], nó giống như “//” trong C++.
Từ khóa seft
Biểu thức OCL[5] luôn được đặt trong một ngữ cảnh cụ thể, và để chỉ ra thể hiện
của đối tượng trong ngữ cảnh đó chúng ta sử dụng từ khóa seft.
1.2.2.2 Khai báo một bất biến - invariant
Một ràng buộc bất biến là một ràng buộc được liên kết tới một lớp cụ thể trong một
ngữ cảnh cụ thể. Mục đích của một ràng buộc bất biến là chỉ rõ sự bất biến tại một khía
cạnh nào đó của lớp. Một ràng buộc bất biến chứa một biểu thức OCL[5]. Biểu thức này
phải đúng cho mọi thể hiện của phân loại lớp tại mọi thời điểm. Chỉ khi một thể hiện thực
thi một phép toán thì không cần đánh gía biểu thức này là đúng.
Cú pháp khai báo một bất biến[5]:
Khai báo một bất biến bắt đầu với từ khóa inv, tiếp đến là tên của bất biến.
Ví dụ : context Company --khai báo ngữ cảnh có tên là Company
inv : seft. numberOfEmployees > 50 --Khai báo một bất biến.
Ý nghĩa : Mọi thể hiện của đối tượng Company phải thỏa mãn ràng buộc
numberOfEmployees > 50 tại mọi thời điểm.
Từ khóa seft tham chiếu tới thể hiện của đối tượng Company, sử dụng toán tử “.” để chỉ
tới thuộc tính numberOfEmployees của đối tượng Company.
1.2.2.3 Tiền điều kiện và hậu điều kiện – pre & post condition
Tiền điều kiện và hậu điều kiện là các ràng buộc liên kết tới phương thức của một
phân loại lớp. Mục đích của tiền điều kiện là chỉ rõ điều kiện phải có trước khi phương
thức thực thi. Tiền điều kiện chứa một biểu thức OCL[5] (trả về kết quả Boolean). Biểu
thức OCL[5] này phải được đánh giá là đúng bất cứ khi nào phương thức bắt đầu thực thi,
nhưng việc đánh giá này chỉ áp dụng cho thể hiện thực thi phương thức.Mục đích của hậu
điều kiện là chỉ rõ điều kiện phải có sau khi thực thi phương thức. Hậu điều kiện cũng
được biểu diễn bằng một biểu thức OCL[5] (trả về kết quả Boolean). Việc đánh giá biểu
7
thức OCL[5] tại thời điểm kết thúc thực thi phương thức. Bên trong ràng buộc tiền điều
kiện không sử dụng toán tử @pre nhưng bên trong ràng buộc hậu điều kiện có thể sử
dụng @pre để tham chiếu tới giá trị của tiền điều kiện[5].
Cú pháp[5]:
context Typename::operationName(para1 : Type1, para2 : Type2,...)Return Type
pre: --Khai báo các tiền điều kiện
post: --Khai báo các hậu điều kiện
hoặc:
context Typename::operationName(para1 : Type1, para2 : Type2,...)Return Type
pre preconditionName : --Khai báo tiền điều kiện
post postconditionName: --Khai báo hậu điều kiện
Ví dụ :
context Person::income(d : Date) Return interger
pre preOK: d > 0 --Tiền điều kiện: đảm bảo d > 0
post postOK: result > 5000
--Hậu điều kiện đảm bảo trả về kết quả > 5000.
1.2.2.4 Ngữ cảnh gói – package context
Một biểu đồ UML[1] thường có nhiều biểu đồ con trong đó. Do vậy OCL[5] cung
cấp cho chúng ta cặp từ khóa package và endpackage để làm tăng sự rõ ràng khi nhóm
lại các khai báo các bất biến, tiền điều kiện hậu điều kiện... thuộc về cùng một ngữ cảnh
nào đó trong cụm từ khóa package và endpackage.
Cú pháp[5]:
package Package::SubPackage
--Bắt đầu bằng từ khóa package
context X inv : --Khai báo các bất biến
context X ::operationName(para1 : Type1, para2: Type2,...) Return Type
pre preconditionName : --Khai báo các tiền điều kiện
post postconditionName: --Khai báo các hậu điều kiện
...
endpackage
--Kết thúc với từ khóa endpackage
1.2.2.5 Biểu thức bodyB
Biểu thức body là một biểu thức kiên kết tới một phương thức của phân loại lớp.
Nó được đánh dấu tới một phương thức truy vấn. Hành vi của một biểu thức OCL[5] như
8
một body phương thức phải thỏa mãn kiểu kết quả trả về của phương thức. Biểu thức
body có thể sử dụng lẫn với các biểu thức trong ràng buộc tiền điều kiện và hậu điều kiện.
Cú pháp[5]:
context TypeName::operation(para1 : Type1, para2 : Type2...): Return Type
body : --Biểu thức OCL.
Ví dụ [5]:
context
Person::getCurrentSpouse(): Person
pre : seft.isMarried = true
body : seft.mariages->select(m | m.ended = false).spouse
1.2.2.6 Giá trị khởi tạo và giá trị dẫn xuất – Initial and Derived Values
Một biểu thức khởi tạo giá trị là một biểu thức được liên kết tới một thuộc tính của
một phân loại lớp hoặc một mút liên kết – association End. Giá trị khởi tạo thuộc tính bởi
biểu thức phải phù hợp với kiểu của thuộc tính được đinh nghĩa trước đó trong phân loại
lớp. Tương tự, giá trị khởi tạo của một liên kết phải phù hợp với loại mút liên kết. Ví dụ
như, giá trị khởi tạo của mút liên kết là loại đính kèm với phân loại lớp khi số liên kết tối
đa là một, khi mút liên kết nhiều hơn một thì phải là một OrderedSet. Một biểu thức dẫn
xuất cũng là một biểu thức được liên kết tới một thuộc tính của một phân loại lớp hoặc là
một liên kết cuối. Giá trị thuộc tính dẫn xuất tạo ra bởi biểu thức OCL[5] cũng phải phù
hợp với kiểu của thuộc tính được định nghĩa trước đó. Khác với biểu thức khởi tạo giá tri,
biểu thức dẫn xuất là một bất biến. Giá trị thuộc tính, hoặc giá trị liên kết cuối luôn bằng
giá trị được đánh giá trong biểu thức dẫn xuất[5].
Cú pháp[5] :
Khởi tạo giá trị thuộc tính :
context TypeName::AtributeName:Type
init : --Biểu thức OCL để khởi tạo giá trị thuộc tính
Dẫn xuất giá trị mút liên kết[5]
context TypeName::associcationRoleName:Type
derived: --Biểu thức OCL để dẫn xuất giá trị liên kết
Ví dụ[5]:
context Person::income:Interger --Khởi tạo giá trị thuộc tính income của đối tượng
Person
init: parents.income->sum()*1%
derived: if underAge
then parents.income->sum()*1%
9
else job.salary
endif
1.2.2.7 Biểu thức let
Một biến hoặc chức năng được định nghĩa bởi biểu thức let có thể được sử dụng
đồng nhất giống như thuộc tính, phương thức của một lớp. Và biểu thức let chỉ được sử
dụng trong một biểu thức OCL[5], điều này gần giống như việc khai báo biến, phương
thức của một lớp là kiểu private .Các biến trong biểu thức let phải được định kiểu và khởi
tạo giá trị trước khi sử dụng trong biểu thức OCL[5].
Ví dụ:
context Person inv :
let income : Interger = self.job.salary->sum() in
--Khai báo biểu thức let, income được khai báo kiểu interger và được khởi tạo giá trị
if isUnemployed then
income < 100
else
income > 100
endif
1.2.2.8 Biểu thức def
Một ràng buộc được định nghĩa trong biểu thức def được liên kết tới một lớp. Trong
biểu thức def có thể chứa các biểu thức let. Việc khai báo biểu thức là def cũng tương ứng
như việc khai báo một biến, phương thức có dạng public trong lập trình hướng đối tượng.
Và khi đó biểu thức dạng def được sử dụng bởi các biểu thức OCL[5] khác nhau.
Ví dụ[5]:
context Person
def : income:Interger = seft.job.salary->sum()
def: hasTitle(t: String):Boolean = seft.job->exists(title = t)
--Khai báo ngữ cảnh mà sẽ khai báo các biểu thức def
--Sau khi khai báo biểu thức def như trên, thì biến income sẽ được sử dụng trong
các biểu thức thuộc ngữ cảnh Person mà không cần khai báo lại.
1.2.3 Kiểu tập hợp và các phép toán trên tập hợp
OCL cung cấp 4 kiểu tập hợp : Set, OrderedSet, Bag và Sequence và một tập hợp
trừu tượng cho tất cả các kiểu tập hợp khác Collection
10
Bảng 1. Kiểu dữ liệu tập hợp trong OCL
Kiểu tập hợp
Ý nghĩa
Set
Tập bao gồm các phần tử toán học. Các phần tử trong tập hợp
không được lặp lại.
OrderedSet
Bag
Là một Set. Nhưng các phần tử được sắp xếp theo thứ tự.
Là một tập hợp các phần tử cho phép sự lặp lại các phần tử.
Sequence
Tập bao gồm các phần tử được sắp xếp, và cho phép một phần tử
được xuất hiện nhiều lần.
Các phép toán trên Collection
Bảng 2. Phép toán trên tập hợp OCL
Phép toán
Giá trị trả về
Ý nghĩa
=(c: Collection(T)) Boolean
Trả về true nếu 2 tập hợp cùng kiểu và cùng có
số lượng phần tử, thứ tự phần tử.
<>(c:Collection(T)) Boolean
Trả về true nếu 2 tập hợp không bằng nhau
Số lượng phần tử có trong tập hợp
c->size()
Interger
c->includes(object : Boolean
T)
true nếu object là một phần tử của tập hợp
c->excludes(object : boolean
T)
Trả về giá trị true nếu object không thuộc tập
hợp c
c->count(object : T) interger
Trả về số lần xuất hiện của phần tử object
trong tập hợp c
c1->includesAll(c2: boolean
Collection(T))
Trả về true nếu c1 chứa tất cả phần tử c2
c->isEmpty()
boolean
Trả về true nếu c là tập rỗng hay số lượng
phần tử là 0
c->notEmpty()
c->max()
boolean
Type
Trả về true nếu số phần tử của c lớn hơn 0
Trả về giá trị lớn nhất của tập hợp c, với kiểu
11
là Type (kiểu dữ liệu trong tập hợp c). Chỉ
dùng cho tập có kiểu Interger và Real
c->min()
c->sum()
Type
Type
Trả về giá trị nhỏ nhất trong tập c. Chỉ dùng
cho tập có kiểu Interger hoặc Real.
Trả về tổng các phần tử trong tập c. Áp dụng
cho tập Interger và Real.
c1->product(c2:
Collection(T2))
Set(Tuple(first Phép tích đề các giữa 2 tập hợp trả về là 1 tập
: T1, second : hợp.
T2))
c->asSet()
Set(T)
Loại bỏ các phần tử lặp lại trong tập hợp
c->asOrderedSet()
c->asSequence()
c->asBag()
OrderedSet(T) Trả về tập hợp OrderedSet
Sequence(T)
Bag(T)
Trả về tập hợp Sequence
Trả về tập hợp Bag
c->flatten()
Collection(T2) Loại bỏ các phần tử không có cùng kiểu với
kiểu dữ liệu của tập hợp
1.2.4 Biểu thức lặp trên tập hợp
Các biểu thức lặp trên Colltection cũng đúng trên Set, OrderedSet, Bag và Sequence
Bảng 3. Biểu thức lặp trên tập hợp OCL
Collection Set
OrderedSet
Bag
Sequence
exists
select
select(ex:
select
select(expression
Oclexpression):OrderedSet(T)
:Oclexpression):Seque
forAll
reject
reject(ex:
reject
reject
Oclexpression):OrderedSet(T)
isUnique collectNested collectNested(ex:
Oclexpression):Sequence(T)
collectNested collectNested
any
sortedBy
sortedBy(ex:
sortedBy
sortedBy
Oclexpression):OrderedSet(T)
12
one
collect
1.3 Kết luận
Như vậy trong chương 1, em đã trình bày những khái niệm cơ bản trong UML[1] và
OCL[5]. Trọng tâm của chương một là trình bày về biểu đồ lớp, các thành phần của một
lớp, liên kết giữa các lớp trong biểu đồ. Một điều dễ nhận thấy là UML[1] với hệ thống ký
pháp trực quan giúp chúng ta dễ hiểu về hệ thống. Chúng ta sử dụng thêm OCL[5] để đặc
tả các ràng buộc chặt chẽ hơn cho các yếu tố mô hình UML[1]. Tuy nhiên các công cụ
đặc tả UML[1] với OCL[5] hiện nay không cung cấp khả năng tự đánh giá tính đúng đắn
của mô hình được xây dựng ví dụ như việc kiểm tra tính đúng đắn của các ràng buộc
OCL[5], hay khả năng tự sinh thể hiện cụ thể cho mô hình. Một giải pháp là chuyển đổi
mô hình UML[1] sang mô hình Alloy[2] để có thể kiểm tra và sinh thể hiện từ đặc tả mô
hình tự động bằng công cụ Alloy Analyzer[6].
Chương 2, em sẽ trình bày khái quát về Alloy[2], công cụ Alloy Analyzer[6].
Chương 2. Giới thiệu Alloy và công cụ Alloy Analyzer
13
2.1 Khái quát về Alloy
Lịch sử hình thành, phát triển: Alloy[2] được đưa ra và phát triển tại học viện công
nghệ Massachusetts - Massachussets Instutite Techology của Mỹ. Người có công đóng
góp lớn trong đó là giáo sư Daniel Jackson[6].
Alloy[2] là ngôn ngữ mô hình dựa trên logic vị từ bậc nhất. Mô hình Alloy[2] chứa
các khai báo: ký hiêu- ký hiệu, sự kiện - fact,trường - field,mệnh đề- predicate, chức năng
- function. Mỗi ký hiệu biểu diễn tập các nguyên tử - atoms thành phần thực thể cơ bản
của Alloy[2]. Mỗi trường – field thuộc về một ký hiệu biểu diễn quan hệ giữa hai hoặc
nhiều ký hiệu khác. Quan hệ trong Alloy[2] cũng giống như quan hệ trong cơ sở dữ liệu
là tập các bộ nguyên tử.
Có rất nhiều sự tương đồng giữa Alloy[2], biểu đồ lớp UML[1] và OCL[5]. Cụ thể
như : Alloy[2] là ngôn ngữ mô hình hóa hướng đối tượng, Alloy[2] cũng có các quan hệ
đặc trưng của hướng đối tượng như quan hệ kế thừa,...thêm nữa các khai báo bắt đầu với
từ khóa sự kiện trong Alloy[2] là các ràng buộc vĩnh viễn, tức là bất cứ khi nào thực hiện
mô hình thì thể hiện của mô hình phải thỏa mãn các ràng buộc trong sự kiện, điều này rất
giống với các khai báo bất biến trong đặc tả OCL[5] đối với biểu đồ lớp, ngoài ra
Alloy[2] là ngôn ngữ dựa trên logic vị từ bậc nhất do vậy nó dễ dàng biểu diễn các biểu
thức ràng buộc logic, điều này giúp cho việc chuyển các đặc tả OCL[5] sang Alloy[2]
được dễ dàng hơn.
Alloy[2] chủ yếu được sử dụng để mô hình và phân tích các hệ thống phức tạp về
mặt cấu trúc, hành vi ví dụ như các hệ thống: “name servers, network configuration
protocols, acess control, telephony, scheduling, document structuring, key management,
cryptography, instant messaging, railway switching, filesystem synchonization, sematic
web”[6].Trong kỹ nghệ phần mềm Alloy[2] được “sử dụng chủ yếu ở giai đoạn đặc tả và
phân tích và thiết kế hệ thống”[6].
2.2 Mô hình Alloy
Trong phần này chúng ta cùng tìm hiểu những khái niệm cơ bản về các phần cấu
thành lên mô hình Alloy[2] và cách xây dựng một mô hình Alloy[2].
Một mô hình Alloy[2] thường chứa các khai báo bắt đầu với các từ khóa : sig, pred,
func, check, run, fact. Các khai báo bắt đầu với từ khóa sig giống như khai báo bắt đầu
với từ khóa class trong C++, theo sau khai báo bắt đầu với từ khóa pred là các mệnh đề
logic, cũng tương tự như vậy với các từ khóa func, fact. Cụ thể:
2.2.1 Khai báo ký hiệu - signature
Một ký hiệu giới thiệu một tập các nguyên tử. Một khai báo ký hiệu bắt đầu với từ
khóa sig:
sig A {}
14
giới thiệu một tập tên A. Thực sự thì một ký hiệu thì khác một tập hợp ở điểm, trong một
ký hiệu chúng ta có thể khai báo thêm các quan hệ bên trong đó và có thể định nghĩa một
kiểu mới.
Một ký hiệu có thể là một mở rộng của một ký hiệu khác. Ví như : sig A extend B
{}, thì A là một mở rộng của B.
Một khai báo
m sig A {}
có ý nghĩa là số lượng A là m. Đây là một ràng buộc cho A.
Một khai báo quan hệ bên trong một ký hiệu sẽ giống như khai báo một trường của
ký hiệu đó.
Một khai báo
sig A { f: e }
giới thiệu một quan hệ f trong miền A và khoảng biến thiên bị ràng buộc bởi biểu thức e.
Xét về mặt ý nghĩa thì chúng ta có thể viết như sau :
f: A -> e hoặc
all this : A | this.f : e
có nghĩa là nếu chúng ta có một thành phần đặc biệt là this luôn trỏ tới A thì tập hợp biểu
diễn bởi this.f là một tập con của e.
Bằng cách thêm vào lượng từ cho biểu thức e chúng ta có một khai báo dạng
sig A {f : m e}
khi đó this.f luôn luôn có m thành phần trong tập e.
Alloy[2] cho phép chúng ta xây dựng các lớp trừu tượng bằng cách thêm từ khóa
abstract trước khai báo một ký hiệu. Có thể khai báo các ký hiệu thừa kế từ lớp trừu tượng
này.
2.2.2 Khai báo sự kiện - fact
Một nhóm các ràng buộc có liên hệ và luôn luôn tồn tại và được thực thi cùng
chương trình được tập hợp lại trong một sự kiện. Trong một mô hình Alloy[2] có thể tồn
tại nhiều sự kiện khác nhau. Thứ tự các ràng buộc trong một sự kiện và thứ tự giữa các sự
kiện trong mô hình Alloy[2] là không quan trọng, chúng được thực thi cùng lúc trong
chương trình.
Khai báo một sự kiện với từ khóa fact. Một sự kiện có thể có tên hoặc không có tên.
fact [tên ] {khai báo các ràng buộc }
Một sự kiện cũng giống như một ràng buộc bất biến trong lập trình hướng đối tượng.
Nó tham chiếu tới đối tượng, buộc đối tượng phải giữ các ràng buộc trong toàn bộ quá
trình tồn tại của nó.
15
2.2.3 Khai báo mệnh đề và chức năng – predicate & fuction.
Trong mô hình Alloy[2] ngoài các ràng buộc bất biến kiểu sự kiện luôn luôn được
thực thi thì còn một số ràng buộc chỉ thực thi khi được gọi đến hoặc được sử dụng lại
trong mô hình đó chính là các ràng buộc thuộc nhóm mệnh đề - predicate và chức năng-
function.
Một chức năng là một biểu thức được đặt tên. Nó có tham biến, số lượng tham biến
là tùy chọn. Và tùy chọn có kết quả trả về hay không. Chức năng trong Alloy[2] hoàn
toàn có cấu trúc giống như chức năng trong các ngôn ngữ lập trình. Khai báo một chức
năng bắt đầu với từ khóa func
func [tên chức năng][danh sách tham biến]: [Kiểu dữ liệu trả về]{các ràng
buộc}
Một mệnh đề là một ràng buộc được đặt tên. Nó cũng có danh sách tham biến, số
lượng tham biến là tùy chọn. Khi một mệnh đề được gọi đến thì một biểu thức phải cung
cấp cho mỗi tham biến của mệnh đề có nghĩa là ràng buộc trong mệnh đề tương ứng với
mỗi tham biến sẽ được thay thế bằng một biểu thức khởi tạo. Khai báo một mệnh đề bắt
đầu với từ khóa pred
pred[tên mệnh đề](danh sách tham biến) {Khai báo ràng buộc}
2.2.4 Khai báo khẳng định - assertion
Một khẳng định - assertion là một ràng buộc. Một khẳng định tồn tại độc lập không
phụ thuộc và các sự kiện, mệnh đề...Nhóm những ràng buộc khẳng định một điều gì đó
được tập hợp lại vào một khẳng định. Đôi khi, trong mô hình một khẳng định dùng để
kiểm tra một hoặc nhiều sự kiện. Kết quả thực hiện một khẳng định sẽ cho một trong 2 kết
quả là tìm ra phản ví dụ cho khẳng định bên trong khẳng định được thực thi hoặc không
tìm thấy phản ví dụ, điều này là rất có ích để kiểm tra tính toàn vẹn của mô hình. Trong
mô hình có thể dùng nhiều khẳng định và các khẳng định được đặt tên. Khai báo khẳng
định bắt đầu với từ khóa assert.
assert [tên khẳng định] {các biểu thức ràng buộc }
2.2.5 Lệnh trong Alloy
Trong Alloy[2] khi muốn phân tích mô hình chúng ta phải viết lệnh. Lệnh bắt đầu
với từ khóa run thông báo cho bộ phân tích Alloy[2] tìm kiếm thực thể của một mệnh đề
xác định. Lệnh bắt đầu với từ khóa check thông báo cho bộ phân tích tìm kiếm phản ví dụ
cho một khẳng định xác định. Trong khi đưa ra các dòng lệnh chúng ta có thể đưa thêm
vào phạm vi, phạm vi sẽ giới hạn số lượng các thể hiện phải có trong một mệnh đề hoặc
là số lượng phản ví dụ.
Để xác định chính xác phạm vi dòng lệnh thì cần thiết phải giới hạn cho mỗi ký hiệu
. Việc thực hiện giới hạn cho ký hiệu cha cũng thỏa mãn giới hạn cho ký hiệu con.
16
2.2.6 Khai báo mô đun
Alloy[2] cung cấp một hệ thống mô đun đơn giản nó cho phép chia một mô đun lớn
thành nhiều mô đun nhỏ hơn và cũng tiện lợi trong việc tạo ra các thư viện riêng được
đinh nghĩa trước đó. Mỗi mô đun tương ứng với một file. Mỗi mô đun biểu diễn bằng tên
đường dẫn tương ứng với tên file trong hệ thống. Khai báo một mô đun bắt đầu với từ
khóa module tiếp đến là tên đường dẫn.
module đường_dẫn_mô_đun
Mỗi mô đun muốn sử dụng một mô đun khác thì phải đính nó vào bằng cách sử
dụng khai báo bắt đầu bằng từ khóa import và theo sau là đường dẫn tới file.
import đường_dẫn_mô_đun
Mô đun chính là không gian tên cho các khai báo bên dưới nó. Khi có 2 ký hiệu có
tên giống nhau thì lúc này muốn sử dụng ký hiệu đó thì cần thêm vào trước đó không gian
tên chính là tên đường dẫn mô đun. Thông thường thì mỗi đường dẫn mô đun sẽ có một
biệt danh cho nó để tránh sự dài dòng trong trình bày.
2.2.7 Thực thi mô hình Alloy
Trong phần trước chúng ta đã tìm hiểu các thành phần cơ bản của một mô hình
Alloy[2] ký hiệu, sự kiện, trường, mệnh đề ... trong phần này chúng ta tìm hiểu cách thực
thi mô hình tức là làm thế nào để đưa ra các thể hiện mô hình, hoặc tìm ra các thể hiện sai
của mô hình.
Alloy[2] cung cấp cho chúng ta công cụ phân tích tự động Alloy Analyzer, với sự
giúp sức của công cụ sẽ đưa ra các thể hiện theo ý muốn của chúng ta một cách nhanh
chóng và trực quan.
Các thể hiện được tìm ra khi chúng ta thực thi dòng lệnh run. Thể hiện của mô hình
là các cụ thể hóa của các ký hiệu với các trường - field và phải thỏa mãn các ràng buộc
trong sự kiện. Chỉ những ký hiệu được chỉ rõ trong sự kiện thì mới cần phải thỏa mãn sự
kiện đó, điều này tương tự như từ khóa context trong OCL[5], sẽ chỉ ra đối tượng nào
được chỉ ra trong ngữ cảnh- context đó thì mới cần tuân thủ các biểu thức OCL[5] được
khai báo trong đó.
2.3 Công cụ Alloy Analyzer
Từ phiên bản đầu tiên được phát hành kèm theo bộ phân tích Alloy Analyzer[6], đến
thời điểm hiện tại Alloy[2] đang là phiên thứ 4 và kèm theo nó là bộ phân tích Alloy
Analyzer[6] phiên bản thứ 4. Bộ phân tích Alloy Analyzer[6] là một công cụ mạnh mẽ sử
dụng để tìm kiếm tất cả thể hiện của một mô hình được đặc tả trong mô hình Alloy[2].
Bằng cách thức chạy một mệnh đề (run mệnh đề), bộ phân tích Alloy Analyzer[6] sẽ tìm
kiếm tất cả thể hiện mô hình thỏa mãn các ràng buộc mô hình hoặc bộ phân tích Alloy
Analyzer[6] sẽ tìm các thể hiện là phản ví dụ của đặc tả mô hình khi chay lệnh check
17
Giao diện chính của bộ phân tích Alloy Analyzer[6]
Hình 2. Công cụ Alloy Analyzer
“Sử dụng công cụ cung cấp cho chúng ta các tùy chọn cho việc trình diễn thể hiện
mô hình như : dạng cây thư mục, dạng siêu dữ liệu XML hay dạng Visualsation là dạng
biểu diễn đồ họa của mô hình”[6].
2.4 Ví dụ đặc tả Alloy
Đặc tả danh sách địa chỉ.
Mô tả phi hình thức
ContactBook là một cuốn danh bạ địa chỉ các cá nhân trong đó có:
Tên ,địa chỉ (nơi làm việc và nhà riêng), số điện thoại (di động, và cố định), địa chỉ
mail,
Các ràng buộc : Không được viết tên, địa chỉ của cùng một người nhiều lần
Các chức năng : Thêm, sửa, xóa một người theo tên
18
Đặc tả Alloy
Thể hiện của mô hình bao gồm các ký hiệu và thỏa mãn các ràng buộc trong sự
kiện. Rõ ràng nếu chỉ sử dụng UML[1] thì chúng ta không thể biểu diễn được các ràng
buộc nói trên. Trong khi đó đặc tả ràng buộc cho ví dụ trên bằng Alloy[2] thì ngắn gọn và
dễ
dàng.
Kết quả
Contact là ký hiệu ảo, nó có các trường mail - địa chỉ hòm thư, addr - địa chỉ nhà,
mobile – số điện thoại, và tele – số điện thoại cố đinh. Mỗi một Contact đều có đủ các
trường trên. Các ký hiệu Name và Address đều kế thừa từ ký hiệu ảo Contact. Contacts là
một ký hiệu trong đó chỉ có một trường biểu diễn quan hệ giữa hai ký hiệu Name và
Address.
Ràng buộc được đưa vào buộc các thể hiện Name, Contact thỏa mãn rằng mỗi thể
hiện của Name chỉ xuất hiện trong Contacts – Danh bạ một lần và trong Contacts – Danh
bạ không có trường hợp các trường mail, addr, mobile, tele xuất hiện hai lần trong đó.
19
Hình 3. Kết quả thực thi mô hình Alloy
Kết quả thực thi mệnh đề : “thêm địa chỉ” –addContact
Mệnh đề thêm địa chỉ được biểu diễn trong Alloy[2] như sau. Đầu vào của mệnh đề
là các biến có kiểu Contacts, Name, Address. Chúng ta định nghĩa rằng việc thêm vàm địa
chỉ tức là ta có một Contacts mới và Contacts mới chính là Contacts cũ thêm với địa chỉ
muốn thêm vào.
Hình 4. Kết quả thực thi mệnh đề "thêm”
Chương 3. Chuyển đổi biểu đồ lớp với đặc tả OCL sang mô hình Alloy
20
Phần trước chúng ta đã biết Alloy[2] là một ngôn ngữ mô hình hóa dựa trên logic vị
từ bậc nhất. Alloy[2] cung cấp các khai báo trừu tượng, các khai báo thừa kế. Cả UML[1]
và Alloy[2] đều làm việc trên tư tưởng hướng đối tượng. Do đó việc chuyển đổi giữa
Alloy[2] và biểu đồ lớp UML[1] là có thể và đảm bảo ý nghĩa được bảo toản. Ngoài ra,
Alloy[2] cũng rất thích hợp trong việc biểu diễn các ràng buộc bởi vì nó dựa trên logic vị
từ bậc nhất do vậy việc chuyển các biểu thức OCL[5] sang Alloy[2] cũng hoàn toàn là có
thể.Hơn thế nữa công cụ phân tích cho Alloy[2] cũng rất mạnh. Dựa vào công cụ Alloy
Analyzer chúng ta có thể trong một thời gian ngắn tìm được ra những thể hiện của mô
hình hoặc kiểm tra độ chính xác của mô hình Alloy[2] ở các mức độ khác nhau bằng cách
đưa ra các loại ràng buộc sự kiện hoặc mệnh đề hoặc khẳng định.
Trong thực tế Alloy[2] đã được sử dụng trong việc kiểm chứng, các vấn đề đòi hỏi
những ràng buộc phức tạp, độ chính xác cao được chuyển thành các mô hình trong
Alloy[2], sau đó các mô hình được kiểm chứng thông qua công cụ Alloy Analyzer.
Một biểu đồ lớp UML[1] với những đặc tả OCL[5] sau khi chuyển được sang mô
hình Alloy[2] sẽ rất có lợi trong việc đưa ra các mô hình đối tượng là một thể hiện cụ thể
của biểu đồ lớp. Ngoài ra còn có lợi trong việc kiểm chứng tính đúng đắn của biểu đồ lớp
bằng cách đưa ra các phản ví dụ là thể hiện cụ thể của biểu đồ lớp vi phạm các ràng buộc
OCL[5].
Như vậy, với những kiến thức đã tìm hiểu về biểu đồ lớp UML[1], đặc tả OCL[5]
cho biểu đồ lớp, Alloy[2] và công cụ Alloy Analyzer. Chúng ta cũng đã làm rõ sự cần
thiết chuyển đổi biểu đồ lớp UML[1] với đặc tả OCL[5] sang Alloy[2]. Khi tiến hành
chuyển đổi chúng ta sẽ chuyển các yếu tố của mô hình UML[1] sang các yếu tố tương
ứng trong mô hình Alloy[2] để đảm bảo tương ứng ngữ nghĩa. Dưới đây là mô hình thực
hiện việc chuyển đổi.
21
Hình 5. Mô hình chuyển đổi biểu đồ lớp với đặc tả OCL sang mô hình Alloy
Mô hình chuyển đổi sẽ có các bước:
Bước thứ nhất : Chuyển biểu đồ lớp UML[1] với các liên kết phức tạp (kết tập, hợp
thành, tổng quát hóa,..) sang biểu đồ lớp với các liên kết đơn giản hơn.
Bước thứ hai : Chuyển biểu đồ lớp UML[1] nhận được từ bước thứ nhất sang mô
hình Alloy[2].
Bước thứ ba : Chuyển các đặc tả OCL[5] sang ràng buộc Alloy[2].
Sau khi thực hiện bước thứ ba, lúc này chúng ta có thể sử dụng kết quả của bước này
thông qua công cụ Alloy Analyzer[6] để đưa ra các thể hiện mô hình.
3.1 Chuyển biểu đồ lớp UML với các liên kết phức tạp sang biểu đồ lớp UML với
các liên kết đơn giản
Mục đích của việc chuyển đổi biểu đồ lớp với các liên kết phức tạp sang biểu đồ lớp
UML[1] với các liên kết đơn giản hơn để làm đơn giản hơn việc chuyển đổi biểu đồ lớp
UML[1] sang mô hình Alloy[2] mã vẫn đảm bảo ngữ nghĩa mô hình tương đương.
Thay vì chuyển đổi một biểu đồ lớp UML[1] với các liên kết phức tạp như quan hệ
kết tập, hợp thành, tổng quát hóa chúng ta sẽ chỉ phải chuyển các biểu đồ lớp UML[1] với
chỉ các liên kết nhị phân. Trong quá trình chuyển đổi này chúng ta sẽ đưa thêm vào các
biểu thức OCL[5] để đảm bảo sự tương đương về ngữ nghĩa giữa biểu đồ lớp UML[1]
trước khi chuyển và biểu đồ lớp UML[1] sau khi chuyển.
22
Tải về để xem bản đầy đủ
51 trang
13/05/2025
160
Bạn đang xem 30 trang mẫu của tài liệu "Khóa luận Chuyển đổi đặc tả UML với OCL sang đặc tả alloy", để tải tài liệu gốc về máy hãy click vào nút Download ở trên.
File đính kèm:
- khoa_luan_chuyen_doi_dac_ta_uml_voi_ocl_sang_dac_ta_alloy.pdf
