Descripción del Curso
Un sistema es de misión crítica (o confiable) si su operación anómala puede resultar en la pérdida de vidas, afectación significativa a la propiedad o daño al medio ambiente, entre otros. Este es el caso, por ejemplo, de aparatos médicos, control de tráfico aéreo y plantas de energía. Cada día hay más sistemas de misión crítica y se pronostica que, con el paso del tiempo, sean cada vez más poderosos y esenciales.
Este curso explora varias técnicas que permiten construir rápidamente prototipos de sistemas confiables y demostrar – mecánica y matemáticamente– la confiabilidad de estos prototipos desde su diseño. En particular, este curso presenta: (i) diferentes lógicas que pueden ser usadas para especificar sistemas y propiedades, (ii) conceptos como mecanismos de composición y abstracción, (iii) lenguajes y notaciones para especificar prototipos y (iv) herramientas que apoyan en el proceso de diseño y análisis de prototipos.
En este curso se hace énfasis en ejemplos y casos de estudio tomados de aplicaciones de software reales.
Información Básica
-
Profesor:
-
Créditos: 4
-
Horas de Clase: 3/semana
-
Horas de trabajo independiente: 9 / semana
-
Prerequisitos: Ninguno
Objetivos
Al finalizar el curso los participantes podrán:
-
Indicar las propiedades de misión crítica de un sistema dado e identificar qué lógicas pueden emplearse para especificarlas.
-
Diseñar el prototipo de un sistema confiable y formular algunas de sus propiedades de misión crítica como una fórmula lógica.
-
Evaluar la validez de una propiedad de misión crítica para un prototipo usando herramientas de apoyo, explicando el resultado obtenido.
-
Explicar cuáles son las ventajas y limitaciones de algunas lógicas comúnmente usadas para especificar propiedades de sistemas.
-
Formular contraejemplos para prototipos de sistemas confiables mal diseñados.
Metodología
El curso contará con clases expositivas para explicar las técnicas, los métodos y las herramientas para diseñar y analizar prototipos de sistemas confiables a partir de casos de estudio. El participante practicará por medio de diferentes tareas y proyectos que se asignarán a lo largo del semestre.
Contenido
| Sesión | Tema | Bibliografía |
|---|---|---|
| 1 | Introducción | [1] |
| 2 | Lógica proposicional | [1] |
| 3 | Lógica de predicados | [1] |
| 4 | Lógica temporal | [1,2] |
| 5 | Propiedades de sistemas confiables | [2,4] |
| 6,7,8 | Diseño orientado por especificación | [4] |
| 9,10 | Invariantes | [3,4] |
| 11,12,13,14 | Verificación de invariantes y model checking | [4,5] |
| 15 | Abstracción y composición | [4,5] |
| 16 | Otras técnicas y herramientas |
Evaluación
| Descripción | Porcentaje |
|---|---|
| Tareas | 25% |
| Proyecto I | 25% |
| Proyecto II | 25% |
| Proyecto III | 25% |
Bibliografía
-
Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Second edition. Cambridge University Press. 2004.
-
Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag. 2012.
-
Zohar Manna and Amir Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag. 1995.
-
Jean-Raymond Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press. 2010.
-
Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn Talcott. All About Maude: A High-Performance Logical Framework. Springer-Verlag. 2007.