Desarrollo Formal de Sistemas (300CIS002)

Información Básica

  • Créditos: 3
  • Horas de Clase: 5 / semana (3 horas de clase, 2 de taller)
  • Horas de trabajo independiente: 4 / semana
  • Pre-requisitos: Introducción a la Programación (300CIP001) y Lógica en Ciencias de la Computación (300CIG002)
  • Tipo de curso: Núcleo de Formación Fundamental.

Descripción del Curso

El curso busca ilustrar sobre la conveniencia de utilizar el modelamiento formal para la construcción de sistemas confiables. Mediante el estudio de casos, el curso promueve la necesidad de asignar el grueso del esfuerzo de modelamiento en la especificación, el diseño y la verificación, antes que en la implementación y depuración. Se utiliza con este fin el método Event-B, apoyado en software de generación automática de obligaciones de prueba y de generación automática de código en Java. El curso estudia también el modelamiento formal de sistemas concurrentes mediante Chequeo de Modelos (“Model-checking”), apoyado en herramientas como Spin-Promela.

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. Conocer los fundamentos teóricos de Chequeo de Modelos (“Model Checking” )
    1. Expresar el modelo de un sistema mediante estructuras de Kripke
    2. Formular propiedades de un modelo en lógicas temporales (LTL, CTL)
    3. Conocer estrategias básicas para determinar si un modelo cumple una propiedad
  11. Aplicar Chequeo de Modelos para verificar sistemas concurrentes
    1. Entender las bases de un lenguaje de modelado para concurrencia (Promela-Spin)
    2. Conocer ejemplos clásicos de chequeo de modelos en concurrencia
    3. Saber modelar un sistema concurrente simple en Promela-Spin
    4. Formular propiedades de seguridad y vivacidad de un sistema en LTL, CTL
    5. Usar herramientas (xSpin, iSpin) para verificar el modelo

Se desarrollan competencias en

(A) La habilidad para aplicar conocimientos de matemáticas, ciencias e ingeniería.

(B) La habilidad para analizar un problema e identificar los requerimientos necesarios para su definición y solución.

(E) El entendimiento de la responsabilidad profesional y ética.

(G) La habilidad para analizar los impactos de la computación y la ingeniería en las personas, organizaciones y la sociedad.

(I) La habilidad para usar las técnicas, destrezas y herramientas modernas para la práctica de la computación.

(J) La habilidad para aplicar los fundamentos y principios de las matemáticas y de la computación en el modelamiento y diseño de sistemas computacionales de manera que se demuestre comprensión de las ventajas y desventajas en las decisiones de diseño.

(K) La habilidad para aplicar los principios de diseño y desarrollo de software en la construcción de sistemas de diferente complejidad.

Contenido

Capítulo 1: Introducción

Sesión Horas teóricas Prácticas acompañadas Temas Profundidad Bibliografía
1 2 Presentación del curso. Por qué fallan los sistemas [ 1,cap 1,2]
2 2 2 Uso de matemáticas en modelamiento de sistemas [ 9,cap 1]
3 2 2 Dónde integrar métodos formales de diseño [ 10,cap 1]

Total de Horas: 10.

Sesión Horas de trabajo independiente Temas Bibliografía
1-3 8 Tareas semanales, especificación en lógica [ 9,cap 1]

Capítulo 2: Diseño de sistemas simples

Sesión Horas teóricas Prácticas acompañadas Temas Profundidad Bibliografía
4 1 La noción de modelo: parte estática y dinámica [ 9,cap 2]
5 2 2 Máquinas, contextos. Un sistema simple [ 8,cap 4] [ 10,2.1-2.4]

Total de Horas: 5.

Sesión Horas de trabajo independiente Temas Bibliografía
4,5 16 Tareas semanales, resolución de problemas en temas vistos [ 8,cap 4] [ 10,2.1-2.4]

Capítulo 3: Obligaciones de prueba

