| dc.description.abstract |
Đề tài này tập trung vào việc nghiên cứu các đặc tính, mô hình hóa các hệ thời
gian thực xác suất và khả năng áp dụng trong việc kiểm chứng mô hình nhằm kiểm
chứng tự động các thuộc tính của hệ thời gian thực xác suất bằng công cụ. Phạm vi
nghiên cứu của đề tài bao gồm: (1) nghiên cứu các tính chất Markov của các hệ
thống, các loại chuỗi Markov và các tính chất của nó; (2) các hệ tự động thời gian
thực xác suất và các phương pháp kiểm chứng tự động tính chất của hệ thời gian
thực xác suất; (3) nghiên cứ công cụ kiểm chứng mô hình PRISM và khả năng áp
dụng trong việc kiểm chứng các tính chất của hệ thời gian thực xác suất, (4) Áp
dụng nghiên cứu trong việc mô hình hóa giao thức Alternative Bit Protocol bằng hệ
thời gian thực xác suất và thực hiện cài đặt trên công cụ PRISM, thực hiện kiểm
chứng tự động các tính chất của hệ thống bằng khả năng kiểm chứng của PRISM. |
vi |