Verificación formal de programas en la práctica

Intentaré dar una respuesta sucinta a algunas de sus preguntas.Tenga en cuenta que este no es estrictamente mi campo de investigación, por lo que parte de mi información puede estar desactualizada / ser incorrecta.

1. Hay muchas herramientas que están diseñadas específicamente para probar propiedades formalmente de Java y C ++.

   Sin embargo, necesito hacer una pequeña digresión aquí: ¿qué significa probar la corrección de un programa? El verificador de tipos de Java demuestra una propiedad formal de un programa Java, es decir, que ciertos errores, como agregar un float y un int, nunca ¡ocurrir! Imagino que está interesado en propiedades mucho más fuertes, a saber, que su programa nunca puede entrar en un estado no deseado, o que la salida de una determinada función se ajusta a una determinada especificación matemática. En resumen, existe un amplio gradiente de lo que puede significar «probar que un programa es correcto», desde propiedades de seguridad simples hasta una prueba completa de que el programa cumple una especificación detallada.

   Ahora voy a asumir que está interesado en probar propiedades sólidas sobre sus programas. Si está interesado en propiedades de seguridad (su programa puede no alcanzar un cierto estado), entonces, en general, parece que el mejor enfoque es comprobación del modelo . Sin embargo, si desea especificar completamente el comportamiento de un programa Java, lo mejor es utilizar un lenguaje de especificación para ese lenguaje, por ejemplo JML . Existen lenguajes para especificar el comportamiento de los programas en C, por ejemplo, ACSL , pero no conozco C ++.

2. Una vez que tenga sus especificaciones, debe demostrar que el programa cumple con esa especificación.

   Para esto, necesita una herramienta que tenga un entendimiento formal de ambos su especificación y la semántica operativa de su lenguaje (Java o C ++) para expresar el teorema de adecuación , es decir, que la ejecución del programa respeta la especificación.

   Esta herramienta también debería permitirle formular o generar la prueba de ese teorema. Ahora ambas tareas (especificar y probar) son bastante difíciles, por lo que a menudo se separan en dos:

   • Una herramienta que analiza el código, la especificación y genera el teorema de adecuación. Como mencionó Frank, Krakatoa es un ejemplo de tal herramienta.

   • Una herramienta que demuestra el teorema ( s), de forma automática o interactiva. Coq interactúa con Krakatoa de esta manera, y existen algunas herramientas automatizadas poderosas como Z3 que también se pueden usar.

   Un punto (menor): hay algunos teoremas que son demasiado difíciles de probar con métodos automatizados, y se sabe que los probadores automáticos de teoremas ocasionalmente tienen errores de solidez que los hacen menos confiables. Esta es un área donde Coq brilla en comparación (¡pero no es automática!).

3. Si desea generar código Ocaml, entonces definitivamente escriba en Coq (Gallina) primero, luego extraiga el código. Sin embargo, Coq es terrible para generar C ++ o Java, si es que es posible.

4. ¿Pueden las herramientas anteriores manejar problemas de subprocesamiento y rendimiento? Probablemente no, los problemas de rendimiento y roscado se manejan mejor con herramientas diseñadas específicamente, ya que son problemas particularmente difíciles. No estoy seguro de tener herramientas para recomendar aquí, aunque el proyecto PolyNI de Martin Hofmann parece interesante.

En conclusión: la verificación formal de programas Java y C ++ del «mundo real» es un campo grande y bien desarrollado, y Coq es adecuado para partes de esa tarea. Puede encontrar una descripción general de alto nivel aquí , por ejemplo.

Comentarios

