Luận Văn Thạc Sĩ Kiểm Chứng Các Tính Chất Thời Gian Thực Cho Hệ Thống Đồng Thời Bằng RT-SPIN

Kiểm Chứng Các Tính Chất Thời Gian Thực Cho Hệ Thống Đồng Thời Bằng RT-SPIN​

Tìm hiểu cơ sở lý thuyết cho kiểm chứng mô hình, một công nghệ tự động trong đó mô hình với tập trạng thái hữu hạn của hệ thống và một tính chất logical, hệ thống sẽ kiểm tra xem tính chất đó. Spin một công cụ kiểm chứng mô hình. Spin là công cụ nhằm phân tích tính logic của hệ thống đồng thời, các giao thức giao tiếp dữ liệu. Hệ thống được mô hình hóa bởi ngôn ngữ Promela, trình bày các hệ thống thời gian thực. Nghiên cứu atomat thời gian mô hình hóa các hành vi hệ thống thời gian thực. Cung cấp các định nghĩa, đồ thị chuyển trạng thái với ràng buộc thời gian sử dùng nhiều đồng hồ giá trị thực. Otomat thời gian chấp nhận chấp nhận từ ký tự và thời gan – trình tự vô hạn với giá trị thời gian liên kết với ký tự vào; xem xét các tính chất đóng với Otomat xác định và không xác đinh; xét ứng dụng của lý thuyết nhằm kiểm thử các yêu cầu của hệ thống với các trạng thái hữu hạn. Giới thiệu mở rộng thời gian thực với công cụ spin và Promela, có hai thành công bao gồm RtSpin (Real-time Spin) và DtSpin (Discrete time Spin) nhằm mở rộng Spin với thời gian. Trong đó RtSpin dựa trên mô hình thời gian liên tục, DtSpin dựa trên mô hình thời gian rời rạc. Đưa ra một số thực nghiệm với công cụ RtSpin và DtSpin.

• Luận văn thạc sĩ Công nghệ thông tin
• Chuyên ngành Công nghệ phần mềm
• Người hướng dẫn khoa học: TS. Nguyễn Trường Thắng
• Tác giả: Nguyễn Tài Tuấn
• Số trang: 73
• Kiểu file: PDF
• Ngôn ngữ: Tiếng Việt
• Trường Đại học Công nghệ. Đại học Quốc gia Hà Nội 2013

Link Download
http://dlib.vnu.edu.vn/iii/cpro/DigitalItemViewPage.external?lang=vie&sp=1012476
https://drive.google.com/drive/folders/1yLBzZ1rSQoNjmWeJTM6cEZ3WGQHg04L1