Tóm tắt Luận văn Mô hình hóa và kiểm chứng các chương trình phần mềm hướng khía cạnh

3 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ PHẠM NHƯ UYỂN MÔ HÌNH HÓA VÀ KIỂM CHỨNG CÁC CHƯƠNG TRÌNH PHẦN MỀM HƯỚNG KHÍA CẠNH Ngành: Công nghệ Thông tin Chuyên ngành: Kỹ thuật Phần mềm Mã số: 60480103 NGƯỜI HƯỚNG DẪN KHOA HỌC: PGS.TS Trương Ninh Thuận HÀ NỘI - 2016 4 CHƯƠNG 1: ĐẶT VẤN ĐỀ 1.1 Sự cần thiết của đề tài Có rất nhiều công trình nghiên cứu tập trung vào kiểm chứng mô hình hướng khía cạnh sử dụng các kỹ thuật khác nhau như UML [10], kiểm chứng mô hình (model checking) [9], Petri-net [4], và B [7] nhưng không phù hợp với một hệ thống dựa trên các sự kiện. Một số công trình nghiên cứu đã khai thác những kí hiệu của UML hoặc mở rộng những kí hiệu UML để cụ thể hóa những vấn đề crosscutting. Tuy nhiên, những nghiên cứu này đã không giải quyết những khía cạnh kiểm chứng do bản chất không chính thức hoặc bán chính thức của UML. Ubayashi và Tamain [8] đã đề xuất một phương pháp để kiểm chứng chương trình AOP sử dụng mô hình kiểm tra. Phương pháp nhằm vào các giai đoạn lập trình và ứng dụng các mô hình kiểm tra để có kết quả đan code của lớp và aspect. Phương pháp này đảm bảo sự chính xác trong kiểm chứng, tuy nhiên lại bỏ qua các vấn đề kiểm chứng mô đun. Điều này có nghĩa là rất khó có thể sử dụng phương pháp này để xác minh phần mềm lớn. Dianxiang Xu [9] đã đề xuất sử dụng máy trạng thái và kiểm chứng những chương trình sử dụng aspect. Chúng đã chuyển hóa các mô hình đan và các lớp mô hình không bị ảnh hưởng bởi aspect thành các chương trình FSP, mà sẽ được kiểm chứng bởi mô hình LTSA chống lại các thuộc tính hệ thống mong muốn. Tuy nhiên, phương pháp này cần phải chuyển hóa chương trình cơ bản và aspect sang mô hình trạng thái trước khi khởi động mô hình FSP [7] Sử dụng B để kiểm chứng đan aspect. Tác giả này trình bày lớp cơ bản và một số aspect liên quan của AspectJ trong ngôn ngữ B. Nó nhằm mục đích đạt được lợi ích từ các minh chứng tạo ra bởi công cụ B để đảm bảo chính xác của aspectJ thành phần. Để giải quyết vấn đề này, EAOP [3] cho phép xem xét hệ thống mối quan hệ giữa point-cut và để thực hiện các aspect khi nhận được sự kiện được phát sinh bởi chương trình cơ bản. Tuy nhiên, mô hình này không đi kèm với phương pháp đặc tả cụ thể chính thức cũng như không cung cấp bất kỳ cơ chế để xác minh tính chất của nó chính thức. Trong bài này, chúng tôi đề xuất một phương pháp dựa trên mô hình hóa phương thức trên Event-B [2] để phân tích một ứng dụng EAOP. Đầu tiên, chúng ta xác định các thành phần của nó trong Event-B nơi sử dụng các Event- B cơ chế làm 5 mịn để mô hình cơ bản và chương trình giám sát. Sau đó, khai thác Event – B để chứng minh được tạo ra để kiểm tra xem các hạn chế áp dụng bởi aspect cross-cuts. 1.2. Nội dung đề tài Lập trình hướng khía cạnh dựa trên sự kiện (EAOP) mô hình cho phép xem xét hệ thống mối quan hệ giữa point-cut và để thực hiện các aspect khi nhận được sự kiện được phát sinh bởi chương trình cơ bản. Tuy nhiên, mô hình này không đi kèm với phương pháp đặc tả cụ thể chính thức cũng như không cung cấp bất kỳ cơ chế để xác minh tính chất của nó chính thức. Trong bài này, chúng tôi đề xuất một phương pháp dựa trên mô hình hóa phương thức trên Event-B để phân tích một ứng dụng EAOP. Đầu tiên, chúng ta xác định các thành phần của nó trong Event-B nơi sử dụng các Event- B cơ chế làm mịn để mô hình cơ bản và chương trình giám sát. Sau đó, chúng ta khai thác Event – B để chứng minh được tạo ra để kiểm tra xem các hạn chế áp dụng bởi aspect cross-cuts. Cuối cùng, phương pháp đề xuất được minh họa chi tiết với một chương trình ATM. 1.3. Đóng góp của luận văn Đóng góp của luận văn liên quan việc mô hình hóa và kiểm chứng EAOP sử dụng phương pháp hình thức Event-B. Phương pháp mà chúng tôi đề xuất dựa trên việc dịch một chương trình EAOP thành các máy của Event-B, tận dụng các cơ chế làm mịn để kiểm chứng những ràng buộc trong chương trình trong mỗi aspect. Với mong muốn kiểm tra chương trình có còn lưu giữ một số định nghĩa thuộc tính sau khi đan chương trình. Luận văn cũng minh họa phương pháp mô hình hóa và kiểm chứng trong một chương trình ATM. 1.4. Cấu trúc luận văn Các phần còn lại của luận văn sẽ được trình bày bao gồm các phần sau: CHƯƠNG 2: EAOP VÀ EVENT-B Giới thiệu khái quát những kiến thức cơ bản vể EAOP. Mô hình kiến trúc EAOP. Trình bày những kiến thức tổng quan về phương pháp mô hình hóa Event-B, 6 mô tả cấu trúc của mô hình, các thành phần. Trình bày công cụ kiểm chứng tự động Rodin. CHƯƠNG 3: MÔ HÌNH HÓA VÀ KIỂM CHỨNG CÁC PHẦN MỀM HƯỚNG KHÍA CẠNH. Tập trung vào việc mô hình hóa và kiểm chứng chương trình phần mềm hướng khía cạnh đưa ra cách định nghĩa hướng khía cạnh hệ thống hướng sự kiện trong Event-B. Mô hình hóa hệ thống lập trình hướng khía cạnh sử dụng Event-B. Kiểm chứng hệ thống. CHƯƠNG 4: ÁP DỤNG BÀI TOÁN. Áp dụng phương pháp đã trình bày ở trên để mô hình hóa và kiểm chứng bài toán máy ATM. CHƯƠNG 5: KẾT LUẬN. Kết luận tổng thể các kết quả đạt được trong luận văn và hướng phát triển của luận văn. 7 CHƯƠNG 2. EAOP VÀ EVENT-B 2.1. Event-based Aspect Oriented Programming Nền tảng chung của EAOP được trình bày trong [3]. EAOP chú ý đến các sự kiện phát sinh ra trong quá trình thực hiện chương trình độc lập với bất kỳ ngôn ngữ lập trình cụ thể. Tính năng chính của mô hình là aspect có thể định nghĩa một hành động cho một chuỗi các sự kiện thay vì cá nhân chỉ như mô tả trong mô hình AOP. Nó có những đặc điểm chính sau:  Aspect: được định nghĩa về các sự kiện sinh ra trong quá trình thực hiện chương trình.  Cross-cuts: giảm chuỗi sự kiện, có thể bao gồm các trạng thái thay đổi, được xác định bởi mô hình sự kiện đó được kết hợp trong quá trình thực hiện chương trình.  Một cross-cuts được chọn, một hành động liên quan được thực hiện. 2.2. Các đăc điểm của AOP a. Điểm nối (join point) Join point [13]: có thể là bất kỳ điểm nào có thể xác định được khi thực hiện chương trình. Có thể là lời gọi hàm đến một phương thức hoặc một lệnh gán cho một biến của đối tượng. Trong Aspect mọi thứ đều xoay quanh join point. b. Hướng cắt (pointcut) Pointcut [13]: là 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à một 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 đối số của phương thức đó. c. Mã hành vi (advice) Advice [13]: là mã được thực hiện tại một join point mà được chọn bởi poincut. Advice tương tự cấu trúc của hàm cung cấp các thức, các hành động đan xen tại các join point mà nó được chọn bởi pointcut. Poincut và advice sẽ hình thành nên các luật đan kết các quan hệ đan xen. 8 Advice được chia thành 3 loại:  Before: được thực hiện trước join point.  After: được thực hiện sau join point.  Around: bao quanh sự thực hiện join point, advice này có thể thực hiện vòng, thực hiện tiếp của mã nguồn ban đầu hoặc thực hiện thay đổi ngữ cảnh (tham số của hàm, ...). d. Khía cạnh (aspect) Aspect [13]: là phần tử trung tâm của AspectJ, 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. e. Thực thi cắt ngang (crosscutting) Crosscutting [13]: trong aspectj, là quá trình biên dịch thực thi các quy tắc đan cá mô đun cắt ngang vào mô đun chính. Thực thi cắt ngang có 2 loại:  Thực thi cắt ngang động (dynamic crosscutting): là việc đan các advice mới vào quá trình thực thi một chương trình. Trình biên dịch sẽ dựa vào tập các quy tắc đan để xác định điểm đan để chèn thêm hoặc thay thế luồng thực thi của chương trình bằng mô đun cắt ngang. Từ đó, làm thay đổi hành vi của hệ thông.  Thực thi cắt ngang tĩnh (static crosscutting) là quá trình đan một sửa đổi vào cấu trúc tĩnh của lớp, giao diên, hay các khía cạnh của hệ thống. Chức năng chính của thực thi cắt ngang tĩnh là hỗ trợ cho thực thi cắt ngang đông. 9 f. Đan mã aspect AspectJ cho phép đan xen mã aspect với các chương trình Java ở ba mức khác nhau mức mã nguồn, mã bytecode và tại thời điểm nạp chương trình khi chương trình gốc chuẩn bị được thực hiện. Đan ở mức mã nguồn (source code weaving), AspectJ sẽ nạp các mã aspect và Java ở mức mã nguồn (.aj và .java), sau đó thực hiện biên dịch để sinh ra mã đã được đan xen bytecode, dạng .class. Đan xen ở mức mã bytecode (byte code weaving), AspectJ sẽ dịch lại và sinh mã dạng .class từ các các mã aspect và Java đã được biên dịch ở dạng (.class). Đan xen tại thời điểm nạp chương trình (load time weaving), các mã của aspectvà Java dạng .class được cung cấp cho máy ảo Java (JVM). Khi JVM nạp chương trình để chạy, bộ nạp lớp của AspectJ sẽ thực hiện đan xen và chạy chương trình. Với việc đan xen ở mức mã bytecode và tại thời điểm nạp chương trình thì phương pháp này có thể được sử dụng mà không yêu cầu phải có mã nguồn. Khi thay đổi đặc tả thì mới phải phải sinh và biên dịch lại mã aspect [18]. 2.2.1. Quản lý các concerns hệ thống Concern được chia làm 2 loại:  Concern thành phân: thể hiện các chức năng nội tại của mô đun.  Concern đan xen: thể hiện các quan hệ ràng buộc giữa các mô đun trong hệ thống. Việc xác định được các concern trong hệ thống, chúng ta sẽ tập trung vào các concern một cách độc lập và sẽ giảm độ phức tạp của hệ thống. Các concern đan xen nhau giữa các mô đun, các kỹ thuật thi công hiện tại sẽ trộn chúng vào một mô đun. Hình vẽ sau sẽ minh họa: Với mô hình biển diễn nhiều chiều của các concern được ánh xạ trên các ngôn ngữ một chiều như sau. Trong thiết kế phần mềm cách tốt nhất để đơn giản các hệ thống phức tạp là xác định các concern rồi mô đun hóa chúng. OOP được thiết kế để phục vụ việc mô đun hóa các concern cơ bản, nhưng khi gặp concern mức hệ thống thì OOP không đáp ứng được yêu cầu. Hình sau minh họa ví dụ thiết kế dùng phương pháp truyền thống. Ngay cả khi bạn có một bản thiết kế tốt của logging mô đun như: cung cấp 10 các API trừu tượng (Abstract API), giấu các định dạng log mesage ... Các mô đun còn lại vẫn cần phải nhúng các đoạn mã để gọi các logging API [13]. 2.2.2. Phương pháp luận của AOP Tuy nhiên cộng đồng nghiên cứu AOP đưa ra 3 bước sau:  Aspectual decomposition: chúng ta phân tách các yêu cầu nhằm xác định các concern lõi và concern đan xen. Các concern lõi được tách ra khỏi các concern đan xen.  Concern implementation: thực thi các concern một cách độc lập.  Aspectual Recomposotion: chỉ ra các quy luật kết hợp bằng cách tạo ra các aspect còn được gọi là quá trình đan mã, sử dụng các thông tin trong aspect để cấu thành hệ thống đích [13]. Hình 8: Các giai đoạn phát triển sử dụng phương pháp AOP 2.2.3. Ưu điểm của AOP Những ưu điểm của phương pháp AOP như sau:  Tách biệt chức năng hơn của các mô đun độc lập.  Tính năng mô đun hóa cao hơn.  Phát triển hệ thống dễ dàng hơn.  Kết nối được với các thiết kế trong tương lai. 11  Tăng khả năng sử dụng lại mã.  Giảm thời gian thi công hệ thống.  Giảm giá thành hệ thống. 2.2.4. Nhược điểm của AOP Mặc dù phương pháp AOP có nhiều ưu điểm, song phương pháp AOP vẫn còn có những nhược điểm là:  AOP thực ra không giải quyết vấn đề mới, không giải quyết vấn đề chưa giải quyết.  AOP không là cứu cánh cho các nhà thiết kế cẩu thả.  AOP phá vỡ tính đóng gói. 2.3. Event-B Event-B [2] là một phương pháp hình thức dựa trên lý thuyết và tập hợp, ngôn ngữ thay thế tổng quát và logic vị từ bậc một (first order logic). Event-B bao gồm các ký pháp, phương pháp và công cụ hỗ trợ quá trình phát triển phần mềm bằng cách làm mịn (refinement). Quá trình làm mịn bằng cách xây dựng máy trừu tượng sau đó làm mịn dần cho đến khi nhận được một máy thực thi, tương tự như mã nguồn của chương trình [19]. 2.3.1 Máy và ngữ cảnh Các mô hình Event-B được mô tả bởi 2 cấu trúc cơ bản là máy (machines) và ngữ cảnh (context). Trong đó, máy dùng để mô tả phân động của mô hình bao gồm biến, bất biến, định lý, và các sự kiện tương tác với môi trường. Ngữ cảnh mô tả phần tĩnh của mô hình, chứa các tập hợp, hằng, tiên đề và định lý [19]. Một mô hình có thể chỉ gồm có máy hoặc ngữ cảnh hoặc sự kết hợp giữa máy và ngữ cảnh. Một máy có thể không hoặc tham chiếu một vài ngữ cảnh. Các máy và ngữ cảnh của mô hình được làm mịn bằng cách bổ sung các hằng, biến, bất biến, định lý, sự kiên. 12 2.3.2. Sự kiện Mô hình hệ thống Event-B được bắt đầu từ các sự kiện trừu tượng quan sát được có thể xảy ra trong hệ thống, từ đó đặc tả các trạng thái và hành vi của hệ thống ở mức trừu tượng cao hơn. Một sự kiện evt tác động lên (một danh sách) biến trạng thái v, với điều kiện G (x, v) và hành động A (x, v, v') được mô tả như sau [19]: evt = any x where G (x, v) then A (x, v, v’) 2.3.3. Phân rã và kết hợp Một trong những đặc trưng quan trọng nhất của Event-B [2] đó là khả năng bổ sung các sự kiện mới trong quá trình làm mịn, tuy nhiên khi bổ sung các sự kiện sẽ làm tăng độ phức tạp của tiến trình làm mịn do phải xử lý nhiều sự kiện và nhiều biến trạng thái. Ý tưởng chính của sự phân rã là phân chia mô hình M thành các mô hình con M1Mn, các mô hình con này dễ dàng được làm mịn hơn so với mô hình ban đầu [19]. 2.3.4. Công cụ Rodin là bộ công cụ mã nguồn mở dựa trên nền tảng Eclipse để mô hình và kiểm chứng tự động trong Event-B. Kiến trúc và công cụ được minh họa hình dưới. Trong đó, Event-B UI cung cấp cho người dùng giao diện để chỉnh sửa mô hình Event-B. Event-B Core gồm có 3 thành phần: kiểm tra tĩnh (kiểm tra cú pháp trong mô hình Event-B), máy kiểm chứng (nơi thực hiện các kiểm chứng đơn giản làm cho dễ dàng tự động hóa), và máy quản lý kiểm chứng (quản lý kiểm chứng và chứng cứ liên quan). Các Rodin Core bao gồm 2 thành phần: kho Rodin (quản lý kiên trì dữ liệu) và người xây dựng Rodin (công việc lập lịch tùy thuộc vào những thay đổi trong kho Rodin). Event-B UI Event-B Core Rodin Core Event-B Library Eclipse platform Hình 14: Mô hình kiến trúc Rodin 13 CHƯƠNG 3: MÔ HÌNH HÓA VÀ KIỂM CHỨNG CÁC PHÂN MỀM LẬP TRÌNH HƯỚNG KHÍA CẠNH 3.1. Trình bày lập trình hướng khía cạnh hệ thống hướng sự kiện trong Event- B EAOP là lập trình hướng khía cạnh hệ thống hướng sự kiện. Nếu chương trình ban đầu phát ra một sự kiện hoặc chuỗi các sự kiện, các thành phần giám sát thực hiện các khía cạnh liên quan. Sau đây, một số định nghĩa: Định nghĩa 3.1 (chương trình cơ bản). Một chương trình cơ bản gồm 4-tuple BP=, trong đó E là tập các sự kiện, A là chuỗi các hành động, V là tập các thuộc tính của chương trình, C là tập các thuộc tính ràng buộc. Chúng ta xem chương trình cơ bản như một chương trình hệ thống hướng sự kiên, chỉ đơn giản bao gồm các sự kiện, hành động, các biến, và những ràng buộc. Những ràng buộc này được xem như là đặc tính mong muốn của các ứng dụng bởi vì nó phải thỏa mãn một số các điều kiện. Định nghĩa 3.2 (cross-cut). Một crosscut, được xác định bởi CCE, qui định một chuỗi các sự kiện đại diện cho những điểm xác định đánh giá chương trình cơ bản. Một aspect trong mô hình EAOP gồm biến mới và một cross-cut trong đó chứa các chương trình cơ bản. Định nghĩa 3.3 (aspect). Một aspect trong mô hình EAOP gồm có A=<Vr, CC×S> trong đó S là tập các advice liên quan đến cross-cut CC và Vr trạng thái biến. Ví dụ: Một ứng dụng EAOP có chứa một aspect thì chuyển một file mã nguồn đến máy chủ bất cứ khi nào nó được sửa đổi trong phiên làm việc. Chương trình được thực hiện với A=<{}, {login → do_login, modigy → commit_svn, logout → do_logout}>, trong đó login, modify và logout là 3 sự kiện, do_login, commit_svn và do_logout là 3 advice tương ứng. 14 3.2. Mô hình hệ thống lập trình hướng khía cạnh sử dụng Event-B. Trong phần này, dựa trên các định nghĩa ở phần 3.1, chúng tôi trình bày các quy luật dịch để dịch một ứng dụng lập trình hướng khía cạnh hệ thống hướng sự kiện với Event-B. Luật 1: chương trình cơ bản P = thì được dịch sang một máy M trừu tượng Event-B sao cho e  E là ánh xạ từ sự kiện của máy M, hành động của các chương trình cơ bản được mô tả thân của sự kiện Event-B, các biến của chương trình được chuyển dịch thành biến của máy M, và những ràng buộc của chương trình thì được mô tả bởi mệnh đề biến số Event-B. Luật 2: Aspect được thể hiện khi một chuỗi sự kiện phát ra bởi chương trình cơ bản. Chúng tôi xây dụng mô hình aspect sử dụng cơ chế lọc Event-B. Nói cụ thể hơn, mỗi aspect được chuyển hóa thành một máy cụ thể có thể lọc được máy trừu tượng (đại diện cho một chương trình cơ bản). Luật 3: Những advice liên kết với sự kiện trong một aspect thì được dịch sang các hành động của những sự kiện Event-B tương ứng. 3.3. Kiểm chứng hệ thống Sau những đặc tả các ứng dụng trong Event-B, chúng tôi khai thác nghĩa vụ kiểm chứng để kiểm chứng những ràng buộc của nó. Vì thế có một aspect có thể thay đổi trong một chương trình cơ bản, có có thể gây ra xung đột đối với những ràng buộc trong chương trình cơ bản. Vì thế chúng tôi cần phải đảm bảo rằng các aspect nhau không làm thay đổi rằng buộc này. Đề xuất 1: Với những quy luật chuyển dịch được đề xuất ở phần 3.2 một aspect duy trì những ràng buộc của chương trình cơ bản. Chứng minh: Cho P = là chương trình cơ bản, a = là một aspect, trong đó v là một biến mới, e  E, s là một advice. Khi v là một biến, phải thỏa mãn các ràng buộc c(v), được bổ trợ bởi aspect (khi v’ là v sau khi mở rộng aspect). Chúng ta cần chứng minh rằng, c(v’) vẫn nắm giữ. 15 Với luật 1, e được dịch thành ev của máy M, cho g(ev) là bảo vệ của sự kiện Event-B, biến v được dịch thành vb trong Event-B. Chúng ta có bất biến I trong Event-B có nghĩa là duy trì những ràng buộc của chương trình cơ bản (i). Với luật 2, chúng ta làm mịn máy M’ chứa chương trình làm mịn sự kiện ev_r với bảo vệ g(ev_r) (ii). Với luật 3, liên kết giữa advice trong sự kiện ev_r, được dịch từ hành động sang sự kiện, gán biến vb cho vb’ (có nghĩa là A(vb,vb’)) (iii). INV chứng minh nghĩa vụ làm mịn máy M’ được tạo ra như sau. g(ev_r)  I(vb) ⊢ I(vb’) (1) Nếu nắm công thức 1, với chuyển dịch (i), (ii), (iii), chúng ta có thể kết luận rằng c(v'). 16 CHƯƠNG 4: ÁP DỤNG BÀI TOÁN Áp dụng các các lý thuyết đã trình bày về mô hình hóa và kiểm chứng các phần mềm hướng khía cạnh đã ở trên. Kết quả của quá trình kiểm tra chương trình có còn lưu giữ một số định nghĩa thuộc tính sau khi đan chương trình bảo tồn hệ thống ban đầu không? Trong phần này, thứ tự các bước để thực hiện chương trình được mô tả như sau: Đầu tiên, một chương trình AOP được thực hiện kết hợp với các đan xen các sự kiện của chương trình được mô hình EAOP. Thứ hai, từ các định nghĩa trong lập trình hướng khía cạnh dựa sự kiện trong Event-B ta mô hình hóa được tập luật. Cuối cùng, các tập luật kết hợp với mô hình EAOP được đưa ra cho vào công cụ RODIN để kiểm chứng bài toán có được bảo tồn hệ thống ban đầu không? Hình 15: Phương pháp mô hình hóa và kiểm chứng các chương trình hướng khía cạnh 17 Áp dụng phương pháp mô hình hóa và khiểm chứng các chương trình hướng khía cạnh với máy ATM. Chương trình được thiết kế để xử lý giao dịch thẻ tín dụng của máy ATM của người dùng có 3 sự kiện: withdraw, deposit và transfer khi người dùng rút tiền gửi, gửi tiền gửi hoặc chuyển tiền gửi từ tài khoản ngân hàng của họ. Các tài khoản ngân hàng của người sử dụng cần phải đáp ứng yêu cầu tài khoản luôn lớn hơn không. Đầu tiên, ta có một chương trình java ứng dụng AOP mô tả máy ATM gồm 3 file: Transaction.java, Exchange.java, updatetr.ja. Trong đó, class transaction mô tả chức năng gửi tiền, rút tiền trên máy ATM. Class exchange mô tả chức năng chuyển tiền trên máy ATM. Aspect updatetr mô tả crosscut của chương trình. File Transaction.java package banking; public class Transaction { int amt,ac; float bal; public int getac() { return ac; } public float deposit (int amt) { this.bal=bal+amt; System.out.println("deposit:"); return bal; } public float withdraw (int amt) { this.bal-=amt; System.out.println("withdraw:"); return bal; } } File Exchange.java package banking; 18 public class Exchange { private Transaction T1,T2; public Transaction getac1() { return T1; } public Transaction getac2() { return T2; } public void transfer (int amt) { T1.bal+= amt; T2.bal-= amt; } } File updatetr.ja package banking; public aspect updatetr { pointcut cross () : execution (void Transaction.deposit(int)) || execution (void Transaction.withdraw(int)) || execution (void Exchange.transfer(int)); after() returning: cross() { Display.update(); System.out.println("aspect after:"); } } Áp dụng EAOP vào bài toán, chúng ta có chương trình cơ bản P = như sau: E = {open, close, withdraw, deposit, transfer}, V = { bal, amount}, trong đó bal và amount là số dư tài khoản và số tiền muốn rút hoặc gửi, C = bal > 0 là trạng thái yêu cầu bắt buộc, A = { withdraw_act, deposit_act}. Sau luật 1, chúng ta đạt được mô hình hệ thống hướng sự kiện Event-B như minh họa (inv1 và inv2 không những định nghĩa 2 biến mà còn chắc chắn các hạn chế của chương trình luôn luôn thỏa mãn). Có 5 sự kiện trong máy tương ứng với 5 sự kiện của chương trình cơ bản là open, close, withdraw, deposit và transfer. Event-B đặc tả của chương trình cơ bản: 19 Trong đó, sự kiện mở tài khoản của ứng dụng được thể hiện như sau: open ≙ STATUS ordinary ANY p a WHERE grd1 : p∈ PRS grd2 : a ∉ action THEN act1 : owner(a) ≔p act2 : bal(a)≔0 act3 : action ≔ action ∪ {a} END Sự kiện đóng tài khoản ATM của ứng dụng được thể hiện sau: close ≙ STATUS ordinary ANY a WHERE grd1 : a ∈ action grd2 : bal(a)=0 THEN act1 : owner ≔ {a} ⩤ owner act2 : bal ≔ {a} ⩤ bal act3 : action ≔ action ∖ {a} END Sự kiện rút tiền gửi trên máy ATM của ứng dụng được mô tả như sau: withdraw ≙ STATUS ordinary ANY a q WHERE grd1 : a ∈ action grd2 : q ∈ ℕ 20 grd3 : q≤bal(a) THEN act1 : bal(a)≔ bal(a)−q END Sự kiện gửi tiền gửi trên máy ATM của ứng dụng được mô tả như sau: deposit ≙ STATUS ordinary ANY a q WHERE grd1 : a∈action grd2 : q∈ ℕ THEN act1 : bal(a)≔bal(a)+q END Sự kiện chuyển tiền gửi trên máy ATM của ứng dụng được mô tả như sau: transfer ≙ STATUS ordinary ANY src dest amt WHERE grd1 : src ∈ action grd2 : dest ∈ action grd3 : amt ∈ ℕ grd4 : src ∈ dom(bal) grd5 : dest ∈ dom(bal) grd6 : src ≠ dest grd7 : amt ≤ bal(src) THEN act1 : bal ≔ bal {dest ↦ (bal(dest)+amt), src ↦ (bal(src)−amt)} END 21 Chúng ta tạo một aspect rút tiền gửi tính phí và cung cấp tiền thưởng cho người sử dụng rút tiền. Chúng tôi cần thêm nhiều hơn 3 biến mới là a, q, và b để định lại các giá trị tương ứng. Trong trường hợp làm mịn sự kiện withdraw_c, advice bổ sung bal được chuyển dịch thành act1, act2. Để tạo ra mô hình một cách chính xác, chúng tôi củng cố sự bảo vệ của sự kiện withdraw_c bằng cách thêm vào một mệnh đề nữa grd3: bal(a) > q chỉ ra rằng a lớn hơn q aspect cần kiểm tra điều kiện này advice. Sự kiện mở rộng withdraw_c rút tiền trên máy ATM được Event-B đặc tả của aspect mô tả như sau: withdraw_c ≙ extended STATUS ordinary REFINES withdraw ANY a q b WHERE grd1 : a ∈ action grd2 : q ∈ ℕ grd3 : q≤bal(a) grd4 : b ∈ action grd5 : b≠a THEN act1 : bal(a)≔ bal(a)−q act2 : inbank ≔ inbank ∪ {b ↦ q} END Kết quả thực hiện soạn thảo trên công cụ Rodin, sinh và kiểm chứng tự động các mệnh đề cần chứng minh. 22 Kết quả của quá trình mô hình hóa và kiểm chứng tự động được thể hiện qua bảng Statistics, cho thấy toàn bộ các ràng buộc được chứng minh đảm bảo mục đã đặt ra. 23 CHƯƠNG 5: KẾT LUẬN 5.1. Những đóng góp của luận văn Những đóng góp chính của kết quả trong việc mô hình hóa và kiểm chứng các phần mềm hướng khía cạnh, kết quả cụ thể như sau: Mô hình hóa và kiểm chứng phần mềm hướng khía cạnh dựa sự kiện là đúng đắn. EAOP là phương pháp tiếp cận mở rộng cho lập trình hướng khía cạnh. Nó kết hợp ưu điểm của cả lập trình hướng khía cạnh và kiến trúc dựa sự kiện. Chúng tôi trình bày một phương pháp mới để tạo mẫu và kiểm chứng một ứng dụng hướng khía cạnh dựa sự kiện sử dụng phương pháp hình thức Event-B. Phương pháp mà chúng tôi đề xuất dựa trên việc dịch một chương trình EAOP thành các kí hiệu Event-B, tận dụng các cơ chế làm mịn để kiểm chứng những ràng buộc trong chương trình trong mỗi aspect. 5.2. Hướng phát triển Tiếp tục nghiên cứu và phát triển các phương pháp mô hình hóa và kiểm chứng phần mềm với phương pháp hình thức Event-B. Cài đặt bổ trợ công cụ kiểm chứng mã nguồn mở Rodin. Hoàn thiện hơn nữa mô hình hóa kiểm chứng các phần mềm hướng khía cạnh dựa sự kiện. Tiếp tục phát triển cần phải mở rộng cùng với crosscuts tinh xảo hơn vào mô hình EAOP. 24 TÀI LIỆU THAM KHẢO [1]. Event-B and the rodin platform. 2012. [2]. J.R. Abrial. Modeling in Event-B: System and software engineering. Cambridge University Press, New York, NY, USA 1st edition, 2010. [3]. R. Douence and M. Sudholt. A model and a tool for event-based aspect-oriented programming (eaop). Technical Report TR 02/11/INFO. Ecole des Mines de Nantes, 2002. [4]. L. Guan, X. Li, and H. Hu. A petri net-based approach for supporting aspect oriented modeling. In Theoretical Aspects of Software Engineering, 2008, pages 83-90, June 2008. [5]. Holzer, L. Ziarek, K. Jayaram, and P. Eugster. Putting events in context: Aspects for event-based distributed programming. In Proceedings of the Tenth International Conference on Aspect-oriented Software Development, AOSD '11, pages 241-252, New York, NY, USA, 2011. ACM. [6]. O. Ligot, J. Bendisposto, and M. Leuschel. Debugging event-b models using the prob disprover plug-in. Proceedings AFADL'07, Juni 2007. [7]. T. N. Thuan and N. V. Ha. Using b to verify the weaving of aspects. In Software Engineering Conference, 2007. APSEC 2007. 14th Asia-Pacifc, pages 199-205, Dec 2007. [8]. N. Ubayashi and T. Tamai. Aspect-oriented programming with model checking. In Proceedings of the 1st international conference on Aspect-oriented software development, AOSD '02, pages 148-154, New York, NY, USA, 2002. ACM. [9]. D.-X. Xu, O. El-Ariss, W.-F. Xu, and L.-Z. Wang. Aspect-oriented modeling and verication with fnite state machines. J. Comput. Sci. Technol., 24(5):949- 961, Sept. 2009. [10]. J. Zhang, Y. Chen, and G. Liu. Modeling aspect-oriented programming with uml profile. In Education Technology and Computer Science, 2009. ETCS '09. First International Workshop on, volume 2, pages 242-245, March 2009. [11]. Anh-Hoang Truong, Phuc Dinh Nguyen, Tuyen Luu, Checking implementations of UML 2.0 sequence diagrams. [12]. Joseph D. Gradecki, Nicholas Lesiecki, Mastering AspectJAspect-Oriented Programming in Java - Wiley, 1 edition (March 7, 2003). [13]. Ramnivas Landdad. AspectJ in Action practicalaspect-oriented programming. Manning publishing -2004. 25 [14]. Visser W, et.al, Model Checking Programs, 15th IEEE International Conference on Automated Software Engineering, 2000 [15]. R. Douence, P.Fradet, and M. Sudholt. A framework for the detection and resolution of aspect interactions. In Proc. of the ACM SIGPLAN/SIGSOFT Conf. on Generative Programming and Component Engineering (GPCE), October 2002. [16]. R. Douence, O. Motelet, and M. Sudholt. A formal definition of crosscuts. In Proc. of the 3rd Int. Conf. on Metalevel Architectures and Separation of Crosscutting Concerns, volume 2192 of LNCS. Springer Verlag, September 2001 [17]. Trịnh Thanh Bình, Trương Anh Hoàng, Nguyễn Việt Hà, Kiểm chứng giao thức tương tác giữa các thành phần trong chương trình đa luồng sử dụng lập trình hướng khía cạnh, Chuyên san Các công trình nghiên cứu, phát triển và ứng dụng CNTT-TT, Tạp chí Công nghệ thông tin & Truyền thông, T. V-1, S. 4 (24), 36-45, 2010. [18]. Trịnh Thanh Bình, Trương Ninh Thuận, Nguyễn Việt Hà, Kiểm chứng sự tuân thủ về ràng buộc thời gian trong các ứng dụng phần mềm, Tạp chí Tin học và Điều khiển học, T. 26, S. 2, 173-184, 2010. [19]. Trịnh Thanh Bình (2011). Kiểm chứng các thành phần Java tương tranh. Luận án tiến sỹ, Trường Đại học Công Nghệ, Đại học Quốc Gia Hà Nội, tr. 6,7.