Métodos formales: ¿solo una buena práctica de ingeniería? (2024)

 (brooker.co.za)
1 puntos por GN⁺ 2025-01-12 | 1 comentarios | Compartir por WhatsApp

  • Introducción

    • Marc Brooker es un ingeniero en AWS que trabaja con bases de datos y sistemas serverless, y enfatiza la importancia de los métodos formales en la ingeniería de software.

  • Importancia de los métodos formales

    • Los métodos formales son esenciales para ahorrar tiempo y costos en sistemas a gran escala, sistemas distribuidos y sistemas críticos de bajo nivel.
    • La ingeniería de software es un ejercicio de optimización de tiempo y costos.
    • Los métodos formales reducen el costo de retrabajo y permiten manejar los cambios de interfaz en etapas tempranas, aumentando la velocidad y eficiencia del desarrollo de software.

  • Alcance de aplicación de los métodos formales

    • En el software impulsado por requisitos de usuario que cambian rápidamente, el valor de los métodos formales puede ser limitado.
    • En sistemas a gran escala, distribuidos y de bajo nivel, los métodos formales reducen significativamente el retrabajo y la densidad de errores.

  • Métodos formales y herramientas

    • Los métodos formales y el razonamiento automatizado incluyen diversas herramientas, y se usan de forma útil en los sistemas cloud a gran escala de AWS.
    • Existen lenguajes de especificación como TLA+, P y Alloy, además de model checkers, herramientas de simulación determinista y lenguajes de programación conscientes de la verificación.

  • Conclusión

    • Las herramientas que ayudan a pensar en el diseño del sistema durante la etapa de diseño aceleran el desarrollo de software, reducen el riesgo y permiten desarrollar sistemas óptimos.
    • Para los ingenieros que trabajan con sistemas complejos y a gran escala, los métodos formales forman parte de las buenas prácticas de ingeniería.

Lecturas relacionadas

1 comentarios

 
GN⁺ 2025-01-12
Opiniones de Hacker News

  • La verificación formal de software depende en gran medida del tipo de software y del proceso de desarrollo. La mayoría de los proyectos de software no son compatibles con requisitos formales

    • El desarrollo y el diseño de software a menudo avanzan al mismo tiempo, pero eso no encaja bien con los métodos formales
    • Los sistemas críticos para la seguridad, como el software aeroespacial, pueden beneficiarse enormemente de la verificación formal

  • A menudo aparece la afirmación de que los métodos formales pueden resolver la complejidad del software

    • Puede resultar atractiva para quienes prefieren enfoques académicos
    • Sin embargo, faltan casos convincentes sobre cómo los métodos formales realmente resuelven problemas
    • Se insinúa que aprender herramientas como TLA permite entender su utilidad

  • Hay dos tipos principales de métodos formales: técnicas extrínsecas, separadas del código, y técnicas intrínsecas, que van junto con el código

    • Las técnicas intrínsecas operan en el nivel funcional del código, mientras que las extrínsecas analizan formalmente modelos del código
    • Actualmente estamos en una edad dorada de la investigación en métodos formales, y las técnicas intrínsecas están recibiendo más atención

  • Los métodos formales ligeros pueden mantenerse junto con la base de código y ofrecer más información que las pruebas unitarias

    • Este enfoque encaja bien con las prácticas habituales de desarrollo de software

  • La verificación formal de software sigue siendo una tarea muy difícil y solo vale la pena en casos extremos

    • Requiere conocimientos de nivel experto y, en la mayoría de los sistemas, es muy compleja
    • Aprender herramientas como Lean es difícil, pero la documentación es buena

  • Muchos artículos sobre métodos formales se sienten como generación de leads para consultores

    • Habría que esperar a que los métodos formales realmente produzcan código de alta calidad

  • Un método formal ligero es la verificación de trazas usando Linear Temporal Logic

    • Es una forma simple y potente de registrar eventos y ejecutar condiciones sobre trazas de ejecución

  • Los métodos formales modernos, como TLA+ y Alloy, son tan fáciles de aprender como Python

    • Muchos sistemas en la nube han sido verificados con estas herramientas (por ejemplo: Azure Cosmos DB, Dynamo DB, MongoDB, CockroachDB)