Model Checking

Una técnica automática de verificación que explora exhaustivamente el espacio de estados de un modelo formal de sistema (habitualmente un sistema de transición de estados finitos) para determinar si el modelo satisface una especificación expresada en una lógica temporal o modal, proporcionando trazas contraejemplo cuando la propiedad se viola.

La comprobación de modelos es el proceso de verificación algorítmica que explora el espacio de estados de un modelo formal para determinar si satisface una especificación dada, a menudo expresada en lógicas temporales o modales.