- En sistemas grandes, distribuidos y críticos de bajo nivel, los métodos formales no deben verse como un paso adicional solo para la corrección, sino como una práctica de ingeniería que reduce tiempo y costos
- En software, el diseño y la implementación se mezclan fácilmente, por lo que una corrección tardía del diseño se traduce de inmediato en retrabajo de implementación y costos por cambios de API
- Si se revisan en detalle el comportamiento y las interfaces antes de implementar, se puede reducir la densidad de bugs y los problemas posteriores a producción, y llegar más rápido a un diseño correcto
- En áreas donde los requisitos de usuario cambian rápido o que son difíciles de formalizar, como la UI, la documentación o la lógica de precios, la utilidad de un diseño formal previo y total puede ser menor
- Herramientas como TLA+ y P también pueden usarse para revisar optimizaciones y restricciones en la etapa de diseño, ayudando a reducir los trade-offs entre corrección y rendimiento
Métodos formales como buena práctica de ingeniería
- Los métodos formales son una parte importante de las buenas prácticas de ingeniería de software
- Tienen especial valor para ingenieros que trabajan con sistemas a gran escala, sistemas distribuidos y sistemas críticos de bajo nivel
- Se parte de la premisa de que la ingeniería, en última instancia, busca optimizar tiempo y costos
- También se consideran rendimiento, escalabilidad, sostenibilidad y eficiencia
- Los métodos formales no son baratos ni fáciles, y tampoco encajan bien en todas las formas de desarrollo, pero la intuición de que solo aumentan costos no siempre es correcta
Dos caminos para reducir costos
- El primero es reducir el retrabajo
- A diferencia de otras ramas de la ingeniería, en software el diseño y la construcción pueden ocurrir al mismo tiempo con facilidad
- Es posible empezar a implementar incluso cuando el diseño aún no está suficientemente avanzado
- Esa flexibilidad es una fortaleza del software, pero también puede convertir iteraciones de diseño en iteraciones de implementación, elevando el costo
- El segundo es gestionar el costo del cambio
- Cuando una API o un sistema ya tiene clientes, cambiarlo se vuelve mucho más caro y difícil
- Según Hyrum’s Law, con un número suficiente de usuarios de una API, alguien terminará dependiendo de cualquier comportamiento observable, sin importar lo que diga el contrato
- Aislar el comportamiento de un sistema detrás de una API es una idea clave de la ingeniería de software, pero sigue existiendo el límite de que los usuarios pueden depender incluso de detalles de implementación
- Aunque se puede reimplementar por completo el sistema detrás de una API, la abstracción no elimina por sí sola el costo del cambio
- El trabajo de diseño formal puede reducir el costo de retrabajo y permitir tratar antes los cambios de interfaz, aumentando la velocidad y la eficiencia de la construcción de software
Sistemas donde el diseño formal encaja bien
- No se aplica de la misma manera a todo el software
- En software con muchos requisitos de usuario que evolucionan rápido o son difíciles de formalizar, el valor del diseño previo puede debilitarse
- Aquí entran la UI, los sitios web y la implementación de lógica de precios
- En estas áreas suele haber mucho retrabajo continuo, por lo que el costo del diseño previo puede crecer
- La idea base de Agile es avanzar en paralelo en la implementación y el levantamiento de requisitos para reducir el tiempo hasta el lanzamiento
- Permite completar la implementación incluso cuando la recopilación de requisitos sigue en curso
- En muchos casos, este desarrollo en paralelo es óptimo o una condición necesaria para poder avanzar
- En cambio, muchas partes de los sistemas grandes, distribuidos y de bajo nivel tienen requisitos bien comprendidos
- Al menos existe una porción estática suficientemente grande de requisitos
- En esos casos, el diseño formal previo puede reducir de forma considerable el retrabajo y la densidad de bugs durante la implementación y después de producción
- Cuanto más se parezcan los requisitos a leyes físicas, mayor será el valor del diseño y del diseño formal; cuanto más se parezcan a opiniones de usuarios, menor será ese valor
Límites de documentar y formalizar requisitos
- Es muy valioso dejar claros por escrito los requisitos de usuario, ya sea de forma formal o informal
- Si los requisitos no se escriben, se desperdicia tiempo y puede generarse fricción porque cada persona avanza en direcciones distintas
- Formalizar todos los requisitos humanos puede ser difícil o no ser económicamente razonable
- Requisitos estéticos de UI
- Legibilidad de la documentación
- Consistencia en los nombres de API
- Las diferencias de opinión sobre los enfoques formales también surgen de ideas distintas sobre qué son exactamente y de qué manera aportan valor
- Métodos como UML, que trasladan el código a diagramas extensos, pueden perder valor si no abordan directamente las preguntas difíciles
- Incluso un trabajo valioso puede volverse inútil si se hace con un mal enfoque o malas herramientas
Métodos formales y herramientas útiles en la práctica
- Los métodos formales y el razonamiento automatizado cubren un campo amplio y existen muchas herramientas
- El conjunto de herramientas que resultó útil en el ámbito de grandes sistemas cloud fue el siguiente
- Lenguajes de especificación y model checkers relacionados como P, TLA+ y Alloy
- Herramientas de simulación determinista como turmoil
- Se usan junto con fuzzing para explorar sistemáticamente el espacio de estados mediante pruebas
- Lenguajes de programación orientados a la verificación como Dafny y verificadores de código como Kani
- Técnicas de simulación numérica
- Métodos cercanos a lo formal como dibujar tablas de decisión, tablas de verdad y máquinas de estados explícitas en pizarras o documentos de diseño
- Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3 es un buen punto de partida para revisar métodos formales ligeros
- Verificar la implementación no es el único objetivo
- Herramientas como TLA+ y P tienen gran valor para revisar diseños de forma más rápida y concreta antes de implementar
Construir software más rápido y más veloz, más pronto
- Cuando se escribió en 2015 How Amazon Web Services Uses Formal Methods, el foco era principalmente la corrección
- Verificar propiedades de seguridad y vivacidad del diseño
- Llegar más rápido al diseño correcto
- En el caso de un equipo que usaba TLA+ para un sistema interno de gestión de locks, fue importante que habían validado optimizaciones agresivas
- Herramientas como TLA+ no solo ayudan a construir sistemas más rápido, sino también a construir sistemas más rápidos
- Permiten explorar con rapidez optimizaciones posibles
- Ayudan a encontrar las restricciones que realmente importan
- Permiten comprobar si la optimización propuesta es correcta
- En muchos casos, los métodos formales reducen los difíciles trade-offs entre corrección y rendimiento en los que los sistemas suelen caer
El valor de las herramientas usadas en la etapa de diseño
- Usar en la etapa de diseño herramientas que ayudan a pensar la arquitectura del sistema puede acelerar mucho el desarrollo de software
- Ayuda a reducir riesgos y permite construir desde el inicio sistemas mejor optimizados
- Para ingenieros que crean sistemas grandes y complejos, los métodos formales son parte de una buena práctica de ingeniería
1 comentarios
Opiniones de Hacker News
La verificación formal de software, como reconoce el texto, depende mucho del tipo de software y del proceso de desarrollo.
Para usar verificación formal hay que contar con requisitos formales sobre el comportamiento del software, pero la mayoría de los proyectos y filosofías de diseño no encajan con eso. Si el desarrollo y el diseño avanzan juntos sin tener claro siquiera qué se quiere, es difícil aplicar métodos formales. Aun así, los ámbitos que dependen de especificaciones previas, como sistemas pequeños y críticos para la seguridad, pueden obtener grandes beneficios; el software aeroespacial es un ejemplo representativo.
Hoy ya no es una técnica que requiera un doctorado o años de investigación para aprenderse, y lo mismo aplica a escribir especificaciones básicas de alto nivel. Si usas un model checker, aprendes algo sobre el sistema que estás modelando, y resulta útil incluso si solo lo usas para documentación o capacitación. La fuerza fundamental de los métodos formales está en que te obligan a pensar las cosas hasta el final. Muchos desarrolladores creen que pueden implementar algoritmos de concurrencia solo con su cabeza, un type checker y algunas pruebas unitarias, pero después de ejecutar un model checker y encontrar errores en el diseño y en sus supuestos, no queda otra que volverse más humilde. Hay muchos sistemas distribuidos más pequeños de lo que uno cree, y el espacio de estados suele ser mucho mayor de lo esperado antes de formalizarlo.
Por ejemplo, a una máquina de estados muy complicada le agregué pruebas basadas en propiedades para asegurar que, sin importar con qué entradas extrañas se llamara al endpoint, la máquina de estados interna no hiciera transiciones inválidas. Eso fue posible porque, aunque el código alrededor no tenía una especificación formal, la máquina de estados sí la tenía, y también encontré bugs sutiles que las pruebas unitarias tradicionales jamás habrían detectado.
Pero para obtener los beneficios de los métodos formales hay que comparar el comportamiento del programa con algo que no sea el propio programa, y ese algo también debe estar escrito en un lenguaje formal. Hay que entender con precisión el comportamiento deseado, pero no hace falta cubrir todo el comportamiento del software. Las pruebas unitarias automatizadas también son especificaciones formales, y ejecutarlas es un método de verificación formal. Son especificaciones y verificaciones más débiles que lo que normalmente se llama métodos formales, pero no hay una diferencia cualitativa clara ni en lo conceptual ni en la práctica. Si a un software se le pueden aplicar pruebas, es muy probable que también se le puedan aplicar métodos de especificación formal más ricos, y la relación costo-beneficio se aprende por ensayo y error, igual que al aprender a hacer pruebas.
Al final, la cuestión es cuánto más dinero y tiempo se quiere gastar para poder llamarlo “ágil”. Paradójicamente, la etapa tradicional de requisitos es la más barata de las tres opciones y también la que mejor encaja con el espíritu ágil original, porque permite converger rápido con el cliente en el momento en que el costo de cambio es más bajo: cambiar una línea de texto.
Aun así, se pueden obtener beneficios al comprobar que no se omitió ningún caso y que no hay contradicciones dentro del sistema.
Sobre los métodos formales, a menudo veo el razonamiento de “el software es grande, complejo y difícil de acertar; por lo tanto, métodos formales”.
Por un lado, me gustaría que eso fuera cierto. Soy fuerte en la forma académica de aprender, así que también me beneficiaría personalmente, y en la práctica resulta frustrante que, cuando el software realmente falla por su complejidad, uno termine buscando a tientas la causa. Pero casi nunca se muestra de forma convincente cómo los métodos formales resuelven ese problema. Este texto es mejor en cuanto señala que la mayor parte del “diseño” moderno es una pérdida de tiempo, pero no explica lo suficiente por qué TLA es mejor que UML. Suena casi como una insinuación de que, si uno invierte meses o años en TLA, alcanza una iluminación y entiende su utilidad de una manera que no puede explicarse a quienes no la han alcanzado. El cálculo o la estadística bayesiana también tienen algo de eso, así que no es imposible, pero al final uno vuelve al juicio de gerente de proyecto: “si de verdad fuera tan útil, más gente lo usaría y sus beneficios se harían evidentes por sí solos”. Si existe desde hace mucho y no se ha asentado ampliamente, es muy probable que haya una razón.
Cuando uno se encuentra con un problema difícil de razonar, termina usando algún “método”. Si se trata de un protocolo de comunicación, conviene describirlo como una máquina de estados, y TLA encaja mejor en ese nicho. Últimamente no ha habido muchos problemas que justifiquen ese nivel de esfuerzo, pero cuando aparecen, tiene un valor enorme. Con los lenguajes específicos de dominio pasa lo mismo: para evitar muchos problemas, es mucho mejor usar un framework de parser que escribir un parser propio. Hoy, la mayor parte del retrabajo viene de cambios de requisitos y de clientes que dicen “eso no es” sin saber qué quieren realmente. En parte es porque quienes hacen las solicitudes no piensan lo suficiente en las implicaciones de sus propios requisitos, pero sobre todo porque el conocimiento necesario para tomar buenas decisiones no se concentra lo suficiente en un solo lugar.
Los métodos formales son claramente una gran inversión. Aun así, aunque en general no se hayan consolidado, algunas de sus ideas sí entraron en los sistemas de tipos modernos.
La impresión que me quedó es que la rigurosidad de un verificador formal impone límites a la complejidad del diseño, aunque solo sea porque debe terminar en un tiempo y con una memoria razonables. Tal vez la verdadera victoria de exigir verificación formal sea resolver el problema de que “el software es grande, complejo y difícil de acertar” haciendo que resulte molesto manejar programas grandes y complejos.
Me gustaría ver descendientes de las pruebas basadas en propiedades que usen técnicas de SAT o TLA para reducir rápida y repetiblemente el espacio de entrada. Mediante parsing y cobertura de código, debería poder inferirse que pasar 12 a una función no puede tomar una rama distinta de pasar 11, pero que valores como -1 o 2^17 < n < 2^32 sí podrían hacerlo.
Todavía la mayoría de los proyectos de software fracasan. Esto no es un “fallo de mercado”, sino más bien simplemente “fallar al construirlo”.
Hay dos grandes ramas de métodos formales: las técnicas extrínsecas, que están separadas del código en sí y normalmente razonan sobre la especificación del código, y las técnicas intrínsecas, que se incorporan al código y razonan sobre él de forma más directa.
Históricamente, las técnicas intrínsecas como los sistemas de tipos razonaban sobre el código a nivel de función, mientras que las técnicas extrínsecas, como los verificadores de modelos decidibles tipo Spin/P, trabajaban con modelos de código descritos mediante formalismos como autómatas. Creo que ahora estamos en una edad dorada de la investigación en métodos formales, y parece haber una tendencia a preferir cada vez menos las técnicas extrínsecas frente a los métodos intrínsecos impulsados por avances en sistemas de tipos y proyectos como Verus. https://github.com/verus-lang/verus
He visto preguntas sobre cómo funcionaría esto en un lenguaje con una huella grande como Rust, pero todavía no he visto una buena respuesta. Me gustaría leer más al respecto.
Sonaba como si se dijera que las técnicas intrínsecas se prefieren porque no obligan a escribir y mantener una especificación separada, pero en la práctica no es así.
Me gusta la parte que señala los métodos formales ligeros. Mantener una colección de estrategias de proptest junto a la base de código no es una inversión mucho mayor que escribir pruebas unitarias manuales, pero da mucha mejor comprensión gracias a una cobertura amplia y a casos de falla pequeños y comprensibles.
Sobre todo, este enfoque encaja bien con las prácticas habituales de desarrollo de software. https://crates.io/crates/proptest
Sé hasta cierto punto cómo escribir buenas pruebas y el esfuerzo que requieren, pero un LLM puede crear pruebas mejores mucho más rápido que yo. Es incluso posible que haga menos trabajo a medias que yo cuando me canso de tareas repetitivas y aburridas. Si eres ingeniero de software, deberías tener el reflejo de automatizar lo que se siente repetitivo, y hoy también se genera documentación, lo que hace que se haga con más frecuencia y antes. Los LLM podrían provocar una pequeña revolución en la adopción de la verificación formal. Generar especificaciones correctas es tedioso, pero si hay suficiente contexto —código que funciona, documentación, pistas— puede ser una tarea relativamente fácil para un LLM. Si, en lugar de escribir todas las especificaciones a mano, se pueden generar y luego revisarlas, da mucha más ganas de hacerlo. Usar Rust también es una señal de que te importa la corrección, y su compilador es una de las herramientas más cercanas a demostrar que un sistema probablemente es correcto sin usar métodos formales. Es probable que sea mucho más fácil que añadir métodos formales a un lenguaje que ni siquiera tiene compilador ni tipos explícitos.
La verificación formal de software sigue siendo demasiado difícil de usar como para que valga la pena, salvo en casos extremos. En cambio, la verificación formal de hardware ya está al nivel de que no hay razón para no usarla.
Sigo intentando aprenderla, pero en la mayoría de los sistemas tienes que ser un experto del nivel de “alguien que escribió el compilador”. Por ejemplo, intenté demostrar un codificador/decodificador varint y pude con 1 o 2 bytes, pero no más allá. Al pedir ayuda, resultó deberse a detalles internos imposibles de conocer, como que dentro del compilador el bucle solo se desplegaba 5 veces. Últimamente estoy aprendiendo Lean y me gusta, pero me encuentro con documentación de este estilo: “Definitional equality includes η-equivalence…”. No intento desacreditar a Lean; al contrario, me parece que su documentación está entre las mejores de las alternativas.
Los métodos formales no tienen por qué ser complejos. El problema es que la mayoría de los métodos formales fueron diseñados como ejercicios académicos para mostrar algún tema específico que le interesaba a un profesor. TLA+ también está más cerca de haber sido diseñado para escribir papers.
Entre los métodos formales ligeros, uno que no es muy conocido pero que me gusta es la verificación de trazas usando lógica temporal lineal: https://en.m.wikipedia.org/wiki/Linear_temporal_logic
Básicamente solo necesitas registrar eventos, y en una arquitectura basada en eventos puede salirte prácticamente gratis. Luego ejecutas predicados como
Always(Locked, Implies(Eventually(Unlocked)))sobre la traza de ejecución. También puedes aplicarlo a trazas pasadas y combinarlo con pruebas de estrés o fuzzing para explorar el espacio de estados. Es simple, potente y ampliamente aplicable; no necesitas un modelo, solo predicados.Los métodos formales implican una justificación exhaustiva sobre el comportamiento del sistema. En TLA o sistemas similares, aunque se trate de una máquina de estados y no del sistema real, el resultado es una prueba de que una propiedad LTL/CTL/TLA se cumple para todos los comportamientos del sistema, es decir, para todas las trazas o árboles de trazas.
La discusión anterior fue en junio de 2024: https://news.ycombinator.com/item?id=40753989
15 Years of Formal Methods at AWS: Just Good Engineering Practice? - https://news.ycombinator.com/item?id=40283052 - mayo de 2024, 1 comentario
Demasiado lento. Planear es casi fosilizarse, y cualquier documento puede usarse como prueba en tu contra en el tribunal ágil.
La mayoría de lo que he leído sobre métodos formales se siente como generación de prospectos para consultores.
Eso en sí está bien, pero resulta desagradable cuando alguien actúa como si hubiera alcanzado la iluminación mediante los métodos formales y te dice que, si compras un paquete de capacitación para tus empleados o colegas, o si lo contratas, va a corregir tus malos hábitos de programación, incluso hábitos irresponsablemente peligrosos. Avísenme cuando los métodos formales realmente generen código de alta calidad que no pueda desviarse de la especificación.
En una especificación formal normalmente no se define ese nivel de detalle, sino el comportamiento general del sistema. Por eso una sola especificación suele corresponder a muchos programas con diferencias sutiles. Esa es también la razón por la que el código no alcanza como documentación: no se puede saber qué fue una elección intencional y qué fue accidental. El código es demasiado concreto para explicar requisitos de alto nivel. En cambio, verificar un programa contra una especificación es más factible de implementar.
Algunos defensores actuales de los métodos formales ven a quienes no los usan como “flojos” o “tontos”, y quieren presentarse como superiores porque “hacen lo correcto” o porque “dominaron un lenguaje complejo”.
Por supuesto, no son todos, y conozco gente buena, pero algunos en realidad son más bien personas de un solo truco. Si les preguntas qué otros sistemas de métodos formales aprendieron o probaron en los últimos años, dicen que están “demasiado ocupados” para aprender algo nuevo. Entre los métodos formales recientes más fáciles de usar están FizzBee, que usa un dialecto de Python y se lee como pseudocódigo; Quint, con una sintaxis más sencilla; y P, con una sintaxis familiar para usuarios de C#. El autor de este artículo también escribió alguna vez que los métodos formales solo resolvían la mitad de su problema: https://brooker.co.za/blog/2022/06/02/formal.html
Pero el problema que menciona ahí ya lo resuelve PRISM, que ni siquiera es nuevo. Brooker simplemente no quiere mirar a su alrededor ni aprender.