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

Giới thiệu nội dung

Đặc Tả Và Kiểm Chứng Các Phần Mềm Tương Tranh

Tác giả: Lê Hồng Phong

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

Nội dung tài liệu:

Khóa luận tập trung vào việc đặc tả và kiểm chứng các phần mềm tương tranh, đặc biệt là các hệ thống nhúng và điều khiển, nơi mà lỗi phần mềm có thể gây ra hậu quả nghiêm trọng. Đề tài áp dụng phương pháp hình thức, sử dụng máy hữu hạn trạng thái (Finite State Process – FSP) để mô tả thiết kế và mã nguồn của phần mềm. Công cụ phân tích máy hữu hạn trạng thái (LTSA) được sử dụng để kiểm chứng tính đúng đắn của thiết kế và mã nguồn. Nghiên cứu thực nghiệm tập trung vào việc kiểm chứng một applet Java bằng cách đặc tả thiết kế bằng FSP và chuyển mã nguồn Java sang FSP để kiểm chứng sự tương thích.

Mục lục chi tiết:

  • Chương 1: Giới thiệu
  • Chương 2: Các khái niệm cơ bản
  • Chương 3: Kiểm chứng thiết kế
  • Chương 4: Kiểm chứng cài đặt
  • Chương 5: Kết luận