El despliegue cada vez mayor de Sistemas Ciberfísicos (CPS) autónomos (por ejemplo, coches autónomos, UAV) agrava la necesidad de métodos de verificación formal eficientes. En este contexto, el principal obstáculo a superar es el enorme número de escenarios que deben evaluarse. La Verificación de Modelos Estadística (SMC) es un enfoque basado en simulación que promete superar tal obstáculo utilizando métodos estadísticos para muestrear el conjunto de escenarios. Existen muchas herramientas de SMC, y han sido revisadas en varios trabajos. En este artículo, haremos un resumen de las herramientas de SMC basadas en Monte Carlo para proporcionar criterios de selección basados en Indicadores Clave de Rendimiento (KPI) para la actividad de verificación (por ejemplo, minimizar el tiempo o costo de verificación), así como en las características del entorno, el tipo de modelo de sistema, el lenguaje utilizado para definir los requisitos a verificar, el enfoque de inferencia estadística utilizado y el algoritmo que lo implementa. Además, identificaremos los desafíos de investigación abiertos en el campo de las herramientas de SMC.