• Gracias por esta publicación y las referencias que agregaste. En mi humilde opinión, el objetivo de los ingenieros de software es poder lanzar rápidamente sistemas que 1) siempre proporcionarán resultados correctos, 2) nunca fallarán. Podría ver un problema de regresión aquí, donde es posible que desee probar que la especificación en sí es » libre de errores » 🙂 tipo de como intentar definir » la proposición verdadera de un lenguaje » con un metalenguaje, luego necesitar otro metalenguaje para eso, luego otro uno …
• El problema es que lo que el usuario » quiere » generalmente no se expresa en un ¡idioma! Por lo general, no hay una respuesta formal a la pregunta: » ¿esta especificación formal se ajusta a mi idea informal? «. Es ‘ posible probar una especificación formal y demostrar que tiene ciertas propiedades matemáticas, pero en última instancia, es necesario relacionar las matemáticas con el mundo real, que es un proceso no formal.
• Sí, por supuesto, siempre me di cuenta de que los métodos formales solo podían comenzar desde un punto bien definido.Si esa especificación se ajusta o no a las necesidades conscientes / inconscientes / no descubiertas de los usuarios de la vida real es otro problema, no abordable con métodos formales (pero ciertamente un problema para los ingenieros).
• Un teorema es por definición un proposición probada. Entonces, probablemente no quieras » probar el teorema «.
• @nbro Wikipedia parece estar de acuerdo contigo. Mathworld, sin embargo, define un teorema como una proposición que » puede demostrarse mediante operaciones matemáticas aceptadas «. En este caso, dar pruebas de teoremas no solo es posible, sino necesario para justificar llamarlos así. 🙂 (esto es un contraataque, por supuesto)

Me gustaría mencionar tres aplicaciones notables de métodos formales / herramientas de verificación formales en la industria o sistemas reales no triviales. Tenga en cuenta que tengo poca experiencia en este tema y solo los aprendo leyendo artículos.

1. La herramienta de código abierto Java Pathfinder (JPF para abreviar) lanzado por la NASA en 2005 es un sistema para verificar programas ejecutables de código de bytes de Java (consulte Java Pathfinder @ wiki ). Se ha utilizado para detectar inconsistencias en el software ejecutivo del K9 Rover en NASA Ames.

2. Este documento: Uso de la comprobación de modelos para encontrar errores graves del sistema de archivos @ OSDI «04 muestra cómo utilizar Verificación de modelos para encontrar errores graves en los sistemas de archivos. Un sistema llamado FiSC se aplica a tres sistemas de archivos ampliamente utilizados y probados: ext3, JFS y ReiserFS, y se encuentran 32 errores graves. Ganó el premio al mejor artículo.

3. Este documento: Cómo Amazon Web Services usa métodos formales @ CACM «15 describe cómo AWS aplica métodos formales a sus productos como S3, DynamoDB, EBS y el administrador de bloqueo distribuido interno. Se centra en la herramienta TLA + de Lamport. Por cierto, Lamport ha utilizado de forma intensiva su propia caja de herramientas TLA. A menudo ofrece una verificación formal (bastante completa) en TLA de los algoritmos / teoremas propuestos por él mismo (así como por los coautores) en los apéndices de los artículos.

Una La especificación de un programa es (más o menos) un programa escrito en otro lenguaje de programación. Como resultado, la especificación ciertamente incluirá sus propios errores.

La ventaja de la verificación formal es que, como el programa y la especificación son dos implementaciones separadas, sus errores serán diferentes. Pero no siempre: una fuente común de errores, los casos pasados por alto, a menudo coincidirán. Por lo tanto, la verificación formal no es una panacea: aún puede pasar por alto una cantidad no trivial de errores.

Una desventaja de la verificación formal es que puede imponer algo así como el doble del costo de implementación, probablemente más (necesita un especialista en especificación formal, y necesita utilizar las herramientas más o menos experimentales que vienen con él; eso no será barato).

Supongo que configurar casos de prueba y andamios para ejecutarlos automáticamente sería un mejor uso de su tiempo.

Comentarios

• La ventaja de la verificación formal es que … Una segunda desventaja de la verificación formal es que … Esto es confuso.
• Creo que el desajuste entre la especificación y la tarea informal es un problema de análisis de requisitos de software, no un problema de programación.

