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.
Al finalizar el curso los participantes podrá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.
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.
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.
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.
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.
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.
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.
A. La habilidad para aplicar conocimiento de matemáticas, ciencias e ingeniería.
B. La habilidad para diseñar y conducir experimentos así como para analizar e interpretar datos.
C. La habilidad para diseñar un sistema, componente o proceso para satisfacer necesidades deseadas dentro de restricciones realistas.
D. La habilidad para funcionar en equipos multidisciplinarios.
E. La habilidad para identificar, formular y resolver problemas de ingeniería.
F. El entendimiento de la responsabilidad profesional y ética.
G. La habilidad para comunicarse efectivamente.
H. La educación amplia y necesaria para entender los impactos de las soluciones de ingeniería en contextos globales económicos, ambientales y sociales.
I. El reconocimiento de la necesidad de, y la habilidad para, continuar el aprendizaje a lo largo de la vida.
J. El conocimiento de asuntos contemporáneos.
K. La habilidad para usar las técnicas, destrezas y herramientas modernas de ingeniería necesarias para la práctica de la ingeniería.
Resultados de Programa | ||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|
A | B | C | D | E | F | G | H | I | J | K | ||
Relevancia | 3 | 3 | 2 | 1 | 5 | 2 |
Resultados del Programa | Objetivos del Curso | Actividades de aprendizaje | Instrumentos de medición |
---|---|---|---|
A. Conocimiento técnico. | todos | Solución ejercicios | Tareas, Exámenes, proyectos |
B. Habilidades experimentales. | 3.1,3.2,3.3,3.4 | Solución de Tareas | Tareas, Exámenes, proyectos |
C. Diseño de ingeniería. | todos | Solución ejercicios | Tareas, Exámenes, proyectos |
D. Trabajo en equipo | 6.1, 6.2, 6.3, 6.4 | Solución de ejercicios | Tareas en clase |
E. Solución problemas de ingeniería. | Todos | Solución ejercicios | Tareas, Exámenes, proyecto |
F. Responsabilidad ética. | Desarrollo sin errores. Práctica de las reglas del curso | Observancia de las reglas del curso. sistemas verificados. | Tareas, Proyectos |
G. Comunicación efectiva. | 4.1, 6.1, 7 y Proyecto | Escritura de requerimientos y especificación | Proyectos, Tareas. |
H. Amplitud de conocimiento. | Lecturas, Proyecto | Proyectos | |
I. Aprendizaje de por vida. | Lecturas | Proyectos | |
J. Asuntos contemporáneos. | 4.1, 4.2, 4.3, 4.4 | Proyectos | Proyectos |
K. Uso de herramientas de ingeniería. | todos | Solución ejercicios | Exámenes, proyecto |
Porcentaje | |
---|---|
Tareas,talleres y quices | 15 % |
Proyecto 1 | 32.5 % |
Proyecto 2 | 32.5 % |
Examen | 20 % |
Está permitido el uso de notas de clase, bibliografía y calculadoras. No está permitido el uso de computadores personales ni teléfonos celulares.
Obligatoria
Salón de clase con computador y proyector.