Á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