Introducción al Modelado de Sistemas (300IGO001)

 

Información Básica

  • Créditos: 2
  • Horas de Clase: 3 / semana
  • Horas de trabajo independiente: 3 / semana
  • Horas de Laboratorio al semestre:
  • Prerequisitos: ninguno
  • Tipo de curso: Núcleo de Formación Fundamental

Descripción del Curso

Este curso introduce nociones básicas para diseñar de manera precisa el modelo de un sistema y para razonar sobre su comportamiento. Utilizando el lenguaje de “event B” los estudiantes definen propiedades de las observaciones del sistema, junto con acciones que determinan cambios en ellas para diferentes contextos. Mediante el uso de software de animación de modelos en “event B”, los estudiantes analizan el comportamiento del sistema y verifican que respeta las propiedades esperadas.

Objetivos

Al finalizar el curso los participantes podrán:

  • Identificar las diferencias entre los modelos usados en computación y en otras disciplinas.
  • Enumerar ejemplos de problemas que las ingenierías y la computación pueden abordar.
  • Reconocer los componentes de un sistema y sus interacciones.
  • Modelar un sistema utilizando técnicas de abstracción y refinamiento.
  • Observar el comportamiento de un sistema por medio de la simulación de su modelo.
  • Establecer propiedades simples acerca del comportamiento de un sistema y verificarlas en el modelo construido.

Contenido

Capítulo 1: Introducción

Sesión Horas de Clase Tópicos Bibliografía
1 1.5 Qué es un sistema. Ejemplos de sistemas físicos. La noción de “observación”. Ejemplos de observaciones. Especificación de observaciones [3,cap I][1,cap 1] [2, cap 1] [6, Cap 1]
2 1.5 Componentes estático y dinámico de un sistema. Ejemplos simples del mundo cotidiano. Relación entre componentes estático y dinámico [1,cap 1][3, cap II, 2.1] [6, Cap 1]
3,4 3 La noción de “invariante” de un sistema. Relación entre observaciones e invariante. Qué es el “comportamiento” de un sistema. [1,cap 1][3, cap II, 2.1] [6, Cap 1]
5,6 3 Diseñar un sistema: ejemplos [1,cap 2]

Total de Horas: 9.

Capítulo 2: El lenguaje Event B

Sesión Horas de Clase Tópicos Bibliografía
7 1.5 Qué es un modelo en Event B. [1,cap 2] [3, cap II, 2]
8 1.5 Observaciones: la noción de “tipo”. Conjuntos y sus operaciones. Predicados simples [1,cap 2] [2, Part I.1, I.2] [6, Cap 1]
9 1.5 Modelar con conjuntos. Uso de las operaciones de conjuntos para establecer propiedades de las observaciones [2,Part I.2]
10 1.5 La noción de “evento”. Guarda y acción de un evento. Observaciones antes y después de un evento [1,cap 2][3, cap II.2]
11 1.5 Ejemplos de sistemas simples en Event B [1,cap 2]

Total de Horas: 7.5.

Capítulo 3: Herramienta de modelado en Event B: Rodin

Sesión Horas de Clase Tópicos Bibliografía
12 1.5 Qué es y qué permite modelar Rodin. Cómo instalar. Los “Plugins” necesarios y las funcionalidades que proveen. Práctica guiada en el laboratorio. [6, Cap. 2] [4,cap 2.1-2.3]
13 1.5 Los editores en Rodin. Contexto y máquina. Su relación con componentes en Event B. Partes constantes y variables de un modelo en Rodin. La relación “sees”. Escribir eventos en Rodin. Práctica guiada en el laboratorio. [6, Cap 2] [4,cap 2.4, 2.5] [3, Part II.2]
14,15 2 Ejemplos de modelos en Rodin. Qué es “animar” un modelo. Uso del chequeador de modelos ProB. Animación paso a paso. Verificar propiedades. Práctica guiada [6, Cap. 2] [4,cap 2.4]

Total de Horas: 5.

Capítulo 4: Diseño de sistemas: predicados sobre colecciones y aritméticos

