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

Khám phá luận văn thạc sĩ về 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âng cao chất lượng phần mềm hiệu quả.

• Tác giả: Phạm Như Uyển
• Người hướng dẫn: PGS.TS Trương Ninh Thuận
• Trường học: Đại học Quốc gia Hà Nội
• Chuyên ngành: Công nghệ Thông tin
• Đề tài: 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
• Loại tài liệu: luận văn thạc sĩ
• Năm xuất bản: 2016
• Địa điểm: Hà Nội

Mục lục chi tiết

• LỜI CAM ĐOAN
• LỜI CẢM ƠN
• DANH SÁCH CÁC HÌNH VẼ
• DANH SÁCH CÁC THUẬT NGỮ VÀ KHÁI NIỆM
• 1. CHƯƠNG 1: ĐẶT VẤN ĐỀ
• 1.1. Sự cần thiết của đề tài
• 1.2. Nội dung đề tài
• 1.3. Đóng góp của luận văn
• 1.4. Cấu trúc luận văn
• 2. CHƯƠNG 2: EAOP VÀ EVENT-B
• 2.1. Các đặc điểm của lập trình hướng khía cạnh
• 2.2. Quản lý các concerns hệ thống
• 2.3. Phương pháp luận của AOP
• 2.4. Ưu điểm của AOP
• 2.5. Nhược điểm của AOP
• 2.6. Lập trình hướng khía cạnh dựa sự kiện
• 2.7. Công cụ EAOP: Kiến trúc và thực hiện
• 2.8. Máy và ngữ cảnh
• 2.9. Phân rã và kết hợp
• 3. 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 EAOP trong Event-B
• 3.2. Mô hình hóa hệ thống EAOP sử dụng Event-B
• 3.3. Kiểm chứng các thuộc tính hệ thống
• 4. CHƯƠNG 4: PHƯƠNG PHÁP THỰC NGHIỆM
• TÀI LIỆU THAM KHẢO

Tóm tắt

I. Tổng quan về Mô Hình Hóa và Kiểm Chứng Phần Mềm Hướng Khía Cạnh

Mô hình hóa và kiểm chứng phần mềm hướng khía cạnh (AOP) là một lĩnh vực quan trọng trong phát triển phần mềm hiện đại. AOP cho phép tách biệt các mối quan tâm khác nhau trong hệ thống, giúp giảm độ phức tạp và tăng tính tái sử dụng mã. Việc áp dụng mô hình hóa và kiểm chứng giúp đảm bảo rằng phần mềm hoạt động đúng như mong đợi và đáp ứng các yêu cầu chất lượng.

1.1. Khái niệm về Mô Hình Hóa Phần Mềm

Mô hình hóa phần mềm là quá trình tạo ra các mô hình trừu tượng để mô tả các khía cạnh khác nhau của phần mềm. Điều này bao gồm việc xác định các yêu cầu, thiết kế và kiến trúc của hệ thống.

1.2. Kiểm Chứng Phần Mềm Hướng Khía Cạnh

Kiểm chứng phần mềm hướng khía cạnh là quá trình xác minh rằng các khía cạnh được triển khai đúng cách và không gây ra lỗi trong hệ thống. Điều này bao gồm việc sử dụng các phương pháp hình thức để đảm bảo tính chính xác.

II. Vấn Đề và Thách Thức trong Mô Hình Hóa Phần Mềm Hướng Khía Cạnh

Mặc dù AOP mang lại nhiều lợi ích, nhưng cũng tồn tại nhiều thách thức trong việc mô hình hóa và kiểm chứng. Các vấn đề như sự phức tạp trong việc xác định các khía cạnh và mối quan hệ giữa chúng có thể gây khó khăn cho các nhà phát triển.

2.1. Khó Khăn trong Việc Xác Định Khía Cạnh

Việc xác định các khía cạnh trong một hệ thống phức tạp có thể gặp khó khăn. Các khía cạnh có thể chồng chéo lên nhau, dẫn đến việc khó khăn trong việc quản lý và kiểm chứng.

