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. 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

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 ]

Total de Horas: 6.

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

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

Total de Horas: 12.

Integración Curricular

Resultados de Programa (ABET)

(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.

(C) La habilidad para diseñar, implementar y evaluar procesos y sistemas computacionales.

(D) La habilidad para funcionar en equipos de trabajo.

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

(F) La habilidad para comunicarse efectivamente.

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

(H) El reconocimiento de la necesidad de, y la habilidad para, continuar con el desarrollo profesional.

(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.

Relevancia del curso con los resultados de programa

Resultados de Programa
A B C D E F G H I J K
Relevancia 1 2 1 1 1 5 5

Escala: (1) baja relevancia - (5) alta relevancia.

Integración de objetivos, contenido y metodología del curso

Resultados del Programa Indicadores de Desempeño Objetivos/Contenido del Curso Actividades de aprendizaje Instrumentos de medición
(A) Aplicación de Conocimientos (A1) Identificar los fundamentos científicos y los principios de ingeniería que rigen un proceso o sistema. (Conocimiento) Cap 1,2,3 Exposiciones del profesor, solución de ejercicios, tareas y lecturas Exámenes, proyecto y tareas
(B) Análisis de problemas y requerimientos (B1) Describir procesos de manera declarativa ignorando los detalles de su implementación. (Comprensión). (B2) Utilizar el lenguaje propio de las matemáticas, la lógica y la ingeniería para especificar requerimientos funcionales y no funcionales de un sistema o proceso. (Aplicación). (B3) Sintetizar la información, evidencias y hechos necesarios para analizar un problema. (Análisis - Síntesis). Todos Exposiciones del profesor, discusiones en clase, solución de ejercicios, tareas Exámenes, proyecto, tareas
(E) Responsabilidad profesional y ética (E1) Identificar los códigos de ética relacionados con la disciplina. (Conocimiento). Todos lecturas, tareas tareas
(G) Impactos de la computación y la ingeniería (G1) Identificar los eventos históricos y contemporáneos que la computación y la ingeniería han afectado. (Comprensión). Cap 1 Proyecto Proyecto, manejo de la notación
(I) Uso de herramientas y técnicas (I2) Utilizar herramientas de diseño, modelamiento y simulación. (Aplicación). Cap 3,4,5 Tareas, lecturas Proyecto y Tareas
(J) Modelamiento y diseño de sistemas computacionales (J2) Relacionar conceptos y principios teóricos para la resolución efectiva de un problema. (Síntesis). (J3) Combinar principios de matemáticas, computación e ingeniería para modelar una situación. (Síntesis). Todos Exposiciones del profesor, tareas, proyecto Exámenes, proyecto y tareas
(K) Desarrollo de software (K2) Implementar e integrar componentes de software respetando los criterios de diseño. (Aplicación). (K3) Establecer invariantes y propiedades de componentes de software. (Análisis). Todos Exposiciones del profesor, tareas Exámenes, proyecto y tareas

Recomendaciones del Director del Programa

Reglas del curso

Calificación y Balance de Evaluación del Curso

Instrumento Porcentaje A B C D E F G H I J K
Tareas y Talleres 15 % 6% 13% 6% 6% 13% 25% 31%
Primer Parcial 30 % 6% 13% 6% 6% 38% 31%
Segundo Parcial 30 % 6% 13% 6% 6% 38% 31%
Proyecto 25% 6% 13% 6% 6% 13% 25% 31%

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

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

Material de este semestre

 
materias/dfp.txt · Última modificación: 2016/07/26 14:27 por crueda
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki