Verificación formal del programa en la práctica

66

Como ingeniero de software, escribo mucho código para productos industriales. Cosas relativamente complicadas con clases, hilos, algunos esfuerzos de diseño, pero también algunos compromisos para el rendimiento. Realizo muchas pruebas, y estoy cansado de probar, así que me interesé en las herramientas de prueba formales, como Coq, Isabelle ... ¿Podría usar una de estas para probar formalmente que mi código está libre de errores y listo? ¿con eso? - pero cada vez que reviso una de estas herramientas, me alejo convencido de que son utilizables para la ingeniería de software cotidiana. Ahora, eso solo podría ser yo, y estoy buscando consejos / opiniones / ideas sobre eso :-)

Específicamente, tengo la impresión de que hacer que una de estas herramientas funcione para mí requeriría una gran inversión para definir adecuadamente al probador los objetos, métodos ... del programa en consideración. Entonces me pregunto si el probador no se quedaría sin energía dado el tamaño de todo con lo que tendría que lidiar. O tal vez tendría que deshacerme de los efectos secundarios (esas herramientas de prueba parecen funcionar realmente bien con lenguajes declarativos), y me pregunto si eso daría como resultado un "código probado" que no podría usarse porque no sería rápido o suficientemente pequeño. Además, no tengo el lujo de cambiar el idioma con el que trabajo, tiene que ser Java o C ++: no puedo decirle a mi jefe que voy a codificar en OXXXml de ahora en adelante, porque es el único idioma en que puedo probar la exactitud del código ...

¿Podría alguien con más experiencia en herramientas de prueba formal comentar? Nuevamente, me ENCANTARÍA usar una herramienta de prueba formal, creo que son geniales, pero tengo la impresión de que están en una torre de marfil que no puedo alcanzar desde la zanja de Java / C ++ ... (PS: I también LOVE Haskell, OCaml ... no me hagas una idea equivocada: soy un fanático de los lenguajes declarativos y las pruebas formales, solo estoy tratando de ver cómo podría hacer que esto sea realmente útil para la ingeniería de software)

Actualización: Dado que esto es bastante amplio, intentemos las siguientes preguntas más específicas: 1) ¿hay ejemplos de uso de probadores para probar la corrección de los programas industriales Java / C ++? 2) ¿Coq sería adecuado para esa tarea? 3) Si Coq es adecuado, ¿debería escribir el programa en Coq primero y luego generar C ++ / Java desde Coq? 4) ¿Podría este enfoque manejar optimizaciones de subprocesos y rendimiento?

programming-languages program-correctness software-verification Franco
fuente
3
Entiendo y aprecio tu problema, pero no entiendo qué es esta pregunta después (como una publicación SE). ¿Discusión? ¿Experiencia? Ninguno de los dos es adecuado para SE. El "¿Qué puedo hacer?" El tono me hace sentir que esta es una pregunta demasiado amplia también.
Raphael
3
Ya veo ... Estoy de acuerdo en que esta pregunta no se formuló claramente. Entonces, digamos: 1) ¿hay ejemplos de uso de probadores para probar la corrección de los programas industriales Java / C ++? 2) ¿Coq sería adecuado para esa tarea? 3) Si Coq es adecuado, ¿debería escribir el programa en Coq primero y luego hacer que Coq genere C ++ / Java a partir de eso? 4) ¿Podría este enfoque hacer frente a la optimización de subprocesos y rendimiento?
Frank
2
Entonces son cuatro preguntas, entonces. 1) probablemente sea mejor en Ingeniería de Software, ya que es poco probable que encuentre aquí a (muchos) profesionales de la industria. 2) sabe algo subjetivo, pero podemos tener personas aquí que pueden ofrecer una perspectiva objetiva. 3) es, por lo que puedo decir, completamente subjetivo. 4) Es una buena pregunta para este sitio. En resumen: separe sus preguntas, vaya a Ingeniería de software con la primera y piense detenidamente si puede esperar una respuesta objetiva (!) Aquí (!) Antes de publicar 2).
Raphael
10
Estás describiendo el sueño de la verificación formal, pero estamos muy lejos de estar allí. AFAIK, la verificación del programa es una tarea no rutinaria, y solo se aplica a programas muy simples. Dicho esto, creo que esta pregunta es acertada para el sitio, y agradecería que alguien del área admita los límites de su campo, explicando el estado del arte y las limitaciones (tal vez al vincular a alguna encuesta )
Yuval Filmus
99
El problema con la verificación de los programas de C ++ es que C ++ no es un lenguaje bien definido. No creo que la verificación a gran escala sea posible hasta que muchas partes de los sistemas de software (SO, bibliotecas, lenguajes de programación) realmente se rediseñen para admitir la verificación. Como es bien sabido, no puedes volcar 200000 líneas de código en alguien y decir "verificar". Debe verificar y escribir código juntos, y debe adaptar sus hábitos de programación al hecho de que también está verificando.
Andrej Bauer

