Refinamiento de la abstracción guiado por contraejemplos

Para razonar sobre la corrección de un programa, en particular aquellos que involucran el concepto de tiempo para la concurrencia , se utilizan modelos de transición de estados. En particular, los modelos de estados finitos pueden utilizarse junto con la lógica temporal en la verificación automática. ^{[ 6 ]} El concepto de abstracción se fundamenta, por lo tanto, en un mapeo entre dos estructuras de Kripke . Específicamente, los programas pueden describirse con autómatas de flujo de control (CFA). ^{[ 7 ]}

Defina una estructura de Kripke.${\displaystyle M}$como${\displaystyle \langle S,s_{0},R,L\rangle }$, dónde

• ${\displaystyle S}$es un conjunto finito de estados,
• ${\displaystyle s_{0}}$es un estado inicial en${\displaystyle S}$,
• ${\displaystyle R}$es una relación de transición total, y
• ${\displaystyle L}$es una función que etiqueta cada estado con un conjunto de nombres proposicionales que se cumplen en él.

Una abstracción de${\displaystyle M}$se define por${\displaystyle \langle S_{\alpha },s_{0}^{\alpha },R_{\alpha },L_{\alpha }\rangle }$dónde${\displaystyle \alpha }$es una asignación de abstracción que asigna cada estado en${\displaystyle S}$a un estado en${\displaystyle S_{\alpha }}$. ^{[ 5 ]}

Para preservar las propiedades críticas del modelo, el mapeo de abstracción asigna el estado inicial en el modelo original.${\displaystyle s_{0}}$a su contraparte${\displaystyle s_{0}^{\alpha }}$en el modelo abstracto. El mapeo de abstracción también garantiza que se conserven las relaciones de transición entre dos estados.

En cada iteración, se realiza una verificación del modelo abstracto. La verificación de modelos acotada, por ejemplo, genera una fórmula proposicional que luego se comprueba para determinar su satisfacibilidad booleana mediante un solucionador SAT . ^{[ 5 ]}

Cuando se encuentran contraejemplos, se examinan para determinar si son ejemplos espurios, es decir, ejemplos no auténticos que surgen de la subabstracción del modelo. Un contraejemplo no espurio refleja la incorrección del programa, lo cual puede ser suficiente para finalizar el proceso de verificación y concluir que el programa es incorrecto. El objetivo principal del proceso de refinamiento es manejar los contraejemplos espurios. Los elimina aumentando la granularidad de la abstracción.

El proceso de refinamiento garantiza que los estados sin salida y los estados malos no pertenezcan al mismo estado abstracto. Un estado sin salida es uno alcanzable sin transición saliente, mientras que un estado malo es uno con transiciones que provocan el contraejemplo. ^{[ 2 ]}