¿Los métodos formales de verificación de programas tienen un lugar en la industria?

Question

eché un vistazo en Hoare Logic en la universidad. Lo que hicimos fue realmente simple. La mayoría de lo que hice fue probar la corrección de programas simples que consistían en while bucles, if declaraciones y secuencia de instrucciones, pero nada más. ¡Estos métodos parecen muy útiles!

¿Los métodos formales se utilizan ampliamente en la industria?

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

Answer 1

Esta es una pregunta muy cercana a mi corazón (soy un investigador de la verificación de software usando lógicas formales), por lo que probablemente no te sorprenderá cuando digo que creo que estas técnicas tienen un lugar útil, y todavía no usado lo suficiente en la industria.

Existen muchos niveles de "métodos formales", así que supongo que se refiere a aquellos que descansan sobre una base matemática rigurosa (en lugar de, digamos, seguir un proceso de estilo de 6-Sigma). Algunos tipos de métodos formales han tenido gran éxito, siendo los sistemas de tipo un solo ejemplo. Las herramientas de análisis estático basadas en análisis de flujo de datos también son populares, la verificación de modelos es casi omnipresente en el diseño de hardware, y los modelos computacionales como Pi-Cálculo y CCS parecen inspirar algún cambio real en el diseño de lenguaje práctico 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 tenido grandes avances en la industria; esto es por más razones de las que puedo enumerar, pero sospecho que es sobre todo la complejidad de escribir y luego probar especificaciones para programas reales (tienden a grande, y no se pueden expresar las propiedades de muchos entornos del mundo real). Diversos subcampos en este tipo de razonamiento ahora están haciendo grandes avances en estos problemas: la lógica de separación es uno.

Esto es parte de la naturaleza de la investigación en curso (difícil). Pero debo confesar que nosotros, como teóricos, no hemos logrado educar a la industria sobre por qué nuestras técnicas son útiles, para mantenerlas relevantes para las necesidades de la industria, y para que sean accesibles para los desarrolladores de software. En cierto nivel, ese no es nuestro problema: somos investigadores, a menudo matemáticos, y el uso práctico no está en nuestras mentes. Además, las técnicas que se están desarrollando a menudo son demasiado embrionarias para su uso en sistemas a gran escala: trabajamos en programas pequeños, en sistemas simplificados, hacemos funcionar las matemáticas y seguimos adelante. Aunque no creo que compremos estas excusas: deberíamos ser más activos al impulsar nuestras ideas y obtener un ciclo de retroalimentación entre la industria y nuestro trabajo (una de las razones principales por las que volví a investigar).

Es probablemente una buena idea para mí para resucitar mi weblog, y hacer algo más puestos en estas cosas ...

Answer 2

"¿Los métodos formales se usan en la industria?"

Sí.

La declaración assert en muchos lenguajes de programación se relaciona con métodos formales para verificar un programa.

"¿Los métodos formales se utilizan ampliamente en la industria?"

Nº

"¿Estos métodos utilizados para probar el software de misión crítica?"

A veces. Con más frecuencia, se usan para demostrar que el software es seguro. Más formalmente, se usan para probar ciertas aseveraciones relacionadas con la seguridad sobre el software.

Answer 3

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 gran retraso de Windows Vista: comenzando con Vista, gran parte del núcleo es realmente verificado formalmente wrt. a ciertas propiedades como ausencia de interbloqueos, ausencia de fugas de información, etc.

Esto ciertamente no es típico, pero es probablemente la aplicación más importante de verificación de programas formales, en términos de su impacto (después de todo, casi todos los humanos ser de alguna manera, forma o forma afectada por una computadora con Windows).

Answer 4

Sí, se utilizan, pero no en todas las áreas. Hay más métodos que solo la lógica de Hoare, algunos se usan más, otros menos, dependiendo de la idoneidad para una tarea dada. El problema común es que el software es difícil y verificar que todo sea correcto todavía es un problema demasiado difícil.

