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: 142 trang
Dung lượng: Đang cập nhật

Giới thiệu nội dung

Kiểm Chứng Các Thành Phần Java Tương Tranh

Tác giả: Trịnh Thanh Bình

Lĩnh vực: Công nghệ Thông tin

Nội dung tài liệu:

Luận án này tập trung vào việc đề xuất và nghiên cứu các phương pháp kiểm chứng chương trình tương tranh ở cả giai đoạn thiết kế và cài đặt mã nguồn. Ở mức thiết kế, luận án áp dụng phương pháp hình thức Event-B để kiểm chứng các ràng buộc thứ tự giữa các tiến trình tương tranh, đảm bảo tính nhất quán của đầu ra. Phương pháp này sử dụng mô hình trừu tượng và mô hình làm mịn để biểu diễn các sự kiện và tương tác giữa chúng, với kỹ thuật đồng bộ hóa semaphore. Tính đúng đắn được bảo đảm thông qua việc sinh và chứng minh tự động các mệnh đề cần chứng minh. Đồng thời, luận án còn đề xuất phương pháp kiểm chứng sự đồng thuận của hệ thống đa thành phần tương tranh, sử dụng máy trừu tượng và ngữ cảnh kết hợp với giao thức tương tác. Tại mức cài đặt mã nguồn, luận án sử dụng phương pháp lập trình hướng khía cạnh (Aspect-Oriented Programming – AOP) kết hợp với công cụ JPF (Java PathFinder) để kiểm chứng sự tuân thủ giữa thực thi và đặc tả.

Mục lục chi tiết:

  • Lời cam đoan
  • Lời cảm ơn
  • Từ viết tắt
  • Danh mục các hình vẽ
  • Danh mục các bảng biểu
  • Chương 1: Mở đầu
  • Chương 2: Kiến thức cơ sở
  • Chương 3: Ràng buộc thứ tự giữa các tiến trình tương tranh
  • Chương 4: Sự đồng thuận của hệ thống đa thành phần
  • Chương 5: Sự tuân thủ giữa thực thi và đặc tả giao thức tương tác
  • Chương 6: Ràng buộc thời gian giữa các thành phần trong chương trình tương tranh
  • Chương 7: Kết luận
  • Phụ lục A, B, C