SINH CA KIỂM THỬ CHO CÁC HỆ THỐNG PHẢN ỨNG SỬ DỤNG CÔNG CỤ KIỂM CHỨNG MÔ HÌNH NUSMV

Abstract

Kiểm thử phần mềm là một trong những hoạt động đóng vai trò quan trọng nhằm nâng cao chất lượng phần mềm, đặc biệt các hệ thống phản ứng. Trong các kỹ thuật kiểm thử, kiểm chứng mô hình là một kỹ thuật hữu hiệu nhằm tìm lỗi trên mô hình đó. Hiện nay, có nhiều nghiên cứu về các kỹ thuật và công cụ kiểm chứng mô hình. Trong bài báo này, chúng tôi nghiên cứu việc ứng dụng công cụ kiểm chứng mô hình NuSMV để tạo các ca kiểm thử cho các hệ thống phản ứng. NuSMV đưa ra các phản ví dụ, thông thường các phản ví dụ này có ý nghĩa là hướng dẫn, phân tích, tìm kiếm nguồn gốc nguyên nhân gây ra lỗi. Đối với các hệ thống phản ứng, các phản ví dụ được xem là các ca kiểm thử nhằm phát hiện lỗi. Chúng tôi dùng ngôn ngữ SMV để mô hình hóa yêu cầu và các điều kiện bao phủ, và sử dụng logic thời gian LTL hoặc CLT để định nghĩa các thuộc tính bẫy. Từ các mô hình SMV và các thuộc tính bẫy, công cụ kiểm chứng mô hình NuSMV được sử dụng để sinh ra ca kiểm thử. Giải pháp được thử nghiệm cho một hệ thống phản ứng thực tế.