Introducción al Modelado de Sistemas (300IGO001)

Información Básica

  • Créditos: 2
  • Horas de trabajo acompañado: 3 / semana (1 hora de clase, 2 de taller)
  • Horas de trabajo independiente: 3 / semana
  • Pre-requisitos: Ninguno
  • Tipo de curso: Núcleo de Formación Fundamental

Descripción del Curso

En este curso se estudian nociones básicas para: (i) diseñar de manera precisa el modelo de un sistema y (ii) razonar matemáticamente sobre su comportamiento. Utilizando un lenguaje de especificación – formal y ejecutable –, 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 y de ejecución de modelos, los estudiantes analizan el comportamiento del sistema y verifican que este respeta las propiedades esperadas.

Objetivos

Al finalizar el curso los participantes podrán:

  1. Reconocer los elementos de un sistema y sus interacciones.
    1. Separar los elementos estáticos y dinámicos que conforman un sistema.
    2. Identificar propiedades de los elementos de un sistema.
    3. Distinguir cómo varían los elementos dinámicos de un sistema.
    4. Identificar condiciones necesarias, sobre los elementos de un modelo, para su evolución.
  2. Modelar un sistema utilizando técnicas de abstracción y refinamiento.
    1. Diseñar una especificación usando números para representar los elementos de un sistema.
    2. Crear nuevos conjuntos para representar los elementos de un sistema y usarlos en el diseño de especificaciones.
    3. Organizar asociaciones entre elementos de conjuntos en relaciones y funciones matemáticas.
    4. Usar el lenguaje de las matemáticas para definir condiciones sobre los elementos de un sistema.
  3. Analizar el comportamiento de un sistema por medio de la simulación de su modelo.
    1. Relacionar el cambio de los elmentos de un modelo con respecto a la dinámica del sistema asociado.
    2. Comprender cómo se han introducido errores en un modelo e inferir cómo corregirlos.
    3. Comprender cuáles son las limitaciones de las simulaciones y entender por qué no es trivial garantizar la ausencia de erroes en un modelo.
  4. Establecer propiedades simples acerca del comportamiento de un sistema y verificarlas en el modelo construido.
    1. Demostrar algorítmicamente la preservación de invariantes de un modelo, limitada a un conjunto de estados iniciales.
    2. Probar algorítmicamente la ausencia de deadlocks, limitado a un conjunto de estados iniciales.

Se desarrollan competencias en

  1. event-B (intermedio)
  2. Rodin (intermedio)

Contenido

Capítulo 1: Introducción

Sesión Horas teóricas Prácticas acompañadas Temas Profundidad Bibliografía
1 1 0.5 Qué es un sistema. Ejemplos de sistemas físicos. La noción de “observación”. Ejemplos de observaciones. Especificación de observaciones Familiaridad [3,cap 1][1,cap 1] [2, cap 1] [6, Cap 1]
2 1 0.5 Componentes estático y dinámico de un sistema. Ejemplos simples del mundo cotidiano. Relación entre componentes estático y dinámico Familiaridad [1,cap 1][3, cap 2, 2.1] [6, Cap 1]
3,4 2 1 La noción de “invariante” de un sistema. Relación entre observaciones e invariante. Qué es el “comportamiento” de un sistema. Uso [1,cap 1][3, cap 2] [6, cap 1]
5,6 2 1 Diseñar un sistema: ejemplos Familiaridad [1,cap 2]

Total de Horas: 9.

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

Total de Horas: 9.

Capítulo 2: El lenguaje Event B

Sesión Horas teóricas Prácticas acompañadas Tópicos Profundidad Bibliografía
7 1 0.5 Qué es un modelo en Event B. Evaluación [1,cap 2] [3, cap 2]
8 1 0.5 Observaciones: la noción de “tipo”. Conjuntos y sus operaciones. Predicados simples Evaluación [1,cap 2] [2,part I.1, I.2] [6, Cap 1]
9 1 0.5 Modelar con conjuntos. Uso de las operaciones de conjuntos para establecer propiedades de las observaciones Evaluación [2,Part I.2]
10 1 0.5 La noción de “evento”. Guarda y acción de un evento. Observaciones antes y después de un evento Evaluación [1,cap 2][3, cap 2.2]
11 1 0.5 Ejemplos de sistemas simples en Event B Familiaridad [1,cap 2]

Total de Horas: 7.5.

