¿Los métodos formales de verdad del programa tienen un lugar en la industria?

Question

Vislézcé Lógica de Hoare en la Universidad. Lo que hicimos fue realmente simple. La mayor parte de lo que hice fue demostrar la corrección de programas simples que consisten en while bucles, if declaraciones y secuencia de instrucciones, pero nada más. ¡Estos métodos parecen muy útiles!

¿Se utilizan ampliamente los métodos formales en la industria?

¿Se utilizan estos métodos para probar el software de la misión crítica?

Answer 1

Esta es una pregunta cercana a mi corazón (soy un investigador en verificación de software utilizando lógicas formales), por lo que probablemente no se sorprenderá cuando diga que creo que estas técnicas tienen un lugar útil, y aún no se usan lo suficiente en el industria.

Hay muchos niveles de "métodos formales", por lo que asumiré que te refieres a aquellos que descansan sobre una base matemática rigurosa (en lugar de, por ejemplo, siguiendo un proceso de estilo de 6 sigma). Algunos tipos de métodos formales han tenido un gran éxito: los sistemas de tipo son un ejemplo. Las herramientas de análisis estático basadas en el análisis de flujo de datos también son populares, la verificación de modelos es casi ubicua en el diseño de hardware, y los modelos computacionales como PI-Calculus y CCS parecen inspirar algún cambio real en el diseño práctico del lenguaje para la concurrencia. El análisis de terminación es uno que ha tenido mucha prensa recientemente: el proyecto SDV en Microsoft y el trabajo de Byron Cook son ejemplos recientes de crossover de investigación/práctica en métodos formales.

El razonamiento de Hoare, hasta ahora, no ha hecho grandes incursiones en la industria: esto es por más razones de las que puedo enumerar, pero sospecho que se trata principalmente de la complejidad de escribir y luego probar especificaciones para programas reales (tienden a obtener grande, y no expresar propiedades de muchos entornos del mundo real). Varios subcampos en este tipo de razonamiento ahora están haciendo grandes incursiones en estos problemas: la lógica de separación es uno.

Esta es en parte la naturaleza de la investigación continua (dura). Pero debo confesar que nosotros, como teóricos, hemos fallado por completo en educar a la industria sobre por qué nuestras técnicas son útiles, para mantenerlos relevantes para las necesidades de la industria y hacerlas accesibles para los desarrolladores de software. En algún nivel, ese no es nuestro problema: somos investigadores, a menudo matemáticos, y el uso práctico no es lo más importante en nuestras mentes. Además, las técnicas que se desarrollan a menudo son demasiado embrionarias para su uso en sistemas a gran escala: trabajamos en programas pequeños, en sistemas simplificados, que las matemáticas funcionen y sigan adelante. Sin embargo, no compro muchas excusas: deberíamos ser más activos para impulsar nuestras ideas y obtener un ciclo de retroalimentación entre la industria y nuestro trabajo (una de las principales razones por las que volví a la investigación).

Probablemente sea una buena idea para mí resucitar mi weblog y hacer más publicaciones sobre estas cosas ...

Answer 2

Bueno, Sir Tony Hoare se unió a Microsoft Research hace unos 10 años, y una de las cosas que comenzó fue una verificación formal del kernel de Windows NT. De hecho, esta fue una de las razones del largo retraso de Windows Vista: comenzando con Vista, grandes partes del núcleo son En realidad formalmente verificado WRT. a ciertas propiedades, como ausencia de plazos, ausencia de fugas de información, etc.

Esto ciertamente no es típico, pero probablemente sea la aplicación más importante de la verificación formal del programa, en términos de su impacto (después de todo, casi todos los seres humanos tienen una forma o forma afectada por una computadora que ejecuta Windows).

Answer 3

No puedo comentar mucho sobre el software de misión crítica, aunque sé que la industria de la aviónica utiliza una amplia variedad de técnicas para validar el software, incluidos los métodos de estilo Hoare.

Los métodos formales han sufrido porque los primeros defensores como Edsger Dijkstra insistieron en que deberían usarse en todas partes. Ni los formalismos ni el soporte de software estaban a la altura del trabajo. Los defensores más sensatos creen que estos métodos deben usarse en problemas que son difíciles. No se usan ampliamente en la industria, pero la adopción está aumentando. Probablemente los mejores incursiones han sido en el uso de métodos formales para verificar propiedades de seguridad de software. Algunos de mis ejemplos favoritos son el GIRAR Modelo Checker y el código de compra de George Necula.

Alejarse de la práctica y en la investigación, Microsoft's Singularidad El proyecto del sistema operativo se trata de utilizar métodos formales para proporcionar garantías de seguridad que normalmente requieren soporte de hardware. Esto a su vez conduce a un rendimiento más rápido y garantías más fuertes. Por ejemplo, en singularidad han demostrado que si un controlador de dispositivo de terceros está permitido en el sistema (lo que significa que se han demostrado condiciones de verificación básicas), entonces posiblemente no puede derribar todo ese sistema operativo, lo peor puede hacer es una manguera es propio dispositivo.

Los métodos formales aún no se usan ampliamente en la industria, pero se usan más ampliamente que hace 20 años, y dentro de 20 años se utilizarán más ampliamente. Entonces estás a prueba de futuro :-)

Answer 4

Sí, se usan, pero no ampliamente en todas las áreas. Hay más métodos que solo Hoare Logic, algunos se usan más, algunos menos, dependiendo de la idoneidad para la tarea dada. El problema común es que el software es biiiiiiig y verifica que todo es correcto es que es un problema demasiado difícil.

