Métodos Formales De Ingeniería De Software.

Intención del curso en el contexto general del plan de estudios

Es un curso de nivel avanzado en el área de ingeniería de software en donde los alumnos aprenden a valorar la utilidad de las herramientas formales en Ing. de Software, así como a usar algunas técnicas concretas y herramientas computacionales para especificar propiedades de un sistema de software y verificarlas formalmente.

Objetivo general del curso:

Al finalizar este curso el estudiante será capaz de aplicar una metodología de métodos formales para el desarrollo de software, especificar en un lenguaje formal un producto de software, especificar en un lenguaje formal (no necesariamente el mismo) las propiedades críticas de diseño de dicho software, y verificar que éste cumple las propiedades especificadas.

Competencias que desarrolla el curso:

Competencias relacionadas con conocimiento de tareas o formas de llevarlas a cabo:

C1. Ser capaz de identificar y justificar los escenarios donde la aplicación de métodos formales de software puede ser más benéfica desde el punto de vista del costo y beneficio.

C2. Ser capaz de encontrar, para un sistema de software, las propiedades -expresables matemáticamente- que pueden tener más impacto en cuanto a la calidad, seguridad o utilidad de dicho sistema.

C3. Ser capaz de modelar formalmente las características y propiedades que debe tener un sistema de software.

C4. Ser capaz de verificar formalmente que un sistema de software cumple con propiedades previamente establecidas, con ayuda de una herramienta computacional.

Competencias relacionadas con habilidades analíticas y creativas:

• Especificación formal de propiedades

• Identificación y solución de problemas

• Toma de decisiones

• Análisis de problemas

• Análisis y síntesis de información

• Análisis del costo-beneficio

TÉCNICA DIDÁCTICA: Aprendizaje basado en proyectos

El instructor del curso debe confeccionar el contenido temático, considerando el modelo que adoptará para el desarrollo formal de software. El curso contempla el estudio obligatorio de la verificación de modelos (model checking), que puede complementarse con de otra técnica más relacionada con demostración de teoremas (proof checking).

Para especificar sistemas fijos y acotados, y analizar sus condiciones (modales) temporales, se sugiere que el instructor seleccione una de las siguientes herramientas (con los métodos asociados):

• SMV, Symbolic Model Checking

• SPIN, Communicating Automata

• CADP, Process Algebras

• DESIGN/CPN, Coloured Petri Nets

Mientras que para especificar sistemas genéricos, familias de sistemas, y analizar sus propiedades, se sugiere que el instructor seleccione una de las siguientes herramientas (con los métodos asociados):

• Isabelle, HOL, PVS, etc., Lógicas de orden mayor

• NuPRL, System F, etc., Teoría de tipos

• Otter, Vampire, SPASS, etc., Lógica de primer orden (con igualdad)

Al seleccionar estas herramientas, el instructor tiene el compromiso de cerrar el módulo 2, estudiando sólo los temas relacionados.

4. Temas y Sub-temas

1 Panorama de Métodos Formales en Ing. de Software

1.1 ¿Qué es un método formal?

1.2 Algunas aplicaciones industriales

1.3 El papel de los métodos formales en ingeniería de software

1.3.1 Procesos más rigurosos

1.3.2 Desarrollo de software usando métodos formales

1.4 Limitaciones de los métodos formales

1.5 Un panorama de los métodos formales

1.5.1 Especificación de comportamiento (autómatas, álgebra de procesos, lógica temporal, etc.)

1.5.2 Especificaciones basadas en teoría de conjuntos (notación Z, VDM, el método B, etc.)

1.5.3 Especificaciones algebraicas (tipos, tipos de datos abstractos, semántica)

1.5.4 Verificación de programas mediante aserciones (lógica de Hoare, lógica dinámica)

2 Nociones Básicas y Herramientas Matemáticas (elegir sólo las necesarias)

2.1 Revisión de conceptos matemáticos

2.1.1 Diagnóstico de lagunas en conceptos matemáticos (Teoría de Conjuntos, Relaciones y funciones, Secuencias, Lógica proposicional, Consecuencia lógica, Algebras y morfismos, Inducción matemática).

2.1.2 Plan individualizado de revisión.

2.2 Ramas de la lógica (Teoría de modelos, Teoría de demostraciones, Teoría axiomática de conjuntos y teoría de tipos, Teoría de lo computable).

2.3 Lógica Temporal.

2.4 Aplicación de la Lógica de Hoare a la prueba de programas.

2.4.1 Revisión de los conceptos de Precondiciones y postcondiciones.

2.4.2 Reglas de la lógica de Hoare.

2.4.3 Cálculo de precondiciones más débiles.

2.5 Recursividad y Puntos fijos.

2.6 Inducción matemática bien fundada

2.6.1 Puntos fijos

3 Especificación de Sistemas de Software y de sus propiedades

3.1 Enfoques de especificación de un sistema (comportamiento, estructura (algebraico), etc.)

3.2 Descripción de sistemas mediante autómatas, procesos, tipos, funciones, relaciones, lenguaje imperativo, etc.)

3.3 Sintaxis del lenguaje de especificación

3.4 Semántica del lenguaje de especificación

3.5 Especificando con lógica temporal

3.5.1 Propiedades de calidad de alcance (“reachability properties”)

3.5.1.1 Cálculo del grafo de calidad de alcance

3.5.2 Propiedades de salvedad (“safety properties”)

3.5.2.1 Definición

3.5.2.2 Salvedad en la práctica

3.5.2.3 El método de variables de historia

3.5.3 Propiedades de vivacidad (“liveness properties”)

3.5.3.1 Vivacidad en el modelo o en la propiedad

3.5.3.2 Verificación bajo hipótesis de vivacidad

3.5.3.3 Vivacidad acotada

3.5.4 Propiedad de sin inter-bloqueos (“deadlock-freeness”)

3.5.4.1 Sin inter-bloqueos vs salvedad, vivacidad

3.5.4.2 Sin inter-bloqueos en combinación con abstracción

...