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.

Principio

Traducir el sistema a un modelo de estados finito o simbólico, expresar la propiedad deseada en una lógica de especificación (p. ej. LTL, CTL) y realizar una búsqueda exhaustiva (explícita, simbólica, acotada o reducida por orden parcial) de los estados alcanzables para comprobar la propiedad; los contraejemplos son trazas de ejecución concretas que violan la propiedad.

Demostración

Verificar una propiedad de seguridad LTL en un sistema concurrente de estados finitos usando model checking simbólico con BDDs o bounded model checking basado en SAT: si la propiedad falla, la herramienta devuelve una traza finita que muestra la secuencia de transiciones que conduce a la violación, útil para depuración.

Aplicación incorrecta

Aplicar model checking ingenuamente a sistemas de estados infinitos sin abstracción, asumir que bounded model checking prueba propiedades no acotadas, o interpretar erróneamente contraejemplos producidos bajo abstracciones (contraejemplos espurios) como errores reales.

Consecuencia

Model checking proporciona detección automática de errores guiada por contraejemplos y, cuando es factible, garantías de corrección para el modelo explorado; exige formalizar con precisión el comportamiento y los requisitos del sistema pero se enfrenta al problema de explosión del espacio de estados que limita la escalabilidad.

Inversión

En lugar de exploración exhaustiva de estados, puede emplearse verificación deductiva o demostración automática que razonan simbólicamente sobre clases de comportamientos; la inversión intercambia automatización y contraejemplos concretos por generalidad y obligaciones de prueba.

Límite

Más adecuado para sistemas finitos o finitamente representables, o para sistemas susceptibles de abstracción correcta; diferentes lógicas y tipos de modelos (temporales, probabilísticos, híbridos) requieren algoritmos extendidos. Model checking comprueba la corrección del modelo respecto a una especificación, no la implementación real ni las suposiciones del entorno salvo que estén modeladas.

Tensión semántica

Existe tensión entre model checking de estado explícito, métodos simbólicos (BDD, SAT/SMT) y enfoques de abstracción/ refinamiento: las decisiones afectan la escalabilidad, la interpretabilidad de contraejemplos y si los resultados son exhaustivos o acotados. También hay un compromiso entre búsqueda totalmente automática y técnicas de prueba interactivas.

Síntesis

Model checking es un análisis automatizado y exhaustivo de un modelo formal frente a especificaciones temporales o lógicas que proporciona contraejemplos concretos para depuración y, cuando procede, garantías de corrección; su eficacia depende de la representación, la abstracción y las técnicas de búsqueda que mitiguen la explosión del espacio de estados.