Respuestas:

35

Trataré de 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 / incorrecta.

  1. Hay muchas herramientas que están específicamente diseñadas para probar formalmente las propiedades 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 tipo Java prueba una propiedad formal de un programa Java, a saber, que ciertos errores, como agregar ay floatan int, ¡nunca pueden ocurrir! Me 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, hay un amplio gradiente de lo que puede significar "probar que un programa es correcto", desde simples propiedades de seguridad hasta una prueba completa de que el programa cumple con una especificación detallada.

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

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

    Para esto, necesita una herramienta que tenga una comprensión formal tanto de su especificación como de 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 Frank mencionó, Krakatoa es un ejemplo de dicha herramienta.

    • Una herramienta que demuestra el teorema (s), de forma automática o interactiva. Coq interactúa con Krakatoa de esta manera, y hay 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 automáticos, y se sabe que los probadores de teoremas automáticos ocasionalmente tienen errores de solidez que los hacen menos confiables. Esta es un área donde Coq brilla en comparación (¡pero no es automático!).

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

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

En conclusión: la verificación formal de los 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.

cody
fuente
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í está "libre de errores" :-) algo así como tratar de definir la "proposición verdadera de un lenguaje" con un metalenguaje, y luego necesitar otro meta- lenguaje para eso, luego otro ...
Frank
66
¡El problema es que lo que el usuario "quiere" generalmente no se expresa en un lenguaje formal! Generalmente 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, debe relacionar las matemáticas con el mundo real, que es un proceso no formal.
cody
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 solucionable con métodos formales (pero ciertamente un problema para los ingenieros).
Frank
Un teorema es, por definición, una proposición probada. Entonces, probablemente no quieras "probar el teorema".
nbro
@nbro Wikipedia parece estar de acuerdo contigo. Mathworld, sin embargo, define un teorema como una proposición que " puede demostrarse que es verdadera 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 contraquibble, por supuesto)
cody
15

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

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

  2. Este documento: Uso de la verificación de modelos para encontrar errores graves del sistema de archivos @ OSDI'04 muestra cómo usar la 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 muy probados: ext3, JFS y ReiserFS, y se encuentran 32 errores graves. Ganó el Premio al Mejor Papel.

  3. Este documento: Cómo Amazon Web Services utiliza 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 usado intensamente su propia caja de herramientas TLA. A menudo da una verificación formal (bastante completa) en TLA de los algoritmos / teoremas propuestos por él mismo (así como por sus coautores) en los apéndices de los documentos.

hengxina
fuente
4

Una especificación formal 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, dado que 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 un número no trivial de errores.

