Desarrollo Formal de Programas (300CIS002)

 

Información Básica

Descripción del curso

El curso busca ilustrar sobre la conveniencia de utilizar
una metodología no tradicional de modelamiento de sistemas
y desarrollo de software: el modelamiento formal
mediante el estudio de casos promueve la necesidad de asignar
el grueso del esfuerzo de modelamiento en la especificación y
el diseño, antes que en la implementación y depuración.
Se utiliza con este fin el método B, apoyado en software de
generación automática de obligaciones de prueba y de
generación automática de código en Java

Objetivos

Al finalizar el curso los estudiantes podrán:

  1. Identificar las ventajas de desarrollar software formalmente.
    1. Reconocer qué hay que verificar de un sistema
    2. Explicar el uso de las pruebas en el diseño
    3. Defender la ventaja de animar un modelo formal
  2. Argumentar por qué los métodos formales son un mecanismo de aseguramiento de la calidad del software.
    1. Contrastar verificación y “testing”
    2. Justificar la trazabilidad de los requerimientos
    3. Predecir corrección de una especificación mediante pruebas interactivas
    4. Argumentar cómo insertar métodos formales en el ciclo de desarrollo
  3. Describir formalmente sistemas completos mediante refinamiento formal.
    1. Expresar requerimientos en invariantes y eventos
    2. Indicar propiedades de seguridad y de ausencia de bloqueos
    3. Reconocer la diferencia entre modelo abstracto y refinamiento
    4. Expresar un sistema en una jerarquía de máquinas
  4. Diseñar y verificar sistemas utilizando el método Event-B.
    1. Proponer variables para representar observaciones
    2. Formular propiedades como invariantes de máquinas
    3. Reconocer constantes de un sistema
    4. Colectar constantes y sus propiedades como axiomas en los contextos
    5. Construir el modelo del sistema en Rodin
    6. Desarrollar estrategias para verificar el sistema en Rodin
  5. Integrar las obligaciones de prueba en el proceso de desarrollo de software y entender su importancia.
    1. Relacionar cada obligación con propiedades del sistema
    2. Revisar el modelo a partir de las pruebas interactivas en Rodin
    3. Formular las obligaciones de prueba de un modelo
    4. Contrastar las guardas de los eventos y el invariante, a partir de las pruebas
  6. Expresar el modelo de un sistema en una herramienta de apoyo al desarrollo formal
    1. Identificar los atributos de la herramienta que expresan cada componente del sistema
    2. Reconocer qué componen máquinas y contextos
    3. Distinguir variables, invariantes y eventos
  7. Analizar estrategias para realizar una prueba interactiva
    1. Identificar la suficiencia/insuficiencia de las hipótesis
    2. Distinguir la aplicabilidad de cada probador en Rodin
    3. Inferir cuándo es necesario agregar hipótesis
    4. Seleccionar expresiones que conviene abstraer
  8. Aplicar las pruebas interactivas para el desarrollo y la verificación de sistemas
    1. Interpretar obligaciones no descargadas con posibles fallas del modelo
    2. Emplear chequeo de modelos como verificación previa de un sistema
    3. Predecir guardas adicionales de los eventos a partir de las pruebas
  9. Modelar formalmente un programa
    1. Identificar la precondición en los contextos
    2. Relacionar la máquina abstracta a la poscondición
    3. Inferir el invariante del programa
    4. Relacionar la poscondición a obligación de prueba en el refinamiento
    5. Inferir guardas en los eventos del invariante y la poscondición
    6. Calcular el variante del sistema
    7. Experimentar mediante chequeo de modelos
  10. Construir un programa a partir de su modelo formal
    1. Generar asignaciones a partir de la inicialización
    2. Combinar eventos de avance en un ciclo
    3. Formular condiciones del ciclo a partir de eventos finales
  11. Aplicar herramientas de chequeo de modelos en el diseño
    1. Demostrar la ausencia de bloqueos mediante chequeo de modelos
    2. Descubrir violaciones a invariantes animando el modelo en la herramienta
    3. Categorizar violaciones de invariante con componentes del modelo

Evaluación

 

Contenido

Capítulo 1: Introducción

Sesión Horas de Clase Tópicos Bibliografía
1 2 Presentación del curso. Por qué fallan los sistemas [ 1,cap 1,2]
2 2 Uso de matemáticas en modelamiento de sistemas [ 9,cap 1]
3 2 Dónde integrar métodos formales de diseño [ 10,cap 1]

Total de Horas: 6.

Capítulo 2: Diseño de sistemas simples

Sesión Horas de Clase Tópicos Bibliografía
4 2 La noción de modelo: parte estática y dinámica [ 9,cap 2]
5 2 Máquinas, contextos. Un sistema simple [ 8,cap 4] [ 10,2.1-2.4]

Total de Horas: 4.

Capítulo 3: Obligaciones de prueba

Sesión Horas de Clase Tópicos Bibliografía
6 2 Qué probar de un sistema, invariantes [ 8,cap 4] [ 10,cap 5]
7 2 Prueba de inicializacón y de eventos: ejemplos [ 8,caps 1,2,3], [ 10,cap 2, cap 5]
8 2 El cálculo de secuentes. Pruebas en Rodin [ 3,cap 2] [ 10,cap 2]

Total de Horas: 6.

Capítulo 4: Refinamiento de un sistema

Sesión Horas de Clase Tópicos Bibliografía
6 2 Jerarquía de modelos. [ 10,cap 2]
7 2 Relación de la abstracción y el refinamiento. Ejemplos [ 8,caps 1,2,3], [ 10,cap 2]
8 2 Obligaciones de prueba del refinamiento [ 8,caps 1,2,3], [ 10,cap 2]
9 2 Pruebas de refinamiento en Rodin. Estrategias y Ejemplos [ 8,caps 3,4], [ 10,cap 2, cap 3]

Total de Horas: 8.

Capítulo 5: Diseño de refinamientos

Sesión Horas de Clase Tópicos Bibliografía
6 2 Invariante de encadenamiento [ 10,cap 3 ]
7 2 Refinamiento de eventos [ 10,cap 2, cap 3 ], [ 10,cap 2]
8 2 Eventos nuevos en el refinamiento [ 8,caps 3,4], [ 10,cap 2,3]
9 2 Ejemplos de diseño, pruebas, simulación en ProB [ 8,caps 3,4], [ 10,cap 2, cap 3]
10 2 Simulación y chequeo de sistemas en ProB [ 7]

Total de Horas: 10.

Capítulo 6: Patrones de diseño

Sesión Horas de Clase Tópicos Bibliografía
11 2 Qué es un patrón de diseño [ 10,cap 3 ]
12 2 Sincronización fuerte, ejemplos [ 10,cap 2, cap 3 ], [ 10,cap 2]
13 2 Sincronización débil, ejemplos 10,cap 2,3]

Total de Horas: 6.

Capítulo 7: Diseño de programas secuenciales

Sesión Horas de Clase Tópicos Bibliografía
14 2 El modelo de un programa [ 10,cap 4 ], [ 6]
15,16 4 Ejemplos de diseño formal de programas [ 7] [ 10 15.1-15.3]
17 2 Refinamiento de programas, variante e invariante [ 6] [ 10 15.4-15.9] [ 10,cap 4 ]
18,19 4 Optimizar a partir del invariante, ejemplos [ 1,cap 10]
20 2 Simular programas (“model-checking”) en ProB [ 7]
21 2 Estrategias de pruebas de programas [ 10,cap 5 ]

Total de Horas: 16.

Capítulo 8: Diseño de programas concurrentes y distribuidos

Sesión Horas de Clase Tópicos Bibliografía
22 2 Qué es diferente en programas concurrentes [ 10 cap 6]
23 2 Ejemplos de modelos de programas concurentes [ 10 cap 6 y cap 7]

Total de Horas: 4.

Bibliografía

  1. Abrial, Jean-Raymond. The B-Book. Assigning Programs to Meanings. 1a ed.
  2. Wordsworth, J.B. Software engineering with B.
  3. Huth, M.R. and Ryan,M. Logic in computer science : modelling and reasoning about systems. 1ed.
  4. MATISSE Event B Reference manual Manual
  5. Abrial, Jean-Raymond Guidelines to formal Systems Introducción
  6. Abrial, Jean-Raymond sequential program construction desarrollo de programas
  7. Rodin Project User manual manual de Rodin
  8. EventB Descripción El lenguaje de Event B (leer con cuidado el capítulo IV, de Abrial)
  9. EventB Libro (parte) y Slides de Abrial http://www.event-b.org/abook.html
  10. Abrial, Jean-Raymond. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010
  11. De eventB.org Estrategia de uso de probadores de Rodin http://wiki.event-b.org/index.php/Rodin_Provers
  12. Requerimientos en Rodin Tutorial http://pror.org/content/tutorial

Material de este semestre

Curso en Moodle

Material adicional del Curso