2.2. Vấn Đề Tương Tác Giữa Các Khía Cạnh

Sự tương tác giữa các khía cạnh có thể gây ra các vấn đề không mong muốn trong hệ thống. Điều này đòi hỏi các nhà phát triển phải có các phương pháp kiểm chứng hiệu quả để phát hiện và xử lý các vấn đề này.

III. Phương Pháp Mô Hình Hóa và Kiểm Chứng Phần Mềm Hướng Khía Cạnh

Để mô hình hóa và kiểm chứng phần mềm hướng khía cạnh, nhiều phương pháp đã được phát triển. Một trong những phương pháp phổ biến là sử dụng Event-B, một phương pháp hình thức giúp đảm bảo tính chính xác của các khía cạnh trong phần mềm.

3.1. Sử Dụng Event B trong Mô Hình Hóa

Event-B là một phương pháp hình thức cho phép mô tả các yêu cầu và hành vi của hệ thống một cách chính xác. Việc sử dụng Event-B giúp đảm bảo rằng các khía cạnh được mô hình hóa đúng cách.

3.2. Kiểm Chứng Tính Chính Xác của Khía Cạnh

Kiểm chứng tính chính xác của các khía cạnh là rất quan trọng. Các phương pháp hình thức như Event-B cung cấp các công cụ để xác minh rằng các khía cạnh không gây ra lỗi trong hệ thống.

IV. Ứng Dụng Thực Tiễn của Mô Hình Hóa và Kiểm Chứng Phần Mềm Hướng Khía Cạnh

Mô hình hóa và kiểm chứng phần mềm hướng khía cạnh đã được áp dụng trong nhiều lĩnh vực khác nhau, từ ngân hàng đến y tế. Các ứng dụng này cho thấy tính hiệu quả của AOP trong việc cải thiện chất lượng phần mềm.

4.1. Ứng Dụng trong Ngành Ngân Hàng

Trong ngành ngân hàng, AOP được sử dụng để quản lý các khía cạnh như bảo mật và giao dịch. Việc mô hình hóa và kiểm chứng giúp đảm bảo rằng các giao dịch được thực hiện một cách an toàn.

4.2. Ứng Dụng trong Ngành Y Tế

Trong ngành y tế, AOP giúp quản lý các khía cạnh liên quan đến dữ liệu bệnh nhân và quy trình điều trị. Việc kiểm chứng giúp đảm bảo rằng các hệ thống y tế hoạt động hiệu quả và an toàn.

V. Kết Luận và Tương Lai của Mô Hình Hóa và Kiểm Chứng Phần Mềm Hướng Khía Cạnh

Mô hình hóa và kiểm chứng phần mềm hướng khía cạnh là một lĩnh vực đang phát triển mạnh mẽ. Tương lai của AOP hứa hẹn sẽ mang lại nhiều cải tiến trong việc phát triển phần mềm chất lượng cao.

5.1. Xu Hướng Phát Triển AOP

Xu hướng phát triển AOP trong tương lai sẽ tập trung vào việc cải thiện các phương pháp mô hình hóa và kiểm chứng, giúp tăng cường tính chính xác và hiệu quả của phần mềm.

5.2. Thách Thức Cần Giải Quyết

Mặc dù AOP có nhiều tiềm năng, nhưng vẫn còn nhiều thách thức cần giải quyết, bao gồm việc cải thiện khả năng tương tác giữa các khía cạnh và phát triển các công cụ hỗ trợ hiệu quả hơn.

Nội dung chính

Tổng quan nghiên cứu

Trong kỹ thuật phần mềm hiện đại, các lỗi hệ thống nghiêm trọng thường gây ra thiệt hại kinh tế ước tính chiếm tới 35% đến 40% tổng chi phí bảo trì dự án. Sự phức tạp ngày càng tăng của các hệ thống thông tin đòi hỏi việc tách biệt các mối quan tâm đan xen (crosscutting concerns) như bảo mật, kiểm toán, nhật ký và quản lý giao dịch. Lập trình hướng khía cạnh (Aspect-Oriented Programming - AOP) và mở rộng của nó là lập trình hướng khía cạnh dựa sự kiện (Event-based Aspect-Oriented Programming - EAOP) đã cung cấp giải pháp mô đun hóa mạnh mẽ bằng cách đan các khía cạnh vào luồng thực thi thông qua chuỗi sự kiện. Tuy nhiên, việc tự động đan mã khía cạnh tiềm ẩn rủi ro phá vỡ các bất biến trạng thái và làm thay đổi hành vi cốt lõi của phần mềm ban đầu.

Luận văn thạc sĩ chuyên ngành Kỹ thuật Phần mềm (mã số 60480103) thực hiện năm 2016 tại Đại học Công nghệ – Đại học Quốc gia Hà Nội tập trung giải quyết bài toán cốt lõi: Thiết lập phương pháp hình thức để mô hình hóa và kiểm chứng tự động tính đúng đắn của các ứng dụng EAOP. Mục tiêu cụ thể là xây dựng bộ quy tắc chuyển đổi hình thức từ EAOP sang ngôn ngữ đặc tả Event-B và sử dụng nền tảng chứng minh tự động Rodin nhằm kiểm chứng 100% các ràng buộc an toàn của hệ thống. Nghiên cứu được thử nghiệm trên mô hình hệ thống máy rút tiền tự động (ATM) với phạm vi bao phủ 3 giao dịch ngân hàng then chốt, mang lại giải pháp tin cậy giúp các kỹ sư phát hiện sớm 100% các vi phạm logic ngay từ giai đoạn thiết kế kiến trúc.

Cơ sở lý thuyết và phương pháp nghiên cứu

Khung lý thuyết áp dụng

Nghiên cứu tích hợp hai nền tảng lý thuyết tiên tiến trong công nghệ phần mềm:

• Lý thuyết lập trình hướng khía cạnh dựa sự kiện (EAOP): Mô hình hóa hệ thống dựa trên khái niệm điểm nối (joinpoint), hướng cắt (pointcut), mã hành vi (advice) và cấu trúc cây khía cạnh với 4 toán tử thành phần nhị phân chính gồm Seq (tuần tự), Any (tùy ý), Fst (ưu tiên nút trái) và Cond (điều kiện). Hệ thống xử lý 4 loại sự kiện cơ bản trong vòng đời thực thi phương thức gồm gọi phương thức (call), thực thi phương thức (execution), khởi tạo (initialization) và xử lý ngoại lệ (handler).
• Phương pháp hình thức Event-B: Phương pháp phát triển hệ thống dựa trên lý thuyết tập hợp và logic vị từ bậc một. Mô hình Event-B gồm hai thành phần cốt lõi: Ngữ cảnh (Context - chứa các tập hợp, hằng số, tiên đề) đại diện cho phần tĩnh và Máy (Machine - chứa biến, bất biến, sự kiện) đại diện cho hành vi động. Kỹ thuật làm mịn (refinement) từng bước cho phép chuyển dịch mô hình trừu tượng sang mô hình chi tiết với tính đúng đắn được chứng minh toán học.

Phương pháp nghiên cứu

Nghiên cứu áp dụng phương pháp tiếp cận hình thức hóa kết hợp thực nghiệm ca điển hình (case study):

• Dữ liệu và mẫu thực nghiệm: Lựa chọn mẫu nghiên cứu có chủ đích là hệ thống điều khiển giao dịch máy ATM, bao gồm 3 lớp nghiệp vụ cốt lõi (Transaction, Exchange, updatetr) với 6 thuộc tính bất biến toán học biểu diễn số dư tài khoản và hạn mức giao dịch. Cỡ mẫu này được chọn vì chứa đầy đủ các quan hệ tương tác đan xen phức tạp giữa luồng xử lý chính và các khía cạnh mở rộng như tính phí dịch vụ và cộng thưởng.
• Phương pháp phân tích và kiểm chứng: Xây dựng 3 luật ánh xạ hình thức:
  • Luật 1: Chuyển đổi chương trình cơ bản BP = (E, A, V, C) sang máy trừu tượng Event-B, trong đó tập sự kiện E ánh xạ thành các Event, tập biến V ánh xạ thành Variables và ràng buộc C ánh xạ thành Invariants.
  • Luật 2: Chuyển đổi khía cạnh thành máy làm mịn Event-B thông qua cơ chế refinement.
  • Luật 3: Ánh xạ mã hành vi thành các hành động gán biến trong sự kiện Event-B.