Por ejemplo, el Proverso del Teorema (un software que ayuda a los humanos a probar la corrección del programa) ACL2 se ha utilizado para demostrar que una cierta unidad de procesamiento de punto flotante no tiene un cierto tipo de error. Fue una gran tarea, por lo que esta técnica no es demasiado común.

La verificación del modelo, otro tipo de verificación formal, se usa bastante ampliamente hoy en día, por ejemplo, Microsoft proporciona un tipo de verificador de modelos en el kit de desarrollo del controlador y se puede usar para verificar el controlador para un conjunto de errores comunes. Los controladores de modelos también se usan a menudo para verificar los circuitos de hardware.

Las pruebas rigurosas también pueden considerarse una verificación formal: hay algunas especificaciones formales de las cuales las rutas del programa deben probarse, etc.

Answer 5

"¿Se utilizan métodos formales en la industria?"

Sí.

los assert La declaración en muchos lenguajes de programación está relacionada con métodos formales para verificar un programa.

"¿Se utilizan ampliamente los métodos formales en la industria?"

No.

"¿Se utilizan estos métodos para probar el software de la misión crítica?"

Algunas veces. Más a menudo, se utilizan para demostrar que el software es seguro. Más formalmente, se utilizan para demostrar ciertas afirmaciones relacionadas con la seguridad sobre el software.

Answer 6

Hay dos enfoques diferentes para los métodos formales en la industria.

Un enfoque es cambiar el proceso de desarrollo por completo. La notación Z y el método B mencionado están en esta primera categoría. B se aplicó al desarrollo de la línea de metro sin conductor 14 en París (si tiene la oportunidad, escalar en el carro delantero. No es frecuente que tenga la oportunidad de ver los rieles frente a usted).

Otro enfoque más incremental es preservar los procesos de desarrollo y verificación existentes y reemplazar solo una de las tareas de verificación a la vez por un nuevo método. Esto es muy atractivo, pero significa desarrollar herramientas de análisis estáticas para salir de idiomas que a menudo no son fáciles de analizar (porque no estaban diseñados para serlo). Si vas a (por ejemplo)

http://dblp.uni-trier.de/db/indices/a-tee/d/delmas:david.html

(Lo siento, solo un hipervínculo permitido para nuevos usuarios :()

Encontrará casos de aplicaciones prácticas de métodos formales para la verificación de los programas C (con analizadores estáticos Astrée, Advertir, Fluctuat, Frama-C) y el código binario (con herramientas de ABSINT GMBH).

Por cierto, dado que mencionó Hoare Logic, en la lista anterior de herramientas, solo la advertencia se basa en Hoare Logic (y Frama-C tiene un complemento de lógica de Hoare). Los otros dependen de la interpretación abstracta, una técnica diferente con un enfoque más automático.

Answer 7

Mi área de especialización es el uso de métodos formales para el análisis de código estático para mostrar que el software está libre de errores de tiempo de ejecución. Esto se implementa utilizando una técnica de métodos formales "Interpretación abstracta" conocida. La técnica esencialmente le permite probar ciertos atributos del programa AS/W. Por ejemplo, demuestre que A+B no se desbordará o x/(xy) no dará como resultado una división por cero. Una herramienta de análisis estático de ejemplo que utiliza esta técnica es Polyspace.

Con respecto a su pregunta: "¿Se utilizan ampliamente los métodos formales en la industria?" y "¿Se utilizan estos métodos para probar el software de la misión crítica?"

La respuesta es sí. Esta opinión se basa en mi experiencia y en el apoyo de la herramienta Polyspace para las industrias que dependen del uso de software integrado para controlar los sistemas críticos de seguridad, como el acelerador electrónico en un automóvil, el sistema de frenado para un tren, controlador de motores a reacción, bomba de infusión de administración de fármacos, bomba de infusión de fármacos, etc. Estas industrias usan este tipo de herramientas de métodos formales.

No creo que todo el 100% de estos segmentos de la industria estén utilizando estas herramientas, pero el uso está aumentando. Mi opinión es que las industrias aeroespaciales y automotrices lideran con la industria de dispositivos médicos rápidamente aumentando el uso.

Answer 8

Polyspace es un producto comercial AA (horriblemente caro, pero muy bueno) basado en la verificación del programa. Es bastante pragmático, ya que se escala de las 'pruebas unitarias mejoradas que probablemente encontrarán algunos errores' para 'los próximos tres años de su vida se gastarán mostrando que estos 10 archivos tienen cero defectos'.

Se basa más en la verificación negativa ('este programa no corromperá su pila') en su lugar, la verificación positiva ('Este programa hará precisamente lo que estas 50 páginas de ecuaciones dicen que lo hará').

Answer 9

Para agregar a Jorg's responder, aquí hay un entrevista con Tony Hoare. Las herramientas que Jorg se refiere, creo, son prefacios y prefijo. Ver aquí para más información.

Answer 10

Además de otros enfoques de procedimiento más, la lógica de Hoare estaba en la base de Diseño por contrato, introducido como una técnica orientada a objetos por Bertrand Meyer en Eiffel (Ver el artículo de Meyer de 1992, página 4). Si bien el diseño por contrato no es lo mismo que los métodos de verificación formales (para una cosa, DBC no demostrar Cualquier cosa hasta que se ejecute el software), en mi opinión, proporciona un uso más práctico.