|
|
Profesores:
Objetivos:
El objetivo del curso es complementar los conocimientos de modelado
y simulación del alumno en formalismos aplicables al diseño
y verificación rigurosos de sistemas software, y en menor medida
de sistemas físicos. Algunos diagramas del estándar de diseño
software UML se pueden transformar en
modelos descritos en formalismos con semántica rigurosa que permiten
la simulación y la demostración de propiedades del sistema
software que estamos modelando. Un ejemplo típico es la transformación
de Statecharts a Redes de Petri para su posterior análisis y simulación
con el fin de encontrar posibles errores de diseño. Por otra parte
también se pretende proporcionar al alumno los conocimientos necesarios
para modelar sistemas complejos, es decir, sistemas compuestos de componentes
que deben describirse mediante formalismos diferentes. Para ello se introducirán
conceptos de meta-modelado, modelado multi-formalismo y modelado en múltiples
niveles de abstracción.
Temario (tentativo):
Introducción a la simulación Discreta
-
Conceptos de Modelado y Simulación discreta. Transparencias
(actualizadas 2/11/2003)
-
Visión basada en eventos. Ejemplos con grafos de Eventos.
-
Visión basada en procesos. Ejemplos con GPSS.
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.
Introducción al (meta-)modelado de Software con UML
-
Conceptos de Modelado de Software en UML Transparencias
(actualizadas 2/11/2003)
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.
-
Andreas Hennig, Rainer Wasgint. “Performance Modelling of Software Systems
in UML-Tools for the Software Developer”. ESM’2002 Proceedings, pp.:
94-99.
Introducción a las Redes de Petri. Se introducen las Redes
de Petri, las técnicas para su análisis y se presentan brevemente
sus distintas variantes. Las redes de Petri son el formalismo adecuado
para definir y comprobar rigurosamente el funcionamiento de gran variedad
de sistemas físicos y software, como protocolos de red, interfaces
de usuario, etc. Transparencias
(actualizadas 24/11/2003)
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.
-
Gianfranco Balbo. “An Introduction to Generalized Stochastic Petri Nets”
-
Petri Nets World: http://daimi.au.dk/PetriNets/
-
Curso Modelling&Simulation de Hans Vangheluwe de la Escuela de Informática
de la Universidad de McGill, Montreal, Canadá: http://moncs.cs.mcgill.ca
Gramáticas de Grafos. Las gramáticas de grafos son
un formalismo riguroso y visual para la manipulación de grafos.
Se estudiarán en relación con la especificación de
lenguajes visuales y la formalización de la semántica de
UML. Transparencias
(actualizadas 11/12/2003)
BIBLIOGRAFÍA:
-
Rozenberg, G., y otros (eds) 1997. "Handbook of Graph Grammars and Computing
by Graph Transformation". World Scientific. Volúmenes 1, 2 and 3.
-
Baresi, L. and Heckel. R, Foundations and Applications of Graph Transformation:
An introduction from a software engineering perspective. [presentacion
(pdf)].
Introducción a Model Checking. La técnica de model-checking
permite determinar si un modelo cumple cierta propiedad, expresada como
una fórmula en lógica temporal.Transparencias
(actualizadas 29/12/2003)
BIBLIOGRAFÍA:
-
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/
Modelado Multi-Paradigma.
(Meta-Modelado, Multi-Formalismo, Múltiples niveles
de abstracción). Los sistemas complejos (lógicos o físicos)
necesitan modelarse combinando diversos formalismos. En esta sección
introducimos un marco general (modelado multi-paradigma) para el modelado,
simulación y análisis de dichos sistemas.
BIBLIOGRAFÍA:
-
Vangheluwe, H. 2000. DEVS as a common denominator for multi-formalism
hybrid systems modelling. IEEE Symposium on Computer-Aided Control System
Design, pp.:129--134. IEEE Computer Society Press.
-
Sesión en el IEEE International Symposium on Computer-Aided Control
Systems Design 2000: http://www-er.df.op.dlr.de/kondisk/campam.html
-
"AToM3:
A Tool for Multi-Formalism Modelling and Meta-Modelling". Juan de Lara,
Hans Vangheluwe. Fundamental Approaches to Software Engineering - FASE'02
, in European Joint Conferences on Theory And Practice of Software - ETAPS'02
. Grenoble. France, April 2002. Lecture Notes in Computer Science, Springer
Verlag.
-
"Where do operations come from? A Multiparadigm Specification Technique".
Zave, P., Jackson, M. IEEE Transactions on Software Engineering, Vol.22,
no 7, July 1996.
-
MetaEdit+ Home Page.
LINKS RELACIONADOS:
Curso de Modelado y
Simulación de Hans
Vangheluwe en la Escuela de Informática de la Universidad de
McGill en Canadá.
Curso
de doctorado "Precise Modelling" de Duminda
Wijesekera en la Universidad George Mason, Virginia, USA.
http://www.metamodel.com/
Forma de Evaluación (tentativa):
Se propondrán artículos que el alumno deberá
leer, criticar y finalmente exponer. Además se propondrán
trabajos prácticos de modelado para complementar la visión
teórica adquirida durante el curso. En principio, los trabajos prácticos
se desarrollarán utilizando el lenguaje de programación Python,
y opcionalmente utilizando/extendiendo la herramienta de (meta-)modelado
AToM3.
|
