|
Curso de Postgrado: Desarrollo Formal de Software Dirigido por Modelos
Información de cursos anteriores:
Profesores:
Objetivos:
- El estudio de técnicas para la generación automática de software a partir de modelos de alto nivel,
utilizando Lenguajes de Dominio
Específico (LDEs).
- El uso de tecnologías actuales para el Desarrollo Dirigido por
Modelos, como son las basadas en el Eclipse
Modeling Framework (EMF).
- El estudio de técnicas para la
verificación y simulación de los modelos a partir de los
cuales se genera el software.
El curso está estructurado en dos partes:
- Desarrollo
Dirigido por Modelos. Se presentarán
técnicas basadas en meta-modelado para la descripción de LDEs (con sintaxis
textual o visual), la generación automática de código, la ingeniería inversa y la
transformación de modelos. Como caso particular, se usarán de manera práctica
diversas herramientas basadas en EMF: la familia de lenguajes Epsilon,
Xtext, GMF.
- Análisis
de Modelos. Se estudiarán técnicas y formalismos
de simulación (simulación discreta y Redes de Petri),
así como de verificación formal (Model Checking) de
modelos.
Evaluación:
Asistencia regular a clase (en torno al 75% de las mismas), ejercicios, y realización de un
proyecto final práctico.
Avisos:
- Publicada una lista de proyectos aquí. Todos los
estudiantes deben elegir uno antes del 14 de Noviembre.
Temario:
Parte
I: Desarrollo de Software Dirigido por Modelos
- Tema 1: Introducción al
Desarrollo de Software Dirigido por Modelos. [Transparencias]
Bibliografía:
- Stahl, T., Völter, M. "Model-Driven Software
Development". Wiley, 2006.
- Raistrick, Chris. Model driven architecture with
executable UML. Cambridge University Press. 2004.
- Página web de la
OMG sobre MDA.
Lecturas recomendadas:
Bibliografía:
- Grady Booch, James Rumbaugh, Ivar Jacobson. The Unified
Modeling
Language
User Guide. Addison-Wesley, 1999.
- Perdita Stevens, Rob Pooley. “Utilización de UML
en
Ingeniería
del Software con Objetos y Componentes”. Addison Wesley, 2002.
- Craig Larman. “Applying UML and Patterns”. Prentice Hall.
2002.
Lecturas recomendadas:
Proyectos ejemplo para la parte 2:
Bibliografía:
Bibliografía:
- Ehrig, H., Ehrig, K., Prange, U., Taentzer, G. 2006.
"Fundamentals of Algebraic Graph Transformation". Springer.
- Ehrig, H., Engels, G., Kreowski, H.-J., Rozenberg, G. 1999.
"Handbook of Graph Grammars and Computing by Graph Transformation". Vol
1. Foundations. World Scientific.
- QVT: http://www.omg.org/docs/ptc/05-11-01.pdf
- Página de Epsilon
Parte
II: Análisis de Modelos
- Tema 6: Técnicas de
simulación discreta. Transparencias
[PDF]
Bibliografía:
- Fishman, G. S. Discrete Event Simulation. Modeling,
Programming and Analysis.
Springer Series in Operations Research. 2001.
- Bernard P. Zeigler, Herbert Praehofer, and Tag Gon Kim.
Theory of Modelling
and Simulation: Integrating Discrete Event and Continuous Complex
Dynamic
Systems. Academic Press, second edition, 2000.
- Tema 7: Redes de Petri y Model Checking. Transparencias
[PDF][PDF]
Bibliografía:
- Tadao Murata. Petri nets: Properties, analysis and
applications.
Proceedings
of the IEEE, 77(4):541-580, April 1989.
- Peterson, J.L. Petri Net Theory and the Modeling of
Systems.
Prentice-Hall,
INC., Englewood Cliffs, N.J. 1981.
- Petri Nets World: http://daimi.au.dk/PetriNets/
- E. M. Clarke, O. Grumberg, D. Peled. "Model Checking".
MIT
Press.
1999.
- Emerson, E. A. “Temporal and Modal Logic”.
Handbook of
Theoretical
Computer Science, Vol B. Elsevier. 1990.
- Model Checking @ CMU: http://www-2.cs.cmu.edu/~modelcheck/
- Página web de la herramienta Spin: http://spinroot.com/
|
