Show simple item record

dc.contributorOlarte Vega, Carlos Alberto
dc.creatorGómez Hernández, Carlos Eduardo
dc.date2014-06-24
dc.date.accessioned2015-07-21T17:03:39Z
dc.date.available2015-07-21T17:03:39Z
dc.identifier.citationGó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.spa
dc.identifier.urihttp://hdl.handle.net/11522/3138
dc.descriptionLos 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.spa
dc.description.abstractFormal 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.spa
dc.formatapplication/pdfspa
dc.format.extent65 p.spa
dc.languagespaspa
dc.publisherPontificia Universidad Javerianaspa
dc.relationhttp://webview.javerianacali.edu.co/cgi-olib/?oid=564605spa
dc.relation.urihttp://hdl.handle.net/11522/3261
dc.rightsEl o los autores otorgan licencia de uso parcial de la obra a favor de la Pontificia Universidad Javeriana Seccional Cali, teniendo en cuenta que en cualquier caso, la finalidad perseguida siempre será facilitar, difundir y promover el aprendizaje, la enseñanza y la investigación. Con la licencia el o los autores autorizan a la Pontificia Universidad Javeriana Seccional Cali: la publicación en formato o soporte material, de acuerdo con las condiciones internas que la Universidad ha establecido para estos efectos. La edición o cualquier otra forma de reproducción, incluyendo la posibilidad de trasladarla al sistema o entorno digital. La inclusión en cualquier otro formato o soporte como multimedia, colecciones, recopilaciones o, en general, servir de base para cualquier otra obra derivada. La comunicación y difusión al público por cualquier procedimiento o medio (impreso o electrónico). La inclusión en bases de datos y en sitios web, sean éstos onerosos o gratuitos, existiendo con ellos previo convenio perfeccionado con la Pontificia Universidad Javeriana Cali para efectos de satisfacer los fines previstos. En estos eventos, tales sitios tendrán las mismas facultades que las aquí concedidas para la referida universidad, con las mismas limitaciones y condiciones. El o los autores continúan conservando los correspondientes derechos sin modificación o restricción alguna, puesto que de acuerdo con la legislación colombiana aplicable, el acuerdo jurídico con la Pontificia Universidad Javeriana Cali, en ningún caso conlleva la enajenación del derecho de autor y de sus conexos. EL AUTOR, expresa que el artículo, folleto o libro objeto de la presente autorización es original y la elaboró sin quebrantar ni suplantar los derechos de autor de terceros, y de tal forma, el recurso electrónico aquí presentado es de su exclusiva autoría y tiene la titularidad sobre éste. PARÁGRAFO: en caso de queja o acción por parte de un tercero referente a los derechos de autor sobre el recurso electrónico en cuestión, EL AUTOR, asumirá la responsabilidad total, y saldrá en defensa de los derechos aquí autorizados; para todos los efectos, la Pontificia Universidad Javeriana Cali actúa como un tercero de buena fe.spa
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/2.5/co/*
dc.subjectFacultad de Ingenieríaspa
dc.subjectCarrera de Ingeniería de Sistemas y Computaciónspa
dc.subjectDiseño de softwarespa
dc.subjectEvent-Bspa
dc.subjectNTCCspa
dc.subjectPatrones de diseñospa
dc.titleEspecificación de patrones de diseño en event-B como procesos NTCCspa
dc.typeinfo:eu-repo/semantics/bachelorThesisspa
dc.audiencePontificia Universidad Javeriana communityspa
dc.contributor.roleConsultor de tesisspa
dc.coverageCali; Lat: 03 24 00 N degrees minutes; Lat: 3.4000 decimal degrees; Long: 076 30 00 W degrees minutes; Long: -76.5000 decimal degreesspa
dc.creator.degreeIngeniero de Sistemas y Computaciónspa
dc.publisher.facultyFacultad de Ingenieriaspa
dc.publisher.programCarrera de Ingeniería de Sistemas y Computaciónspa
dc.pubplace.cityCalispa
dc.rights.accesoAcceso abiertospa
dc.rights.accessRightsinfo:eu-repo/semantics/openAccessspa
dc.rights.ccAtribución-NoComercial-SinDerivadas 2.5 Colombia*
dc.source.bibliographicCitationJean-Raymond Abrial. Modeling in event-b, system and software engineering (1ra ed.) Cambridge University Press, 2010.spa
dc.source.bibliographicCitationDominique Cansell, Dominique M´ery, and Joris Rehm. “Time Constraint Patterns for Event B Development”. In: B. 2007, pp. 140– 154.spa
dc.source.bibliographicCitationPierre-Malo Deni´elou and Nobuko Yoshida. “Multiparty Session Types Meet Communicating Automata”. In: ESOP. Ed. by Helmut Seidl. Vol. 7211. Lecture Notes in Computer Science. Springer, 2012, pp. 194–213. isbn: 978-3-642-28868-5.spa
dc.source.bibliographicCitationThai Son Hoang, Andreas F¨urst, and Jean-Raymond Abrial. “EventB Patterns and Their Tool Support”. In: SEFM. 2009, pp. 210– 219.spa
dc.source.bibliographicCitationAlan C. Shaw Lubomir F. Bic. Operating Systems Principles (1ra ed.) Prentice-Hall/Pearson Education, 2002.spa
dc.source.bibliographicCitationMogens Nielsen, Catuscia Palamidessi, and Frank D. Valencia. “Temporal Concurrent Constraint Programming: Denotation, Logic and Applications”. In: Nord. J. Comput. 9.1 (2002), pp. 145–188.spa
dc.source.bibliographicCitationCarlos Olarte and Camilo Rueda. Communicating Systems in Event-B. Tech. rep. 2014. url: http:%20//cic.puj.edu.co/ ~caolarte/sessionB/.spa
dc.source.bibliographicCitationCarlos Olarte, Camilo Rueda, and Frank D. Valencia. “Models and emerging trends of concurrent constraint programming”. In: Constraints 18.4 (2013), pp. 535–578.spa
dc.source.bibliographicCitationVijay A. Saraswat. Concurrent Constraint Programming. MIT Press, 1993.spa
dc.source.bibliographicCitationMichael Sipser. Introduction to Theory of Computation (2nd Ed.) Thompson Course Technology, 2005.spa
dc.source.repositoryreponame:Vitela: Repositorio Institucional PUJspa
dc.source.institutioninstname:Pontificia Universidad Javeriana Cali.spa
dc.type.hasversioninfo:eu-repo/semantics/publishedVersionspa
dc.type.spaTrabajo de Gradospa


Files in this item

Thumbnail
Thumbnail
Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record

Atribución-NoComercial-SinDerivadas 2.5 Colombia
Except where otherwise noted, this item's license is described as Atribución-NoComercial-SinDerivadas 2.5 Colombia