Usted hace algunas preguntas diferentes. Estoy de acuerdo en que parece que los métodos formales de verificación para aplicaciones industriales / comerciales no son tan comunes. Sin embargo, uno debe darse cuenta de que muchos principios de «verificación formal» están incorporados en los compiladores para determinar la exactitud del programa. así que, en cierto modo, si usa un compilador moderno, «está usando gran parte del estado del arte en la verificación formal.

Dice» Estoy cansado de probar «pero verificación formal no es realmente un sustituto de las pruebas. en cierto modo, es una variación de las pruebas.

Mencionas Java.Hay muchos métodos de verificación formales avanzados integrados en un programa de verificación de Java llamado FindBugs que de hecho se pueden ejecutar en grandes bases de código. Tenga en cuenta que presentará tanto «falsos positivos como falsos negativos» y los resultados deben ser revisados / analizados por un desarrollador humano. Pero tenga en cuenta que incluso si no presenta defectos funcionales reales, generalmente presenta «antipatrones» que deben evitarse en el código de todos modos.

No hace más mención de su aplicación particular que no sea «industrial» . La verificación formal en la práctica tiende a depender de la aplicación en particular.

Las técnicas de verificación formal parecen ser ampliamente utilizadas en EE para probar la corrección del circuito, p. en diseño de microprocesadores.

A continuación se muestra un ejemplo de una encuesta de herramientas de verificación formal en el campo de EE por Lars Philipson .

Comentarios

• Es ‘ engañoso decir que » un Muchos de los principios de » verificación formal » están integrados en los compiladores para determinar la corrección del programa «. A lo que te refieres es a la verificación de tipo estática que hacen algunos compiladores, pero las propiedades verificadas de esa manera son bastante simples, p. evitando agregar un número y una cadena. Esto es útil, pero está muy lejos de lo que generalmente se entiende por » verificación formal «.
• no se refiere específicamente a la verificación de tipos estáticos, aunque ese es un ejemplo simple / común. En mi humilde opinión, las técnicas de optimización del compilador, que están muy extendidas y son avanzadas, son más o menos similares a los principios formales de verificación, porque implican técnicas avanzadas para determinar / mostrar la equivalencia de las variantes optimizadas del programa. por lo que parece que es importante evitar el problema de » mover los postes de meta » aquí y no asumir que simplemente porque un compilador lo hace o está construido en el compilador, no es una verificación formal.
• acordó que esto no es un entendimiento común. las técnicas de optimización son, a grandes rasgos, la creación de un modelo de comportamiento del programa, por ejemplo, de un bucle o subrutina, y la optimización de ese modelo, y luego la generación de un nuevo código que sea demostrablemente equivalente. por lo que algunas de estas optimizaciones son bastante sofisticadas al reorganizar el código & para mí, hacen uso de principios formales de verificación. parece haber muchos otros ejemplos de métodos de verificación formales en el compilador … la pregunta original planteaba muchas preguntas diferentes, como muchos han notado, y definitivamente no intento responder todas las preguntas contenidas en él.
• De manera que parece haber algunos principios de verificación formales que también se utilizan en el JRE, motor de tiempo de ejecución de Java, por ejemplo, optimización dinámica, etc. i> sueño de verificación formal » referido por filmus arriba, en mi humilde opinión, una abstracción quimérica, y la industria pragmática / utilitaria / realista la reconoce en gran medida como tal. Se ha sabido durante décadas que las grandes bases de código tienen $ x $ errores / defectos por $ y $ K líneas de código y esto nunca cambiará sin importar cómo avance la teoría / tecnología, es un hecho de naturaleza humana. y de hecho los teoremas matemáticos creados por humanos tienen las mismas propiedades, ¡aunque esto no es muy apreciado!

Quizás, un verificador de modelos puede ser útil.

http://alloytools.org/documentation.html La aleación es un verificador de modelos .

Una bonita presentación que explica el concepto de verificación de modelos usando Alloy: https://www.youtube.com/watch?v=FvNRlE4E9QQ

En la misma familia de herramientas vienen las «pruebas basadas en propiedades», todas tratan de encontrar un contraejemplo para el modelo de especificación dado de su software.