Kiểm thử mô hình là một kỹ thuật cho phép tìm kiếm triệt để các lỗi có thể trong không gian trạng thái của mô hình. Kiểm thử là một phương pháp phổ biến để nâng cao chất lượng của một sản phẩm phần mềm được tạo ra bằng cách kiểm tra lỗi trong việc thực hiện chương trình theo một số chuẩn được gọi là chuẩn bao phủ. Kiểm thử là quá trình rất tốn kém nếu nó không được hỗ trợ bởi một phương pháp (và công cụ) để tạo ra các bộ test. Và phương pháp kiểm chứng  mô hình sẽ hỗ trợ tạo ra các test case cho kiểm thử đơn vị theo chuẩn bao phủ. Phương pháp này dựa trên việc tự động phát sinh mô hình từ mã nguồn với việc truyền vào các breakpoint. Các test case thu được như là một phản ví dụ của công thức LTL (Linear Temporal Logic) sẽ tự động được tạo ra dựa trên các chuẩn bao phủ đã được lựa chọn.

Tải file Một phương pháp hiệu quả sinh dữ liệu kiểm thử mức đơn vị tại đây