Luận Văn Chuyển đổi đặc tả uml với ocl sang đặc tả alloy

Ơ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
1.1.1 Mục đích của UML . 2
1.1.2 Miền ứng dụng của UML 2
1.1.3 Hệ thống biểu đồ trong UML 3
1.1.4 Biểu đồ lớp . 3
1.2 OCL – Object Constraint Language 5
1.2.1 Biểu diễn đặc tả OCL 6
1.2.2 Đặc tả OCL trên biểu đồ lớp 7
1.2.3 Kiểu tập hợp và các phép toán trên tập hợp . 10
1.2.4 Biểu thức lặp trên tập hợp . 12
1.3 Kết luận . 13
Chương 2 . Giới thiệu Alloy và công cụ Alloy Analyzer 13
2.1 Khái quát về Alloy 14
2.2 Mô hình Alloy 14
2.2.1 Khai báo ký hiệu - signature 14
2.2.2 Khai báo sự kiện - fact 15
2.2.3 Khai báo mệnh đề và chức năng – predicate & fuction . 16
2.2.4 Khai báo khẳng định - assertion 16
2.2.5 Lệnh trong Alloy . 16
2.2.6 Khai báo mô đun . 17
2.2.7 Thực thi mô hình Alloy . 17
2.3 Công cụ Alloy Analyzer . 17
2.4 Ví dụ đặc tả Alloy . 18
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 Quan hệ nhị phân với các lượng từ 23
3.1.2 Chuyển quan hệ tổng quát hóa sang quan hệ nhị phân . 25
3.1.3 Chuyển quan hệ kết tập và tạo thành sang quan hệ nhị phân 28
3.1.4 Chuyển các thành phần của lớp sang Alloy 29
3.1.5 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
3.2 Những vấn đề khi chuyển đổi 35
3.3 Kết luận . 36
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 Yêu cầu của hệ thống 37
4.1.1 Yêu cầu chức năng 37
4.1.2 Ràng buộc cho hệ thống 37
4.2 Thiết kế cơ sở dữ liệu . 38
4.2.1 Biểu đồ lớp . 38
4.2.2 Các ràng buộc được mô tả bằng OCL 38
4.3 Chuyển đổi mô hình thiết kế sang Alloy 39
Kết luận 42
TÀI LIỆU THAM KHẢO