Sesión Horas de Clase Tópicos Bibliografía
16 1.5 Los requerimientos de un sistema. Cómo especificarlos. Requerimientos en Rodin. Relacionar requerimientos y componentes del modelo. Ejemplos [5,cap 1]
17 1.5 Predicados sobre expresiones aritméticas. Modelo completo de sistemas con observaciones aritméticas. Ejemplos [1,cap 2] [2, part I.1, I.2] [4, cap 2.5]
18 1.5 Conjuntos: especificar elementos y colecciones. Pertenencia e inclusión. Especificar agregación y eliminación de elementos en colecciones. Propiedades de operaciones sobre conjuntos. Predicados sobre conjuntos. Su uso en las guardas de los eventos. Ejemplos [2, part I.1, I.2] [4, cap 2.5]
19 1.5 Conjuntos y predicados aritméticos en contextos y en máquinas. Axiomas e invariantes. Limitaciones de conjuntos simples en el diseño de sistemas. Ejemplos [2, part I.2, I.3] [4, cap 2.5]

Total de Horas: 6.

Capítulo 5: Especificar datos estructurados

Sesión Horas de Clase Tópicos Bibliografía
20 1.5 Tablas: especificación mediante relaciones. Operaciones básicas sobre relaciones en Event B. Sistemas que observan datos estructurados. Ejemplos. [2, Part I.2, I.3] [1,cap 9]
21 1.5 Tipos de relaciones. Su uso en la especificación. Notación en Event B y en Rodin. [4,cap 5-7]
22 1.5 Relaciones vs funciones. Notación y uso en especificaciones. Tipos de funciones y relación con estructuras de datos. Operaciones generales sobre funciones y relaciones. [2, Part I.2, I.3] [1,cap 9]
23 1.5 Uso de funciones en especificación de secuencias y arreglos. Relaciones y funciones en los contextos y máquinas. Modificación de relaciones en eventos. Ejemplos de diseño [1,cap 1]
24 1.5 Animación de modelos con relaciones constantes. Inicialización de relaciones: consistencia con axiomas. Ejemplos. [1,cap 2] [1,cap 3]

Total de Horas: 7.5.

Capítulo 6: Diseño jerárquico de modelos

Sesión Horas de Clase Tópicos Bibliografía
25 1.5 Estructuración de Sistemas grandes. Relación “extends” entre contextos. Relación “refines” entre máquinas. Especificación en EventB e implementación Rodin. [3,cap II.3] [1, cap 5]
25 1.5 La noción de refinamiento de un modelo. Invariante del refinamiento y su relación con la abstracción. Eventos abstractos y eventos concretos. [1,cap 5]
26 1.5 Concretar modelos mediante cadenas de refinamientos. Ilustración en Rodin. [1,cap 2, 3]
27 1.5 Acción de eventos e invariante del refinamiento. Desarrollo de los eventos a partir del invariante. Ejemplos [1,cap 2, 3]

Total de Horas: 6.

Capítulo 7: Diseño de un modelo completo

Sesión Horas de Clase Tópicos Bibliografía
28,29,30,31 6 Diseño completo de un modelo jerárquico de tamaño mediano. Implantación en Rodin. Animación en ProB [1,cap 5] [3, cap II.3]

Total de Horas: 6.

Matriculación

  1. 2011-1: 20
  2. 2010-2: 20
  3. 2010-1: 20

Recursos

Bibliografía

  1. Jean-Raymond Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press. 2010.
  2. Jean-Raymond Abrial. The B-Book, Assigning Programs to Meanings. Cambridge University Press. 2005.
  3. EventB Language. http://rodin.cs.ncl.ac.uk/deliverables/D7.pdf
  4. Rodin Hand Book. http://handbook.event-b.org/current/html/tutorial.html
  5. Requirements Specification Tutorial. http://wiki.event-b.org/index.php/Requirements_Tutorial
  6. Camilo Rueda. Introducción al Modelado de Sistemas, 2013.
    1. Capítulo 1.Cap 1
    2. Capítulo 2.Cap 2
    3. Capítulo 3.Cap 3
    4. Capítulo 4.Cap 4
    5. Capítulo 5.Cap 5

Instalaciones

Salón de clase con computador y proyector.

Material Adicional