Tóm tắt Luận án Áp dụng kiểm tra mô hình và phân tích khái niệm hình thức để phân loại và phát hiện mã độc

Một phương pháp đáng chú ý trong các nghiên cứu giải quyết vấn đề bùng nổ không gian trạng thái là phương pháp kiểm tra thành phần, phương pháp này được xây dựng dựa trên các kỷ thuật trừu tượng và phân rã.

Mục tiêu của cách tiếp cận này là để kiểm tra các mô hình con riêng lẻ và sau đó kiểm tra mô hình trừu tượng tổng hợp để kết luận rằng kết qua kiểm tra là chính xác. Để phân chia một mô hình thành các mô hình con, các kỹ thuật phân rã được sử dụng. Mỗi mô hình con có không gian trạng thái riêng và quá trình kiểm tra được bắt đầu bằng cách kiểm tra từng mô hình con. Các kỹ thuật trừu tượng hoá được áp dụng để giảm kích thước của từng mô hình con sau khi đã kiểm tra, từ đó giảm kích thước của mô hình trừu tượng tổng hợp được xây dựng bằng cách kết hợp các mô hình con trừu tượng này.