Una desventaja de la verificación formal es que puede imponer algo como el doble del costo de implementación, probablemente más (necesita un especialista en especificación formal y necesita usar 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.

vonbrand
fuente
La ventaja de la verificación formal es que ... Una segunda desventaja de la verificación formal es que ... Esto es confuso.
hengxin
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.
Kaveh
3

La verificación formal ahora es posible para los programas escritos en un subconjunto de C ++ diseñado para sistemas integrados críticos para la seguridad. Consulte http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.ppt para una breve presentación, y http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.pdf para obtener el artículo completo.

dc42
fuente
55
Gracias por los enlaces. Sería útil al menos una breve descripción general de su contenido, para protegerse contra la rotura de enlaces, especialmente porque sus enlaces son a un sitio web corporativo: estos tienden a reorganizarse periódicamente, eliminando todos los enlaces en el sitio.
David Richerby el
2

Haces 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 compiladores incorporan principios de "verificación formal" para determinar la corrección del programa! de alguna manera, si usa un compilador moderno, está utilizando gran parte del estado del arte en la verificación formal.

Usted dice "Estoy cansado de las pruebas" pero la verificación formal no es realmente un sustituto de las pruebas. en cierto modo es una variación en las pruebas.

Mencionas Java. Hay muchos métodos avanzados de verificación formal integrados en un programa de verificación de Java llamado FindBugs que, de hecho, pueden ejecutarse en grandes bases de código. Tenga en cuenta que aparecerá 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 está produciendo defectos funcionales reales, generalmente presenta "antipatrones" que de todos modos deben evitarse en el código.

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 particular.

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

Aquí hay un ejemplo de una encuesta de herramientas de verificación formal en el campo de EE realizada por Lars Philipson .

vzn
fuente
2
Es engañoso decir que "una gran cantidad de principios de" verificación formal "están integrados en los compiladores para determinar la corrección del programa". A lo que se refiere es a la verificación de tipo estática que hacen algunos compiladores, pero las propiedades verificadas de esa manera son bastante simples, por ejemplo, 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".
Martin Berger
2
no se refería específicamente a la verificación de tipo estático, aunque ese es un ejemplo simple / común. Las técnicas de optimización del compilador de imho, que son amplias y avanzadas, son más o menos similares a los principios formales de verificación, ya que implican técnicas avanzadas para determinar / mostrar la equivalencia de las variantes de programa optimizadas. por lo tanto, parece importante evitar el problema de los "postes de meta móviles" aquí y no asumir que simplemente porque un compilador lo hace o está integrado en el compilador, no es una verificación formal.
vzn
2
acordó que esto no es un entendimiento común. aproximadamente, las técnicas de optimización están creando un modelo de comportamiento del programa, por ejemplo, de un bucle o subrutina, y optimizando ese modelo, y luego generando un nuevo código que es demostrablemente equivalente. por lo que algunas de estas optimizaciones son bastante sofisticadas en la reorganización del código y para mí utilizan principios de verificación formales. Parece que hay muchos otros ejemplos de métodos formales de verificación en el compilador ... la pregunta original formuló muchas preguntas diferentes, como muchos han notado, definitivamente no estoy tratando de responder a todas las preguntas que contiene.
vzn
2
por cierto, parece haber algunos principios formales de verificación también utilizados en el motor de tiempo de ejecución de Java, JRE, por ejemplo, optimización dinámica, etc ...
vzn
3
ese es "el sueño de la verificación formal" mencionado anteriormente por filmus, en mi opinión una abstracción quimérica, y la industria pragmática / utilitaria / realista lo reconoce en gran medida como tal. grandes bases de código se conocen desde hace décadas para tener inherentemente errores / defectos por K-líneas de código y esto no cambiará sin importar cómo los avances teoría / tecnología, es un hecho de la humana naturaleza. y, de hecho, los teoremas matemáticos creados por el hombre tienen las mismas propiedades, ¡aunque esto no es muy apreciado! yxy
vzn
1

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

http://alloytools.org/documentation.html Alloy es un verificador de modelos.

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

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

TIC Tac
fuente