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

14

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

  • ¿Qué tan útil lo has encontrado?
  • ¿En qué consistió tu entrenamiento de FM (por ejemplo, un curso, un libro)?
  • ¿Qué herramientas de FM usas?
  • ¿Qué ventajas en velocidad / calidad le ha dado en comparación con no usar FM?
  • ¿Qué tipo de software creas con FM?
  • Y si no usa FM directamente ahora, ¿valió la pena aprender al menos ??

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

Fondo

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 la salida principal de nuestro campo, como un código que generalmente es 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. Tales hechos sombríos están bien cubiertos en la literatura, e introducidos 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 último < a href="http://en.wikipedia.org/wiki/Edsger_W._Dijkstra"> E. Dijkstra ) para abordar (una de) las causas principales de los errores: la falta de rigor matemático en la programación. Dijkstra, por ejemplo, abogó por que los estudiantes desarrollen un programa y sus pruebas juntos .

La FM parece ser mucho más frecuente en los currículos de CS en Europa en comparación con los EE. UU. Pero en los últimos años, nuevos enfoques y herramientas de FM "ligeras" como Alloy han atraído cierta atención. Aún así, la FM está lejos de ser un uso común en la industria, y espero algunos comentarios aquí 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 si alguien puede y lo hará; o tal vez la FM realmente ilustra la división entre la academia (¡la FM es el futuro!) y la industria (la FM es casi inútil).

    
pregunta limist 08.10.2010 - 00:51

7 respuestas

9

Absolutamente inútil para cualquier cosa no trivial.

Tuve un curso llamado, adecuadamente, "Métodos formales" que se centró en Alloy. No puedo ver cómo se usa en ninguna parte. Tuvo 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.

    
respondido por el Fishtoaster 08.10.2010 - 01:16
6

Tengo experiencia en CSP (Comunicar procesos secuenciales). No para tocar mi propia bocina, pero escribí mi tesis de maestría sobre CSP cronometrada, 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 completé mi título y obtuve 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 sistemas embebidos. 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 "interpretarlos" en el marco de su elección. El inglés simple y los diagramas funcionan mejor para eso, mientras que las pruebas de unidad e integración han estado haciendo un buen trabajo de "verificar" la exactitud del código. Creo que los métodos formales permanecerán en el mundo académico por algún tiempo .

    
respondido por el ysolik 08.10.2010 - 01:16
4

He leído algunos libros sobre métodos formales y he aplicado algunos. Mi reacción inmediata fue: "Caramba, estos libros me dicen cómo ser un buen programador, siempre y cuando sea un matemático perfecto". Otra debilidad es que solo puedes 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 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 hacer 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 detecté que es más útil en general es el concepto de invariante, una declaración sobre un programa y su estado que siempre es cierto. Cualquier cosa de la que puedas razonar es buena.

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

    
respondido por el David Thornley 08.10.2010 - 15:49
3

Tomé un curso de posgrado en análisis de programas formales, donde nos enfocamos en la semántica operacional. Hice mi trabajo final sobre el esfuerzo de seL4, revisando los métodos formales que utilizaron. Mi principal conclusión en términos prácticos 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, había una enorme cantidad de restricciones en el código real. Es muy difícil describir formalmente una computadora física, incluyendo I / O.

    
respondido por el Paul Nathan 08.10.2010 - 17:33
2

Autodidacta TLA + el año pasado, lo he estado usando desde entonces. Es una de las primeras herramientas que utilizo cada vez que comienzo un proyecto. El error que cometen la mayoría de las personas es que asumen que los métodos formales son una cosa de 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 verificas que una especificación abstracta de tu proyecto no rompa tus invariantes. A diferencia de la verificación, la especificación es lo suficientemente práctica como para usarla 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 (muy) simple de PlusCal 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 de código especifica cinco nodos que se ejecutan simultáneamente, ejecutando transferencias en un orden arbitrario, donde cada transferencia es una pieza de datos arbitraria a un nodo arbitrario. Además, hemos especificado que cualquier transferencia dada puede fallar y causar 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 orden, las tasas de falla, etc., nuestros requisitos aún se mantienen. Hablando de eso, vamos a añadir 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 verificador de modelos encontrará un estado de falla. También podemos especificar "cualquier dato dado 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 esto con una prueba de unidad!

La principal limitación de especificación es que existe independientemente de su código real. Solo puede decirle que su diseño es correcto, no que lo haya implementado correctamente. Pero es más rápido de especificar que de verificar y atrapa los errores que son demasiado sutiles para la prueba, por lo que creo que vale la pena el esfuerzo. Casi cualquier código que implique concurrencia o sistemas múltiples es un buen lugar para una especificación formal.

    
respondido por el Hovercouch 11.09.2017 - 23:04
1

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.

    
respondido por el mouviciel 08.10.2010 - 09:43
1

Antes trabajaba en un departamento en ICL, antes de que Fujitsu los comprara. Tenían algunos contratos grandes de tipo gubernamental que requerían prueba de 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 validaría el código a medida que se ejecutaba, con una gran luz verde o roja para pasar / fallar.

Fue una cosa increíble, pero, como lo señala estimado @FishToaster , fue inútil para cualquier cosa no trivial.

    
respondido por el JBRWilkinson 08.10.2010 - 10:52

Lea otras preguntas en las etiquetas