Đề tài 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 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 ...................................................................................................................... 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 1 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 2 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,... 3 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. 4  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á