2.5.24 FPL/Metodologías de Desarrollo Formal

Temas:
Non Core

• Lenguajes y metodologías de especificación formal
• Demostradores de teoremas (theorem provers), asistentes de prueba (proof assistants) y lógicas
• Verificadores de restricciones (constraint checkers)
• Tipos dependientes (cuantificación universal como función dependiente, cuantificación existencial como producto dependiente)
• Especificación y descarga de pruebas (proof discharge) para sistemas de software completamente verificados usando pre/post condiciones, tipos de refinamiento (refinement types), etc.
• Modelado formal e implementación/refinamiento manual de sistemas de software.
• Uso de pruebas simbólicas (symbolic testing) y fuzzing en el desarrollo de software.
• Verificación de modelos (model checking).
• Comprensión de situaciones donde los métodos formales pueden aplicarse efectivamente y cómo estructurar el desarrollo para maximizar su valor.

Aprendizaje esperado (Learning Outcomes):
NonCore:

1. Usar técnicas de modelado formal para desarrollar y validar arquitecturas [Usar]
2. Usar lenguajes de programación asistidos por pruebas (proof assisted) para desarrollar artefactos de software completamente especificados y verificados [Usar]
3. Usar soporte de verificador y especificación en lenguajes de programación para validar formalmente propiedades del sistema [Usar]
4. Integrar herramientas de validación simbólica en un flujo de trabajo de programación [Integrar]
5. Discutir cuándo y cómo los métodos formales pueden usarse efectivamente en el proceso de desarrollo [Debatir]