Show simple item record

dc.contributorTamura Morimitsu, Eugenio
dc.creatorGirón Ruiz, Juan Pablo
dc.date2014
dc.date.accessioned2018-04-10T16:55:25Z
dc.date.available2018-04-10T16:55:25Z
dc.identifier.citationGirón Ruiz, J. P. (2014, ) Modelado, prueba y verificación de sistemas distribuidos usando RTDS e IFX. Pontificia Universidad Javeriana, Cali.spa
dc.identifier.urihttp://hdl.handle.net/11522/10025
dc.descriptionGarantizar que los diseños de sistemas Hardware/Software no presenten problemas, se ha convertido en un reto cada vez mayor. El uso de técnicas formales como el Model Checking garantiza de forma exhaustiva que los sistemas satisfagan una propiedad pero no la ausencia de errores. Por otro lado, el uso de pruebas funcionales de caja negra, permite tener una noción de qué tan bien está construido el diseño del sistema, pero no es la mejor manera para valorar módulos críticos de un sistema distribuido. El presente trabajo de grado está subdivido en tres grandes partes con el objetivo de explicar una metodología para la minimización de errores que combina una técnica formal y una no formal sobre un caso de estudio que corresponde al sistema de parqueo de la Ponti cia Universidad Javeriana Cali, PUJC. Para el modelado del caso de estudio se hace uso de los diagramas de Secuencia de Mensajes, Message Sequence Message, MSC, y del lenguaje de Especi cación y Descripción, conocido como Speci cation and Description Language, SDL por sus siglas en inglés, sobre la herramienta RealTime Developer Studio RTDS de PragmaDev, al igual que la simulación y pruebas funcionales de caja negra por medio del lenguaje Testing and Test Control Notation version 3 (TTCN-3). Por otra parte, se hace uso de la técnica de Model Checking sobre la herramienta IFx de Verimag para veri car formalmente propiedades expresadas por observadores, sobre un módulo crítico del sistema del caso de estudio.spa
dc.description.abstractOne of the contemporary biggest challenges when designing Hardware/Software systems is guaranteeing that they are free of defects. The use of formal techniques like Model Checking allows ensuring that systems satisfy a given property because of exhaustive veri cation; however, they do not guarantee that the system has no errors. On the other hand, the use of functional black box testing, provides a notion of how well designed the system is, but this approach is not the best way to evaluate the critical modules of a distributed system. This work is subdivided into three major parts in order to explain a methodology for minimizing errors that combines two techniques, one is formal and the other one is semiformal on a case study corresponding to the parking system at the Ponti cia Universidad Javeriana Cali, PUJC. Using PragmaDev's Real Time Developer Studio (RTDS), the model was described using Message Sequence Charts (MSC) and the Speci cation and Description Language (SDL); its simulation tool and the Testing and Test Control Notation version 3 (TTCN-3) were used for black box functional testing. Finally, by using the Verimag's IF language and the IFx toolset, Model Checking techniques were applied to formally verify properties expressed by observers on a critical component of the system.spa
dc.formatapplication/pdfspa
dc.format.extent149 páginasspa
dc.languagespaspa
dc.publisherPontificia Universidad Javerianaspa
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.subjectPrograma Ingeniería Electrónicaspa
dc.subjectModelado de sistemas distribuidosspa
dc.subjectPruebas funcionalesspa
dc.subjectModel Chechingspa
dc.subjectVerificación formal SDL, MSC, TTCN-3, IFspa
dc.subjectHerramientas IFXspa
dc.titleModelado, prueba y verificación de sistemas distribuidos usando RTDS e IFXspa
dc.typeinfo:eu-repo/semantics/bachelorThesisspa
dc.audiencePontificia Universidad Javeriana communityspa
dc.audienceResearchsspa
dc.audienceJournalistsspa
dc.audienceOtherspa
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 Electrónicospa
dc.creator.emailjpgironruiz@gmail.comspa
dc.publisher.facultyIngenieríaspa
dc.publisher.programIngeniería Electrónicaspa
dc.pubplace.cityCalispa
dc.pubplace.stateValle del Caucaspa
dc.rights.accesoAcceso abiertospa
dc.rights.accessRightsinfo:eu-repo/semantics/openAccessspa
dc.rights.ccAtribución-NoComercial-SinDerivadas 2.5 Colombia*
dc.source.bibliographicCitationPaul Ammann and Je O utt. Introduction to Software Testing. Cambridge University Press, 1 edition, 2008.spa
dc.source.bibliographicCitationLehtmets Andrus and Anna Rannaste. TTCN-3 Basic Introduction. pages 1 17, 2011.spa
dc.source.bibliographicCitationJaime Arias. Model Checking for tcc Calculus. Technical report, Programa de Ingeniería Electrónica, Ponti cia Universidad Javeriana Cali, Cali, 2012.spa
dc.source.bibliographicCitationJ.P. Bowen, K. Bogdanov, J.A. Clark, M. Harman, R.M. Hierons, and P. Krause. FORTEST: formal methods and testing. In Proceedings 26th Annual International Computer Software and Applications, pages 91 101. IEEE Comput. Soc, 2002.spa
dc.source.bibliographicCitationMarius Bozga, Susanne Graf, Ober Ileana, Ober Iulian, and Sifakis Joseph. Formal Methods for the Design of Real-Time Systems, volume 3185 of Lecture Notes in Computer Science. Springer Berlin Heidelberg, Berlin, Heidelberg, 2004.spa
dc.source.bibliographicCitationMarius Bozga, Susanne Graf, Ileana Ober, Iulian Ober, and Joseph Sifakis. Tools and Applications II: The IF Toolset. In Bernardo, Marco; Corradini, Flavio, editor, International School on Formal Methods for the Design of Computer, Communication, and Software Systems, volume 3185 of Lecture Notes in Computer SCience, pages 237 267, Bertinoro, Italy, September 2004. Springer.spa
dc.source.bibliographicCitationChristel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press, 2008.spa
dc.source.bibliographicCitationJonathan P. Bowen. The Ethics of Safety-Critical Systems. Communications of the ACM, 43:91 -97, 2000.spa
dc.source.bibliographicCitationAdolfo Bravo and Jaime Parra. Veri cación formal de Sistemas. Technical report, Programa Computación,Universidad Autonoma Metropolitana Unidad de Iztapalapa, Mexico, 2006.spa
dc.source.bibliographicCitationCoulouris, Jean Dollimore, and Tim Kindberg. Distributed Systems: Concepts and Design. Addison Wesley; 4 edition, 2005.spa
dc.source.bibliographicCitationEdmund M. Clarke and Jeannette M. Wing. Formal methods: state of the art and future directions. ACM Computing Surveys, 28(4):626 643, December 1996.spa
dc.source.bibliographicCitationMichael Ebner. TTCN-3 Test Case Generation from Message Sequence Charts. In In Workshop on Integrated-reliability with Telecommunications and UML Languages (ISSRE04:WITUL), 2004.spa
dc.source.bibliographicCitationETSI's TTCN-3.org Editorial Team. Introduction TTCN-3. Disponible en: http:// www.ttcn-3.org/index.php/about/introduction. Accesado el día 08/05/14.spa
dc.source.bibliographicCitationLimor Fix. 25 Years of Model Checking, volume 5000 of Lecture Notes in Computer Science. Springer Berlin Heidelberg, Berlin, Heidelberg, January 2008.spa
dc.source.bibliographicCitationJens Grabowski, Dieter Hogrefe, György Réthy, Ina Schieferdecker, Anthony Wiles, and Colin Willcock. An introduction to the testing and test control notation (TTCN-3). Computer Networks, 42(3):375 403, June 2003.spa
dc.source.bibliographicCitationSusanne Graf and Guoping Jia. Veri cation Experiments on the {Mascara} Protocol. In Model Checking Software, 8th International SPIN Workshop, Toronto, Canada, May 19-20, 2001, Proceedings, volume 2057 of LNCS. Springer Verlag, May 2001.spa
dc.source.bibliographicCitationEdgardo Hames. Falluto : Un model checker para la veri cación de sistemas tolerantes a fallas. Technical report, Facultad de matemática, Astronomía y Física,Universidad Nacional de Córdoba, Cordoba, Argentina, 2009.spa
dc.source.bibliographicCitationRobert M. Hierons, Paul Krause, Gerald Lüttgen, Anthony J. H. Simons, Sergiy Vilkomir, Martin R. Woodward, Hussein Zedan, Kirill Bogdanov, Jonathan P. Bowen, Rance Cleaveland, John Derrick, Jeremy Dick, Marian Gheorghe, Mark Harman, and Kalpesh Kapoor. Using formal speci cations to support testing. ACM Computing Surveys, 41(2):1 76, February 2009.spa
dc.source.bibliographicCitationC.A.R Hoare. How Did Software Get So Reliable Without Proof ?, volume 1051 of Lecture Notes in Computer Science. Springer Berlin Heidelberg, Berlin, Heidelberg, 1996.spa
dc.source.bibliographicCitationBernard Homès. Fundamentals of Software Testing. John Wiley & Sons, Inc, 2013.spa
dc.source.bibliographicCitationIEEE Guide for Software Veri cation and Validation Plans. pages i 87, 1994.spa
dc.source.bibliographicCitationSoftware and systems engineering Software testing Part 1:Concepts and de nitions. pages 1 64, September 2013.spa
dc.source.bibliographicCitationITU-T. ITU-T Rec. Z.100 Formal description techniques (FDT) Speci cation and Description Language (SDL), 2002.spa
dc.source.bibliographicCitationThomas Kropf. Introduction to Formal Hardware Veri cation. Springer-Verlag New York, Inc., 1st edition, 1999.spa
dc.source.bibliographicCitationC lin Jebelean Marius Minea. Experience with Formal Veri cation of SDL Protocols. In Proceedings of the NATO Advanced Research Workshop on Concurrent Information Processing and Computing, pages pp. 185 -192, Romania, 2003. Al. I. Cuza University Press.spa
dc.source.bibliographicCitationIván Georgiev Mikovski, José Antonio González Martínez, and Nicolás Mon Trotti. FlexiMC Framework: framework exible para model checking. 2009.spa
dc.source.bibliographicCitationSergio Pérez and Arturo Terceros. Validación de Modelos Uando IF Toolbox. Technical report, Programa de Ingeniería Electrónica, Universidad Autónoma Metropolitana Unidad Iztapalpa, Mexico, 2006.spa
dc.source.bibliographicCitationAdriaan Michael Reniers. Message Sequence Charts Syntax and Semantics. PhD thesis, UnivesiteitsDrukkerij, Eindhoven, 1999.spa
dc.source.bibliographicCitationKlaus Schneider. Veri cation of Reactive Systems: Formal Methods and Algorithms. Springer, 2004.spa
dc.source.bibliographicCitationIna Schieferdecker. Test Automation with TTCN-3: State of the Art and a Future Perspective. In ICTSS 2010, Test Automation with TTCN-3, Natal, Brazil, 2010.spa
dc.source.bibliographicCitationBo stjan Vlaovi c, Aleksander Vre ze, Zmago Brezoçnik, and Tatjana Kapus. Veri cation of an SDL Speci cation a Case Study. Electrotechnical Review, 72:14 21, 2005.spa
dc.source.bibliographicCitationColin Willcock, Thomas Deiÿ, Stephan Tobies, Stefan Keil, Federico Engler, and Stephan Schulz. An Introduction to TTCN-3. John Wiley & Sons, second edi edition, 2011.spa
dc.source.bibliographicCitationJim Woodcock, Peter Gorm Larsen, Juan Bicarregui, and John Fitzgerald. Formal methods: Practice and experience. ACM Computing Surveys, 41(4):1 36, October 2009.spa
dc.source.repositoryVitela: Repositorio Institucional PUJspa
dc.source.institutioninstname:Pontificia Universidad Javeriana Cali.spa
dc.subject.lembModeladospa
dc.subject.lembIngeniería de Softwarespa
dc.subject.lembParqueaderos -- Métodos de simulación -- Pontificia Universidad Javeriana -- Cali (Colombia)spa
dc.subject.lembProcesamiento de datos electrónicosspa
dc.subject.lembSDL (Lenguaje de programación)spa
dc.subject.lembRTDS (Lenguaje de programación)spa
dc.type.hasversioninfo:eu-repo/semantics/publishedVersionspa
dc.type.spaTrabajo de Gradospa


Files in this item

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