it-swarm-es.com

Si aprendió métodos formales para el software, ¿qué tan útil lo ha encontrado?

Si ha recibido formación en el uso de métodos formales (FM) para la programación:

  • ¿Qué tan útil lo has encontrado?
  • ¿Qué implicó su formación en FM (por ejemplo, un curso, un libro)?
  • ¿Qué herramientas de FM usas?
  • ¿Qué ventajas en velocidad/calidad le ha aportado en comparación con no utilizar FM?
  • ¿Qué tipo de software creas con FM?
  • Y si no usa directamente FM ahora, ¿al menos valió la pena aprenderlo?

Tengo curiosidad por escuchar tantas experiencias/opiniones sobre FM como se puedan encontrar en esta comunidad; Estoy empezando a leer sobre ello y quiero saber más.

Antecedentes

La programación y el desarrollo/ingeniería de software son algunas de las habilidades/profesiones humanas más nuevas en la Tierra, por lo que no es sorprendente que el campo sea inmaduro, lo que se muestra en el resultado principal de nuestro campo, como un código que suele ser tardío y propenso a errores. La inmadurez de la industria también se muestra por el amplio margen (al menos 10: 1) en la productividad entre los codificadores promedio y superior. Estos hechos tristes están bien cubiertos en la literatura y presentados por libros como Código completo de Steve McConnell .

El uso de métodos formales (FM) ha sido propuesto por figuras importantes en software/CS (por ejemplo, el tardío E. Dijkstra ) para abordar (una de) las causas fundamentales de errores: la falta de rigor matemático en la programación. Dijkstra, por ejemplo, abogó por que los estudiantes desarrollen un programa y su prueba juntos .

FM parece ser mucho más frecuente en los planes de estudio de informática en Europa en comparación con los EE. UU. Pero en los últimos años, nuevos enfoques y herramientas FM "ligeras" como Alloy han atraído cierta atención. Aún así, FM está lejos de ser un uso común en la industria, y espero recibir comentarios sobre por qué.

Actualizar

A partir de ahora (14/10/2010), de las 6 respuestas a continuación, nadie ha defendido claramente el uso de FM en el trabajo del "mundo real". Tengo mucha curiosidad por saber si alguien puede y lo hará; o quizás FM realmente ilustra la división entre la academia (¡FM es el futuro!) y la industria (FM es en su mayoría inútil).

17
limist

Absolutamente inútil para cualquier cosa que no sea trivial.

Tenía un curso llamado, acertadamente, "Métodos formales" que se enfocaba en Alloy; no puedo ver el uso de eso en ningún lado. Tenía otra clase que se centró en el modelado de concurrencia con LTSA, igualmente inútil.

El problema es que la mayoría de los errores y problemas en el software (al menos en mi experiencia) surgen de la complejidad que ocurre por debajo del nivel de abstracción de esas herramientas.

8
Fishtoaster

Tengo experiencia en CSP (Comunicando Procesos Secuenciales). No es para tocar mi propia bocina, pero escribí mi tesis de maestría en Timed CSP, particularmente "compilando" especificaciones escritas en métodos formales en C++ ejecutable. Puedo decir que tengo algo de experiencia con métodos formales. Una vez que terminé mi carrera y conseguí un trabajo en la industria, no he estado usando métodos formales en absoluto. Los métodos formales son todavía demasiado teóricos para ser aplicados en la industria. Los métodos formales han encontrado alguna aplicación práctica en el área de los sistemas integrados. Por ejemplo, la NASA utiliza métodos formales en sus proyectos. Yo especularía que los métodos formales están muy lejos de ser ampliamente adoptados en la industria. Simplemente no tiene sentido escribir especificaciones de software en métodos formales y luego "interpretarlas por humanos" en el marco de su elección. El inglés simple y los diagramas funcionan mejor para eso, mientras que las pruebas unitarias y de integración han estado haciendo un buen trabajo al "verificar" la corrección del código. Creo que los métodos formales permanecerán en el mundo académico durante algún tiempo.

7
ysolik

Tomé un curso de posgrado en análisis de programas formales, donde nos enfocamos en la semántica operativa. Hice mi trabajo final sobre el esfuerzo de SEL4, revisando los métodos formales que usaron. Mi principal conclusión en términos de practicidad fue que tiene un valor marginal. No solo tienes que escribir el programa, tienes que escribir la prueba. Guau. Dos fuentes de errores. No sólo uno. Además, hubo una enorme cantidad de restricciones impuestas al código real. Es muy difícil describir formalmente una computadora física, incluido E/S.

4
Paul Nathan

Los diagramas de estado y las redes de Petri son útiles para modelar y analizar protocolos y sistemas en tiempo real. Primero ayudan a diseñar una solución. En segundo lugar, ayudan a encontrar casos de prueba para software interesante en situaciones muy específicas.

4
mouviciel

He leído algunos libros sobre métodos formales y los he aplicado. Mi reacción inmediata fue: "Vaya, estos libros me dicen cómo ser un buen programador, siempre que sea un matemático perfecto". Otra debilidad es que solo se puede probar la equivalencia con otra descripción formal. Escribir una especificación formal para un programa equivale a escribir un programa en un lenguaje de nivel superior, y no hay forma de que pueda evitar la introducción de errores en una especificación razonablemente grande.

Nunca he hecho que los métodos formales funcionen a gran escala. Pueden ser útiles para conseguir algo pequeño y complicado y para convencerme de que son correctos. De esa manera, puedo trabajar con bloques de construcción un poco más grandes y, a veces, hacer un poco más.

Una cosa que aprendí que es más útil en general es el concepto de invariante, una declaración sobre un programa y su estado que siempre es cierta. Todo lo que pueda razonar es bueno.

Como se mencionó anteriormente, no soy un matemático perfecto, por lo que mis pruebas a veces contienen errores. Sin embargo, en mi experiencia, estos tienden a ser grandes errores tontos que son fáciles de detectar y corregir.

4
David Thornley

Autodidacta TLA + el año pasado, lo he estado usando desde entonces. Es una de las primeras herramientas que uso cada vez que comienzo un proyecto. El error que comete la mayoría de las personas es que asumen que los métodos formales son un todo o nada: o no estás usando métodos formales o tienes una verificación completa. Sin embargo, hay algo entre ellos: especificación formal, donde verifica que una especificación abstracta de su proyecto no rompa sus invariantes. A diferencia de la verificación, la especificación es lo suficientemente práctica para su uso en la industria.

Los lenguajes de especificación son más expresivos que los lenguajes de programación. Por ejemplo, aquí hay una especificación PlusCal (muy) simple para un almacén de datos distribuidos:

process node \in 1..5 \* Nodes
variables online = TRUE,
          stored \in SUBSET data; \* Some set
begin 
  Transfer:
    either
      with node \in Nodes, datum \in stored do
        node.stored := node.stored \union {datum};
      end
    or \* crash
      online := FALSE;
    end either;
end process;

Este fragmento especifica cinco nodos que se ejecutan simultáneamente, ejecutando transferencias en un orden arbitrario, donde cada transferencia es una pieza arbitraria de datos a un nodo arbitrario. Además, hemos especificado que cualquier transferencia determinada puede fallar y hacer que el nodo se bloquee. ¡Y podemos simular todos estos comportamientos en el verificador de modelos TLA +! De esa manera, podemos probar que, independientemente del pedido, las tasas de falla, etc., nuestros requisitos se mantienen. Hablando de eso, agreguemos un par de requisitos. Primero, que nunca transferimos datos a un nodo fuera de línea:

[][\A node \in Nodes: ~online => UNCHANGED node.stored]_vars

En nuestra versión simplificada, el comprobador de modelos encontrará un estado de falla. También podemos especificar "cualquier dato está en al menos un nodo en línea":

\A d \in data: \E n \in Nodes: n.online /\ d \in n.stored

Que también fallará. ¡Buena suerte comprobando estos con una prueba unitaria!

La principal limitación de la especificación es que existe independientemente de su código real. Solo puede decirle que su diseño es correcto, no que lo implementó correctamente. Pero es más rápido especificar que verificar y detecta errores que son demasiado sutiles para probarlos, así que considero que vale la pena el esfuerzo. Prácticamente cualquier código que involucre concurrencia o múltiples sistemas es un buen lugar para una especificación formal.

3
Hovercouch

Solía ​​trabajar en un departamento de ICL, antes de que Fujitsu los comprara. Tenían algunos contratos grandes de tipo gubernamental que requerían ¡prueba que el software funcionaba como se anunciaba, por lo que construyeron una máquina que tomaría la especificación formal escrita en [ ~ # ~] z [~ # ~] y valide el código mientras se ejecuta, con una gran luz verde o roja para pasar/no aprobar.

Fue algo asombroso, pero, como señala el estimado @FishToaster , fue inútil para algo que no sea trivial.

1
JBRWilkinson