Heurísticas de búsqueda de prueba automática en la herramienta de análisis invariante de maude

La herramienta Invariant Analyzer es una herramienta interactiva que mecaniza un sistema de inferencia para probar las propiedades de seguridad de los sistemas concurrentes, que pueden ser de estado infinito o cuyo conjunto de estados iniciales puede ser infinito. Este documento presenta la heurísti...

Full description

Autores:
Rocha, Camilo
Tipo de recurso:
Trabajo de grado de pregrado
Fecha de publicación:
2013
Institución:
Universidad Autónoma de Bucaramanga - UNAB
Repositorio:
Repositorio UNAB
Idioma:
spa
OAI Identifier:
oai:repository.unab.edu.co:20.500.12749/8909
Acceso en línea:
http://hdl.handle.net/20.500.12749/8909
Palabra clave:
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
Proof-search heuristics
Rewriting logic
Innovaciones tecnológicas
Ciencias de la computación
Desarrollo tecnológico
Ingeniería de sistemas
Heurística de búsqueda de pruebas
Reescritura de lógica
Rights
License
Derechos de autor 2013 Revista Colombiana de Computación
id UNAB2_faf0c375525ddbb52706c5e837a9bc5f
oai_identifier_str oai:repository.unab.edu.co:20.500.12749/8909
network_acronym_str UNAB2
network_name_str Repositorio UNAB
repository_id_str
dc.title.none.fl_str_mv Heurísticas de búsqueda de prueba automática en la herramienta de análisis invariante de maude
dc.title.translated.none.fl_str_mv Automatic proof-search heuristics in the maude invariant analyzer tool
dc.title.translated.eng.fl_str_mv Automatic Proof-Search Heuristics in the Maude Invariant AnalyzerTool
title Heurísticas de búsqueda de prueba automática en la herramienta de análisis invariante de maude
spellingShingle Heurísticas de búsqueda de prueba automática en la herramienta de análisis invariante de maude
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
Proof-search heuristics
Rewriting logic
Innovaciones tecnológicas
Ciencias de la computación
Desarrollo tecnológico
Ingeniería de sistemas
Heurística de búsqueda de pruebas
Reescritura de lógica
title_short Heurísticas de búsqueda de prueba automática en la herramienta de análisis invariante de maude
title_full Heurísticas de búsqueda de prueba automática en la herramienta de análisis invariante de maude
title_fullStr Heurísticas de búsqueda de prueba automática en la herramienta de análisis invariante de maude
title_full_unstemmed Heurísticas de búsqueda de prueba automática en la herramienta de análisis invariante de maude
title_sort Heurísticas de búsqueda de prueba automática en la herramienta de análisis invariante de maude
dc.creator.fl_str_mv Rocha, Camilo
dc.contributor.author.spa.fl_str_mv Rocha, Camilo
dc.contributor.googlescholar.none.fl_str_mv Rocha, Camilo [en&oi=sra]
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
Proof-search heuristics
Rewriting logic
Innovaciones tecnológicas
Ciencias de la computación
Desarrollo tecnológico
Ingeniería de sistemas
Heurística de búsqueda de pruebas
Reescritura de lógica
dc.subject.keywords.eng.fl_str_mv Technological innovations
Computer science
Technology development
Systems engineering
Investigations
Information and communication technologies
ICT's
Proof-search heuristics
Rewriting logic
dc.subject.lemb.spa.fl_str_mv Innovaciones tecnológicas
Ciencias de la computación
Desarrollo tecnológico
Ingeniería de sistemas
dc.subject.proposal.spa.fl_str_mv Heurística de búsqueda de pruebas
Reescritura de lógica
description La herramienta Invariant Analyzer es una herramienta interactiva que mecaniza un sistema de inferencia para probar las propiedades de seguridad de los sistemas concurrentes, que pueden ser de estado infinito o cuyo conjunto de estados iniciales puede ser infinito. Este documento presenta la heurística de búsqueda automática de pruebas en el núcleo de la herramienta Maude Invariant Analyzer Tool, que proporciona un grado sustancial de automatización y puede descargar automáticamente muchas obligaciones de prueba sin la intervención del usuario. Estas heurísticas pueden aprovechar los predicados de igualdad definidos por ecuaciones e incluir técnicas de reescritura, reducción y búsqueda de pruebas basadas en SMT.
publishDate 2013
dc.date.issued.none.fl_str_mv 2013-12-01
dc.date.accessioned.none.fl_str_mv 2020-10-27T00:20:26Z
dc.date.available.none.fl_str_mv 2020-10-27T00:20:26Z
dc.type.coar.fl_str_mv http://purl.org/coar/resource_type/c_2df8fbb1
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/8909
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/8909
dc.language.iso.spa.fl_str_mv spa
language spa
dc.relation.none.fl_str_mv https://revistas.unab.edu.co/index.php/rcc/article/view/2017/1802
dc.relation.uri.none.fl_str_mv https://revistas.unab.edu.co/index.php/rcc/article/view/2017
dc.relation.references.none.fl_str_mv R. Bruni and J. Meseguer. Semantic foundations for generalized rewritetheories.TheoreticalComputerScience,360(1-3):386–414, 2006.
E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MITPress, Cambridge, Massachusetts, 1999.
M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and C. L. Talcott, editors. All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, volume 4350 of Lecture Notes in Computer Science. Springer, 2007.
M. Clavel and M. Egea. ITP/OCL: Arewriting-based validation tool for UML+OCLstatic class diagrams. In M. Johnson and V. Vene, editors, AMAST, volume 4019 of Lecture Notes in Computer Science, pages 368–373. Springer, 2006.
F. Durán and J. Meseguer. AChurch-Rosser checker tool for conditional ordersorted equational maude specifications. In P. C. Ölveczky, editor, WRLA, volume 6381 of Lecture Notes in Computer Science, pages 69–85. Springer, 2010.
F. Durán, C. Rocha, and J. M. Álvarez. Towards a Maude Formal Environment. In Formal Modeling: Actors, Open Systems, Biological Systems, volume 7000 of Lecture Notes in Computer Science, pages 329–351, 2011.
R. Gutiérrez, J. Meseguer, and C. Rocha. Order-sorted equality enrichments modulo axioms. In F. Durán, editor, Rewriting Logic 120Camilo Rochaz and Its Applications, volume 7571 of Lecture Notes in Computer Science, pages 162–181. Springer Berlin Heidelberg, 2012.
J.Hendrix.DecisionProceduresforEquationallyBasedReasoning. PhD thesis, University of Illinois at Urbana-Champaign, April 2008.
J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96(1):73–155, 1992.
J. Meseguer. Membership algebra as a logical framework for equational specification. In F. Parisi-Presicce, editor, WADT, volume 1376 of Lecture Notes in Computer Science, pages 18–61. Springer, 1997.
J. Meseguer and J. A. Goguen. Initially, induction and computability. Algebraic Methods in Semantics, 1986.
K. Ogata and K. Futatsugi. Formal analysis of the bakery protocol with consideration of nonatomic reads and writes. In S. Liu, T. Maibaum, and K. Araki, editors, Formal Methods and Software Engineering, volume 5256 of Lecture Notes in Computer Science, pages 187–206. Springer Berlin Heidelberg, 2008.
C. Rocha. Symbolic Reachability Analysis for Rewrite Theories. PhD thesis, University of Illinois at Urbana-Champaign, 2012.
C. Rocha and J. Meseguer. Proving safety properties of rewrite theories. In A. Corradini, B. Klin, and C. Cîrstea, editors, CALCO, volume 6859 of Lecture Notes in Computer Science, pages 314–328. Springer, 2011.
G. Ro ̧su and A. ̧ Stef?anescu. Matching Logic: ANew Program Verification Approach (NIER Track). In ICSE’11: Proceedings of the 30th International Conference on Software Engineering, pages 868–871. ACM, 2011.
S. Tang, H. Mai, and S. T. King. Trust and protection in the Illinois Browser Operating System. In R. H. Arpaci-Dusseau and B. Chen, editors, OSDI, pages 17–32. USENIX Association, 2010.
P. Viry. Equational rules for rewriting logic. Theoretical Computer Science, 285:487–517, 2002.
dc.rights.none.fl_str_mv Derechos de autor 2013 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 Atribución-NoComercial-SinDerivadas 2.5 Colombia
rights_invalid_str_mv Derechos de autor 2013 Revista Colombiana de Computación
http://creativecommons.org/licenses/by-nc-sa/4.0/
http://creativecommons.org/licenses/by-nc-nd/2.5/co/
Atribución-NoComercial-SinDerivadas 2.5 Colombia
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. 14 Núm. 2 (2013): Revista Colombiana de Computación; 98-121
institution Universidad Autónoma de Bucaramanga - UNAB
bitstream.url.fl_str_mv https://repository.unab.edu.co/bitstream/20.500.12749/8909/2/2017-Texto%20del%20art%c3%adculo-5976-1-10-20140814%20%281%29.pdf.jpg
https://repository.unab.edu.co/bitstream/20.500.12749/8909/1/2017-Texto%20del%20art%c3%adculo-5976-1-10-20140814%20%281%29.pdf
bitstream.checksum.fl_str_mv d0c3a1c32a3cb8b5a6745f27332f4ebd
a38a44d62dd03d77a8fde770bb8d1988
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_ 1814277321493839872
spelling Rocha, Camiloeb2f6c10-76de-461f-9029-f98650724186Rocha, Camilo [en&oi=sra]2020-10-27T00:20:26Z2020-10-27T00:20:26Z2013-12-012539-21151657-2831http://hdl.handle.net/20.500.12749/8909instname:Universidad Autónoma de Bucaramanga UNABrepourl:https://repository.unab.edu.coLa herramienta Invariant Analyzer es una herramienta interactiva que mecaniza un sistema de inferencia para probar las propiedades de seguridad de los sistemas concurrentes, que pueden ser de estado infinito o cuyo conjunto de estados iniciales puede ser infinito. Este documento presenta la heurística de búsqueda automática de pruebas en el núcleo de la herramienta Maude Invariant Analyzer Tool, que proporciona un grado sustancial de automatización y puede descargar automáticamente muchas obligaciones de prueba sin la intervención del usuario. Estas heurísticas pueden aprovechar los predicados de igualdad definidos por ecuaciones e incluir técnicas de reescritura, reducción y búsqueda de pruebas basadas en SMT.La herramienta Invariant Analyzer es una herramienta interactiva que mecaniza un sistema de inferencia para probar las propiedades de seguridad de los sistemas concurrentes, que pueden ser de estado infinito o cuyo conjunto de estados iniciales puede ser infinito. Este documento presenta la heurística de búsqueda automática de pruebas en el núcleo de la herramienta Maude Invariant Analyzer Tool, que proporciona un grado sustancial de automatización y puede descargar automáticamente muchas obligaciones de prueba sin la intervención del usuario. Estas heurísticas pueden aprovechar los predicados de igualdad definidos por ecuaciones e incluir técnicas de reescritura, reducción y búsqueda de pruebas basadas en SMT.application/pdfspaUniversidad Autónoma de Bucaramanga UNABhttps://revistas.unab.edu.co/index.php/rcc/article/view/2017/1802https://revistas.unab.edu.co/index.php/rcc/article/view/2017R. Bruni and J. Meseguer. Semantic foundations for generalized rewritetheories.TheoreticalComputerScience,360(1-3):386–414, 2006.E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MITPress, Cambridge, Massachusetts, 1999.M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and C. L. Talcott, editors. All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, volume 4350 of Lecture Notes in Computer Science. Springer, 2007.M. Clavel and M. Egea. ITP/OCL: Arewriting-based validation tool for UML+OCLstatic class diagrams. In M. Johnson and V. Vene, editors, AMAST, volume 4019 of Lecture Notes in Computer Science, pages 368–373. Springer, 2006.F. Durán and J. Meseguer. AChurch-Rosser checker tool for conditional ordersorted equational maude specifications. In P. C. Ölveczky, editor, WRLA, volume 6381 of Lecture Notes in Computer Science, pages 69–85. Springer, 2010.F. Durán, C. Rocha, and J. M. Álvarez. Towards a Maude Formal Environment. In Formal Modeling: Actors, Open Systems, Biological Systems, volume 7000 of Lecture Notes in Computer Science, pages 329–351, 2011.R. Gutiérrez, J. Meseguer, and C. Rocha. Order-sorted equality enrichments modulo axioms. In F. Durán, editor, Rewriting Logic 120Camilo Rochaz and Its Applications, volume 7571 of Lecture Notes in Computer Science, pages 162–181. Springer Berlin Heidelberg, 2012.J.Hendrix.DecisionProceduresforEquationallyBasedReasoning. PhD thesis, University of Illinois at Urbana-Champaign, April 2008.J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96(1):73–155, 1992.J. Meseguer. Membership algebra as a logical framework for equational specification. In F. Parisi-Presicce, editor, WADT, volume 1376 of Lecture Notes in Computer Science, pages 18–61. Springer, 1997.J. Meseguer and J. A. Goguen. Initially, induction and computability. Algebraic Methods in Semantics, 1986.K. Ogata and K. Futatsugi. Formal analysis of the bakery protocol with consideration of nonatomic reads and writes. In S. Liu, T. Maibaum, and K. Araki, editors, Formal Methods and Software Engineering, volume 5256 of Lecture Notes in Computer Science, pages 187–206. Springer Berlin Heidelberg, 2008.C. Rocha. Symbolic Reachability Analysis for Rewrite Theories. PhD thesis, University of Illinois at Urbana-Champaign, 2012.C. Rocha and J. Meseguer. Proving safety properties of rewrite theories. In A. Corradini, B. Klin, and C. Cîrstea, editors, CALCO, volume 6859 of Lecture Notes in Computer Science, pages 314–328. Springer, 2011.G. Ro ̧su and A. ̧ Stef?anescu. Matching Logic: ANew Program Verification Approach (NIER Track). In ICSE’11: Proceedings of the 30th International Conference on Software Engineering, pages 868–871. ACM, 2011.S. Tang, H. Mai, and S. T. King. Trust and protection in the Illinois Browser Operating System. In R. H. Arpaci-Dusseau and B. Chen, editors, OSDI, pages 17–32. USENIX Association, 2010.P. Viry. Equational rules for rewriting logic. Theoretical Computer Science, 285:487–517, 2002.Derechos de autor 2013 Revista Colombiana de Computaciónhttp://creativecommons.org/licenses/by-nc-sa/4.0/http://creativecommons.org/licenses/by-nc-nd/2.5/co/Atribución-NoComercial-SinDerivadas 2.5 Colombiahttp://purl.org/coar/access_right/c_abf2Revista Colombiana de Computación; Vol. 14 Núm. 2 (2013): Revista Colombiana de Computación; 98-121Innovaciones 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'sProof-search heuristicsRewriting logicInnovaciones tecnológicasCiencias de la computaciónDesarrollo tecnológicoIngeniería de sistemasHeurística de búsqueda de pruebasReescritura de lógicaHeurísticas de búsqueda de prueba automática en la herramienta de análisis invariante de maudeAutomatic proof-search heuristics in the maude invariant analyzer toolAutomatic Proof-Search Heuristics in the Maude Invariant AnalyzerToolinfo:eu-repo/semantics/articleArtículohttp://purl.org/coar/resource_type/c_7a1fhttp://purl.org/coar/resource_type/c_2df8fbb1http://purl.org/redcol/resource_type/CJournalArticleTHUMBNAIL2017-Texto del artículo-5976-1-10-20140814 (1).pdf.jpg2017-Texto del artículo-5976-1-10-20140814 (1).pdf.jpgIM Thumbnailimage/jpeg6190https://repository.unab.edu.co/bitstream/20.500.12749/8909/2/2017-Texto%20del%20art%c3%adculo-5976-1-10-20140814%20%281%29.pdf.jpgd0c3a1c32a3cb8b5a6745f27332f4ebdMD52open accessORIGINAL2017-Texto del artículo-5976-1-10-20140814 (1).pdf2017-Texto del artículo-5976-1-10-20140814 (1).pdfArtículoapplication/pdf1207665https://repository.unab.edu.co/bitstream/20.500.12749/8909/1/2017-Texto%20del%20art%c3%adculo-5976-1-10-20140814%20%281%29.pdfa38a44d62dd03d77a8fde770bb8d1988MD51open access20.500.12749/8909oai:repository.unab.edu.co:20.500.12749/89092022-11-24 19:59:33.844open accessRepositorio Institucional | Universidad Autónoma de Bucaramanga - UNABrepositorio@unab.edu.co

Publicaciones similares