Tóm tắt Luận văn Thạc sĩ Công nghệ thông tin: 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<br /> <br /> ĐẠI HỌC QUỐC GIA HÀ NỘI<br /> TRƯỜNG ĐẠI HỌC CÔNG NGHỆ<br /> <br /> PHẠM NHƯ UYỂN<br /> <br /> MÔ HÌNH HÓA VÀ KIỂM CHỨNG<br /> CÁC CHƯƠNG TRÌNH PHẦN MỀM HƯỚNG KHÍA CẠNH<br /> <br /> Ngành: Công nghệ Thông tin<br /> Chuyên ngành: Kỹ thuật Phần mềm<br /> Mã số: 60480103<br /> <br /> NGƯỜI HƯỚNG DẪN KHOA HỌC: PGS.TS Trương Ninh Thuận<br /> <br /> HÀ NỘI - 2016<br /> <br /> 4<br /> <br /> CHƯƠNG 1: ĐẶT VẤN ĐỀ<br /> 1.1 Sự cần thiết của đề tài<br /> 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<br /> cạnh sử dụng các kỹ thuật khác nhau như UML [10], kiểm chứng mô hình (model<br /> 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<br /> các sự kiện.<br /> 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ở<br /> rộng những kí hiệu UML để cụ thể hóa những vấn đề crosscutting. Tuy nhiên, những<br /> 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<br /> chính thức hoặc bán chính thức của UML. Ubayashi và Tamain [8] đã đề xuất một<br /> phương pháp để kiểm chứng chương trình AOP sử dụng mô hình kiểm tra. Phương<br /> 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<br /> 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<br /> 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<br /> khó có thể sử dụng phương pháp này để xác minh phần mềm lớn.<br /> Dianxiang Xu [9] đã đề xuất sử dụng máy trạng thái và kiểm chứng những<br /> 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ô<br /> 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<br /> 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,<br /> 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<br /> 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.<br /> 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<br /> 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<br /> để đảm bảo chính xác của aspectJ thành phần.<br /> Để 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<br /> 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<br /> 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ể<br /> 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ó<br /> 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<br /> 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<br /> 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<br /> <br /> 5<br /> <br /> mịn để mô hình cơ bản và chương trình giám sát. Sau đó, khai thác Event – B để<br /> chứng minh được tạo ra để kiểm tra xem các hạn chế áp dụng bởi aspect cross-cuts.<br /> 1.2. Nội dung đề tài<br /> 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<br /> 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ự<br /> 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<br /> 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ế để<br /> 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<br /> 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<br /> 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<br /> 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 đó,<br /> chúng ta khai thác Event – B để chứng minh được tạo ra để kiểm tra xem các hạn<br /> chế áp dụng bởi aspect cross-cuts. Cuối cùng, phương pháp đề xuất được minh họa<br /> chi tiết với một chương trình ATM.<br /> 1.3. Đóng góp của luận văn<br /> Đó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<br /> 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<br /> 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<br /> mịn để kiểm chứng những ràng buộc trong chương trình trong mỗi aspect. Với mong<br /> 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<br /> 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<br /> trong một chương trình ATM.<br /> <br /> 1.4. Cấu trúc luận văn<br /> 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:<br /> CHƯƠNG 2: EAOP VÀ EVENT-B<br /> 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<br /> 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,<br /> <br /> 6<br /> <br /> 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<br /> Rodin.<br /> CHƯƠNG 3: MÔ HÌNH HÓA VÀ KIỂM CHỨNG CÁC PHẦN MỀM<br /> HƯỚNG KHÍA CẠNH.<br /> 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<br /> 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<br /> 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<br /> chứng hệ thống.<br /> CHƯƠNG 4: ÁP DỤNG BÀI TOÁN.<br /> Á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<br /> toán máy ATM.<br /> CHƯƠNG 5: KẾT LUẬN.<br /> 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<br /> luận văn.<br /> <br /> 7<br /> <br /> CHƯƠNG 2. EAOP VÀ EVENT-B<br /> 2.1. Event-based Aspect Oriented Programming<br /> Nền tảng chung của EAOP được trình bày trong [3]. EAOP chú ý đến các sự kiện<br /> 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<br /> 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<br /> 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ó<br /> những đặc điểm chính sau:<br />  Aspect: được định nghĩa về các sự kiện sinh ra trong quá trình thực hiện<br /> chương trình.<br />  Cross-cuts: giảm chuỗi sự kiện, có thể bao gồm các trạng thái thay đổi, được<br /> 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<br /> trình.<br />  Một cross-cuts được chọn, một hành động liên quan được thực hiện.<br /> 2.2. Các đăc điểm của AOP<br /> a. Điểm nối (join point)<br /> 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<br /> 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<br /> của đối tượng. Trong Aspect mọi thứ đều xoay quanh join point.<br /> b. Hướng cắt (pointcut)<br /> 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<br /> 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<br /> 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<br /> phương thức, các đối số của phương thức đó.<br /> c. Mã hành vi (advice)<br /> Advice [13]: là mã được thực hiện tại một join point mà được chọn bởi poincut.<br /> 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<br /> join point mà nó được chọn bởi pointcut. Poincut và advice sẽ hình thành nên các<br /> luật đan kết các quan hệ đan xen.<br /> <br />