Técnicas para diseñar y analizar prototipos de sistemas confiables

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

Porcentaje
Tareas 25%
Proyecto I 25%
Proyecto II 25%
Proyecto III 25%

Bibliografía

  1. Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Second edition. Cambridge University Press. 2004.
  2. Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag. 2012.
  3. Zohar Manna and Amir Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag. 1995.
  4. Jean-Raymond Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press. 2010.
  5. 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.
 
materias/tecnicasprototipos.txt · Última modificación: 2016/04/14 13:47 por juancmartinez
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki