4.57.4.1 SE/Métodos Formales. (14 horas) [Nivel Bloom 3]

Referencias Bibliográficas: []

Tópicos

1. Conceptos de métodos formales.
2. Lenguajes de especificación formal.
3. Model checking.
4. Especificaciones ejecutables y no ejecutables.
5. Pre-aserciones y post-aserciones.
6. Verificación formal.
7. Tools en el soporte a métodos formales.

Objetivos

1. Aplicar técnicas de verificación formal a segmentos de software con baja complejidad.
2. Discutir el rol de las técnicas de verificación formal en el contexto de la validación de software y comparar los beneficios con los de model checking.
3. Explicar los beneficios potenciales y los defectos de usar lenguajes de especificación formal.
4. Crear y evaluar pre y post-aserciones para una variedad de situaciones desde lo simple hasta lo complejo.
5. Usar un lenguaje de especificación formal común, formular la especificación de un sistema de software y demostrar los beneficios desde una perspectiva de calidad.