Sesión Horas de trabajo independiente Temas Bibliografía
7-11 7.5 Tareas semanales, resolución de problemas en temas vistos [1,cap 2][2,part 1][3,cap 2][6,cap 1]

Total de Horas: 7.5.

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

Sesión Horas teóricas Prácticas acompañadas Temas Profundidad Bibliografía
12 1 0.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. Familiaridad [6,cap 2] [4,cap 2.1-2.3]
13 1 0.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. Uso [6,cap 2] [4,cap 2.4, 2.5] [3,part 2.2]
14,15 2 1 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 Familiaridad [6,cap 2] [4,cap 2.4]

Total de Horas: 6.

Sesión Horas de trabajo independiente Temas Bibliografía
12-15 6 Tareas semanales, resolución de problemas en temas vistos [3,part 2][4,cap 2][6,cap 2]

Total de Horas: 6.

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

Sesión Horas teóricas Prácticas acompañadas Temas Profundidad Bibliografía
16 1 0.5 Los requerimientos de un sistema. Cómo especificarlos. Requerimientos en Rodin. Relacionar requerimientos y componentes del modelo. Ejemplos Familiaridad [5,cap 1]
17 1 0.5 Predicados sobre expresiones aritméticas. Modelo completo de sistemas con observaciones aritméticas. Ejemplos Uso [1,cap 2] [2,part I.1, I.2] [4,cap 2.5]
18 1 0.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 Evaluación [2,part I.1, I.2] [4,cap 2.5]
19 1 0.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 Evaluación [2,part I.2, I.3] [4,cap 2.5]

Total de Horas: 6.

Sesión Horas de trabajo independiente Temas Bibliografía
16-19 6 Tareas semanales, resolución de problemas en temas vistos [1,cap 2][2,part I][4,cap 2]

Total de Horas: 6.

Capítulo 5: Especificar datos estructurados

Sesión Horas teóricas Prácticas acompañadas Temas Profundidad Bibliografía
20 1 0.5 Tablas: especificación mediante relaciones. Operaciones básicas sobre relaciones en Event B. Sistemas que observan datos estructurados. Ejemplos. Uso [2,part I.2, I.3] [1,cap 9]
21 1 0.5 Tipos de relaciones. Su uso en la especificación. Notación en Event-B y en Rodin. Evaluación [4,cap 5-7]
22 1 0.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. Uso [2,part I.2, I.3] [1,cap 9]
23 1 0.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 Evaluación [1,cap 1]
24 1 0.5 Animación de modelos con relaciones constantes. Inicialización de relaciones: consistencia con axiomas. Ejemplos. Evaluación [1,cap 2,3]

Total de Horas: 7.5.

Sesión Horas de trabajo independiente Temas Bibliografía
20-24 7.5 Tareas semanales, resolución de problemas en temas vistos [1,cap 1,2,3,9][2,part I][4,cap 2,5-7]

Total de Horas: 7.5.

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

Sesión Horas teóricas Prácticas acompañadas Temas Profundidad Bibliografía
25 1 0.5 Estructuración de Sistemas grandes. Relación “extends” entre contextos. Relación de refinamiento entre máquinas. Especificación en Event-B e implementación en Rodin. Uso [3,cap 2.3] [1, cap 5]
26 1 0.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. Evaluación [1,cap 5]
27 1 0.5 Concretar modelos mediante cadenas de refinamientos. Ilustración en Rodin. Evaluación [1,cap 2,3]
28 1 0.5 Acción de eventos e invariante del refinamiento. Desarrollo de los eventos a partir del invariante. Ejemplos Evaluación [1,cap 2,3]

Total de Horas: 6.

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

Total de Horas: 6.

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

Sesión Horas teóricas Prácticas acompañadas Temas Profundidad Bibliografía
29-32 4 2 Diseño completo de un modelo jerárquico de tamaño mediano. Implantación en Rodin. Animación en ProB Evaluación [1,cap 5] [3,cap 2.3]

Total de Horas: 6.

Sesión Horas de trabajo independiente Temas Bibliografía
29-32 6 Tareas semanales, resolución de problemas en temas vistos [1,cap 5] [3,cap 2.3]

Total de Horas: 6.

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. 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, 2016.
    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. Laboratorio de Ingeniería de Sistemas y Computación.

Material de este semestre

Curso en Moodle

Material adicional del curso