Comprobación de modelo

En informática , la verificación de modelos o la verificación de propiedades es un método para verificar si un modelo de estado finito de un sistema cumple con una especificación dada (también conocida como corrección ). Esto generalmente se asocia con sistemas de hardware o software , donde la especificación contiene requisitos de actividad (como evitar el bloqueo de vida ) así como requisitos de seguridad (como evitar estados que representen un bloqueo del sistema ).

Para resolver tal problema algorítmicamente , tanto el modelo del sistema como su especificación se formulan en algún lenguaje matemático preciso. Con este fin, el problema se formula como una tarea en lógica , a saber, comprobar si una estructura satisface una fórmula lógica dada. Este concepto general se aplica a muchos tipos de lógica y muchos tipos de estructuras. Un problema simple de verificación de modelos consiste en verificar si una fórmula en la lógica proposicional es satisfecha por una estructura dada.

La comprobación de propiedades se utiliza para la verificación cuando dos descripciones no son equivalentes. Durante el refinamiento , la especificación se complementa con detalles que son innecesarios en la especificación de nivel superior. No es necesario verificar las propiedades recién introducidas con la especificación original, ya que esto no es posible. Por lo tanto, la estricta verificación de equivalencia bidireccional se relaja a una verificación de propiedad unidireccional. La implementación o diseño se considera como un modelo del sistema, mientras que las especificaciones son propiedades que el modelo debe satisfacer. [2]

Se ha desarrollado una clase importante de métodos de verificación de modelos para verificar modelos de diseños de hardware y software donde la especificación viene dada por una fórmula lógica temporal . El trabajo pionero en la especificación de la lógica temporal fue realizado por Amir Pnueli , quien recibió el premio Turing de 1996 por "un trabajo fundamental que introduce la lógica temporal en la informática". [3] La comprobación de modelos comenzó con el trabajo pionero de EM Clarke , EA Emerson , [4] [5] [6] de JP Queille y J. Sifakis . [7] Clarke, Emerson y Sifakis compartieron el Premio Turing 2007por su trabajo seminal fundando y desarrollando el campo de la verificación de modelos. [8] [9]

La verificación de modelos se aplica con mayor frecuencia a los diseños de hardware. Para el software, debido a la indecidibilidad (consulte la teoría de la computabilidad ), el enfoque no puede ser completamente algorítmico, aplicarse a todos los sistemas y dar siempre una respuesta; en el caso general, puede dejar de probar o refutar una propiedad dada. En hardware de sistemas embebidos , es posible validar una especificación entregada, es decir, por medio de diagramas de actividad UML [10] o redes de Petri interpretadas por control . [11]

La estructura generalmente se proporciona como una descripción del código fuente en un lenguaje de descripción de hardware industrial o un lenguaje de propósito especial. Tal programa corresponde a una máquina de estados finitos (FSM), es decir, un gráfico dirigido que consta de nodos (o vértices ) y aristas . Un conjunto de proposiciones atómicas está asociado con cada nodo, normalmente indicando qué elementos de memoria son uno. Los nodos representan estados de un sistema, los bordes representan posibles transiciones que pueden alterar el estado, mientras que las proposiciones atómicas representan las propiedades básicas que se mantienen en un punto de ejecución.

El software de control de ascensores se puede verificar con un modelo para verificar tanto las propiedades de seguridad, como "La cabina nunca se mueve con la puerta abierta" , [1] como las propiedades de vitalidad, como "Cada vez que se presiona el botón de llamada del piso n , la cabina eventualmente se detendrá en el piso n y abre la puerta" .