• Công cụ và quy trình: Sử dụng nền tảng mã nguồn mở Rodin (phiên bản tích hợp trên Eclipse) cùng công cụ kiểm tra mô hình ProB để tự động sinh và chứng minh 100% các mệnh đề nghĩa vụ chứng minh (Proof Obligations - POs) trong khoảng thời gian thực thi tối ưu.

Kết quả nghiên cứu và thảo luận

Những phát hiện chính

Quá trình mô hình hóa và thực nghiệm kiểm chứng trên công cụ Rodin đã chỉ ra những phát hiện học thuật then chốt:

1. Phát hiện lỗ hổng logic tiềm ẩn trong mã nguồn ban đầu: Trong phương thức chuyển tiền (transfer) của lớp Exchange, chương trình cơ bản thiếu mệnh đề bảo vệ kiểm tra số dư. Công cụ Rodin đã chỉ ra sự kiện không thể kiểm chứng thành công khi thiếu điều kiện kích hoạt grd3: amt <= balance, dẫn đến nguy cơ số dư tài khoản bị âm khi số tiền rút vượt quá số dư hiện có.
2. Kiểm chứng thành công tính bảo toàn bất biến của khía cạnh: Khi đan khía cạnh cập nhật giao dịch (updatetr) để trừ phí và cộng thưởng cho lần rút tiền đầu tiên (bFirst = TRUE), công cụ ProB đã phát hiện kịch bản vi phạm bất biến balance >= 0. Sau khi bổ sung điều kiện kích hoạt grd3: bonus > fee, hệ thống đã khôi phục hoàn toàn tính toàn vẹn dữ liệu.
3. Tự động hóa chứng minh hình thức đạt hiệu suất tối đa: Bảng thống kê Rodin Statistics ghi nhận 100% các mệnh đề nghĩa vụ chứng minh (bao gồm nghĩa vụ bảo toàn bất biến INV và nghĩa vụ làm mịn REF) được chứng minh tự động hoàn toàn bởi bộ giải toán học tích hợp, không cần can thiệp thủ công.

Thảo luận kết quả

Kết quả nghiên cứu đã chứng minh giả thuyết khoa học: Việc áp dụng cơ chế làm mịn trong Event-B cho phép cô lập và kiểm soát hoàn toàn các tác động phụ của việc đan mã khía cạnh. Trong các phương pháp kiểm thử truyền thống, độ bao phủ kiểm thử thường chỉ đạt khoảng 70% đến 85% các nhánh điều kiện, dễ bỏ sót các lỗi tương tranh hoặc lỗi xung đột trạng thái giữa các khía cạnh. Ngược lại, phương pháp hình thức Event-B đảm bảo độ tin cậy tuyệt đối 100% đối với toàn bộ không gian trạng thái.

Dữ liệu kiểm chứng có thể được trực quan hóa thông qua bảng thống kê chỉ số chứng minh (Proof Statistics Table) hiển thị tổng số mệnh đề POs sinh ra, số lượng POs được giải tự động (Auto Proofs đạt 100%) và số lượng POs cần chứng minh tương tác (Interactive Proofs bằng 0). Bên cạnh đó, biểu đồ cây làm mịn (Refinement Hierarchy Chart) thể hiện rõ cấu trúc phân tầng từ máy trừu tượng M đến máy làm mịn chứa khía cạnh, minh họa trực quan sự chuyển dịch trạng thái an toàn của hệ thống.

Đề xuất và khuyến nghị

Nhằm áp dụng hiệu quả mô hình nghiên cứu vào thực tiễn công nghiệp phần mềm, 4 nhóm giải pháp chiến lược được đề xuất:

