Mi cuenta

Estadísticas

Especificación de patrones de diseño en event-B como procesos NTCC

Mostrar el registro completo del ítem

Título: Especificación de patrones de diseño en event-B como procesos NTCC
Autor: Gómez Hernández, Carlos Eduardo
Fecha: 2014-06-24
URI: http://hdl.handle.net/11522/3138
Resumen: Formal methods are important since they specify critical systems. Take for instance a system for assisted surgeries where we expect that each movement controlled by the system corresponds exactly to the doctor’s actions. After all, there is a life in danger. Related to software design, Event-B uses design patterns, similar to other programming languages, in order to reuse already defined models that solve well-known problems. Such patters thus ease the modeling process. NTCC is a process calculus that allows to model in a declarative manner synchronization of process along time units. The general idea of this project is to create models of design patterns in NTCC and propose one way to translate those models into an Event-B structure. For that, we proceed as follows. We propose a NTCC model of the design pattern. Then, by identifying similarities among different models, we propose a general translation from NTCC specifications into Event-B. We also propose a high level language to make more comfortable the specification of patterns. This language, as we shall see, handles different kinds of pattern specifications.
Descripción: Los métodos formales son importantes para modelar sistemas críticos, ya que con ellos se tiene una certeza del correcto funcionamiento de dichos sistemas. Por ejemplo, en el contexto de cirugías asistidas por computador, uno esperaría que cada acción del robot corresponda a la acción que el usuario (en este caso el doctor) esté realizando, después de todo, está en juego la vida de una persona. Dentro del diseño de software, Event-B usa modelos llamados patrones de diseño, y tal como se realiza en programación clásica, el reutilizar código es importante para hacer mejores programas y evitar pensar en problemas que previamente fueron resueltos. Event-B usa los patrones de diseño para reutilizar modelos que previamente han sido verificados, haciendo el proceso de modelamiento más eficiente. NTCC es un lenguaje concurrente que permite expresar de manera declarativa sincronización de procesos en diferentes unidades de tiempo. La idea general del proyecto es crear modelos de patrones de diseño en NTCC y proponer una forma de traducir dichos modelos a una estructura en Event-B. La manera para poderlo realizar es creando modelos generales de algunos patrones de diseño de dichos sistemas, modelarlos en ambos tipos de especifi- cación de sistemas, observar semejanzas y finalmente indicar una traducción generalizada sobre la especificación desde NTCC hasta Event-B. El proyecto de grado entonces explorará estos modelos, analizará sus semejanzas y propondrá un modelo de traducción entre modelos. Para realizarlo propondrá un lenguaje de alto nivel para que el diseñador le sea más sencillo especificar dichos patrones. Este lenguaje, como veremos, se puede traducir de manera simultanea a los dos tipos de especificaciones mencionados anteriormente manteniendo la estructura general del modelo que se quiere especificar. Así, la tarea del modelador resulta más sencilla utilizando el método propuesto en este trabajo de grado.
Tipo: Trabajo de Grado
Citación: Gómez Hernández, C. E. (2014, junio 24). Especificación de patrones de diseño en event-B como procesos NTCC. Pontificia Universidad Javeriana, Cali. Tomado de (http://hdl.handle.net/11522/3138).


Ficheros en el ítem

Ficheros Tamaño Formato Ver
Especificacion_patrones_diseño.pdf 666.5Kb PDF Thumbnail
Resumen y Abstract (Solo Lectura).pdf 30.71Kb PDF Thumbnail

El ítem tiene asociados los siguientes ficheros de licencia:

Este ítem aparece en la(s) siguiente(s) colección(ones)

Mostrar el registro completo del ítem

Atribución-NoComercial-SinDerivadas 2.5 Colombia Excepto si se señala otra cosa, la licencia del ítem se describe como: Atribución-NoComercial-SinDerivadas 2.5 Colombia