Por ejemplo, theorem-prover (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 coma flotante no tiene un cierto tipo de error. Fue una gran tarea, por lo que esta técnica no es muy común.

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

Las pruebas rigurosas también pueden considerarse como una verificación formal: hay algunas especificaciones formales de las rutas de los programas que se deben probar, etc.

Answer 5

Polyspace es un producto comercial un (terriblemente caro, pero muy bueno) basada en la verificación del programa. Es bastante pragmático, en la medida en que se amplía desde 'pruebas unitarias mejoradas que probablemente encontrarán algunos errores' hasta 'los próximos tres años de su vida se utilizarán para mostrar 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 verificación positiva ('este programa hará exactamente lo que dicen estas 50 páginas de ecuaciones').

Answer 6

No puedo comentar mucho sobre el software de misión crítica, aunque sé que la industria de la aviónica usa 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 debían usarse en todas partes. Ni los formalismos ni el soporte de software estuvieron a la altura del trabajo. Los defensores más sensatos creen que estos métodos deberían usarse en problemas que son difíciles. No son ampliamente utilizados en la industria, pero la adopción va en aumento. Probablemente las mayores incursiones han sido en el uso de métodos formales para verificar propiedades de seguridad del software. Algunos de mis ejemplos favoritos son el verificador de modelo SPIN y el código de prueba de George Necula.

Al alejarse de la práctica y la investigación, el proyecto del sistema operativo Singularity de Microsoft trata sobre el uso de 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 sólidas.Por ejemplo, en singularidad han demostrado que si un controlador de dispositivo de terceros está permitido en el sistema (lo que significa que las condiciones de verificación básicas han sido probadas), entonces no es posible que derribe todo el sistema operativo – lo peor que puede hacer es manguera dispositivo propio.

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

Answer 7

Para agregar a Jorg's answer, aquí hay un interview con Tony Hoare. Las herramientas a las que se refiere Jorg, creo, son PREfast y PREfix. Ver here para más información.

Answer 8

Existen 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 que se mencionaron están en esta primera categoría. B se aplicó al desarrollo de la línea 14 del metro sin conductor en París (si tienes la oportunidad, sube al vagón delantero. No es frecuente que tengas la oportunidad de ver los raíles frente a ti).

Otro enfoque, más gradual, 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ático para los lenguajes de salida utilizados que a menudo no son fáciles de analizar (porque no fueron diseñados para ser). Si vas a (por ejemplo)

http://dblp.uni-trier.de/db/indices/a-tree/d/Delmas:David.html

(lo siento, sólo un hipervínculo permitió a los nuevos usuarios :()

encontrará ejemplos de aplicaciones prácticas de métodos formales para la verificación de C programas (con analizadores estáticos Astrée, Caveat, Fluctuat, Frama-C) y código binario (con herramientas de AbsInt GmbH).

Por cierto, ya que mencionó Hoare Logic, en la lista de herramientas anterior, solo aparece Caveat basado en la lógica Hoare (y Frama-C tiene un plug-in de lógica Hoare). Los otros r Ely en la interpretación abstracta, una técnica diferente con un enfoque más automático.

Answer 9

Además de otros enfoques más de procedimiento, la lógica de Hoare estaba en la base de Diseño por contrato, presentado como una técnica orientada a objetos por Bertrand Meyer en Eiffel (see Meyer's article of 1992, página 4). Mientras que Design by Contract no es lo mismo que los métodos de verificación formal (por un lado, DbC no prueba nada hasta que se ejecuta el software), en mi opinión proporciona un uso más práctico.

Answer 10

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 conocida como "interpretación abstracta". La técnica esencialmente le permite probar ciertos atributos de un programa s/w. P.ej. demostrar que a + b no se desbordará o x/(x-y) no dará lugar a una división por cero. Un ejemplo de herramienta de análisis estático que utiliza esta técnica es Polyspace.

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

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

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