CHƯƠNG 1: ĐẶT VẤN ĐỀ 1.1 Sự cần thiết của đề tài Ngày nay, sự phát triển mạnh mẽ của phần mềm ngày càng đóng vai trò quan trọng, được ứng dụng vào tất cả các lĩnh vực trong đời sống xã hội hiện đại. Làm cho tỷ trọng giá trị phần mềm trong các hệ thống ngày càng lớn. Tuy nhiên, trong nhiều hệ thống, lỗi của phần mềm gây ra hậu quả đặc biệt nghiêm trọng, không chỉ thiệt hại nặng nề về mặt kinh tế [14]. 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 để mô hình hóa và kiểm chứng các hệ thống dựa trên 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 đề thực thi cắt ngang (crosscutting). Tuy nhiên, những nghiên cứu này đã không giải quyết những kiểm chứng của khía cạnh do bản chất không hình thức hoặc bán hình thức của UML. Các tác giả Ubayashi và Tamai [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à khía cạnh.
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. Tác giả 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 hướng khía cạnh. Các tác giả đã chuyển hóa đan các mô hình và các lớp mô hình không bị ảnh hưởng bởi khía cạnh thành các quy trình FSP, mà sẽ được kiểm chứng bởi mô hình LTSA kiểm tra đối với các thuộc tính hệ thống muốn có.
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à khía cạnh sang mô hình trạng thái trước khi khởi động mô hình FSP. Tác giả đã dùng B [7] để kiểm chứng đan khía cạnh. Tác giả bài báo trình bày lớp cơ bản và một số khía 9 cạnh liên quan của AspectJ trong ngôn ngữ B 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. Để mô hình hóa và kiểm chứng các hệ thống dựa trên sự kiện, lập trình hướng khía cạnh dựa sự kiện (Event-based Aspect Oriented Programming – EAOP) [3] xác định đan khía cạnh bằng cách phát hiện một chuỗi các sự kiện.
Phương pháp có thể sử dụng khía cạnh thay đổi sự kiện thay vì thay đổi từng lớp riêng biệt. 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. Event-B [2] là một phương pháp hình thức phù hợp hơn cho việc phát triển lớn hệ thống phân tán và hệ thống phản hồi. Phát triển phần mềm trong Event-B bắt đầu bằng việc mô tả các yêu cầu của hệ thống ở mức trừu tượng và sau đó lại làm mịn chúng thông qua một số bước để đạt được mô tả của hệ thống chi tiết có thể chuyển đổi sang mã nguồn.
Tính nhất quán của mô hình và mối quan hệ giữa mô hình trừu tượng và mô hình làm mịn lại thu được bằng phương pháp chứng minh hình thức. Công cụ hỗ trợ cụ thể cho phương pháp hình thức Event-B là công cụ Rodin. Xuất phát từ yêu cầu mô hình hóa và kiểm chứng EAOP và các ưu điểm của phương pháp hình thức Event-B có ý nghĩa thực tiễn trong quá trình phát triển phần mềm. Dẫn đến sự lựa chọn đề tài luận văn tốt nghiệp của tôi là: “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.
Nội dung đề tài Trong luận văn này, đề xuất một phương pháp dựa trên phân tích một ứng dụng EAOP bằng phương pháp hình thức Event-B. Ý tưởng xuất phát từ sự tương đồng giữa cấu trúc sự kiện Event-B và EAOP. Đầu tiên, chúng ta xác định các thành phần ứng dụng trong EAOP chuyển đổi sang mô hình Event-B. Tiếp theo, chúng tôi đưa mô hình hóa tiếp cận thực tế bằng cách sử dụng nền tảng Rodin để kiểm chứng thuộc tính chương trình có còn bảo tồn một số tính chất sau khi thực hiện đan chương trình, các ràng buộc khác dựa trên công cụ chứng minh tự động.
Ưu điểm của cách tiếp cận 10 này là chương trình bao gồm các khía cạnh, biến và các ràng buộc khác được mô hình hóa dễ dàng bằng những đặc tả logic trong Event–B như bất biến và sự kiện. Do đó, tính đúng đắn của hệ thống có thể được chứng minh bằng phương pháp hình thức. Điều đó rất quan trọng cho các nhà phát triển phần mềm phát hiện được các vấn đề ở thời gian thiết kế. Hơn nữa, cách tiếp cận gần với thực tế mà chúng tôi có thể triển khai một công cụ theo ý tưởng chính để chuyển đổi mô hình EAOP từ Event–B sang công cụ Rodin tự động.
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. Đó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 khía cạnh. Với mong muốn kiểm tra chương trình có còn bảo toàn 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. Cấu trúc luận văn Các phần còn lại của luận văn có cấu trúc như 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ề AOP. Sau đó, giới thiệu khái quát cơ bản về 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 hình thức Event-B, mô tả cấu trúc, các thành phần của Event-B.
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 11 Trình bày các định nghĩa được ánh xạ của phương pháp hình thức Event-B, các luật chuyển đổi giữa mô hình chương trình phần mềm hướng khía cạnh dựa sự kiện sang mô hình 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.
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. EAOP VÀ EVENT-B 2. Các đặc điểm của lập trình hướng khía cạnh Lập trình hướng khía cạnh (Khía cạnh Oriented Programming – AOP) [13] là phương pháp lập trình phát triển trên tư duy tách biệt các mối quan tâm khác nhau thành các mô đun khác. AOP là một mô hình lập trình mới mẻ ngăn cách mối quan tâm ở cấp thực hiện.
Trong quan điểm phát triển phần mềm, AOP cho phép các nhà phát triển áp dụng khía cạnh mà thay đổi hành vi các lớp hoặc đối tượng độc lập của bất kỳ hệ thống phân cấp thừa kế. Các phát triển sau đó có thể áp dụng những khía cạnh hoặc trong thời gian chạy hoặc thời gian biên dịch. Ở đây, chúng tôi sẽ mô tả yếu tố chính của AOP: a. 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 khía cạnh mọi thứ đều xoay quanh điểm nối. Điểm nối được phân loại như sau: Điểm nối tại các phương thức. Điểm nối tại hàm khởi tạo (contructor). Điểm nối tại điểm truy cập các thuộc tính.
Điểm nối tại điểm điều khiển ngoại lệ: được biểu diễn trong khối điều khiển ngoại lệ. Điểm nối tại các hành vi. Ta có thể khai báo hướng cắt trong một khía cạnh, một lớp hoặc 13 một giao diện. Giống như phương thức, có thể dùng định danh truy cập (public, private) để giới hạn quyền truy cập đến hướng cắt.
Các hướng cắt có thể có tên hoặc không tên. Các hướng cắt không tên cũng giống như các lớp không tên, được định nghĩa tại nơi sử dụng. Các hướng cắt được đặt tên thì có thể được tham chiếu từ nhiều nơi khác. Bảng ánh xạ giữa các điểm nối được chọn cho các hướng cắt: Loại điểm nối Cú pháp hướng cắt Thực hiện phương thức execution(MethodSignature) Gọi phương thức call(MethodSignature) Thực hiện hàm khởi tạo execution(ConstructorSignature) Gọi hàm khởi tạo 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 () c.
Mã hành vi (advice) Mã hành vi [13] là mã được thực hiện tại một điểm nối mà được chọn bởi hướng cắt. Hay nói cách khác, nếu có hướng cắt là khai báo tên phương thức, thì mã hành 14 vi là phần thân của phương thức đó. Hướng cắt và mã hành vi sẽ hình thành nên các luật đan kết các quan hệ đan xen. Mã hành vi được chia thành 3 loại: Before: được thực hiện trước điểm nối.
After: được thực hiện sau điểm nối. Around: bao quanh sự thực hiện điểm nối, mã hành vi 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,. Khía cạnh (khía cạnh) Khía cạnh là phần tử trung tâm của aspectJ, giống như lớp trong Java. Khía cạnh chứa mã thể hiện các luật đan kết cho các concern [13].
Điểm nối, hướng cắt, mã hành vi được kết hợp trong khía cạnh. Tuy có gần giống các đặc điểm của lớp 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… nhưng, khía cạnh có một số khác biệt cơ bản sau: Khía cạnh không thể khởi tạo trực tiếp. Khía cạnh không thể kế thừa từ một khía cạnh cụ thể (không phải trừu tượng). Khía cạnh 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. Thực thi cắt ngang (crosscutting) Thực thi cắt ngang trong AspectJ, là quá trình biên dịch thực thi các quy tắc đan các mô đun cắt ngang vào mô đun chính [13].
