Combinando ejecución simbólica y verificación de modelos para reducir la sobrecarga del análisis dinámico del programa

Este documento aborda el problema de reducir la sobrecarga de supervisión del tiempo de ejecución para programas en los que se requiere una supervisión detallada de los eventos. Para ello complementamos modelar técnicas de verificación con métodos de razonamiento simbólico y mostrar que, bajo cierta...

Full description

Autores:: Cataño, Néstor

Tipo de recurso:: Trabajo de grado de pregrado

Fecha de publicación:: 2005

Institución:: Universidad Autónoma de Bucaramanga - UNAB

Repositorio:: Repositorio UNAB

Idioma:: eng

id	UNAB2_d72c076a3fe5abc0b25e50fa719bc0bd
oai_identifier_str	oai:repository.unab.edu.co:20.500.12749/9027
network_acronym_str	UNAB2
network_name_str	Repositorio UNAB
repository_id_str
dc.title.spa.fl_str_mv	Combinando ejecución simbólica y verificación de modelos para reducir la sobrecarga del análisis dinámico del programa
dc.title.translated.eng.fl_str_mv	Combining symbolic execution and model checking to reduce dynamic program analysis overhead
title	Combinando ejecución simbólica y verificación de modelos para reducir la sobrecarga del análisis dinámico del programa
spellingShingle	Combinando ejecución simbólica y verificación de modelos para reducir la sobrecarga del análisis dinámico del programa Innovaciones tecnológicas Ciencia de los computadores Desarrollo de tecnología Ingeniería de sistemas Investigaciones Tecnologías de la información y las comunicaciones TIC´s Technological innovations Computer science Technology development Systems engineering Investigations Information and communication technologies ICT's Model checking Java pathfinder Symbolic reasoning Instrumentation Monitoring Invariant strengthening Innovaciones tecnológicas Ciencias de la computación Desarrollo tecnológico Ingeniería de sistemas Investigaciones Tecnologías de la información y la comunicación Comprobación de modelo Buscador de rutas de Java Razonamiento simbólico Instrumentación Supervisión Fortalecimiento invariante
title_short	Combinando ejecución simbólica y verificación de modelos para reducir la sobrecarga del análisis dinámico del programa
title_full	Combinando ejecución simbólica y verificación de modelos para reducir la sobrecarga del análisis dinámico del programa
title_fullStr	Combinando ejecución simbólica y verificación de modelos para reducir la sobrecarga del análisis dinámico del programa
title_full_unstemmed	Combinando ejecución simbólica y verificación de modelos para reducir la sobrecarga del análisis dinámico del programa
title_sort	Combinando ejecución simbólica y verificación de modelos para reducir la sobrecarga del análisis dinámico del programa
dc.creator.fl_str_mv	Cataño, Néstor
dc.contributor.author.spa.fl_str_mv	Cataño, Néstor
dc.contributor.googlescholar.spa.fl_str_mv	Cataño, Néstor [a7qGKHwAAAAJ]
dc.contributor.orcid.spa.fl_str_mv	Cataño, Néstor [0000-0001-5015-5893]
dc.contributor.researchgate.spa.fl_str_mv	Cataño, Néstor [Nestor-Catano]
dc.subject.none.fl_str_mv	Innovaciones tecnológicas Ciencia de los computadores Desarrollo de tecnología Ingeniería de sistemas Investigaciones Tecnologías de la información y las comunicaciones TIC´s
topic	Innovaciones tecnológicas Ciencia de los computadores Desarrollo de tecnología Ingeniería de sistemas Investigaciones Tecnologías de la información y las comunicaciones TIC´s Technological innovations Computer science Technology development Systems engineering Investigations Information and communication technologies ICT's Model checking Java pathfinder Symbolic reasoning Instrumentation Monitoring Invariant strengthening Innovaciones tecnológicas Ciencias de la computación Desarrollo tecnológico Ingeniería de sistemas Investigaciones Tecnologías de la información y la comunicación Comprobación de modelo Buscador de rutas de Java Razonamiento simbólico Instrumentación Supervisión Fortalecimiento invariante
dc.subject.keywords.eng.fl_str_mv	Technological innovations Computer science Technology development Systems engineering Investigations Information and communication technologies ICT's Model checking Java pathfinder Symbolic reasoning Instrumentation Monitoring Invariant strengthening
dc.subject.lemb.spa.fl_str_mv	Innovaciones tecnológicas Ciencias de la computación Desarrollo tecnológico Ingeniería de sistemas Investigaciones Tecnologías de la información y la comunicación
dc.subject.proposal.spa.fl_str_mv	Comprobación de modelo Buscador de rutas de Java Razonamiento simbólico Instrumentación Supervisión Fortalecimiento invariante
description	Este documento aborda el problema de reducir la sobrecarga de supervisión del tiempo de ejecución para programas en los que se requiere una supervisión detallada de los eventos. Para ello complementamos modelar técnicas de verificación con métodos de razonamiento simbólico y mostrar que, bajo ciertas circunstancias, los fragmentos de código no afectan la validez de las propiedades subyacentes. Consideramos las propiedades de seguridad dadas como expresiones regulares sobre eventos generados por el programa. Además, mostramos cómo nuestro marco puede extenderse para considerar programas con ciclos. Probamos nuestra presentación con la ayuda del modelo Java PathFinder corrector [13].
publishDate	2005
dc.date.issued.none.fl_str_mv	2005-06-01
dc.date.accessioned.none.fl_str_mv	2020-10-27T00:21:13Z
dc.date.available.none.fl_str_mv	2020-10-27T00:21:13Z
dc.type.coar.fl_str_mv	http://purl.org/coar/resource_type/c_2df8fbb1
dc.type.coarversion.fl_str_mv	http://purl.org/coar/version/c_970fb48d4fbd8a85
dc.type.driver.none.fl_str_mv	info:eu-repo/semantics/article
dc.type.local.spa.fl_str_mv	Artículo
dc.type.coar.none.fl_str_mv	http://purl.org/coar/resource_type/c_7a1f
dc.type.redcol.none.fl_str_mv	http://purl.org/redcol/resource_type/CJournalArticle
format	http://purl.org/coar/resource_type/c_7a1f
dc.identifier.issn.none.fl_str_mv	2539-2115 1657-2831
dc.identifier.uri.none.fl_str_mv	http://hdl.handle.net/20.500.12749/9027
dc.identifier.instname.spa.fl_str_mv	instname:Universidad Autónoma de Bucaramanga UNAB
dc.identifier.repourl.none.fl_str_mv	repourl:https://repository.unab.edu.co
identifier_str_mv	2539-2115 1657-2831 instname:Universidad Autónoma de Bucaramanga UNAB repourl:https://repository.unab.edu.co
url	http://hdl.handle.net/20.500.12749/9027
dc.language.iso.eng.fl_str_mv	eng
language	eng
dc.relation.none.fl_str_mv	https://revistas.unab.edu.co/index.php/rcc/article/view/1069/1041
dc.relation.uri.none.fl_str_mv	https://revistas.unab.edu.co/index.php/rcc/article/view/1069
dc.relation.uri.spa.fl_str_mv	http://hdl.handle.net/20.500.12749/20373
dc.relation.references.none.fl_str_mv	B. B´erard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit L. Petrucci, Ph. Schnoebelen, and P. Mackenzie. Systems and Software Verification: Model-Checking Techniques and Tools. Springer-Verlag, 1999. E.M. Clarke, O. Grumberg, and D.A. Peled. Model Checking. MIT Press, 2000. T. Colcombet and P. Fradet. Enforcing trace properties by program transformation. In Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 54–66, 2000. C. Flanagan and S. Qadeer. Predicate abstraction for software verification. In Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 191–202. ACM Press, 2002. A.Q. Gates, S. Roach, O. Mondrag´on, and N. Delgado. DynaMICs: Comprehensive support for run-time monitoring. In K. Havelund and G. Rosu, editors, Electronic Notes in Theoretical Computer Science, volume 55. Elsevier, 2001. K. Havelund and G. Rosu. Java PathExplorer — a runtime verification tool. In Proceedings of 6th International Symposium on Artificial Intelligence, Robotics and Automation in Space, ISAIRAS’01, Montreal, Canada, Jun. 18–22 2001. K. Havelund and G. Rosu. Synthesizing monitors for safety properties. In Tools and Algorithms for Construction and Analysis of Systems, pages 342–356, 2002. S. Khurshid, C. Pasareanu, and W. Visser. Generalized symbolic execution for model checking and testing. In Proceedings of TACAS03: Tools and Algorithms for the Construction and Analysis of Systems, volume 2619 of Lecture Notes in Computer Science, Warsaw, Poland, Apr. 2003. M. Kim, S. Kannan, I. Lee, O. Sokolsky, and M. Viswanathan. Java-MaC: a run-time assurance tool for Java programs. In K. Havelund and G. Rosu, editors, Electronic Notes in Theoretical Computer Science, volume 55. Elsevier, 2001. J.C. King. Symbolic execution and program testing. Communications of ACM, 19(7):385–394, 1976. C. Pasareanu and W. Visser. Verification of Java programs using symbolic execution and invariant generation. In Proceedings of Model Checking Software: 11th International SPIN Workshop, Lecture Notes in Computer Science, Barcelona, Spain, Apr. 1-3 2004. Springer-Verlag. W. Pugh. The Omega test: A fast and practical integer programming algorithm for dependence analysis. Communications of the ACM, 31(8), Aug. 1992. W. Visser, K. Havelund, G. Brat, and S.J. Park. Model checking programs. In Proceedings of the 15th IEEE International Conference on Automated Software Engineering, Grenoble, France, Sept. 2000.
dc.rights.none.fl_str_mv	Derechos de autor 2005 Revista Colombiana de Computación
dc.rights.coar.fl_str_mv	http://purl.org/coar/access_right/c_abf2
dc.rights.uri.*.fl_str_mv	http://creativecommons.org/licenses/by-nc-sa/4.0/
dc.rights.uri.none.fl_str_mv	http://creativecommons.org/licenses/by-nc-nd/2.5/co/
dc.rights.creativecommons.*.fl_str_mv	Attribution-NonCommercial-ShareAlike 4.0 International
rights_invalid_str_mv	Derechos de autor 2005 Revista Colombiana de Computación http://creativecommons.org/licenses/by-nc-sa/4.0/ http://creativecommons.org/licenses/by-nc-nd/2.5/co/ Attribution-NonCommercial-ShareAlike 4.0 International http://purl.org/coar/access_right/c_abf2
dc.format.mimetype.spa.fl_str_mv	application/pdf
dc.publisher.none.fl_str_mv	Universidad Autónoma de Bucaramanga UNAB
publisher.none.fl_str_mv	Universidad Autónoma de Bucaramanga UNAB
dc.source.none.fl_str_mv	Revista Colombiana de Computación; Vol. 6 Núm. 1 (2005): Revista Colombiana de Computación; 1-15
institution	Universidad Autónoma de Bucaramanga - UNAB
bitstream.url.fl_str_mv	https://repository.unab.edu.co/bitstream/20.500.12749/9027/1/2005_Articulo_Combinando%20ejecuci%c3%b3n%20simbolica%20y%20verificaci%c3%b3n%20de%20modelos%20para%20reducir%20la%20sobrecarga%20del%20analisis%20dinamico%20del%20programa.pdf https://repository.unab.edu.co/bitstream/20.500.12749/9027/2/2005_Articulo_Combinando%20ejecuci%c3%b3n%20simbolica%20y%20verificaci%c3%b3n%20de%20modelos%20para%20reducir%20la%20sobrecarga%20del%20analisis%20dinamico%20del%20programa.pdf.jpg
bitstream.checksum.fl_str_mv	1cd4581f4d4597db9b9033451e11e08a 73cfed294e179e2db6afaaa8c969ef13
bitstream.checksumAlgorithm.fl_str_mv	MD5 MD5
repository.name.fl_str_mv	Repositorio Institucional \| Universidad Autónoma de Bucaramanga - UNAB
repository.mail.fl_str_mv	repositorio@unab.edu.co
_version_	1814277394257674240
spelling	Cataño, Néstorb564397f-2f6f-4396-8529-3912927cfe36Cataño, Néstor [a7qGKHwAAAAJ]Cataño, Néstor [0000-0001-5015-5893]Cataño, Néstor [Nestor-Catano]2020-10-27T00:21:13Z2020-10-27T00:21:13Z2005-06-012539-21151657-2831http://hdl.handle.net/20.500.12749/9027instname:Universidad Autónoma de Bucaramanga UNABrepourl:https://repository.unab.edu.coEste documento aborda el problema de reducir la sobrecarga de supervisión del tiempo de ejecución para programas en los que se requiere una supervisión detallada de los eventos. Para ello complementamos modelar técnicas de verificación con métodos de razonamiento simbólico y mostrar que, bajo ciertas circunstancias, los fragmentos de código no afectan la validez de las propiedades subyacentes. Consideramos las propiedades de seguridad dadas como expresiones regulares sobre eventos generados por el programa. Además, mostramos cómo nuestro marco puede extenderse para considerar programas con ciclos. Probamos nuestra presentación con la ayuda del modelo Java PathFinder corrector [13].This paper addresses the problem of reducing the runtime monitoring overhead for programs where fine-grained monitoring of events is required. To this end we complement model checking techniques with symbolic reasoning methods and show that, under certain circumstances, code fragments do not affect the validity of underlying properties. We consider safety properties given as regular expressions on events generated by the program. Further, we show how our framework can be extended to consider programs with cycles. We sample our presentation with the aid of the Java PathFinder model checker [13].application/pdfengUniversidad Autónoma de Bucaramanga UNABhttps://revistas.unab.edu.co/index.php/rcc/article/view/1069/1041https://revistas.unab.edu.co/index.php/rcc/article/view/1069http://hdl.handle.net/20.500.12749/20373B. B´erard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit L. Petrucci, Ph. Schnoebelen, and P. Mackenzie. Systems and Software Verification: Model-Checking Techniques and Tools. Springer-Verlag, 1999.E.M. Clarke, O. Grumberg, and D.A. Peled. Model Checking. MIT Press, 2000.T. Colcombet and P. Fradet. Enforcing trace properties by program transformation. In Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 54–66, 2000.C. Flanagan and S. Qadeer. Predicate abstraction for software verification. In Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 191–202. ACM Press, 2002.A.Q. Gates, S. Roach, O. Mondrag´on, and N. Delgado. DynaMICs: Comprehensive support for run-time monitoring. In K. Havelund and G. Rosu, editors, Electronic Notes in Theoretical Computer Science, volume 55. Elsevier, 2001.K. Havelund and G. Rosu. Java PathExplorer — a runtime verification tool. In Proceedings of 6th International Symposium on Artificial Intelligence, Robotics and Automation in Space, ISAIRAS’01, Montreal, Canada, Jun. 18–22 2001.K. Havelund and G. Rosu. Synthesizing monitors for safety properties. In Tools and Algorithms for Construction and Analysis of Systems, pages 342–356, 2002.S. Khurshid, C. Pasareanu, and W. Visser. Generalized symbolic execution for model checking and testing. In Proceedings of TACAS03: Tools and Algorithms for the Construction and Analysis of Systems, volume 2619 of Lecture Notes in Computer Science, Warsaw, Poland, Apr. 2003.M. Kim, S. Kannan, I. Lee, O. Sokolsky, and M. Viswanathan. Java-MaC: a run-time assurance tool for Java programs. In K. Havelund and G. Rosu, editors, Electronic Notes in Theoretical Computer Science, volume 55. Elsevier, 2001.J.C. King. Symbolic execution and program testing. Communications of ACM, 19(7):385–394, 1976.C. Pasareanu and W. Visser. Verification of Java programs using symbolic execution and invariant generation. In Proceedings of Model Checking Software: 11th International SPIN Workshop, Lecture Notes in Computer Science, Barcelona, Spain, Apr. 1-3 2004. Springer-Verlag.W. Pugh. The Omega test: A fast and practical integer programming algorithm for dependence analysis. Communications of the ACM, 31(8), Aug. 1992.W. Visser, K. Havelund, G. Brat, and S.J. Park. Model checking programs. In Proceedings of the 15th IEEE International Conference on Automated Software Engineering, Grenoble, France, Sept. 2000.Derechos de autor 2005 Revista Colombiana de Computaciónhttp://creativecommons.org/licenses/by-nc-sa/4.0/http://creativecommons.org/licenses/by-nc-nd/2.5/co/Attribution-NonCommercial-ShareAlike 4.0 Internationalhttp://purl.org/coar/access_right/c_abf2Revista Colombiana de Computación; Vol. 6 Núm. 1 (2005): Revista Colombiana de Computación; 1-15Innovaciones tecnológicasCiencia de los computadoresDesarrollo de tecnologíaIngeniería de sistemasInvestigacionesTecnologías de la información y las comunicacionesTIC´sTechnological innovationsComputer scienceTechnology developmentSystems engineeringInvestigationsInformation and communication technologiesICT'sModel checkingJava pathfinderSymbolic reasoningInstrumentationMonitoringInvariant strengtheningInnovaciones tecnológicasCiencias de la computaciónDesarrollo tecnológicoIngeniería de sistemasInvestigacionesTecnologías de la información y la comunicaciónComprobación de modeloBuscador de rutas de JavaRazonamiento simbólicoInstrumentaciónSupervisiónFortalecimiento invarianteCombinando ejecución simbólica y verificación de modelos para reducir la sobrecarga del análisis dinámico del programaCombining symbolic execution and model checking to reduce dynamic program analysis overheadinfo:eu-repo/semantics/articleArtículohttp://purl.org/coar/resource_type/c_7a1fhttp://purl.org/coar/resource_type/c_2df8fbb1http://purl.org/redcol/resource_type/CJournalArticlehttp://purl.org/coar/version/c_970fb48d4fbd8a85ORIGINAL2005_Articulo_Combinando ejecución simbolica y verificación de modelos para reducir la sobrecarga del analisis dinamico del programa.pdf2005_Articulo_Combinando ejecución simbolica y verificación de modelos para reducir la sobrecarga del analisis dinamico del programa.pdfArtículoapplication/pdf166831https://repository.unab.edu.co/bitstream/20.500.12749/9027/1/2005_Articulo_Combinando%20ejecuci%c3%b3n%20simbolica%20y%20verificaci%c3%b3n%20de%20modelos%20para%20reducir%20la%20sobrecarga%20del%20analisis%20dinamico%20del%20programa.pdf1cd4581f4d4597db9b9033451e11e08aMD51open accessTHUMBNAIL2005_Articulo_Combinando ejecución simbolica y verificación de modelos para reducir la sobrecarga del analisis dinamico del programa.pdf.jpg2005_Articulo_Combinando ejecución simbolica y verificación de modelos para reducir la sobrecarga del analisis dinamico del programa.pdf.jpgIM Thumbnailimage/jpeg7856https://repository.unab.edu.co/bitstream/20.500.12749/9027/2/2005_Articulo_Combinando%20ejecuci%c3%b3n%20simbolica%20y%20verificaci%c3%b3n%20de%20modelos%20para%20reducir%20la%20sobrecarga%20del%20analisis%20dinamico%20del%20programa.pdf.jpg73cfed294e179e2db6afaaa8c969ef13MD52open access20.500.12749/9027oai:repository.unab.edu.co:20.500.12749/90272023-07-10 12:51:20.044open accessRepositorio Institucional \| Universidad Autónoma de Bucaramanga - UNABrepositorio@unab.edu.co

Combinando ejecución simbólica y verificación de modelos para reducir la sobrecarga del análisis dinámico del programa

Publicaciones similares