Xem trước tài liệu

Đang tải tài liệu...

Thông tin chi tiết tài liệu

Định dạng: PDF
Số trang: 54 trang
Dung lượng: Đang cập nhật

Giới thiệu nội dung

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

Tác giả: Phạm Như Uyển

Lĩnh vực: Công nghệ Thông tin, Chuyên ngành: Kỹ thuật Phần mềm

Luận văn này tập trung vào việc 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, đặc biệt là các hệ thống dựa trên sự kiện. Nghiên cứu đề xuất một phương pháp kết hợp lập trình hướng khía cạnh dựa trên sự kiện (EAOP) với phương pháp hình thức Event-B. Phương pháp này tận dụng sự tương đồng giữa cấu trúc sự kiện của Event-B và EAOP để chuyển đổi các thành phần ứng dụng EAOP sang mô hình Event-B. Thông qua công cụ Rodin, các thuộc tính của chương trình sẽ được kiểm chứng để đảm bảo tính đúng đắn và tính nhất quán sau khi áp dụng các khía cạnh. Nghiên cứu nhằm mục đích phát hiện sớm các vấn đề tiềm ẩn trong giai đoạn thiết kế và minh họa phương pháp bằng một chương trình cụ thể (máy ATM).

Mục lục chi tiết:

  • Mục lục
  • Danh sách các hình vẽ
  • Danh sách các thuật ngữ và khái niệm
  • Chương 1: Đặt vấn đề
    • Sự cần thiết của đề tài
    • Nội dung đề tài
    • Đóng góp của luận văn
    • Cấu trúc luận văn
  • Chương 2: EAOP và Event-B
    • Các đặc điểm của lập trình hướng khía cạnh
      • Điểm nối (join point)
      • Hướng cắt (pointcut)
      • Mã hành vi (advice)
      • Khía cạnh (khía cạnh)
      • Thực thi cắt ngang (crosscutting)
      • Đan mã khía cạnh
      • Quản lý các concerns hệ thống
    • Lập trình hướng khía cạnh dựa sự kiện
      • Công cụ EAOP: Kiến trúc và thực hiện
    • Event-B
      • Máy và ngữ cảnh
      • Sự kiện
      • Phân rã và kết hợp
      • Công cụ
  • 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
    • Trình bày EAOP trong Event-B
    • Mô hình hóa hệ thống EAOP sử dụng Event-B
    • Kiểm chứng các thuộc tính hệ thống
  • Chương 4: Phương pháp thực nghiệm
  • Kết luận
  • Tài liệu tham khảo
  • Phụ lục