Sesión Horas teóricas Prácticas acompañadas Temas Profundidad Bibliografía
6 2 1 Qué probar de un sistema, invariantes [ 8,cap 4] [ 10,cap 5]
7 2 1 Prueba de inicializacón y de eventos: ejemplos [ 8,caps 1,2,3], [ 10,cap 2, cap 5]
8 2 2 El cálculo de secuentes. Pruebas en Rodin [ 3,cap 2] [ 10,cap 2]

Total de Horas: 10.

Sesión Horas de trabajo independiente Temas Bibliografía
6-8 8 Tareas semanales, resolución de problemas en temas vistos [1, cap. 1,2]

Capítulo 4: Refinamiento de un sistema

Sesión Horas teóricas Prácticas acompañadas Temas Profundidad Bibliografía
6 1 Jerarquía de modelos. [ 10,cap 2]
7 1 Relación de la abstracción y el refinamiento. Ejemplos [ 8,caps 1,2,3], [ 10,cap 2]
8 1 2 Obligaciones de prueba del refinamiento [ 8,caps 1,2,3], [ 10,cap 2]
9 3 2 Pruebas de refinamiento en Rodin. Estrategias y Ejemplos [ 8,caps 3,4], [ 10,cap 2, cap 3]

Total de Horas: 10.

Sesión Horas de trabajo independiente Temas Bibliografía
6-9 8 Tareas semanales, resolución de problemas en temas vistos [ 8,caps 3,4], [ 10,cap 2, cap 3]

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 teóricas Prácticas acompañadas Temas Profundidad Bibliografía
11 1 Qué es un patrón de diseño [ 10,cap 3 ]
12 1 1 Sincronización fuerte, ejemplos [ 10,cap 2, cap 3 ], [ 10,cap 2]
13 1 1 Sincronización débil, ejemplos 10,cap 2,3]

Total de Horas: 5.

Sesión Horas de trabajo independiente Temas Bibliografía
11-13 4 Tareas semanales, resolución de problemas en temas vistos 10,cap 2,3]

Capítulo 7: Diseño de programas secuenciales

Sesión Horas teóricas Prácticas acompañadas Temas Profundidad Bibliografía
14 1 El modelo de un programa [ 10,cap 4 ], [ 6]
15,16 4 3 Ejemplos de diseño formal de programas [ 7] [ 10 15.1-15.3]
17 1 1 Refinamiento de programas, variante e invariante [ 6] [ 10 15.4-15.9] [ 10,cap 4 ]

Total de Horas: 10.

Sesión Horas de trabajo independiente Temas Bibliografía
14-17 8 Tareas semanales, resolución de problemas en temas vistos [ 6] [ 10 15.4-15.9] [ 10,cap 4 ]

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

Sesión Horas teóricas Prácticas acompañadas Temas Profundidad Bibliografía
18 2 Estructuras de Kripke, modelos de sistemas [ 13 cap 1,2]
19 2 2 Lógicas temporales LTL, CTL [ 13 cap 2,3 ]
20 2 2 Satisfacción de una fórmula por un modelo, ejemplos [ 13 cap 3,4 ]
21 2 2 El lenguaje Promela-Spin, ejemplos de programas concurrentes
22,23 4 2 exclusión mutua, protocolos: verificación en Spin

Total de Horas: 20.

Sesión Horas de trabajo independiente Temas Bibliografía
18-23 16 Tareas semanales, resolución de problemas en temas vistos [ 13 cap 3,4 ]

Uso de material en exámenes

Está permitido el uso de notas de clase, bibliografía y calculadoras. No está permitido el uso de computadores personales ni teléfonos celulares.

Asistencia

Es obligatoria

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
  13. E. Clark, O. Grumberg, D. Peled Model Checking. MIT Press, 2000

Instalaciones

Salón de clase con computador y proyector. Laboratorio de Ingeniería de Sistemas y Computación.

Material de este semestre

Curso en Moodle

Material adicional del Curso