Comprobación de modelo
En ciencias de la computación , la verificación de modelos o 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 vitalidad (como evitar el bloqueo en vivo ), así como requisitos de seguridad (como evitar estados que representan un bloqueo del sistema ).
Para resolver este problema algorítmicamente , tanto el modelo del sistema como su especificación se formulan en un lenguaje matemático preciso. Para ello, el problema se formula como una tarea en lógica , es decir, comprobar si una estructura satisface una fórmula lógica dada. Este concepto general se aplica a muchos tipos de lógica y a 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 verificación de propiedad 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 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 . Amir Pnueli , quien recibió el premio Turing en 1996, realizó un trabajo pionero en la especificación de la lógica temporal por su "trabajo fundamental en la introducción de la lógica temporal en la ciencia de la computación". [3] La verificación de modelos comenzó con el trabajo pionero de EM Clarke , EA Emerson , [4] [5] [6] por JP Queille y J. Sifakis . [7] Clarke, Emerson y Sifakis compartieron el premio Turing 2007por su trabajo fundamental en la fundación y desarrollo del 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 (ver 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 fallar en probar o refutar una propiedad dada. En hardware de sistemas embebidos , es posible validar una especificación entregada, es decir, mediante diagramas de actividad UML [10] o redes de Petri interpretadas de control . [11]
La estructura generalmente se proporciona como una descripción de 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 se asocia con cada nodo, típicamente 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.
.jpg){kind=link}
.jpg/440px-Two_One_G_(cropped).jpg)