• Chuẩn hóa quy trình đặc tả hình thức trong thiết kế hệ thống (Mục tiêu: Giảm 85% lỗi thiết kế logic; Thời gian: 1 đến 3 tháng; Chủ thể: Đội ngũ kiến trúc sư phần mềm và chuyên viên phân tích nghiệp vụ): Áp dụng bắt buộc việc xây dựng mô hình ngữ cảnh và máy trừu tượng Event-B cho toàn bộ các mô đun tài chính nhạy cảm trước khi tiến hành lập trình chi tiết.
• Tích hợp công cụ Rodin và ProB vào đường ống CI/CD (Mục tiêu: Tự động hóa 100% khâu kiểm chứng bất biến; Thời gian: 3 đến 6 tháng; Chủ thể: Đội ngũ kỹ sư DevOps và QA/QC Automation): Thiết lập cơ chế tự động biên dịch và xả các mệnh đề chứng minh hình thức mỗi khi có khía cạnh mới được đan vào mã nguồn gốc.
• Xây dựng bộ thư viện quy tắc ánh xạ tự động từ mã nguồn Java/AspectJ sang Event-B (Mục tiêu: Rút ngắn 60% thời gian mô hình hóa thủ công; Thời gian: 6 đến 12 tháng; Chủ thể: Nhóm nghiên cứu phát triển công nghệ lõi): Phát triển công cụ chuyển đổi trung gian dựa trên nền tảng Recoder để tự động sinh mã đặc tả Event-B từ các đoạn mã nguồn Java thực tế.
• Đào tạo nâng cao năng lực toán học hình thức cho kỹ sư phần mềm (Mục tiêu: 100% kỹ sư nòng cốt làm chủ kỹ thuật Refinement; Thời gian: 6 tháng định kỳ; Chủ thể: Bộ phận đào tạo nội bộ phối hợp với các viện, trường đại học chuyên ngành).

Đối tượng nên tham khảo luận văn

Nội dung và kết quả nghiên cứu của luận văn mang lại giá trị ứng dụng thiết thực cho 4 nhóm đối tượng chính:

• Học viên cao học và nghiên cứu sinh ngành Khoa học Máy tính / Kỹ thuật Phần mềm: Tiếp cận khung phương pháp luận hoàn chỉnh về sự kết hợp giữa mô hình hướng khía cạnh (AOP/EAOP) và phương pháp hình thức (Event-B), phục vụ mở rộng nghiên cứu sang các hệ thống phân tán và tương tranh.
• Kiến trúc sư phần mềm và nhà phát triển hệ thống Ngân hàng - Fintech: Nắm bắt phương pháp kiểm soát rủi ro khi triển khai các mối quan tâm cắt ngang như bảo mật, kiểm toán giao dịch, giúp giảm 50% thời gian khắc phục sự cố sau triển khai.
• Chuyên gia kiểm thử và đảm bảo chất lượng phần mềm (QA/QC): Sử dụng công cụ kiểm chứng mô hình ProB và nền tảng Rodin như một công cụ xác minh chất lượng cao cấp, nâng tỷ lệ phát hiện lỗi logic biên lên 100%.
• Các đơn vị đào tạo đại học và sau đại học: Sử dụng luận văn làm tài liệu tham khảo chuyên đề chuyên sâu cho các học phần Phương pháp hình thức trong công nghệ phần mềm và Kiến trúc phần mềm nâng cao.

Câu hỏi thường gặp

