Song song hóa kiểm tra mô hình dựa trên đường đi ngẫu nhiên

Tóm tắt

Phương pháp kiểm tra mô hình là một phương pháp hình thức được dùng rộng rãi trong thời gian gần đây để kiểm định tính đúng đắn của các hệ thống phần mềm và phần cứng. Các kỹ thuật dẫn hướng dùng heuristic đã được sử dụng trong một thời gian dài để dẫn hướng việc tìm kiếm vào trong các vùng có khả năng có sai sót. Một kỹ thuật khác là dùng đường đi ngẫu nhiên, nghĩa là chọn các trạng thái đi kiểm tra một cách ngẫu nhiên, để tránh việc dẫn hướng sai lầm. Kỹ thuật này là một kỹ thuật không phải vét cạn nên nó không (thực sự) cần bộ nhớ lớn và như vậy có thể tránh né sự bùng nổ tổ hợp trong bài toán kiểm tra mô hình. Để nâng cao hiệu quả của hướng nghiên cứu này và tận dụng sức mạnh của các hệ thống song song/đa nhân gần đây, việc áp dụng giải pháp song song hóa là rất cần thiết. Nghiên cứu này đề xuất một phương pháp song song hóa giải thuật đường đi ngẫu nhiên để nâng cao hiệu suất kiểm tra. Ngoài ra, nghiên cứu này cũng quan tâm đến việc tăng cường tính đầy đủ của giải thuật kiểu không vét cạn như thế này. Thực nghiệm cho thấy, giải pháp đề ra rất hiệu quả.