Khóa luận Kiểm chứng mô hình aspect-Uml bằng alloy

1 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Bùi Duy Hải KIỂM CHỨNG MÔ HÌNH ASPECT-UML BẰNG ALLOY KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY Ngành: Công nghệ thông tin HÀ NỘI - 2010 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Bùi Duy Hải KIỂM CHỨNG MÔ HÌNH ASPECT-UML BẰNG ALLOY KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY Ngành: Công nghệ thông tin Cán bộ hướng dẫn: Phạm Thị Kim Dung HÀ NỘI - 2010 LỜI CÁM ƠN Đầu tiên tôi xin gửi lời cảm ơn sâu sắc tới cô giáo Ths.Phạm Thị Kim Dung, bộ môn công nghệ phần mềm, khoa công nghệ thông tin, trường đại học công nghệ, đại học Quốc Gia Hà Nội – người đã định hướng đề tài và tận tình hướng dẫn chỉ bảo tôi trong suốt quá trình thực hiện khóa luận tốt nghiệp này. Tôi cũng xin trân trọng cảm ơn quý thầy cô trong Khoa Công nghệ thông tin trường Đại học Công nghệ, Đai học Quốc Gia Hà Nội đã tận tình giảng dạy, truyền đạt những kiến thức quý báu trong suốt bốn năm học làm nền tảng cho tôi thực hiện khóa luận tốt nghiệp này. Con xin cảm ơn cha mẹ và gia đình đã sinh ra và nuôi dạy con khôn lớn, luôn bên cạnh động viên và ủng hộ con trên con đường mà con yêu thích và lựa chọn. Cám ơn các bạn sinh viên Khoa công nghệ thông tin khóa 2006-2010. Các bạn đã giúp đỡ và ủng hộ tôi rất nhiều cũng như đóng góp nhiều ý kiến quý báu, qua đó, giúp tôi hoàn thiện khóa luận tốt hơn. Mặc dù đã rất nỗ lực, cố gắng nhưng chắc hẳn khóa luận của tôi vẫn còn nhiều thiếu sót. Tôi rất mong nhận được nhiều những ý kiến đánh giá quý, phê bình của quý thầy cô, của anh chị và các bạn. Một lần nữa tôi xin chân thành cảm ơn! Hà Nội, tháng 5 năm 2010 Bùi Duy Hải Mục Lục 1 Chương 1 : MỞ ĐẦU........................................................................................6 1.1 Đặt vấn đề ...................................................................................................6 1.2 Cấu trúc khóa luận ......................................................................................6 2 Chương 2: Giới thiệu về mô hình UML và lập trình hướng Aspect ...................7 2.1 Mô hình UML (Unifined Model Language) ................................................7 2.1.1 Lịch sử phát triển của UML ..................................................................7 2.1.2 Ứng dụng của mô hình UML ................................................................9 2.1.3 Các loại biểu đồ UML.........................................................................12 2.2 Ngôn ngữ ràng buộc đối tượng (OCL) ......................................................13 2.3 Lập trình hướng khía cạnh (Aspect Oriented Programming) .....................15 2.3.1 Phương pháp lập trình hướng khía cạnh ..............................................15 2.3.2 Các khái niệm trong Aspect ................................................................21 3 Chương 3: Kiểm chứng mô hình Aspect-UML ...............................................23 3.1 Giới thiệu về Alloy ...................................................................................23 3.1.1 Alloy là gì? .........................................................................................23 3.1.2 Tính chất của ngôn ngữ alloy ..............................................................23 3.1.3 Cấu trúc một chương trình Alloy ........................................................24 3.1.4 Khai báo trong alloy............................................................................24 3.2 Đặc tả mô hình Aspect-UML trong Alloy .................................................28 3.2.1 Mô hình Aspect UML.........................................................................28 3.2.2 Mô hình viễn thông .............................................................................30 3.2.3 Đặc tả mô hình Aspect UML bằng Alloy ............................................32 3.2.4 Kiểm chứng mô hình Aspect UML sử dụng Alloy ..............................37 4 Chương 4 : Kết luận ........................................................................................40 DANH MỤC HÌNH VẼ Hình 1: Hợp nhất các phương pháp thiết kế bằng UML ....Error! Bookmark not defined. Hình 2: Mô hình UML không biểu diễn hết đặc tả ............Error! Bookmark not defined. Hình 3:OPP ......................................................................Error! Bookmark not defined. Hình 4: Sơ đồ lớp của bài toán vẽ hình ...........................................................................16 Hình 5: Dùng AOP giải quyết bài toán vẽ hình .................Error! Bookmark not defined. Hình 6: Mô hình class cho hệ thống viễn thông.................Error! Bookmark not defined. DANH MỤC BẢNG BIỂU Bảng 1: Ánh xạ giữa các loại join point và pointcut tương ứng .......Error! Bookmark not defined. Bảng 2: Chuyển đổi thành phần cấu trúc mô hình Aspect UML sang Alloy ............Error! Bookmark not defined. DANH MỤC NHỨNG TỪ VIẾT TẮT OOP Object Oriented Programming UML Unifined Model Language OCL Object Contraint Language AOP Aspect Oriented Programming 1 Chương 1 : MỞ ĐẦU 1.1 Đặt vấn đề Ngày nay, công nghệ thông tin ngày càng phát triển và được ứng dụng vào tất cả các lĩnh vực của cuộc sống xã hội. Nó tạo ra một diện mạo mới cho xã hội và nhờ đó nền văn minh nhân loại được nâng lên một tầm cao mới. Công nghệ phần mềm là một phần không thể tách rời trong công nghệ thông tin. Hiện nay ngành công nghệ phần mềm trên thế giới đã và đang phát triển như vũ bão. Những tiến bộ của khoa học kĩ thuật phần cứng đã tạo điều kiện thuận lợi cho công nghệ phần mềm ngày càng phát triển không ngừng. Phần mềm được coi là sản phẩm chính của công nghệ phần mềm.Quá trình phát triển phần mềm gồm nhiều giai đoạn: thu thập yêu cầu, phân tích, thiết kế,xây dựng, kiểm chứng , triển khai và bảo trì. Trong đó việc kiểm chứng phần mềm là hết sức quan trọng để đảm bảo chất lượng của một phần mềm. Kiểm chứng mô hình UML cũng đóng góp vào việc kiểm chứng phần mềm.Việc kiểm chứng mô hình UML + OCL đã được giải quyết [2]. Vấn đề đặt ra bây giờ là kiểm chứng mô hình Aspect-UML(là một mô hình UML đơn giản được mở rộng với việc sử dụng Aspect). Nhờ Aspect và các ràng buộc của nó mà mô hình Aspect UML được cung cấp thêm thông tin. Mô hình Aspect UML có thể được kiểm chứng từ các xung đột tương tác Aspect, để làm tự động công việc kiểm chứng mô hình Aspect UML là chuyển đổi mô hình Aspect UML sang ngôn ngữ đặc tả Alloy. Alloy cung cấp một ngôn ngữ đặc tả mô hình đơn giản dựa trên logic cũng như công cụ mô phỏng[]. Trong phạm vi khóa luận này tôi sẽ chỉ ra quy tắc chuyển đổi một mô hình Aspect UML sang ngôn ngữ Alloy. 1.2 Cấu trúc khóa luận Chương 1: Phần mở đầu. Chương 2: Giới thiệu về mô hình UML và lập trình hướng Aspect. Chương 3: Kiểm chứng mô hình Aspect- UML bằng Alloy Chương 4: Kết luận và hướng nghiên cứu trong tương lai. 2 Chương 2: Giới thiệu về mô hình UML và lập trình hướng Aspect 2.1 Mô hình UML (Unifined Model Language) 2.1.1 Lịch sử phát triển của UML Theo [1] những năm đầu của thập kỷ 90 có rất nhiều phương pháp phân tích, thiết kế hệ thống hướng đối tượng và cùng với chúng là các ký hiệu riêng cho từng phương pháp. Số lượng các phương pháp trong khoảng từ 10 đã lên đến gần 50 trong những năm từ 1989 đến 1994. Ba phương pháp phổ biến nhất là OMT (Object Modeling Technique) [James Rumbaugh], Booch91 [Grady Booch] và OOSE (Object-Oriented Software Enginering) [Ivar Jacobson]. Mỗi phương pháp đều có những điểm mạnh và yếu. Như OMT mạnh trong phân tích và yếu ở khâu thiết kế, Booch91 thì mạnh ở thiết kế và yếu ở phân tích. OOSE mạnh ở phân tích các ứng xử, đáp ứng của hệ thống mà yếu trong các khâu khác. Do các phương pháp chưa hoàn thiện nên người dùng rất phân vân trong việc chọn ra một phương pháp phù hợp nhất để giải quyết bài toán của họ. Hơn nữa, việc các ký hiệu khác nhau của các phương pháp đã gây ra những sự mập mờ, nhầm lẫn khi mà một ký hiệu có thể mang những ý nghĩa khác nhau trong mỗi phương pháp. Ví dụ như một hình tròn được tô đen biểu hiện một multiplicity trong OMT lại là một aggregation trong Booch). Thời kỳ này còn được biết đến với tên gọi là cuộc chiến giữa các phương pháp. Khoảng đầu năm 94, Booch đã cải tiến phương pháp của mình trong đó có ứng dụng những ưu điểm của các phương pháp của Rumbaugh và Jacobson. Tương tự Rumbaugh cũng cho đăng một loạt các bài báo được biết đến với tên gọi phương pháp OMT-2 cũng sử dụng nhiều ưu điểm của phương pháp của Booch. Các phương pháp đã bắt đầu hợp nhất, nhưng các kí hiệu sử dụng ở các phương pháp vẫn còn nhiều điểm khác biệt. Cuộc chiến này chỉ kết thúc khi có sự ra đời của UML – một ngôn ngữ mô hình hóa hợp nhất. Tại sao lại là hợp nhất? Đó là do có sự hợp nhất các cách kí hiệu của Booch, OMT và Objectory cũng như các ý tưởng tốt nhất của một số phương pháp khác như hình vẽ sau: Hình 1:Hợp nhất các phương pháp thiết kế bằng UML Bằng cách hợp nhất các kí hiệu sử dụng trong khi phân tích, thiết kế của các phương pháp đó, UML cung cấp một nền tảng chuẩn trong việc phân tích thiết kế. Có nghĩa là các nhà phát triển vẫn có thể tiến hành theo phương pháp mà họ đang sử dụng hoặc là có thể tiến hành theo một phương pháp tổng hợp hơn( do thêm vào những bước ưu điểm của từng phương pháp). Nhưng điều quan trọng là các ký hiệu giờ đây đã thống nhất và mỗi ký hiệu chuẩn của tổ chức OMG (Object Management Group) vào tháng 7-1997. 2.1.2 Ứng dụng của mô hình UML UML là một ngôn ngữ dùng để:  Trực quan hóa  Cụ thể hóa  Sinh mã ở dạng nguyên mẫu  Lập và cung cấp tài liệu UML là một ngôn ngữ bao gồm một bảng từ vựng và các quy tắc để kết hợp các từ vựng đó phục vụ cho mục đích giao tiếp. Một ngôn ngữ dùng cho việc lập mô hình là ngôn ngữ mà bảng từ vựng( các ký hiệu) và các quy tắc của nó tập trung vào việc thể hiện về mặt khái niệm cũng như vật lý của một hệ thống. Mô hình hóa mang lại sự hiểu biết về một hệ thống. Một mô hình không thể giúp chúng ta hiểu rõ một hệ thống, thường là phải xây dựng một số mô hình xét từ những góc độ khác nhau. Các mô hình này có quan hệ với nhau. UML sẽ cho ta biết cách tạo ra và đọc hiểu được một mô hình đươc cấu trúc tốt, nhưng nó không cho ta biết những mô hình nào nên tạo ra và khi nào tạo ra chúng. Đó là nhiệm vụ của quy trình phát triển phần mềm. 2.1.2.1 UML là ngôn ngữ dùng để trực quan hóa Đối với nhiều lập trình viên, không có khoảng cách nào giữa ý tưởng để giải quyết một vấn đề và việc thể hiện điều đó thông qua các đoạn mã. Họ nghĩ ra và họ viết mã. Trên thực tế, điều này gặp một số vấn đề. Thứ nhất, việc trao đổi về các ý tưởng giữa những người lập trình sẽ gặp khó khăn, trừ khi tất cả đều nói cùng một ngôn ngữ. Thậm chí ngay cả khi không gặp trở ngại về ngôn ngữ thì đối với từng công ty, từng nhóm cũng có những “ngôn ngữ” riêng của họ. Điều này gây trở ngại cho một người mới vào để có thể hiểu được những việc đang được tiến hành. Hơn nữa, trong lĩnh vực phần mềm, nhiều khi khó có thể hiểu được nếu chỉ xem xét các đoạn mã lệnh. Ví dụ như sự phân cấp của các lớp, ta có thể phải duyệt rất nhiều đoạn lệnh để hiểu được sự phân cấp của các lớp. Và nếu như người lập trình không mô tả các ý tưởng mà anh ta đã xây dựng thành mã lệnh thì nhiều khi cách tốt nhất là xây dựng lại trong trường hợp một người khác đảm nhận tiếp nhiệm vụ khi anh ta rời khỏi nhóm Đối với nhiều lập trình viên, không có khoảng cách nào giữa ý tưởng để giải quyết một vấn đề và việc thể hiện điều đó thông qua các đoạn mã. Họ nghĩ ra và họ viết mã. Trên thực tế, điều này gặp một số vấn đề. Thứ nhất, việc trao đổi về các ý tưởng giữa những người lập trình sẽ gặp khó khăn, trừ khi tất cả đều nói cùng một ngôn ngữ. Thậm chí ngay cả khi không gặp trở ngại về ngôn ngữ thì đối với từng công ty, từng nhóm cũng có những “ngôn ngữ” riêng của họ. Điều này gây trở ngại cho một người mới vào để có thể hiểu được những việc đang được tiến hành. Hơn nữa, trong lĩnh vực phần mềm, nhiều khi khó có thể hiểu được nếu chỉ xem xét các đoạn mã lệnh. Ví dụ như sự phân cấp của các lớp, ta có thể phải duyệt rất nhiều đoạn lệnh để hiểu được sự phân cấp của các lớp. Và nếu như người lập trình không mô tả các ý tưởng mà anh ta đã xây dựng thành mã lệnh thì nhiều khi cách tốt nhất là xây dựng lại trong trường hợp một người khác đảm nhận tiếp nhiệm vụ khi anh ta rời khỏi nhóm. Xây dựng mô hình sử dụng ngôn ngữ UML đã giải quyết được các khó khăn trên.Khi trở thành một chuẩn trong việc lập mô hình, mỗi kí hiệu mang một ý nghĩa rõ rang và duy nhất, một nhà phát triển có thể đọc được mô hình xây dựng bằng UML do một người khác viết.Những cấu trúc mà việc nắm bắt thông qua đọc mã lệnh là khó khăn nay đã được thực hiện trực quan.Một mô hình rõ ràng, sáng sủa làm tăng khả năng giao tiếp, trao đổi giữa các nhà phát triển. 2.1.2.2 UML là ngôn ngữ để chi tiết hóa Có nghĩa là xây dựng các mô hình một các tỉ mỉ, rõ ràng, đầy đủ ở các mức độ chi tiết khác nhau. Đặc biệt là UML thực hiện việc chi tiết hoá tất cả các quyết định quan trọng trong phân tích, thiết kế và thực thi một hệ thống phần mềm. 2.1.2.3 UML là ngôn ngữ dùng để sinh ra mã ở dạng nguyên mẫu Các mô hình xây dựng bởi UML có thể ánh xạ tới một ngôn ngữ lập trình cụ thể như : Java, C++… thậm chí cả các bảng trong một CSDL quan hệ hay CSDL hướng đối tượng. Việc các yêu cầu có khả năng thường xuyên thay đổi trong quá trình phát triển hệ thống dẫn đến việc các cấu trúc và hành vi của hệ thống được xây dựng có thể khác mô hình mà ta đã xây dựng. Điều này có thể làm cho một mô hình tốt trở nên vô nghĩa vì nó không còn phản ánh đúng hệ thống nữa. Cho nên phải có một cơ chế để đồng bộ xhóa giữa mô hình và mã lệnh. UML cho phép cập nhật một mô hình từ các mã thực thi ( ánh xạ ngược). Điều này tạo ra sự nhất quán giữa mô hình của hệ thống và các đoạn mã thực thi mà ta xây dựng cho hệ thống đó. 2.1.2.4 UML là ngôn ngữ dùng để lập và cung cấp tài liệu Một tổ chức phần mềm ngoài việc tạo ra các đoạn mã lệnh( thực thi) thì còn tạo ra các tài liệu sau:  Ghi chép về các yêu cầu của hệ thống  Kiến trúc của hệ thống  Thiết kế  Mã nguồn  Kế hoạch dự án  Test  Các nguyên mẫu  … 2.1.3 Các loại biểu đồ UML 2.1.3.1 Biểu đồ lớp(class diagram) Bao gồm một tập hợp các lớp, các giao diện, các collaboration và mối quan hệ giữa chúng. Nó thể hiện mặt tĩnh của hệ thống. 2.1.3.2 Biểu đồ đối tượng(Object diagram) Bao gồm một tập hợp các đối tượng và mối quan hệ giữa chúng. Đối tượng là một thể hiện của lớp, biểu đồ đối tượng là một thể hiện của biều đồ lớp. 2.1.3.3 Biểu đồ use case Khái niệm actor: là những người, hệ thống khác ở bên ngoài phạm vi của hệ thống mà có tương tác với hệ thống. Biểu đồ Use case bao gồm một tập hợp các Use case, các actor và thể hiện mối quan hệ tương tác giữa actor và Use case. Nó rất quan trọng trong việc tổ chức và mô hình hóa hành vi của hệ thống. 2.1.3.4 Biểu đồ trình tự(Sequence Diagram) Là một dạng biểu đồ tương tác (interaction), biểu diễn sự tương tác giữa các đối tượng theo thứ tự thời gian. Nó mô tả các đối tượng liên quan trong một tình huống cụ thể và các bước tuần tự trong việc trao đổi các thông báo(message) giữa các đối tượng đó để thực hiện một chức năng nào đó của hệ thống. 2.1.3.5 Biểu đồ hợp tác (Collaboration) Gần giống như biểu đồ Sequence, biểu đồ Collaboration là một cách khác để thể hiện một tình huống có thể xảy ra trong hệ thống. Nhưng nó tập trung vào việc thể hiện việc trao đổi qua lại các thông báo giữa các đối tượng chứ không quan tâm đến thứ tự của các thông báo đó. Có nghĩa là qua đó chúng ta sẽ biết được nhanh chóng giữa 2 đối tượng cụ thể nào đó có trao đổi những thông báo gì cho nhau. 2.1.3.6 Biểu đồ chuyển trạng thái (Statechart) Chỉ ra một máy chuyển trạng, bao gồm các trạng thái, các bước chuyển trạng và các hoạt động. Nó đặc biệt quan trọng trong việc mô hình hóa hành vi của một lớp giao diện(interface class) hay collaboration và nó nhấn mạnh vào các đáp ứng theo sự kiện của một đối tượng, điều này rất hữu ích khi mô hình hóa một hệ thống phản ứng(reactive). 2.1.3.7 Biểu đồ hoạt động(Activity) Là một dạng đặc biệt của biểu đồ chuyển trạng. Nó chỉ ra luồng đi từ hoạt động này sang hoạt động khác trong một hệ thống. Nó đặc biệt quan trọng trong việc xây dựng mô hình chức năng của hệ thống và nhấn mạnh tới việc chuyển đổi quyền kiểm soát giữa các đối tượng. 2.1.3.8 Biểu đồ thành phần (Component) Chỉ ra cách tổ chức và sự phụ thuộc của các thành phần(component). Nó liên quan tới biểu đồ lớp, trong đó một thành phần thường ánh xạ tới một hay nhiều lớp, giao diện , collaboration. 2.2 Ngôn ngữ ràng buộc đối tượng (OCL) OCL (Object constraint language) là ngôn ngữ xây dựng mô hình phần mềm được định nghĩa như một chuẩn thêm vào UML cho phân tích và thiết kế hướng đối tượng . Các biểu thức viết trong OCL phụ thuộc vào các kiểu lớp, giao diện, …) được định nghĩa trong các biểu đồ UML. Các biểu thức viết trong OCL thêm các thông tin quan trọng cho các mô hình hướng đối tượng. Các thông tin này thường khôn thể biểu diễn trong biểu đồ. Trong UML phiên bản 1.1 các thông tin này được giới hạn bởi các ràng buộc, mỗi ràng buộc được định nghĩa như một hạn chế về giá trị nhận được( một hay nhiều) của mộ hệ thống hay mô hình hướng đối tượng. Trong UML phiên bản 2, một mô hình có thể chứa nhiều thông tin thêm hơn là chỉ có ràng buộc. Tất cả các công việc như định nghĩa truy vấn, các giá trị tham chiếu, các quy tăc nghiệp vụ hay các điều kiện trạng thái được viết bằng biểu thức trong một mô hình. OCL là ngôn ngữ chuẩn trong đó các biểu thức được viết một cách rõ ràng dễ hiểu. Một mô hình thường có những thiếu sót do những hạn chế của các biểu đồ. Một biểu đồ đơn giản không thể biểu diễn hết các phát biểu đặc tả. Hình 2: Mô hình UML không biểu diễn hết đặc tả Trong mô hình, quan hệ giữa lớp Flight và lớp Person , phía lớp Person có bản số là 0…* tức là số khách hang là không giới hạn. Trong thực thế số khách hàng bị giới hạn bởi số ghế mà máy bay có, và giới hạn này không thể biểu diễn trong biểu đồ. Trong ví dụ này có một cách chỉ định ràng buộc về bản số thể hiện là thêm vào biểu đồ ràng buộc OCL sau: context Flight inv: passengers->size() <= plane.numberOfSeats. 2.3 Lập trình hướng khía cạnh (Aspect Oriented Programming) 2.3.1 Phương pháp lập trình hướng khía cạnh Có lẽ các khái niệm về lập trình hướng khía cạnh (AOP) hiện nay đã được nhiều người biết đến, vì vậy ở đây tôi sẽ chỉ trình bày lại ngắn gọn các khái niệm cơ bản và đặc điểm chính của AOP. Để trả lời được câu hỏi AOP là gì? Tại sao phải có AOP? chúng ta sẽ bắt đầu tìm hiểu sự hạn chế của các phương pháp lập trình hiện tại trong việc đáp ứng các yêu cầu ngày càng phức tạp của các hệ thống phần mềm. 2.3.1.1 Sự hạn chế của lập trình hướng đối tượng(OOP) Như chúng ta đ ã bi ết trong OOP người ta cố gắng mô tả thế giới thực thành các đối tượng với các thuộc tính và phương thức; cùng với các tính chất của lập trình hướng đối tượng như: tính trừu tượng, tính đóng gói, tính kế thừa và đa h ình đã làm thay đổi hoàn toàn ngành công nghiệp phần mềm. Hình 3: OOP Ta xét một ví dụ cụ thể xây dựng chương trình vẽ hình đơn giản. Một phân tích đơn giản cho yêu cầu của bài toán: - Các hình học cơ bản : điểm, đoạn thẳng, hình chữ nhật , hình tròn,… - Hiển thị các hình ở các vị trí khác nhau trong khung vẽ - Phải cập nhật lại hình tại vị trí mới mỗi khi di chuyển, co giãn hình. Sử dụng OOP ta sẽ mô hình hóa yêu cầu thành các đối tượng sau : - Lớp Shape: là một lớp Abstract chứa phương thức moveBy(int,int) di chuyển hình - Lớp Display: hiển thị hình ảnh. - Lớp Point: mô tả 1 điểm hình học chứa hai thuộc tính là tọa độ x, y được kế thừa từ lớp Shape. - Lớp Line: mô tả 1 đoạn thẳng, chứa 2 thuộc tính là điểm đầu và điểm cuối của đoạn thẳng và được kế thừa từ lớp Shape. Dưới đây là sơ đồ lớp của bài toán Figure 1 Hình 4: Sơ đồ lớp của bài toán vẽ hình Mô hình hóa thành các lớp như vậy ta thấy bài toán đã tương đối ổn. Bây giờ vấn đề đặt ra là mỗi khi ta thay đổi tọa độ của một điểm hay co giãn hình, di chuyển hình ta lại phải vẽ lại hình ở vị trí mới – tức là phải update lại Display. Xét lớp đơn giản nhất là lớp Point, Khi đặt lại tọa độ x, tọa độ y, hay di chuyển Point từ vị trí này sang vị trí khác, ta đều phải update lại Display thông qua phương thức display.update(this). Như vậy, cùng một phương thức display.update(this), ta phải gõ lại ở ba vị trí khác nhau ứng với ba sự thay đổi. Hãy thử tưởng tượng xem nếu chương trình của chúng ta đủ lớn và có khoảng vài ngàn sự thay đổi kiểu như thế thì dòng mã nguồn display.update(this) sẽ phải xuất hiện ở hàng ngàn chỗ khác nhau. Đối với lớp Line hay các lớp khác cũng vậy. Mỗi khi có sự thay đổi hình thì ngay sau sự thay đổi đó sẽ có dòng mã nguồn display.update(this) đi kèm theo nó. Ta có thể chia các chức năng của một phần mềm ra làm hai loại chính: - Thứ nhất là các chức năng thực hiện các nghiệp vụ chính, nghiệp vụ cơ bản của hệ thống (ví dụ như chức năng vẽ điểm, vẽ đoạn thẳng, vẽ hình khối trong bài toán vẽ hình ở trên). - Thứ hai, những chức năng dàn trải trên rất nhiều các mô-đun nghiệp vụ chính – được gọi là các chức năng cắt ngang hệ thống (ví dụ: cập nhật hình, lưu vết, bảo mật) hay được gọi là crosscutting concern. OOP có thể giải quyết rất tốt những chức năng chính của hệ thống, nhưng lại gặp rất nhiều khó khăn trong việc giải quyết các chức năng cắt ngang hệ thống. Khi sử dụng OOP để thực hiện các chức năng cắt ngang hệ thống, hệ thống sẽ gặp phải hai vấn đề chính, đó là: chồng chéo mã nguồn (Code tangling) và dàn trải mã nguồn (Code scattering). - Chồng chéo mã nguồn: Mô-đun chính của hệ thống ngoài việc thực hiện các yêu cầu chính, nó còn phải thực hiện các yêu cầu khác như: tính đồng bộ, bảo mật, lưu vết, lưu trữ. Như vậy, trong một mô đun có rất nhiều loại mã khác nhau, hiện tượng này gọi là chồng chéo mã nguồn. Điều này làm cho tính mô-đun hóa của hệ thống giảm đi, khả năng sử dụng lại mã nguồn thấp, khó bảo trì hệ thống. - Dàn trải mã nguồn: : Cùng một mã nguồn của các chức năng cắt ngang hệ thống được cài đặt lặp đi lặp lại rất nhiều lần ở nhiều mô-đun chính của hệ thống. Ví dụ như trong chương trình vẽ hình ở trên, mã nguồn của chức năng cập nhật hình, lưu vết xuất hiện ở tất cả các mô-đun của hệ thống.Hiện tượng này gọi là dàn trải mã nguồn. 2.3.1.2 Lập trình hướng khía cạnh Lập trình hướng khía cạnh được xây dựng trên các phương pháp lập trình hiện tại như lập trình hướng đối tượng, lập trình có cấu trúc, bổ sung thêm các khái niệm và cấu trúc để mô-đun hóa các chức năng cắt ngang hệ thống (crosscutting concern). Với AOP, các quan hệ cơ bản sử dụng các phương pháp cơ bản. Nếu sử dụng OOP, sẽ thực thi các quan hệ cơ bản dưới hình thức lớp(class). Các aspect trong hệ thống đóng gói các chức năng cắt ngang hệ thống lại với nhau. Chúng sẽ quy định cách các mô-đun khác nhau gắn kết với nhau để hình thành lên hệ thống cuối cùng. Nền tảng cơ bản của AOP khác với OOP là cách quản lý các chức năng cắt ngang hệ thống. Việc thực thi của từng chức năng cắt ngang AOP bỏ qua các hành vi được tích hợp vào nó. Ví dụ một mô-đun nghiệp vụ sẽ không quan tâm nó cần được lưu vết hoặc được xác thực như thế nào, kết quả là việc thực thi của từng concern tiến triển một cách độc lập. Quay trở lại với ví dụ về chương trình vẽ hình đơn giản ở phần trên. Nếu sử dụng AOP, các chức năng cắt ngang hệ thống: cập nhật hình, lưu vết sẽ được giải quyết theo cách sau: Thay vì tích hợp chức năng các mô-đun cắt ngang hệ thống (cập nhật hình, l ưu vết) ngay trong mô-đun nghiệp vụ chính; lập trình viên sẽ tách chúng ra thành các mô- đun mới, gọi là aspect. Hình 2.5 minh họa cho việc thực thi chức năng cập nhật hình bằng AOP và dưới đây là mã nguồn của aspect đó: public aspect UpdateSignaling{ pointcut updateDisplay():execution(void *.setX(int)) || execution(void*.setY(int)) || execution(void*.moveBy(int, int)); after(): updateDisplay(){ display.update(this); } } Hình 5: Dùng AOP giải quyết bài toán vẽ hình Sau khi định nghĩa một aspect như vậy thì bất cứ khi nào có sự thay đổi về hình (setX, setY, moveBy) chương trình sẽ tự động gọi chức năng cập nhật hình, cụ thể ở đây là phương thức display.update(this) mà ta không cần phải lục lọi lại các đoạn mã nguồn để thêm nó dòng mã nguồn này vào. 2.3.1.2.1 Phương pháp luận của AOP Vấn đề cốt lõi của AOP là cho phép chúng ta thực hiện các vấn đề riêng biệt một cách linh hoạt và kết nối chúng lại để tạo nên hệ thống cuối cùng. AOP bổ xung cho OOP bằng việc hỗ trợ một dạng mô-đun khác, cho phép kéo theo thể hiện chung của các vấn đề đan nhau vào một khối. Khối này gọi là ‘aspect’(tạm dịch là ‘lát’ – hàm ý cắt ngang qua nhiều lớp đối tượng). Từ chữ ‘aspect’ này chúng ta có mội phương pháp lập trình mới: Aspect-Oriented Programming. Nhờ mã được tách riêng biệt, các vấn đề đan xen nhau trở nên dễ kiểm soát hơn. Các aspect của hệ thống có thể thay đổi, thêm hoặc xóa lúc biên dịch và có thể tái sử dụng. Một dạng biên dịch đặc biệt có tên là Aspect Weaver thực hiện việc kết hợp các thành phần riêng lẻ thành một hệ thống thống nhất. 2.3.1.2.2 Ưu điểm của AOP AOP là một kỹ thuật mới đầy triển vọng, hứa hẹn đem lại nhiều lợi ích cho việc phát triển phần mềm, dưới đây là một số lợi ích cụ thể của AOP : - Mô-đun hóa những vấn đề đan xen nhau: AOP xác định vấn đề một cách riêng biệt, cho phép mô-đun hóa những vấn đề liên quan đến nhiều lớp đối tượng. - Tái sử dụng mã nguồn tốt hơn: Các aspect là những mô-đun riêng biệt, được kết hợp linh động – đây chính là yếu tố quan trọng để tái sử dụng mã nguồn. - Cho phép mở rộng hệ thống dễ dàng hơn: Một thiết kế tốt phải tính đến cả những yêu cầu hiện tại và tương lai, việc xác định các yêu cầu trong tương lai là một công việc khó khăn. Nhưng nếu bỏ qua các yêu cầu trong tương lai, có thể bạn sẽ phải thay đổi hay thực hiện lại nhiều phần của hệ thống. Với AOP, người thiết kế hệ thống có thể để lại quyết định thiết kế cho những yêu cầu trong tương lai nhờ thực hiện các aspect riêng biệt. 2.3.2 Các khái niệm trong Aspect 2.3.2.1 Join point Join point là bất kỳ điểm nào có thể xác định được khi thực hiện chương trình. Ví dụ: lời gọi hàm, khởi tạo đối tượng. Join point chính là vị trí mà các hành động thực thi cắt ngang được đan vào. Trong Aspect mọi thứ đều xoay quanh join point. 2.3.2.2 Pointcut Pointcut là một cấu trúc chương trình mà nó chọn các join point và ngữ cảnh tại các join point đó.Ví dụ một pointcut có thể chọn một join point là lời gọi đến một phương thức và lấy thông tin ngữ cảnh của phương thức đó như đối tượng chứa phương thức đó, các tham số của phương thức đó. Bảng 1:Ánh xạ giữa các loại join point và pointcut tương ướng Loại join point Cú pháp point cut Thực hiện phương thức execution(MethodSignature) Gọi phương thức call(MethodSignature) Thực hiện hàm dựng execution(ConstructorSignature) Gọi hàm dựng call(ConstructorSignature) Khởi tạo lớp staticinitialization(TypeSignature) Đọc thuộc tính get(FieldSignature) Ghi thuộc tính set(FieldSignature) Thực hiện điều khiển ngoại lệ execution handler (TypeSignature) Khởi tạo đối tượng initialization(ConstructorSignature) Tiền khởi tạo đối tượng preinitialization(ConstructorSignature) Thực hiện advice adviceexecution() 2.3.2.3 Advice Advice là mã thực hiện tại một join point mà được chọn bởi pointcut [7, 12]. Hay nói cách khác, nếu ta coi pointcut là khai báo tên phương thức, thì advice là phần thân của phương thức đó.Pointcut và advice sẽ hình thành nên các luật dan kết các quan hệ đan xen. Advice được chia ra làm ba loại sau: - Before : được thực hiện trước join point. - After: được thực hiện sau join point. - Around: Thực thi xung quanh join point 2.3.2.4 Aspect Aspect là phần tử trung tâm của Aspect, giống như class trong Java. Aspect chứa mã thể hiện các luật đan kết cho các concern. Join point, pointcut, advice được kết hợp trong aspect. Tuy có gần giống các đặc điểm của class trong Java như: chứa thuộc tính, phương thức, có thể khai báo trừu tượng, có thể kế thừa… Tuy nhiên, Aspect có một số khác biệt cơ bản sau: - Aspect không thể khởi tạo trực tiếp. - Aspect không thể kế thừa từ một aspect cụ thể (không phải trừu tượng). Aspect có thể được đánh dấu là có quyền bằng định danh privileged. Nhờ đó nó có thể truy cập đến các thành viên của lớp mà chúng cắt ngang. 3 Chương 3: Kiểm chứng mô hình Aspect-UML 3.1 Giới thiệu về Alloy 3.1.1 Alloy[4] là gì? Trong công nghệ phần mềm, Alloy là một ngôn ngữ đặc tả mô hình hóa cho những biểu thị sự ràng buộc của những cấu trúc phực tạp trong công nghệ phần mềm. Alloy là một công cụ mô hình hóa đơn giản dựa trên thứ bậc logic đầu tiên.Nền tảng toán học của ngôn ngữ này bị ảnh hưởng nặng lề bởi các phép biểu diễn. Mặc dù cú pháp của ngôn ngữ này có trách nhiêm hơn so với ngôn ngữ khác như hạn chế về đối tượng ngôn ngữ. Alloy xác định mục tiêu tạo nên những mô hình vi mô để sau này nó tự động kiểm tra cho sự đứng đắn của các mô hình ấy. Mặc dù Alloy được thiết kế với phân tích tự động trong suy nghĩ, khác với nhiều ngôn ngữ đặc tả thiết kế cho mô hình kiểm tra ở chỗ nó cho phép định nghĩa các mô hình vô hạn .Các đặc tả Alloy có thể bị kiểm tra bằng cách sử dụng Alloy Analyzer. Alloy Analyzer được thiết kế để thực hiện kiểm tra phạm vi hữu hạn, ngay cả trên các mô hình vô hạn. 3.1.2 Tính chất của ngôn ngữ alloy  Đối các mô hình hữu hạn alloy có thể hữu hạn phạm vi kiểm tra: phân tích được đầy đủ các đối tượng đặc tả  Alloy cho phép kiểm tra vô hạn các mô hình vì kiểm tra hữu hạn không nhận được phản ánh đúng từ mô hình cần đặc tả  Alloy có khả năng đặt quan hệ logic giữa các đối tượng trong mô hình  Tự động phân tích và kiểm tra tính đứng đắn của các mô hình  Về cấu trúc dữ liệu: o Xử lý vụng về o Chức năng đệ quy khó diễn tả 3.1.3 Cấu trúc một chương trình Alloy module …. sig A{…} fact F {…} assert a { …} check a scope pred P () {…} run P Ý nghĩa: – sig A: Thiết lập một lớp đối tượng A – fact F: nghĩa là giả sử ràng buộc F vững chắc –assert a: tin tưởng rằng A sau F –check a : tìm một ví dụ không đáp ứng A và F – pred: định nghĩa sự ràng buộc P – run: tìm ra 1 instance thỏa mãn P và F 3.1.4 Khai báo trong alloy Dòng đầu tiên khai báo modul - Sig Object{} định nghĩa một lớp đối tượng - Trừu tượng sig Object ()là trừu tượng sig không có các thành phần ngoại trừ những phần mở rộng của nó - SigFile extends Object ()-sự thiêt lập này có thể được giới thiệu là một tập hợp con của tập khác 3.1.4.1 Các ký hiệu  Sig A{}  sig B extends A {} (nghĩa là B trong A)  sig C extends A {}(C trong A) 3.1.4.2 Khai báo các liên kết Liên kết được khai báo như các trường và các ký hiệu sigObject{} sigDir extends Object { entries: set Object, parent: lone Dir } 3.1.4.3 Các trường  Sig A{f: set X}  Sig B extends A{g:set Y} Nghĩa là : B in A f: A-> X g: B->Y 3.1.4.4 Các dạng thiết lập  Lone: chỉ không hoặc một  All: bất kì số nào  One: chỉ duy nhất một  Some: một hoặc nhiều hơn 3.1.4.5 Facts và Assertions  Fact o Hạn chế được những giả đình luôn luôn giữ(ví dụ như sử dụng các không gian hạn chế của các bộ đếm) o Một mô hình có thể có bất kỳ các con số của fact sigA {} fact { all z: A | F }  Assert: sự liên kết có ý đi theo các fact của mô hình có thể kiểm tra bằng cách sử dụng các lệnh kiểm tra 3.1.4.6 Các hằng số và các toán tử Ngôn ngữ của các mối quan hệ có các hằng và toán tử của mình chúng  Hằng: o None = tập rỗng. o Univ = tập phổ biến o Iden = đồng nhất.  Các toán tử(Operators): o Set operators:  +: hợp nhất sig Vehicle{} {Vehicle = Car+ Truck}  &: giao nhau fact DisSubtrees{all t1, t2: Tree | (t1.^children)&(t2.^children)= none}  -: hiệu số fact dirinothers { all d: Directory - Root | some contents.d }  in : tập con sibling = (brother + sister) sister in sibling  =: bằng nhau o Relational operators:  . : dot (phép nối)  ->: mũi tên (product)  ^ : transitive closure  *: reflexive- transitive closure  ~: đảo vế  [] : box (join)  <: : domain restriction  :> : range restriction  ++ : override o Toán tử logic  ! : negation  && : conjunction (and)  || : disjunction (OR)  => : implication  else : alternative  : bi-implication (IFF) o Logic Cardinalities  = equals  < less than  > greater than  =< less than or equal to  >= greater than or equal to  #r number of tuples in r  0,1,... integer literal  + plus  - minus 3.1.4.7 Predicates - Một pred là tên của một ràng buộc - Không hoặc nhiều hơn sự khai báo cho những lí luận - Có thể sử dụng để đại diện cho một quá trình thực thi - Chỉ được dùng khi được gọi (không như fact) 3.2 Đặc tả mô hình Aspect-UML trong Alloy 3.2.1 Mô hình Aspect UML Vì việc đặc tả mô hình UML+ OCL đã được nghiên cứu và hoàn thành do vậy chúng ta chỉ xem xét đến mô hình Aspect- UML. Phương pháp đặc tả trong bài luận này sẽ xem xét cách phân tích các tương tác aspect trong mô hình A-O được viết trong Aspect UML [5,6]. Aspect-UML là một mô hình đơn giản mở rộng của UML và sử dụng các khái niệm cơ bản của AOP (aspect, các advice, point cut, joint point và các crosscutting). Nó cũng cho phép các chú thích hình thức ví dụ như pre , post conditions, để đặc tả chính xác các trạng thái của các thành phần như join points và advices cũng như context ở pointcut. Nhờ có các chú thích này, mô hình Aspect UML cung cấp thêm thông tin để phân tích các tương tác aspect từ các điểm ngữ nghĩa của khung nhìn. Công việc này do đó đi một bước xa hơn các phương pháp truyển thống dựa trên phân tích chương trình tĩnh mà thường quên đi việc giải quyết ngữ nghĩa gây ra xung đột giữa các aspect. Mô hình Aspect-UML có thể được kiểm tra từ các xung đột tương tác aspect. Một cách để tự động quá trình kiểm chứng là chuyển đổi mô hình Aspect- UML sang ngôn ngữ đặc tả Alloy. Alloy cung cấp một ngôn ngữ đặc tả mô hình đơn giản dựa trên logic đầu tiên như phân tích mô hình và công cụ mô phỏng[]. Một mô hình Alloy được soạn thảo từ một tập hợp các signature xác đinh tập hợp đối tượng và các mối quan hệ giữa chúng. Mô hình này có thể được thêm các rang buộc bởi predicates và assertions. Một mô hình là trừu tượng cái mà thực sự xác định một tập hợp có thể vô hạn của một mô hình hữu hạn. Alloy thực thi đặc tả mô hình bằng cách tìm kiếm mô hình cá biệt đáp ứng một số đặc điểm của đặc tả. Một mô hình có thể được kiểm tra là có giá trị hay là thỏa mãn bên trong các ràng buộc một mô hình cá biệt. Thật vậy, các phân tích Alloy giới hạn việc tìm kiếm các mô hình cá biệt cái mà kích cỡ(về các đối tượng) là thấp hơn cho một số ràng buộc cố đinh bời người sử dụng. Alloy khẳng định hướng tiếp cận đặc tả của nó bằng việc đề xuất giả thuyết phạm vi nhỏ mà theo đó các counterexample phế bỏ một mô hình có khuynh hướng xảy ra trong các ví dụ mô hình nhỏ. Để kiểm chứng mô hình Aspect UML, trước hết chúng ta giả định rằng hệ thống cơ bản và Aspect cả 2 đều được chứng minh là đúng. Bằng việc chuyển đổi mô hình Aspect UML sang Alloy, quá trình đặc tả hình thức của chúng ta có mục đích biểu lộ những loại vấn để tương tác aspect sau đây: (1) vi phạm tài nguyên địa phương, một pre/post condition của adive hoặc point cut là vi phạm do kết hợp của 1 aspect; (2) vi phạm của một lớp, aspect hoặc bất biến hệ thống do thêm vào một aspect. 3.2.2 Mô hình viễn thông Để minh họa cho việc đặc tả mô hình Aspect UML bằng alloy ta sử dụng ví dụ ứng dụng điện thoại. Ứng dụng này là một phỏng đơn giản của một hệ thống điện thoại, trong đó khách bắt đầu chấp nhận, thả và hợp nhất các cuộc gọi trong nội bộ và đường dài. Hệ thống cung cấp các chức năng lõi để mô tả và kết nối khách hàng. Trong các chức năng cơ bản, một người có thể thêm giờ, thanh toán và ngắt các tính năng được mô tả dưới đây:  Tính năng thời gian được liên quan tới thời gian kết nối và giữ thời gian kết nối tổng số cho mỗi khách hàng. Nó xảy ra ở trong khoảng đầu đến cuối của mỗi kết nối.  Tính năng thanh toán có liên quan tới việc tính phí khách hàng cho các cuộc gọi của họ. Một tính phí cho mõi kết nối được tính toán và khi chấm dứt kết nôi nó được bổ sung vào hóa đơn của khách hàng phù hợp  Tính năng ngắt được sử dụng để xử lý các đường truyền bận bằng cách ngắt cuộc gọi. Nó can thiệp vào lúc bắt dầu kết nối bằng cách kiểm tra nếu đích là bận , trong trường hợp này cuộc gọi bị gián đoạn. Hình 6: Mô hình class cho hệ thống viễn thông Hình trên thể hiện bằng cách nào viêc tính giờ, thanh toán và các yêu cầu ngắt cuộc gọi được tích hợp vào trong biểu đồ lớp UML, sử dụng Aspect UML thích hợp. Những yêu cầu crosscutting được bắt tương ứng bằng aspect Timing, Billing và Interrupting cái mà được mô tả như các lớp trong UML được mô tả với stereotype >. Những aspect này cắt ngang ứng dụng cơ bản thông qua 2 point cut được mô hình như một interface đặc biệt có tên là OpComplete và OpDrop. Một quan hệ phụ thuộc > thì thường được sử dụng để liên kết mỗi join point mà nó biểu hiện. Interface của pointcut OpComplete chứa một biểu thức trừu tượng được đặt tên là opComplete(c:Connection) được thực thi khi một trong những joinpoint của nó đạt được. Tương tự interface của OpDrop chức một biểu thức trừu tượng opDrop(c:Connection). Hãy xem xét về ví dụ aspect Timing( aspect Billing và aspect Interrupting cũng tương tự). Nó thực thi cả interface ponitcut OpComplete và OpDrop và do đó cung cấp 1 số advice tương ứng để thực hiện mỗi cái trong chúng. 3.2.3 Đặc tả mô hình Aspect UML bằng Alloy Phần này giải thích cách mà mô hình Aspect UML có thể được chuyển đổi sang đặc tả Alloy để chúng sau này có thể được phân tích bằng Alloy Analyzed. Bảng 2: Chuyển đổi thành phần cấu trúc mô hình Aspect UML sang Alloy. Các class và aspect được chuyển thành các khai báo signature trong Alloy. Các thuộc tính của một lớp hoặc của 1 aspect thì được chuyển thành các mối quan hệ trong các signature tương đồng. Tương tự các liên kết giữa những class và hoặc aspect thì được dịch thành các mối quan hệ. Đối với kiểu người dùng tự định nghĩa kiểu dữ liệu tập hợp , cái mà là tập hợp các giá trị không được có mặt trong UML( ví dụ như kết nối hay ngắt kết nối trong trường hợp chúng tôi nghiên cứu), các enumeration con được chuyển đổi thành các signature kế thừa từ signature được định nghĩa bởi cái kiểu enumeration. Ví dụ, đoạn code Alloy sau đặc tả lớp Connection xuất hiện ở trong mô hình lớp của ứng dụng viễn thông (hình 5). Sig Connection{ status: Status, origin, destination: Device } abstract sig Status{} sig connected, disconnected extends Status{} Đối với aspect Timing, nó được xác định bời đoạn code Alloy sau: sig Timing{ effectiveConnections: set Connection, getTimer: effectiveConnections → some Timer } sig Timer{ startTime, connectionTime: Int, c : Connection } Chuyển đổi ngữ pháp của chú thích Aspect UML sang Alloy Để giải quyết ngữ nghĩa của các tương tác aspect tại join point, mô hình UML đã được mở rộng với các chú thích xác định những giao ước riêng lẻ mà mỗi phương thức / biểu thức advice (thực thi tại join point) phải được lưu ý. Những giao ước đó được khai báo ở các điều kiện trước và sau (post/pre condition). May mắn thay Alloy cũng cho chúng ta đặc tả những ràng buộc mà biểu thức(phương thức và advice tại join point) phải thỏa mãn thông qua việc sử dụng các predicate. Ví dụ: xét 1 phương thức op() với tham số s thuộc kiểu T có hành vi được xác định bởi điều kiện trước là s>0 và điều kiện sau khi thực thi là s<100, Alloy mô tả ràng buộc này predicate sau: pred op(s, s′:T) { // precondition s>0 // postcondition s′ <100} Trong một mô hình Aspect UML chính xác, các tương tác aspect tại join point không bao giờ là nguyên nhân sự vi phạm của các điều kiện riêng lẻ trước và sau của hàm, bất kể bối cảnh thực thi có được lưu tâm. Trong mô hình Alloy, điều này có nghĩa là việc kết hợp các aspect sẽ yêu cầu các thành phần của các ràng buộc của advice với những với ràng buộc join point có liên quan. Nếu không có xung đột, tất cả các trường hợp của mô hình có thể đáp ứng các ràng buộc, mà gây ra bởi việc kết hợp các aspect. Nếu không có xung đột, tất cả các trường hợp của mô hình có thể đáp ứng các ràng buộc, mà gây ra bởi việc kết hợp các aspect. Để minh họa điều này, chúng ta hãy xem xét các predicate của Alloy mà chúng tôi định nghĩa để hạn chế các thực thi kết hợp các phương thức và advice tại join point Drop trong ứng dụng viễn thông. Trong các bước sau đây, chúng tôi sẽ giải thích làm thế nào để xác định (1) những ràng buộc của phương thức drop(), (2) ràng buộc của advice opDropTiming và opDropBilling,(3) những ràng buộc áp đặt bởi các thành phần advice, và cuối cùng (4) các ràng buộc tạo ra bời việc kết hợp các advice tại join point drop(). (1) Các hành vi của phương thức drop() phải thỏa mãn các ràng buộc áp đặt bởi những điều kiện trước và sau của nó. Điều kiện trước phải được thoải mãn bởi mô hình mà mỗi phương thức được thực thi và phương thức thực thi phải rời khỏi mô hình trong trang thái thỏa mãn những điều kiện sau. Trong trường hợp này, trạng thái kết nối được thiết lập để kết nôi khi drop() được gọi, trong khi việc thức thi của nó sau này phải bị hủy để ngắt kết nối. Trạng thái trước và sau việc kết nối tương ứng được nắm bắt bởi các biến c và c’. Những ràng buộc này có thể được đặc tả trong Alloy sử dụng các định nghĩa predicate như bên dưới : pred drop(c, c′: Connection) { c.status= connected && c′.status=disconnected && c′.origin.d_status=idle && c′.destination.d_status=idle } (2) Hành vi của advice opDrop trong aspect Timing được xác định một cách tương tự .Các điều kiện trước của nó ràng buộc giờ liên quan tới việc kết nối (đang bị ngắt) không có một đăng kí nào về thời gian kết nối. Ngược lại, điều kiện sau tác động mạnh mẽ lên thời gian có đăng kí kết nối giá trị thời gian phải lớn hơn hoặc bằng 0. Những ràng buộc này buộc bộ đếm giờ phải thay đổi trạng thái, cái mà hậu quả ảnh hưởng lớn đến aspect Timing cũng để thay đổi trạng thái nó phải cập nhật các trường bao gồm danh sách các bộ tính giờ. Tham số t và t’ được sử dụng để biểu thị trạng thái của aspect Timing trước và sau khi thức thi advice opDrop. Đối với việc kết nối, cá trạng thái của nó (mô hình bởi tham số c )vẫn giữ nguyên. Predicate Alloy sau được sử dụng để xác định ràng buộc áp đặt bởi advice opDrop: pred OpDropTiming(t,t′:Timing, c:Connection) { t.useTimer[c].connectionTime=Null && t′.useTimer[c].connectionTime≥ 0 } Một predicate Alloy phải được định nghĩa để xác định các ràng buộc áp đặt bởi các điều kiện trước vào sau của mỗi advice và join point phương thức được xuất hiện trong mô hình Aspect UML. Trong trường hợp advice opDrop của Billing, các điều khiện trước và sau có tác động mạnh mẽ lên tổng số hóa đơn của người gọi để tăng thêm nếu bộ đếm thời gian đã được ghi lại một thời gian kết nối lớn hơn hoặc bằng 0. Do vậy chỉ có hóa đơn thay đổi trạng thái. Trạng thái này có thể được quan sát nhờ tham số b và b’ trong predicate opDropBilling bên dưới. Predicate này xác định một ràng buộc bắt buộc bởi thực thi advice opDrop của Billing. pred OpDropBilling(b,b′:Billing, t:Timing,c:Connection) { (t.useTimer[c].connectionTime >= 0) && (b.useBill[c.origin.owner].charge ≤ b′.useBill[c.origin.owner].charge) } Hầu hết ta có thể thấy được aspect Billing ngầm đòi hỏi các dịch vụ của aspect Timing. Cách xây dựng này không được khuyến cáo, các aspect nên được định nghĩa độc lập với nhau.Tuy nhiên nếu aspect Timing được thu lại, phân tích của chung tôi có thể phát hiện lỗi của aspect Billing tại join point drop. (3) Khi nhiều hơn một advice của cùng 1 loại(tức là trước hoặc sau) được thực hiện ở cùng 1 join point, những advice đầu tiên cần đồng thời được biên soạn cùng nhau trước khi được đan kết lại ở tại join point này. Các advice đồng thời có sự ưu tiên để biên soạn là ngang nhau theo sau là các yêu cầu xác định bởi những ràng buộc cấp cao. Tuần tự các điều kiện tác động đến điều kiện sau của một hàm trong sự nối tiếp đến điều kiện trước của hàm sau. Nếu các advice đồng thời không được ưu tiên, chúng sẽ được biên soạn liên tục nhưng không phải ở trong một trật tự xác định. Do đó tất cả có thể yêu cầu cần phải được kiểm tra. Một lần nữa điều kiện sau của mộ hàm sẽ được ràng buộc tới điều kiện trước của hàm kế tiếp. Ví dụ Timing và Billing không là các aspect đồng thời tương tác tại join point drop. Advice onDrop tương ứng của chúng cần được biên soạn trong một trật tự khó mà xác định được. Để tác động đến Alloy đi qua tất cả các advice được yêu cầu, chúng ta định nghĩa một predicate được gọi là executeOpDrop cái mà cho phép Alloy có sự lựa chọn thoải mái để cho phép điều kiện sau của predicate opDropBilling tiếp theo điều kiện trước của predicateOpDropTiming hoặc ngược lại. Vậy khi kiểm tra tính hợp lệ của assertion, bộ phân tích alloy sẽ đi qua tất cả các thực thi các predicate, vì thế cố gắng tất cả các yêu cầu của hai advice pre và post constraint. pred executeOpDrop(t,t′:Timing, b,b′:Billing,c:Connection){ OpDropTiming(t,t′,c) && OpDropBilling(b,b′,t′,c) || OpDropBilling(b,b′,t,c) && OpDropTiming(t,t′,c) } (4) Cuối cùng việc tổng hợp kết quả của advice từ các thành phần của OpDropTiming và OpDropBilling là chỉ xảy ra sau khi thực hiện join point drop(). Predicate weaveAtOpDrop ở dưới đây định nghĩa các ràng buộc cưỡng bức bởi việc kết hợp. Predicate này rõ ràng tác động đến hoàn cảnh thỏa mãn ràng buộc c <- đích (định nghĩa bởi pointcut OpDrop trong mô hình Aspect UML)để được lưu tâm nhờ tham số c’. Tham số này đại diện cho trạng thái của kết nối chỉ sau khi thực thi phương thức drop. Nó được thông qua để predicate executeOpDrop định nghĩa tập hợp các ràng buộc gây ra bởi kết hợp các advice để được thực thi chính xác tại điểm đó. Cuối cùng , từ những ảnh hưởng của advice này phải không trái điều kiện khởi tạo của join point drop, chúng tôi buộc các trạng thái cuối của kết nối bị ngắt như dự kiến ban đầu. pred weaveAtOpDrop(t,t′: Timing, b,b′:Billing, c,c′: Connection) { drop(c,c′) && executeOpDrop(t,t′,b,b′,c′) && (c′.status=disconnected) } 3.2.4 Kiểm chứng mô hình Aspect UML sử dụng Alloy Phương pháp kiểm chứng này có mục đích là phát hiện ra sự xen vào các vấn đề: - Sự vi phạm của thuộc tính cục bộ - Sự vi phạm của thuộc tính toàn cục 3.2.4.1 Kiểm chứng sự vi phạm của thuộc tính cục bộ Tại mỗi join point được đưa ra, một aspect ,advices có thể có can thiệp với hệ thống cơ sở hoặc với các aspect khác bởi sự vi phạm cái điều kiện trước và sau của chúng. Các khẳng định thường chắc chắn rằng tất cả các khởi tạo của mô hình ban đầu đều chính xác phải thỏa mãn việc kết hợp các predicate. Ví dụ, trong ứng dụng viễn thông, để kiểm tra liệu aspect Timing và Billing có tương tác chính xác tại join point drop(chúng không vi phạm các đặc tả của hệ thống cơ bản hay không vi phạm tới các aspect khác), công cụ phân tích Alloy đưa ra khẳng định sau: assert testWeaveAtOpDrop { all c: Connection, t:Timing, b: Billing | some c′: Connection, t′:Timing, b′: Billing | (c!=c′)&&(t!=t′)&&(b!=b′) => weaveAtOpDrop(t,t′, b,b′, c,c′) } Nếu khẳng định không hợp lệ thì sẽ xuất hiện counterexample được sinh ra bởi công cụ phân tích Alloy. 3.2.4.2 Kiểm chứng sự vi phạm của các thuộc tính toàn cục Các ràng buộc hệ thống có thể dễ dàng kiểm chứng được bởi các predicate thêm vào trong mô hình Alloy.Trong ứng dụng viễn thông, hai ràng buộc quan trọng có thể được kiểm chững là : - Với mỗi trạng thái của hệ thống số lượng các kết nối luôn nhỏ hơn hoặc bằng 50. - Trạng thái của tất cả các thiết bị ( nguồn hoặc đích ) tham gia vào các kết nối thì không nhàn rỗi. Những bất biến này có thể được kiểm chứng bời những predicate sau: pred limitedConnectedConnections { #{allc:Connection | c.status=connected}≤ 50 } pred deviceIdle { alld:Device,somec:Connection | (dinc.(origin+destination))&&(c.status=connected) => (d.d−status!=idle) }. 4 Chương 4 : Kết luận Trong quá trình thực hiện khóa luận này tôi đã tìm hiểu được những kiến thức cơ bản về kiểm chứng, một trong những công đoạn vô cùng quan trọng giúp phát hiện và sửa lỗi phần mềm nhằm đảm bảo chất lượng phần mềm.Ngoài ra trong khóa luận tôi còn xậy dựng được phương pháp kiểm chứng mô hình Aspect UML bằng Alloy. Cùng với việc kiểm chứng mô hình UML+ OCL đã có sẵn từ trước thì việc kiểm chứng mô hình UML trở lên toàn diện hơn, kiểm chứng trên nhiều phương diện. Do thời gian chưa cho phép tôi vẫn chưa hoàn thành được công cụ tự động đặc tả mô hình UML +OCL + ASPECT bằng Alloy. Những kiến thức trong bài luận này kết hợp với những kiếm thức đặc tả mô hình UML+ OCL có sẵn sẽ giúp tôi hoàn thành công cụ này trong tương lai. TÀI LIỆU THAM KHẢO [1] [2] [3] Farida Mostefaoui DIRO,Julie Vachon , University of Monreal Quebec, Canada Verification of Aspect –UML models using alloy, 2007 [4] Daniel Jackson , Solfware Abstraction: Logic, Language, and Analysis, [5] J.VachonandF.Mostefaoui.Achieving supplementary equirements using aspect- oriented development.In ICEIS, pages584–587, 2004 [6] F.MostefaouiandJ.Vachon.Approche basee sur les r´ eseaux de Petripourla v´erification de la composition danslessyst` emesparaspects. RSTI-L’Objet, 12(2-3):157– 182,September2006.