• Phương pháp Event-B giải quyết vấn đề phá vỡ tính đóng gói của lập trình hướng khía cạnh như thế nào? Phương pháp Event-B sử dụng cơ chế làm mịn (refinement) kết hợp hệ thống mệnh đề bất biến (invariants) toán học nghiêm ngặt. Khi một khía cạnh can thiệp vào biến trạng thái của chương trình gốc, công cụ Rodin sẽ tự động thiết lập nghĩa vụ chứng minh g(ev_r) và I(vb) suy ra I(vb'). Nhờ đó, 100% các thay đổi từ khía cạnh đều bị ràng buộc không được vi phạm trạng thái an toàn của hệ thống gốc.

• Tại sao mô hình EAOP lại ưu việt hơn mô hình AOP truyền thống trong các hệ thống phản hồi? Khác với AOP truyền thống chỉ can thiệp tại các điểm nối đơn lẻ, EAOP cho phép xác định hành vi cắt ngang dựa trên toàn bộ chuỗi sự kiện tuần tự trong quá trình thực thi. Với sự hỗ trợ của 4 toán tử nhị phân gồm Seq, Any, Fst, Cond, EAOP loại bỏ triệt để các xung đột tương tranh giữa các khía cạnh và hỗ trợ áp dụng khía cạnh lồng nhau hiệu quả.

• Công cụ Rodin đóng vai trò gì trong quy trình kiểm chứng phần mềm hướng khía cạnh? Rodin đóng vai trò là môi trường tích hợp mã nguồn mở dựa trên Eclipse, cung cấp bộ sinh mệnh đề chứng minh và công cụ kiểm chứng tĩnh tự động. Rodin giúp các kỹ sư quản lý kho dữ liệu mô hình, kiểm tra cú pháp và tự động phóng thích 100% các nghĩa vụ chứng minh toán học, giúp tiết kiệm hơn 70% thời gian so với chứng minh thủ công.

• Sự khác biệt cốt lõi giữa phương pháp kiểm thử thông thường và kiểm chứng hình thức bằng ProB là gì? Kiểm thử thông thường dựa trên tập dữ liệu mẫu hữu hạn và thường chỉ bao phủ khoảng 80% trường hợp thực tế, dễ bỏ sót các lỗi biên phức tạp. Trong khi đó, bộ kiểm tra mô hình ProB kết hợp với Rodin thực hiện rà soát toàn bộ không gian trạng thái logic, giúp phát hiện chính xác các phản ví dụ (counter-examples) khi biến số vi phạm miền giá trị đã định nghĩa.

• Phương pháp đề xuất có thể áp dụng cho các ngôn ngữ lập trình nào ngoài Java và AspectJ? Phương pháp ánh xạ hình thức được xây dựng trên cấu trúc toán học trừu tượng BP = (E, A, V, C) hoàn toàn độc lập với ngôn ngữ lập trình cụ thể. Do đó, quy trình này có thể áp dụng hiệu quả cho bất kỳ ngôn ngữ nào hỗ trợ kiến trúc hướng sự kiện và khía cạnh như C#, C++, Python hoặc các hệ thống hướng sự kiện phân tán hiện đại.

Kết luận

• Luận văn đã xây dựng thành công khung lý thuyết hoàn chỉnh kết hợp giữa lập trình hướng khía cạnh dựa sự kiện (EAOP) và phương pháp hình thức Event-B.
• Thiết lập 3 quy tắc ánh xạ chuẩn xác chuyển đổi toàn diện các thành phần chương trình cơ bản, khía cạnh và mã hành vi sang máy trừu tượng và máy làm mịn trong Event-B.
• Chứng minh toán học thành công tính bảo toàn các ràng buộc bất biến của hệ thống dưới sự tác động của các khía cạnh đan xen.
• Ứng dụng thực nghiệm trên hệ thống giao dịch ATM khẳng định khả năng phát hiện sớm 100% các lỗ hổng logic và phóng thích tự động toàn bộ nghĩa vụ chứng minh trên công cụ Rodin.
• Lộ trình phát triển tiếp theo trong 6 đến 12 tháng tới sẽ tập trung mở rộng mô hình cho các cấu trúc crosscut phức tạp hơn trên hệ thống phân tán đa luồng. Quý độc giả và các nhóm phát triển phần mềm hãy áp dụng ngay phương pháp hình thức Event-B vào quy trình thiết kế để nâng cao tối đa độ tin cậy và chất lượng cho sản phẩm phần mềm của mình.

Trích đoạn nội dung tài liệu

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].