Métodos y empresas formales [cerrado]

Question

Entonces ...

Enseño métodos formales en ingeniería de software. También enseño "metodologías ágiles". La mayoría de la gente parece pensar que esto es contradictorio. Creo que tiene mucho sentido ... También trabajo para una empresa, donde necesitamos realmente hacer las cosas :) Aunque puedo aplicar mis puntos de habilidad ganados en la especificación " " En el día a día, mis colegas generalmente huyen de la palabra "formal".

Solía ??pensar que esto se debía a la forma intrínseca con la que aprendemos a programar: generalmente nos guiamos para encontrar una solución que funcione, no para entender el problema. Entonces pensé que esto se debía al hecho de que la mayoría de las personas en la comunidad formal no son ingenieros, sino matemáticos o informáticos. Hoy en día, me pregunto si es solo porque la comunidad de métodos formales se esconde detrás de algún tipo de "ofuscación". Ley para usar todos los símbolos disponibles de UNICODE, desarrollar activamente herramientas groseras y no estéticas, y reírse de los estándares.

Sí, me he estado moviendo de un " culparlos " a " culparnos " perspectiva ;-)

Entonces, mi pregunta es: ¿utiliza algún tipo de método formal en su empresa? ¿Los has introducido, o eran requisitos previos? ¿Qué técnicas utilizas para despejar la niebla de las matemáticas de los temores de la gente e incitarlos a usar métodos formales? ¿Qué crees que faltan en las herramientas actuales para un uso más general?

Answer 1

La clave para que las personas compren los métodos o metodologías de cualquiera es mostrarles cómo resuelve los problemas que tienen. Si pueden ver que mejorarán sus vidas, tendrá una mejor oportunidad de lograr que adopten las técnicas.

Y si no les muestra eso, quizás quiso adoptar los métodos basados ??en la filosofía en lugar de en la práctica. A menos que los demás compartan tu filosofía, entonces no vas a llegar a ningún lado. Y tal vez no deberías.

A lo largo de las décadas ha habido una gran cantidad de metodologías. Los más nuevos siempre abordan las deficiencias de los anteriores, sin embargo, los proyectos siguen teniendo problemas y fracasan. ¿Por qué? Porque las estrellas de rock que crean nuevas metodologías son estrellas de rock y han creado una nueva metodología precisamente porque entienden los problemas subyacentes y cómo aplicarlos. Los que vienen después siguen ciegamente la receta, y no funciona tan bien.

Así que creo que lo mejor es enseñar acerca de los problemas subyacentes y luego mostrar cómo varios métodos intentan tratar esos problemas. Las diferencias en empresas, proyectos y equipos son tan grandes que ninguna metodología puede aplicarse con éxito a todas las combinaciones. Aprender a elegir una herramienta adecuada y aplicarla bien es crucial.

Answer 2

Gracias por todas las contribuciones. Son muy perspicaz. Permíteme flamear un poco (aunque no lo tomes como algo personal :-)

La mayoría de las personas parece pensar que los métodos formales solo se refieren a la verificación del programa. O sistemas críticos. Esto puede ser cierto si perseguimos el cliché final: para probar que estamos haciendo el programa correctamente (v. Validación, que pregunta, como dijo un colaborador, si estamos haciendo el programa correcto).

Pero considere herramientas de búsqueda / comprobación de modelos, como Alloy. Aprender a usar una herramienta como esta requiere una cantidad de tiempo despreciable para cualquiera que esté acostumbrado a UML y OO. Aún así, puede darle una visión inmediata sobre su modelo. Por lo general, no toma más de 10 minutos encontrar un contraejemplo sobre un subconjunto lo suficientemente pequeño del modelo que uno intenta usar (y eso incluye, en primer lugar, describir el modelo en Alloy).

Tomemos como ejemplo la ingeniería de requisitos. Normalmente se dibuja mucho UML. Sin embargo, pocas personas usan OCL y muchas reglas de negocios están informalmente anotadas en lenguaje natural. ¿Por qué? ¿Restricciones de tiempo?

Ahora considere el hecho de que la mayoría solo usa su intuición para probar que un modelo es satisfactorio. De nuevo, ¿por qué? ¿Puedo tomar la misma cantidad de tiempo (probablemente incluso menos, ya que no necesito preocuparme por la estética del dibujo) para escribir ese modelo en Alloy, y solo comprobar si es satisfactorio? ¿Y qué tipo de matemáticas necesito ahora? " Predicados " ;? Nombre de fantasía para IFs y booleanos ;-) Cuantificadores? Nombres de lujo para ForEachs () ...

¿Qué pasa con los grandes sistemas de información? No necesitan ser críticos ... Solo intente analizar en su cabeza un diagrama conceptual (¡no de implementación!) Con más de 600 clases. Veo a muchas personas golpeando su cabeza en la pared con errores fáciles de cometer porque no pasaron por alguna restricción, o el modelo permite que sucedan cosas estúpidas.

El hecho es que uno no necesita utilizar enfoques formales de cabeza a cola. Por supuesto, podría probar una aplicación completa en Coq y certificar que cumple al 100% con algunas especificaciones. Este puede ser el enfoque del científico informático / matemático.

Aún así, con una filosofía GTD, ¿por qué no puedo delegar algunas tareas para la computadora y permitir que ayuden a mejorar mi desarrollo? ¿Es realmente una cuestión de "tiempo" o una simple y simple falta de habilidades técnicas y voluntad de aprender / innovar?

Answer 3

Trabajar con la línea de negocio El desarrollo de TI en una empresa significa tener que transferir el conocimiento sobre el negocio de los empresarios reales a los jefes de los desarrolladores. Si bien a mí mismo me parece que las matemáticas abstractas son uno de los mejores pasatiempos que existen, es una herramienta de comunicación terrible. Y la comunicación es de lo que se trata. Si bien es probable que tenga cierto éxito al convencer a la gente de TI de que adopte notaciones más abstractas, básicamente no tengo oportunidad con la gente de negocios.

Si bien hay algunas áreas en las que puedo ver el papel de los métodos formales en una empresa (software especializado en matemática y lógica, necesidad significativa de propiedades demostrables como software de seguridad crítica), brindan poca ayuda para cumplir con los requisitos correctos. p.ej cómo cumplir un pedido de un cliente mediante la emisión de uno o más pedidos de suministro a un conjunto de posibles proveedores externos o internos.

Creo que el jurado aún está deliberando sobre enfoques basados ??en modelos y lenguajes específicos de dominio. Creo que tendrán éxito o fracasarán en función de si proporcionan una respuesta más rápida de TI a los deseos y necesidades del lado empresarial, y si suponen que la gente de negocios tendrá que hacer un estudio significativo.

La tecnología es fácil. La comunicación es difícil. Los métodos formales pueden ayudarnos a hacer las cosas bien, pero los que he visto no hacen nada para ayudarnos a hacer las cosas correctas. (Sí, estos son clichés, pero eso es porque son ineludiblemente y dolorosamente verdaderos).

Answer 4

Estoy tomando un curso sobre 'Especificación y verificación'. Como parte de la estructura del curso estamos haciendo lo siguiente: 1. Herramientas de aprendizaje como PVS (Sistema de verificación de prototipos) http://pvs.csl.sri.com/ y SMV (Software Modeling and Verification) http: //www.cs.cmu .edu / ~ modelcheck / smv.html 2. Aparte de eso, diseccionamos accidentes que ocurrieron debido a fallas en el software. Por ejemplo - Fallo de Ariane V

Siento que los métodos formales son más aplicables a los escenarios donde el costo de falla es más que el costo de diseño. Y parece apto para usarlos en software que se usan en sistemas críticos. Supongo que se usa en aviónica, diseño de chips, etc. y la industria automotriz actual también lo está desarrollando en la práctica.

Answer 5

He intentado que las personas adopten métodos de especificación formal varias veces (Z y Alloy) y he adquirido la misma experiencia que tienen: La mayoría de las personas, aunque sienten que tienen un propósito útil, son muy incómodas al usarlas para trabajo actual.

Bastante divertido, las mismas personas están más que felices de producir diagramas UML totalmente inútiles en grandes cantidades.

Creo que hay dos razones principales para esto:

a.) Muchos desarrolladores se sienten incómodos con el nivel de abstracción requerido por un enfoque formal. El hecho de que la mayor parte de la educación matemática de nivel de entrada sea todo cálculo y matemática no discreta podría tener que ver con esto.

b.) Los métodos formales requieren un enfoque de diseño de abajo hacia arriba en el que usted diseña su modelo central desde cero y lo hace hermético y luego lo conecta a los requisitos reales del usuario al proporcionarle una interfaz. Dado que tendemos a tener requisitos para impulsar los esfuerzos de desarrollo, un enfoque de arriba hacia abajo se siente más natural, aunque a menudo conduce a modelos inconsistentes. Es como reconstruir un sótano debajo de tu casa después de que ya se haya construido.

Answer 6

Los métodos formales no tienen sentido en sistemas donde el costo de la falla es bajo.

En una aplicación web de producción, tienes múltiples cajas de front-end, múltiples cajas de back-end, múltiples cajas de base de datos; si un programa falla en cualquiera de ellas, no es un evento. El hardware es tan barato que puede construir estos sistemas por mucho menos que el costo de especificar formalmente todo su software.