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 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á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. 5  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 6 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] 7 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 8 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ư 9 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% 10 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 --Khai báo ngữ cảnh mà sẽ khai báo các biểu thức def def : income:Interger = seft.job.salary->sum() def: hasTitle(t: String):Boolean = seft.job->exists(title = t) --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 11 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 Là một Set. Nhưng các phần tử được sắp xếp theo thứ tự. Bag 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 c->size() Interger Số lượng phần tử có trong tập hợp c->includes(object : T) Boolean true nếu object là một phần tử của tập hợp c->excludes(object : T) boolean 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: Collection(T)) boolean 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() boolean Trả về true nếu số phần tử của c lớn hơn 0 c->max() Type Trả về giá trị lớn nhất của tập hợp c, với kiểu 12 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() 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. c->sum() Type 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 : T1, second : T2)) Phép tích đề các giữa 2 tập hợp trả về là 1 tập hợp. c->asSet() Set(T) Loại bỏ các phần tử lặp lại trong tập hợp c->asOrderedSet() OrderedSet(T) Trả về tập hợp OrderedSet c->asSequence() Sequence(T) Trả về tập hợp Sequence c->asBag() Bag(T) 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: Oclexpression):OrderedSet(T) select select(expression :Oclexpression):Sequence(T) forAll reject reject(ex: Oclexpression):OrderedSet(T) reject reject isUnique collectNested collectNested(ex: Oclexpression):Sequence(T) collectNested collectNested any sortedBy sortedBy(ex: Oclexpression):OrderedSet(T) sortedBy sortedBy 13 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 14 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 {} 15 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ó. 16 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. 17 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 18 Bộ cài đặt : bao gồm Alloy Analyzer tải về từ địa chỉ và bộ cài JDK 1.5 trở lên tại 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 19 Đặ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 đó. 20 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 21 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. 22 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. 23 3.1.1 Quan hệ nhị phân với các lượng từ Hình 6. Chuyển quan hệ nhị phân với lượng từ[3] Vế trái của hình vẽ trên biểu diễn liên kết nhị phân giữa 2 lớp với lượng từ tham gia. Vế phải là biểu diễn nhị phân của 2 lớp, nhưng lúc này ta không quan tâm tới lượng tử tham gia của 2 lớp trong mối liên hệ. Giải thích viết tắt cho hình 6. ra : Tên vai trò của Class B với Class A, ra : B -> set A rb : Tên vai trò của Class A với Class B, rb : A->set B la..ha : Với một đối tượng là thể hiện của Class B thì số lượng đối tượng của Class A liên hệ với nó trong đoạn từ la đến ha tương tự như vậy với lb..hb. Cả ra, rb đều được gọi với thuật ngữ chung là mút liên kết -association end . Biểu diễn ràng buộc bằng OCL Như đã thấy trong Hình 8 để vế trái và vế phải tương đương nhau thì ta phải thêm vào vế phải ràng buộc OCL[5]. Ràng buộc được đưa ra nhằm biểu diễn ràng buộc về số lượng la..ha và lb..hb thành các ràng buộc OCL[5]. Ràng buộc OCL được thêm vào Ràng buộc tương đương trong Alloy A->forAll(a | a.rb->size >= lb and a.rb- >size forAll(b | b.rb- >size>=la and b.rb->size <= ha)[4] all a : A | #a.rb >=lb and #a.rb <=hb all b: B | #b.ra >=la and #b.ra <=ha Các ràng buộc sẽ được đặt trong các sự kiện trong Alloy[2], điều đó đảm bảo các ràng buộc sẽ luôn luôn được tham chiếu trong suốt quá trình thực thi chương trình. Ví dụ Mô tả : Giả sử chúng ta có liên kết nhị phân giữa 2 lớp Student và Teacher. 24 Hình 7. Ví dụ chuyển quan hệ nhị phân với lượng từ Sau khi chuyển thì lúc này chúng ta không cần quan tâm tới lượng từ tham gia liên kết của 2 lớp nữa. Dưới đây chúng ta sẽ chuyển vế phải của Hình 9 sang biểu diễn Alloy[2]. Ở đây mỗi một lớp chuyển thành một ký hiệu trong Alloy[2], các ràng buộc OCL[5] chuyển tương ứng thành các biểu thức logic Alloy[2]. Bảng 4. Chuyển đặc tả OCL của lớp Student sang Alloy UML[1] và đặc tả OCL Biểu diễn Alloy class Student sig Student class Teacher sig Teacher Student->forAll(s | s.study->size >=5 and s.study->size <=10) and Teacher->forAll(t | t.teach->size >=25 and t.teach->size <=50) all s : Student | #s.study >=5 and #s.study <=10 all t : Teacher | #t.teach >=25 and t.teach <=50 study : Student -> set Teacher chuyển thành một trường trong sig Student teach : Teacher -> set Student chuyển thành một trường trong sig Teacher 25 Biểu diễn đặc tả Alloy Hình 8. Đặc tả Alloy lớp Student 3.1.2 Chuyển quan hệ tổng quát hóa sang quan hệ nhị phân Hình 9. Chuyển quan hệ tổng quát hóa sang quan hệ nhị phân[3] Mô tả : Vế trái Hình 9 biểu diễn quan hệ tổng quát hóa giữa 2 lớp S và G trong đó lớp G là lớp tổng quát hóa, vế phải biểu diễn quan hệ nhị phân giữa 2 lớp S và G và thêm vào đó các lượng tử tham gia quan hệ và ràng buộc. Giải thích Hình 9 rg : Biểu diễn mút liên hệ (association end) giữa 2 lớp S và G và biểu diễn rg : S-> G. Ràng buộc : 26 Chúng ta phải đưa ra ràng buộc để đảm bảo tương đương ngữ nghĩa giữa vế trái và vế phải của hình. Ràng buộc thêm vào đảm bảo một đối tượng của lớp S buộc phải liên hệ với một đối tượng G duy nhất hay là sẽ không có 2 đối tượng thuộc lớp S cùng liên hệ với một đối tượng thuộc lớp G. Biểu diễn ràng buộc bằng OCL S->forAll(s,s’ | ss’ implies s.rg s’.rg ) Ví dụ Mô tả : Giả sử có 2 lớp G và lớp S, trong đó lớp G là lớp tổng quát hóa của lớp S. Lớp G có thuộc tính name kiểu string. Lớp S có thêm thuộc tính old kiểu Old. Mục đích của chúng ta là chuyển quan hệ tổng quát hóa giữa 2 lớp S và G thành quan hệ nhị phân như trình bày ở trên. Hình 10. Ví dụ mô hình chuyển đổi OCL sang Alloy Chuyển vế phải của hình 12 sang biểu diễn Alloy[2]. Mỗi lớp chuyển thành một khai báo ký hiệu trong Alloy[2], mỗi thuộc tính lớp chuyển thành một trường trong ký hiệu tương ứng, mỗi mút liên kết cũng chuyển thành một trường quan hệ trong ký hiệu tương ứng, các ràng buộc OCL[5] chuyển thành các biểu thức ràng buộc logic Alloy[2]. Kiểu của thuộc tính chuyển thành một khai báo ký hiệu. Bảng 5. Quy tắc chuyển quan hệ tổng quát hóa sang quan hệ nhị phân UML và đặc tả OCL Biểu diễn Alloy tương ứng class S sig S Kiểu dữ liệu Old sig Old Thuộc tính old một trường old trong sig S Class G sig G 27 Kiểu dữ liệu string sig string thuộc tính name một trường name trong sig G rg chuyển thành trường trong S ràng buộc OCL : S->forAll(s,s’ | s s’ implies s.rg s’.rg) all s,s’: S | s!= s’ => s.rg != s’.rg và đảm bảo một đối tượng của lớp S chỉ liên hệ với một đối tượng của lớp G. Biểu diễn đặc tả OCL Bên cạnh việc chuyển quan hệ tổng quát hóa hay còn gọi là quan hệ kế thừa trong ngôn ngữ lập trình hướng đối tượng sang quan hệ nhị phân thì chúng ta có thể sử dụng quan hệ kế thừa trong Alloy[2], mỗi lớp trong biểu đồ UML[1] chuyển thành một ký hiệu trong Alloy[2], quan hệ tổng quát hóa biểu diễn trong UML[1] chuyển trực tiếp thành quan hệ kế thừa trong Alloy[2] thông qua cú pháp : sig G{} sig S extends sig G {} Trong đó : G là lớp tổng quát hóa của lớp S. Tổng quát lại quy tắc chuyển đổi đã nêu ở phần 3.1.1 và 3.1.2 chúng ta có quy tắc chuyển đơn giản sau Tên vai trò - role name : Tên vai trò thể hiện vai trò của một lớp với lớp khác, chúng sẽ được chuyển thành các trường quan hệ trong khai báo của ký hiệu tương ứng. Bản số quan hệ -muliticity: Bản số cho biết một đối tượng của lớp này có thể liên hệ với bao nhiêu đối tượng của lớp kia. Bản số quan hệ sẽ được chuyển thành các khai báo bất biến trong OCL[5], tiếp đó các bất biến này được chuyển thành các khai báo logic 28 Alloy[2] và được đặt trong khai báo sự kiện, khai báo này tương đương với khai báo bất biến trong OCL[5], các ràng buộc trong sự kiện luôn luôn được tham chiếu trước tiên khi thực thi chương trình. Tổng quát hóa : Có 2 cách có thể biểu diễn quan hệ này trong Alloy[2], với cách thứ nhất chúng ta sẽ chuyển quan hệ tổng quát hóa sang quan hệ nhị phân bình thường và thêm vào các ràng buộc cho quan hệ, cách thứ 2 chúng ta biểu diễn trực tiếp quan hệ tổng quát hóa trong biểu diễn UML[1] sang quan hệ kế thừa trong Alloy[2] thông qua từ khóa extends. 3.1.3 Chuyển quan hệ kết tập và tạo thành sang quan hệ nhị phân Quan hệ kết tập – Aggregation[1] là dạng đặc biệt của liên kết Association[1], quan hệ kết tập biểu diễn mối quan hệ giữa toàn thể - whole và bộ phận – part. Ràng buộc cho toàn thể - whole chỉ có thể tồn tại khi các bộ phận của nó tồn tại. Quan hệ tạo thành – Composition[1] là dạng đặc biệt của quan hệ kết tập. Quan hệ tạo thành còn thêm ràng buộc cho bộ phận – part, bộ phận chỉ tồn tại bên trong một toàn thể, hay là bộ phận không thể tồn tại ngoài toàn thể. Ngoài ra quan hệ tạo thành còn ràng buộc chia sẻ bộ phận – part tức là, nếu có 2 toàn thể cùng chứa bộ phận như nhau thì 2 toàn thể đó phải trùng nhau. Mô hình chuyển đổi ở đây là từ quan hệ kết tập và tạo thành chuyển sang quan hệ nhị phân và thêm vào quan hệ nhị phân các ràng buộc logic Alloy[2]. Áp dụng quy tắc phần 3.1.1 để chuyển quan hệ nhị phân sang quan hệ trong Alloy[2]. Giải thích hình vẽ: A: Lớp toàn thể - aggregate P : Lớp bộ phận – part rp: Tên vai trò của lớp A đối với lớp P, và rp được biểu diễn rp: A -> set P Ràng buộc Quan hệ kết tập Quan hệ tạo thành 29 Ràng buộc cho toàn thể fact {all a: A | some p: P | p in a.rp} fact {all a: A | some p: P | p in a.rp} Ràng buộc cho bộ phận fact {all p: P | some a: A | p in a.rp} Ràng buộc chia sẻ bộ phận fact {all p: P | some a,a’: A | p in a.rp and p in a’.rp implies a = a’ } 3.1.4 Chuyển các thành phần của lớp sang Alloy Trong các phần 3.1.1, 3.1.2 và 3.1.3 chúng ta đã xem xét và đưa ra cách thức để biểu diễn quan hệ giữa các lớp trong biểu đồ lớp UML[1] sang biểu diễn trong Alloy[2], tuy nhiên các biểu đồ lớp ở trên mới chỉ chứa các lớp được mô tả ở mức khái niệm, các lớp không có thuộc tính, phương thức...Trong phần này sẽ đưa ra cách thức chuyển từng thành phần trong một lớp sang biểu diễn Alloy[2]. Ngoài ra cũng đưa ra cách thức chuyển các kiểu enum sang biểu diễn Alloy[2].  Lớp Mỗi một lớp sẽ được khai báo thành một ký hiệu trong Alloy[2], lớp ảo sẽ được chuyển thành một ký hiệu ảo. Tên lớp chuyển thành tên ký hiệu tương ứng. Hình 11. Chuyển lớp sang ký hiệu Cú pháp biểu diễn ký hiệu : Bắt đầu với từ khóa sig (giống như bắt đầu với từ khóa class), tiếp đến là tên của class tương ứng trong lớp UML[1] . Biểu diễn class Student tương ứng với biểu diễn. 30 Các thuộc tính của lớp sẽ thành các trường được khai báo trong cặp “{}”.  Thuộc tính của lớp Sau khi chuyển một lớp sang một ký hiệu, tiếp đến chúng ta chuyển các thuộc tính của lớp thành các trường trong ký hiệu trong cặp “{}” của ký hiệu tương ứng. Mỗi thuộc tính trong lớp được biểu diễn trong biểu đồ UML[1] với cú pháp tên_thuộc _tính : kiểu_dữ_liệu Tương đương như vậy trong Alloy[2] cũng sẽ là: tên_trường (chính là tên thuộc tính của lớp) : kiểu_dữ_ liệu Các trường trong Alloy[2] được phân cách nhau bởi dấu phẩy “,”. Trong Alloy[2], chỉ hộ trợ 1 số kiểu dữ liệu nguyên thủy. Do vậy, đối với các kiểu dữ liệu của thuộc tính không nằm trong kiểu dữ liệu hỗ trợ của Alloy[2] thì chúng ta sẽ phải tự định nghĩa kiểu dữ liệu đó bằng cách chuyển kiểu dữ liệu đó thành một khai báo ký hiệu. Lớp với thuộc tính Ví dụ trong hình vẽ trên lớp Student có thuộc tính birthday có kiểu dữ liệu Date không được hộ trợ trong Alloy[2] thì chúng ta phải định nghĩa kiểu dữ liệu trên như dưới đây sig Date {day : Int,mont : Int, year : Int} Các trường phân cách nhau bởi dấu phẩy. Và khi đó biểu diễn của lớp Student trong Alloy[2] sẽ đơn giản như sau : sig Student {birthDay : Date} 31  Phương thức của lớp Trong biểu diễn lớp của UML[1], các phương thức được biểu diễn với cú pháp : Kiểu_Trả_về Tên_Phương_thức [biến_1 : Kiểu_của_biến1, biến 2: Kiểu_biến2] {} Kiểu trả về có thể là kiểu void, hoặc một kiểu bất kỳ nào đó, danh sách tham biến là tùy chọn tức là tồn tại các phương thức không có danh sách tham biến. Đến đây chúng ta có 2 cách đều có thể lựa chọn, lựa chọn thứ nhất đối với các phương thức không trả về kết quả (trả về kiểu void) sẽ chuyển thành khai báo mệnh đề trong Alloy[2], lựa chọn thứ hai chuyển các phương thức thành khai báo chức năng trong Alloy[2]. Với cả 2 lựa chọn thì tên phương thức chuyển thành tên mệnh đề hoặc chức năng tùy theo lựa chọn. Danh sách các tham biến và kiểu của chúng được chuyển thành danh sách tham biến của mệnh đề hoặc chức năng tùy theo cách lựa chọn. Như đã đề cập ở phần trước, Alloy[2] chỉ cung cấp một số kiểu dữ liệu là integer ..., do vậy với những kiểu của biến trong danh sách tham biến không nằm trong 2 kiểu của Alloy[2] thì sẽ cần khai báo kiểu của biến đó là một ký hiệu. Giả sử chúng ta có 1 class A với phương thức được khai báo như ở dưới. void operation (para1 : Type1, para2 : Type2) Trong phần trước chúng ta đã đề cấp cách chuyển lớp thành một ký hiệu, các thuộc tính thành các khai báo trường trong ký hiệu tương ứng, tuy nhiên vấn đề là trong khai báo ký hiệu không có khai báo mệnh đề hay chức năng, tất cả khai báo này nằm ngoài ký hiệu. Do đó khi khai báo mệnh đề hay chức năng phải chỉ rõ ký hiệu của nó. Với phương thức operation ở trên chúng ta sẽ chuyển như sau: void operation (para1 : Type1, para2 : Type2) {}-> pred A::operation[para1: Type1, para2 : Type2] {} Đối với phương thức có kết quả trả về typeReturn operation(para1 : Type1, para2 : Type2){} -> 32 fun A::operation[para1 : Type1, para2 : Type2]:typeReturn {} Ví dụ : Cho lớp Student với các đặc tả Hình 12. Lớp với thuộc tính, phương thức và đặc tả OCL Biểu diễn lớp tương ứng trong Alloy : 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 Sự khác biệt OCL[5] và Alloy[2] không cho phép chuyển đổi giữa chúng một cách hoàn toàn. Do vậy chúng ta chỉ đề cập tới một số khía cạnh có thể chuyển đổi từ OCL[5] sang Alloy[2]. Bảng sau mô tả phép chuyển. Các ký hiệu viết tắt col : Biểu diễn một tập hợp – collection trong OCL 33 v : Biến – varable (v) trong biểu thức T : Biểu diễn kiểu của biến be : Biểu diễn biểu thức Boolean e : Biểu diễn biểu thức Bảng 6. Quy tắc chuyển OCL sang Alloy – [4] OCL Alloy col ->forAll(v : T | be) all Tr(v) : Tr(col) | Tr(be) col -> exists(v : T | be) some Tr(v) : Tr(col) | Tr(be) e1 and e2 Tr(e1) && Tr(e2) not e !Tr(e) col -> size() #Tr(col) col -> includes(v : T) Tr(v) in Tr(col) col -> excludes(v : T) Tr(v) ! in Tr(col) col1 -> includesAll(col2) Tr(col2) in Tr(col1) col1 -> excludesAll(col2) Tr(col2) ! in Tr(col1) col -> including(v :T) Tr(col) + Tr(v) col -> excluding(v: T) Tr(col) – Tr(v) col ->isEmpty() no ( col) col ->notEmpty() some (col) if condition then e1 else e2 Tr(condition) =>Tr(e1) else Tr(e2) e.oclIsUndefined #Tr(e) = 0 e -> oclKindOf(v : T) Tr(v) in Tr(e) col1 -> union(col2) Tr(col1) + Tr(col2) col1 -> intersection(col2) Tr(col1) & Tr(col2) 34 col1 ->product(col2) Tr(col1) -> Tr(col2) col->sum() sum Tr(col) Ràng buộc OCL[5] đặc tả biểu đồ UML[1] chúng ta chỉ đề cập tới 2 vấn đề. Vấn đề thứ nhất chuyển các đặc tả bất biến OCL[5] sang biểu thức logic Alloy[2] và vấn đề thứ hai chuyển đặc tả tiền điều kiện và hậu điều kiện của một phương thức sang biểu thức logic Alloy[2].  Bất biến Mỗi bất biến đặc tả OCL[5] được hiểu là ràng buộc cho mọi thể hiện của đối tượng được khai báo trong một ngữ cảnh cụ thể. Do vậy chúng ta sẽ chuyển các bất biến thành các biểu thức ràng buộc Alloy[2] nằm trong sự kiện, và chỉ rõ đối tượng chịu ràng buộc trong sự kiện. Ví dụ với đặc tả lớp Student chúng ta khai báo thuộc tính years (sinh viên năm thứ mấy), giả sử chúng ta có ràng buộc là mọi sinh viên phải là sinh viên năm thứ 1, hoặc 2 ..4. Lớp với thuộc tính và phương thức. Biến seft chỉ các thể hiện của đối tượng Student. Do vậy trong sự kiện chúng ta phải chỉ ra đối tượng Student. Do vậy bất biến này sẽ được viết thành biểu thức logic trong Alloy[2] như sau: fact {all s : Student | int s.years >=1 and int s.years <=4 } all s : Student  Chỉ ra tất cả thể hiện của đối tượng Student. int s.years >=1 and int s.years <=4  Ràng buộc cho thể hiện đối tượng.  Tiền điều kiện, hậu điều kiện của một phương thức. 35 Phần trước chúng ta đã đề cập tới chuyển một phương thức của biểu đồ lớp UML[1] sang Alloy[2]. Khi chuyển một tiền điều kiện và hậu điều kiện của một phương thức trước tiên chúng ta chuyển phương thức đó sang Alloy[2]. Các tiền điều kiện là các điều kiện cho các tham biến, khi đó chúng ta chỉ việc thêm vào các ràng buộc cho các biến trong phương thức được chuyển sang Alloy[2], còn các hậu điều kiện chính là kiểm tra kết quả sau khi thực thi phương thức chúng ta chỉ cần cho biến có kiểu trả về thỏa mãn ràng buộc OCL[5]. Ví dụ chúng ta có phương thức operation(pre : T) và ràng buộc tiền điều kiện là pre > 5 và ràng buộc hậu điều kiện là post < 10. operation(pre : T)  pre operation(pre : T, post : T’) {pre > 5 & post < 10} Tuy vậy việc chuyển các biểu thức hậu điều kiện là tương đối phức tạp. Do vậy trong đây chúng ta chỉ chuyển đổi các biểu thức tiền điều kiện. 3.2 Những vấn đề khi chuyển đổi Mặc dù cả UML[1] và Alloy[2] được thiết kế để mô tả mô hình hướng đối tượng, tuy nhiên UML[1] và Alloy[2] có một số điểm khác biệt trong cách tiếp cận một số khái niệm trong hướng đối tượng ví dụ như cách tiếp cận trong vấn đề thừa kế, ghi đè...do vậy ảnh hưởng tới việc chuyển đổi giữa mô hình UML[1] sang Alloy[2].  Vấn đề thừa kế[4] Cả UML[1] và Alloy[2] đều cung cấp khái niệm thừa kế. Trong UML[1], một lớp con thừa kế từ một hoặc nhiều lớp. UML[1] sử dụng khái niệm “redefine” để thể hiện những thuộc tính hoặc phương thức bị ghi đè ở lớp con. Trong khi đó, một ký hiệu trong Alloy[2] có thể được kế thừa từ một ký hiệu khác và thành phần của ký hiệu là tập con của ký hiệu cha và một ký hiệu con không thể khai báo một trường có tên trùng với tên trường đã có trong lớp cha tức là việc ghi đè trực tiếp trong Alloy[2] là không cho phép.  Không gian tên[4] Mọi thành phần mô hình trong UML[1] đều được định nghĩa trong một không gian tên. Ví dụ như, các lớp trong mô hình UML[1] được đặt trong một không gian tên của gói và các thuộc tính của lớp thì được đặt trong không gian tên của lớp nó thuộc về. Trong khi đó, mọi thành phần trong Alloy[2] đều thuộc về một không gian tên mô đun. Ví dụ như trong đặc tả UML[1] có định nghĩa :”Tập hợp tên của thuộc tính và tên của lớp không cần thiết phải tách rời”. Nhưng trong Alloy[2], tên của ký hiệu có sự tách rời với tên các trường của nó. Chính vì thế trong khi chuyển đổi chúng ta phải chắc chắn tên duy nhất được tạo ra cho mỗi thành phần của Alloy[2] trong cùng một không gian tên mô-đun.  Kiểu được định nghĩa trước[4] Đặc tả UML[1] định nghĩa trước một số kiểu dữ liệu nguyên thủy như (String, Real, Integer...) 36 Trong khi đó, Alloy[2] có một hệ thống kiểu rất đơn giản và chỉ duy nhất kiểu Integer là kiểu dữ liệu nguyên thủy được định nghĩa trước. Ví dụ như kiểu dữ liệu String được đinh nghĩa trước trong UML[1] nhưng không được đinh nghĩa trong Alloy[2], cách tiếp cận cho các vấn đề này là chúng ta khai báo một ký hiệu kiểu String trong mô hình.  Kết tập và tạo thành[4] Trong UML[1] cả kết tập và tạo thành là dạng đặc biệt của liên hệ giữa hai lớp. Alloy[2] không hỗ trợ trực tiếp hai kiểu quan hệ kết tập và tạo thành. Đây là khó khăn khi chuyển đổi biểu đồ lớp với các quan hệ kết tập và tạo thành trong Alloy[2]. Trong khóa luận của mình em có đưa ra cách thức chuyển đổi hai quan hệ trên sang đặc tả Alloy[2] trong phần chương 4.  Mô hình tĩnh và mô hình động[4] Mô hình trong Alloy[2] là mô hình tĩnh. Một mô hình trong Alloy[2] định nghĩa các thể hiện của hệ thống thỏa mãn các ràng buộc. Bản thân Alloy[2] không chứa đựng trong nó khái niệm về trạng thái của hệ thống. Trong khi đó UML[1] sử dụng khái niệm tĩnh để biểu diễn quan hệ cấu trúc giữa các thành phần của hệ thống thông qua các ràng buộc, các đặc tả phương thức với sự thêm vào các điều kiện như tiền điều kiện và hậu điều kiện của phương thức. Một mô hình hệ thống tĩnh được chỉ ra tại một thời điểm thông qua các giá trị của đối tượng, thuộc tính các liên kết giữa các thành phần trong mô hình hệ thống. Một giải pháp cho vấn đề này là sử dụng mẫu mô hình động trong Alloy[2] để giải quyết vấn đề trên. Với cách này chúng ta có thể mô tả được giá trị tiền điều kiện của mỗi phương thức ở trạng thái đầu và mô tả giá trị hậu điều kiện của mỗi phương thức ở trạng thái tiếp theo. 3.3 Kết luận. Như vậy, trong chương 3, em đã trình bày về mô hình chuyển đổi, các quy tắc chuyển đổi giữa các yếu tố của mô hình UML[1] sang các yếu tố mô hình Alloy[2] và các quy tắc chuyển giữa OCL[5] sang Alloy[2]. Cụ thể là các quy tắc chuyển đổi một lớp, các thành phần của lớp sang đặc tả Alloy[2], thể hiện được liên kết nhị phân, các quan hệ kết tập, tạo thành, tổng quát hóa trong biểu diễn biểu đồ lớp UML[1] sang biểu diễn Alloy[2] bằng cách đưa thêm các ràng buộc Alloy[2] logic. Bên cạnh đó, trong chương này còn đề cập tới vấn đề hạn chế khi chuyển đổi từ mô hình UML[1] sang mô hình Alloy[2], có những hạn chế do khách quan và có những yếu tố chủ quan của con người. Trong chương 4, em sẽ trình bày bài toán minh họa áp dụng cho các quy tắc chuyển đổi mà đã nêu trong chương 3. 37 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 4.1 Yêu cầu của hệ thống 4.1.1 Yêu cầu chức năng Hệ thống ATM cung cấp các chức năng chính sau:  Cho phép thao tác với các tài khoản như : thêm, xóa, sửa tài khoản  Cho phép thực hiện các chức năng giao dịch: Rút tiền, gửi tiền, xem thông tin tài khoản. 4.1.2 Ràng buộc cho hệ thống Hệ thống ATM đòi hỏi các ràng buộc sau:  Một máy ATM chỉ có duy nhất các yếu tố sau: màn hình, bàn phím, khe rút tiền.  Tất cả các tài khoản đều nằm trong một cơ sở dữ liệu của ngân hàng. Một tài khoản cụ thể được lưu trữ trong một cơ sở dữ liệu ngân hàng, tức là không tồn tại 2 cơ sở dữ liệu ngân hàng cùng lưu trữ thông tin về một tài khoản cụ thể.  Tại một thời điểm, chỉ có một giao dịch diễn ra.  Hai tài khoản khác nhau thì mã pin và mã cá nhân phải khác nhau.  Mọi tài khoản cụ thể có 2 thông số : tổng số tiền và số tiền có thể sử dụng. Tổng số tiền trong một tài khoản luôn luôn lớn hơn hoặc bằng số tiền có thể sử dụng. Tổng số tiền trong tài khoản nhỏ nhất bằng số dư tài khoản phải có. 38 4.2 Thiết kế cơ sở dữ liệu 4.2.1 Biểu đồ lớp Hình 13. Biểu đồ lớp hệ thống ATM[8] 4.2.2 Các ràng buộc được mô tả bằng OCL Hình 14. Ràng buộc OCL của hệ thống 39 Hình 14 mô tả ràng buộc OCL[5] bên trái và tương đương là đặc tả trong Alloy[2] bên phải. Ràng buộc OCL[5] được mô tả ở đây là ràng buộc cho quan hệ tạo thành giữa 2 lớp Account và lớ BankDatabase. 4.3 Chuyển đổi mô hình thiết kế sang Alloy Lớp ATM: Chuyển đổi lớp ATM sang đặc tả Alloy Hình 15. Đặc tả Alloy của lớp ATM Lớp ATM được chuyển thành khai báo ký hiệu trong Alloy, mỗi thuộc tính của lớp ATM được chuyển thành một trường nằm trong ký hiệu ATM của Alloy. Đối với kiểu của thuộc tính trong lớp ATM thì : Với kiểu dữ liệu được Alloy hỗ trỡ integer thì tất các các kiểu dữ liệu của các thuộc tính khác được khai báo thành các ký hiệu. Trong biểu đồ lớp, lớp ATM tham chiếu tới các lớp BankDatabase,..Screen, Keypad do vậy trong phần thuộc tính của ATM sẽ có các thuộc tính có kiểu là kiểu của các lớp nêu trên. Chúng ta quan sát rằng bản số quan hệ của ATM và BankDatabase, Screen, Keypad đều là 1. Bản số này được biểu diễn thành khai báo hạn định cho trường, chúng ta thấy rằng trong ký hiệu ATM thì hạn định cho các trường là một. 40 Lớp ATM có 3 phương thức. Ba phương thức này được chuyển hoàn toàn thành các mệnh đề - predicate. Danh sách tham biến của các phương thức trong biểu đồ lớp được mang nguyên vẹn thành danh sách tham biến của mệnh đề trong Alloy. Tương tự như vậy đối với các lớp khác. Lớp Account: Chuyển đổi đặc tả lớp Account sang biểu diễn Alloy Hình 16. Đặc tả Alloy của lớp Account Đặc tả ràng buộc hệ thống trong Alloy Đối với mọi thể hiện của Account phải thỏa mãn totalBalance lớn hơn avaiableBalance và totalBalance >5. Ngoài ra, với mọi thể hiện Account cũng phải thỏa mãn : Không có 2 thể hiện nào của Account trùng mã pin và accountNumber 41 Hình 17. Ràng buộc cho hệ thống ATM Kết quả thực thi mô hình 42 Kết luận Trong quá trình thực hiện đề tài Khóa luận tốt nghiệp, em đã tìm hiểu ngôn ngữ UML[1], OCL[5] và các công cụ hỗ trợ đặc tả UML[1] hiện nay. Em cũng đã tìm hiểu các phương pháp để kiểm tra các yếu tố mô hình UML[1] và tập trung vào phương pháp chuyển đổi mô hình UML[1] sang đặc tả Alloy[2] để có thể sử dụng công cụ Alloy Analyzer trong việc phân tích tự động các yếu tố của mô hình. Em đã đặc tả “hệ thống quản lý các tài khoản và các giao dịch ” để minh họa cho phương pháp này. Qua quá trình thực hiện khóa luận, em đã nắm được cách thức đặc tả hệ thống bằng các ngôn ngữ UML[1], OCL[5], Alloy[2] và một phương pháp để kiểm tra các yếu tố mô hình. Trong đó nắm rõ cách thức chuyển đổi biểu đồ lớp UML[1] sang mô hình Alloy[2]. Trong điều kiện xây dựng hoàn chỉnh cơ sở lý thuyết chuyển đổi từ đặc tả biểu đồ lớp UML[1] sang Alloy[2], chúng ta có thể xây dựng công cụ tự động chuyển biểu đồ lớp UML[1] sang Alloy[2]. Alloy[2] cũng hỗ trợ kiểm tra mối quan hệ làm mịn giữa các đặc tả Alloy[2]. Khả năng này của Alloy[2] có thể được sử dụng để kiểm tra mối quan hệ làm mịn giữa 2 đặc tả UML[1]. Tuy nhiên vì thời gian và khả năng có hạn, em chưa thực hiện được ví dụ minh họa cho khả năng này. Em sẽ thực hiện nó trong thời gian tới cùng với việc hoàn thiện các quy tắc chuyển đổi từ mô hình UML[1] sang mô hình Alloy[2] với các trường hợp phức tạp. 43 TÀI LIỆU THAM KHẢO Tài liệu tham khảo tiếng Việt [1]TS. Dương Kiều Hoa – Tôn Thất An – Phân tích và thiết kế hệ thống thông tin theo UML Tài liệu tham khảo tiếng Anh [2] Daniel Jackson – Software Abstractions: Logic, Language, and Analysis – The Mit Press Cambridge, Massachussets London England, 2006 [3]Martin Gogolla, Mark Richters – Expressing UML Class Diagrams Properties with OCL – University of Bremen, FB 3, Computer Science Department , Germany. [4]Kyriakos Anastasakis – UML2Alloy Reference manual – The University of Birmingham School of Computer Science. [5]Object Management Group – Object Constraint Language Version 2.2 [6] [7] [8]Deitel – How to program C++ sixth edition chapter 13