coq - romualfons - ronald seo
¿Se puede usar Coq(fácilmente) como verificador de modelos? (3)
Como dice el título, ¿se puede usar Coq como verificador de modelos? ¿Puedo mezclar la verificación de modelos con la prueba Coq? ¿Es esto habitual? Google habla de un "cálculo µ", ¿alguien tiene experiencia con esto o algo similar? ¿Se recomienda utilizar Coq de esta manera o debo buscar otra herramienta?
Existe cierto trabajo sobre el uso de Coq como verificador de modelos, por ejemplo, consulte https://github.com/coq-contribs/smc . Sin embargo, no sé de personas que hayan usado esto en aplicaciones serias.
Para complementar la respuesta existente con @Pekka, µ-calculus es una notación para hablar de puntos de corrección, que representan soluciones a problemas de accesibilidad.
Un ejemplo de un punto fijo mínimo (μ) es el conjunto más grande de estados que se puede alcanzar comenzando desde algún lugar (por ejemplo, desde la primera línea de un programa). Es un punto de referencia "mínimo", debido a que es el más pequeño entre otros puntos de corrección posibles. Se obtiene comenzando con el conjunto vacío y agregando estados hasta alcanzar un punto fijo. Bajo ciertas condiciones, la existencia de un punto fijo está asegurada por el Knaster-Tarski .
Un ejemplo de un punto fijo más grande (ν) es el conjunto más grande en el que podemos permanecer dentro sin violar algún requisito de seguridad. Es un punto fijo "mayor", porque se obtiene a partir de la recopilación de todos los estados (por lo tanto, desde arriba en el orden parcial de los conjuntos definidos por la relación del subconjunto), y restringiéndolo iterativamente, hasta que alcanzamos un punto fijo. Los puntos de fijación más grandes son duales a los puntos de fijación mínimos, por lo tanto, el mismo teorema se aplica a la existencia y la singularidad. Piense en la búsqueda gráfica como otro ejemplo.
Al alternar el tipo de puntos fijos en una fórmula de cálculo μ, podemos expresar un comportamiento temporal como: "Quiero que sigas yendo y viniendo entre dos ubicaciones", o "Quiero que el servidor continúe respondiendo a cada solicitud que reciba. ".
Luego, podemos modelar la verificación (con un verificador de modelos enumerativo o simbólico) si la propiedad que describimos está implícita en un sistema que hemos diseñado.
SPIN es un verificador de modelos enumerativos: almacena cada estado que explora en una tabla hash e incluye algunos algoritmos para reconocer que no es necesario enumerar todos los estados, pero puede tratar algunos de ellos como representativos de otros estados (desde el Desde la perspectiva de la propiedad que se verifica, esos estados son equivalentes, por lo que basta con razonar solo sobre uno de ellos. Esos métodos se llaman reducción parcial de orden .
NuSMV es un verificador de modelos simbólicos. Todavía busca los estados de un sistema, pero no los representa uno por uno en la memoria. En su lugar, mantiene un seguimiento de los conjuntos de estados, representando esos conjuntos como diagramas de decisión binarios . Estas son estructuras de datos que pueden permanecer pequeñas, incluso cuando representan conjuntos con
10**24estados. Hay garantía aunque para eso. Desafortunadamente, todavía pueden explotar en tamaño, y lamentablemente esto es así para casi todas las funciones booleanas (por lo tanto, casi todos los conjuntos que podemos querer representar), como lo ha proved Claude Shannon .
Las herramientas anteriores están diseñadas y utilizadas para la verification . También hay un enfoque llamado síntesis . Después de estudiar ambos, puede parecer confuso si realmente hay alguna diferencia entre ellos. En un primer encuentro, uno puede pensar que los modelos y las fórmulas son lo que marca la diferencia. Sin embargo, eso es engañoso: los modelos y las fórmulas son intercambiables como métodos de descripción, y también se pueden mezclar.
La diferencia entre verificación y síntesis está en alternancia de quantifiers :
- La verificación tiene una cuantificación uniforme (todo universal, generalmente)
- La síntesis tiene una cuantificación alterna: implica cuantificadores existenciales y universales anidados.
Por supuesto, también se puede verificar una fórmula cuantificada, por ejemplo, para todos /forall x: /exists y: f(x, y) . ¿No es esto solo una verificación? Bueno, lo es, demostrando que no hay ninguna diferencia matemática en el fondo del asunto, entre la síntesis y la verificación. Tradicionalmente, uno se encuentra principalmente en los casos anteriores de cómo aparece la cuantificación en qué problemas se consideran como síntesis y qué problemas se consideran como verificación.
La principal diferencia real entre la síntesis y la verificación es cómo utilizamos el resultado al verificar si una fórmula es verdadera:
En la verificación, ya tenemos la implementación del sistema que deseamos y comprobamos que satisface algunas propiedades deseadas. Si no es así, vamos a (manualmente) intentar arreglar la implementación y luego verificar nuevamente.
En síntesis, hay algunas partes del sistema final que aún no hemos especificado completamente en detalle. Dejamos que ese detalle sea seleccionado por la herramienta que usamos. En otras palabras, la herramienta elimina los cuantificadores existenciales de una manera que hará que la fórmula sea verdadera, y nos dice lo que hizo, para que completemos el sistema de esa manera, asegurando que la fórmula sea verdadera.
Un ejemplo de una herramienta de síntesis en C es gr1c , otro ejemplo en Python es omega . Hay varias otras herramientas .
Sin embargo, si aborda un problema, al menos asegúrese de escribir lo que es el plan, de escribir una especificación .
Uno de los mejores libros sobre estos temas son los sistemas de especificación de Leslie Lamport. Y para convencer que varias representaciones son caras de lo mismo, considere la posibilidad de leer Informática y máquinas estatales .
Un asistente de pruebas como Coq verificará que su prueba es sólida y que cualquier teorema que proponga puede (o no puede) derivarse utilizando axiomas y resultados previamente comprobados. También le brindará apoyo para proponer pasos de prueba para reducir el esfuerzo que tiene que hacer para descargar las pruebas.
Un verificador de modelos, en contraste, enumera simbólicamente el espacio de estado de la especificación y determina si se viola alguna de las condiciones de verificación. En tal caso, proporcionará una traza de error que muestra qué secuencia de cambios de estado activará la violación.
Estos usualmente tienen requisitos de procesamiento de back-end muy diferentes pero, aunque podrían combinarse en una sola herramienta, el comprobador de Coq no parece haberlo hecho.
Leslie Lamport desarrolló el lenguaje de especificación de la lógica temporal de acciones (TLA +), junto con el sistema complementario de prueba TLA + (TLAPS), para razonar sobre grandes especificaciones formales. Se ha ampliado con el PlusCal algorítmico PlusCal que admite la verificación de modelos de los algoritmos que se traducen en una representación TLA +.
El µ-cálculo es una notación utilizada como un soporte de bajo nivel para muchos métodos formales. También debe considerar el problema de la satisfacción booleana para un enfoque de fuerza más bruta. Los probadores de teoremas son generalmente más sofisticados en su diseño y utilizan los conceptos de AI / sistema experto tradicional junto con las bibliotecas de reglas de prueba definidas por los expertos para proporcionar el soporte necesario para cumplir con las obligaciones de prueba.
Como otro ejemplo de una herramienta de prueba, puede ver el método Event-B y la plataforma de desarrollo de Rodin que lo acompaña. Esto, al refinar una especificación, identificará más concretamente las obligaciones de prueba e intentará cumplirlas mecánicamente, dejando las tareas difíciles para que usted haga.
Para ver el modelo puedes mirar:
Entre las opciones libremente disponibles.