Simulation and Verification of Synchronous Set Relations in Rewriting Logic
This paper presents a mathematical foundation and a rewriting logic infrastructure for the execution and property verification of synchronous set relations. The mathematical foundation is given in the language of abstract set relations. The infrastructure consists of an ordersorted rewrite theory in...
- Autores:
-
Rocha, Camilo
Múñoz, César
- Tipo de recurso:
- Conferencia (Ponencia)
- Fecha de publicación:
- 2011
- Institución:
- Escuela Colombiana de Ingeniería Julio Garavito
- Repositorio:
- Repositorio Institucional ECI
- Idioma:
- eng
- OAI Identifier:
- oai:repositorio.escuelaing.edu.co:001/1893
- Acceso en línea:
- https://repositorio.escuelaing.edu.co/handle/001/1893
- Palabra clave:
- Relaciones de conjuntos sincrónicos
Reachability Analysis
Análisis de accesibilidad
Synchronous set relations
- Rights
- openAccess
- License
- http://purl.org/coar/access_right/c_abf2
| id |
ESCUELAIG2_6a7fc7a1df1528166bf2711f903a540f |
|---|---|
| oai_identifier_str |
oai:repositorio.escuelaing.edu.co:001/1893 |
| network_acronym_str |
ESCUELAIG2 |
| network_name_str |
Repositorio Institucional ECI |
| repository_id_str |
|
| dc.title.eng.fl_str_mv |
Simulation and Verification of Synchronous Set Relations in Rewriting Logic |
| title |
Simulation and Verification of Synchronous Set Relations in Rewriting Logic |
| spellingShingle |
Simulation and Verification of Synchronous Set Relations in Rewriting Logic Relaciones de conjuntos sincrónicos Reachability Analysis Análisis de accesibilidad Synchronous set relations |
| title_short |
Simulation and Verification of Synchronous Set Relations in Rewriting Logic |
| title_full |
Simulation and Verification of Synchronous Set Relations in Rewriting Logic |
| title_fullStr |
Simulation and Verification of Synchronous Set Relations in Rewriting Logic |
| title_full_unstemmed |
Simulation and Verification of Synchronous Set Relations in Rewriting Logic |
| title_sort |
Simulation and Verification of Synchronous Set Relations in Rewriting Logic |
| dc.creator.fl_str_mv |
Rocha, Camilo Múñoz, César |
| dc.contributor.author.none.fl_str_mv |
Rocha, Camilo Múñoz, César |
| dc.contributor.researchgroup.spa.fl_str_mv |
Informática |
| dc.subject.armarc.spa.fl_str_mv |
Relaciones de conjuntos sincrónicos Reachability Analysis Análisis de accesibilidad |
| topic |
Relaciones de conjuntos sincrónicos Reachability Analysis Análisis de accesibilidad Synchronous set relations |
| dc.subject.armarc.eng.fl_str_mv |
Synchronous set relations |
| description |
This paper presents a mathematical foundation and a rewriting logic infrastructure for the execution and property verification of synchronous set relations. The mathematical foundation is given in the language of abstract set relations. The infrastructure consists of an ordersorted rewrite theory in Maude, a rewriting logic system, that enables the synchronous execution of a set relation provided by the user. By using the infrastructure, existing algorithm verification techniques already available in Maude for traditional asynchronous rewriting, such as reachability analysis and model checking, are automatically available to synchronous set rewriting. The use of the infrastructure is illustrated with an executable operational semantics of a simple synchronous language and the verification of temporal properties of a synchronous system. |
| publishDate |
2011 |
| dc.date.issued.none.fl_str_mv |
2011 |
| dc.date.accessioned.none.fl_str_mv |
2021-12-03T16:46:09Z |
| dc.date.available.none.fl_str_mv |
2021-12-03T16:46:09Z |
| dc.type.spa.fl_str_mv |
Documento de Conferencia |
| dc.type.coar.fl_str_mv |
http://purl.org/coar/resource_type/c_2df8fbb1 http://purl.org/coar/resource_type/c_c94f |
| dc.type.coarversion.fl_str_mv |
http://purl.org/coar/version/c_970fb48d4fbd8a85 |
| dc.type.version.spa.fl_str_mv |
info:eu-repo/semantics/publishedVersion |
| dc.type.coar.spa.fl_str_mv |
http://purl.org/coar/resource_type/c_8544 |
| dc.type.content.spa.fl_str_mv |
Text |
| dc.type.driver.spa.fl_str_mv |
info:eu-repo/semantics/conferenceObject |
| dc.type.redcol.spa.fl_str_mv |
http://purl.org/redcol/resource_type/ART |
| format |
http://purl.org/coar/resource_type/c_8544 |
| status_str |
publishedVersion |
| dc.identifier.uri.none.fl_str_mv |
https://repositorio.escuelaing.edu.co/handle/001/1893 |
| url |
https://repositorio.escuelaing.edu.co/handle/001/1893 |
| dc.language.iso.spa.fl_str_mv |
eng |
| language |
eng |
| dc.relation.indexed.spa.fl_str_mv |
N/A |
| dc.relation.references.spa.fl_str_mv |
M. AlTurki and J. Meseguer. Reduction semantics and formal analysis of Orc programs. Electronic Notes in Theoretical Computer Science, 200(3):25 – 41, 2008. Proceedings of the 3rd International Workshop on Automated Specification and Verification of Web Systems (WWV 2007). R. Bruni and J. Meseguer. Semantic foundations for generalized rewrite theories. Theoretical Computer Science, 360(1-3):386–414, 2006. C. Chira, T. F. Serbanuta, and G. Stefanescu. P systems with control nuclei: The concept. Journal of Logic and Algebraic Programming, 79(6):326 – 333, 2010. Membrane computing and programming. M. Clavel, F. Dur´an, 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. G. Dowek, C. Mu˜noz, and C. Rocha. Rewriting logic semantics of a plan execution language. Electronic Proceedings in Theoretical Computer Science, 18:77–91, 2010. T. Estlin, A. J´onsson, C. P˘as˘areanu, R. Simmons, K. Tso, and V. Verna. Plan Execution Interchange Language (PLEXIL). Technical Memorandum TM-2006- 213483, NASA, 2006. D. Lucanu. Strategy-based rewrite semantics for membrane systems preserves maximal concurrency of evolution rule actions. Electronic Notes in Theoretical Computer Science, 237:107 – 125, 2009. Proceedings of the 8th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2008). 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 P. Olveczky. Formalization and correctness of the pals architec- ¨ tural pattern for distributed real-time systems. In J. Dong and H. Zhu, editors, Formal Methods and Software Engineering, volume 6447 of Lecture Notes in Computer Science, pages 303–320. Springer Berlin / Heidelberg, 2010. C. Rocha and J. Meseguer. Proving safety properties of rewrite theories. Technical report, University of Illinois at Urbana-Champaign, 2010. http://hdl.handle.net/2142/17407. C. Rocha, C. Mu˜noz, and G. Dowek. A formal library of set relations and its application to synchronous languages. Theoretical Computer Science, 412(37):4853– 4866, 2011. T. Serbanuta. A Rewriting Approach to Concurrent Programming Language Design and Semantics. PhD thesis, University of Illinois at Urbana-Champaign, December 2010. https://www.ideals.illinois.edu/handle/2142/18252. T. Serbanuta, G. Stefanescu, and G. Rosu. Defining and executing p systems with structured data in k. In D. Corne, P. Frisco, G. Paun, G. Rozenberg, and A. Salomaa, editors, Membrane Computing, volume 5391 of Lecture Notes in Computer Science, pages 374–393. Springer Berlin / Heidelberg, 2009. P. Viry. Equational rules for rewriting logic. Theoretical Computer Science, 285(2):487–517, 2002. |
| dc.rights.coar.fl_str_mv |
http://purl.org/coar/access_right/c_abf2 |
| dc.rights.accessrights.spa.fl_str_mv |
info:eu-repo/semantics/openAccess |
| eu_rights_str_mv |
openAccess |
| rights_invalid_str_mv |
http://purl.org/coar/access_right/c_abf2 |
| dc.format.extent.spa.fl_str_mv |
12 páginas. |
| dc.format.mimetype.spa.fl_str_mv |
application/pdf |
| dc.publisher.spa.fl_str_mv |
NASA Langley Research Center |
| dc.publisher.place.spa.fl_str_mv |
Hampton, Virginia. |
| institution |
Escuela Colombiana de Ingeniería Julio Garavito |
| bitstream.url.fl_str_mv |
https://repositorio.escuelaing.edu.co/bitstream/001/1893/1/Simulation%20and%20Verification%20of%20Synchronous%20Set.pdf https://repositorio.escuelaing.edu.co/bitstream/001/1893/2/license.txt https://repositorio.escuelaing.edu.co/bitstream/001/1893/3/Simulation%20and%20Verification%20of%20Synchronous%20Set.pdf.txt https://repositorio.escuelaing.edu.co/bitstream/001/1893/4/Simulation%20and%20Verification%20of%20Synchronous%20Set.pdf.jpg |
| bitstream.checksum.fl_str_mv |
f960a4a90ef58ee3067422ca9708d909 5a7ca94c2e5326ee169f979d71d0f06e 523ef17e0c4c6aa415445c6916aead2c 8ba2503b4d3bff2045770696d63c1a23 |
| bitstream.checksumAlgorithm.fl_str_mv |
MD5 MD5 MD5 MD5 |
| repository.name.fl_str_mv |
Repositorio Escuela Colombiana de Ingeniería Julio Garavito |
| repository.mail.fl_str_mv |
repositorio.eci@escuelaing.edu.co |
| _version_ |
1814355595617107968 |
| spelling |
Rocha, Camiloebfd407af468605647a49186059da397600Múñoz, Césare57e0b9f053d41c599f0ebcb19c2ab06600Informática2021-12-03T16:46:09Z2021-12-03T16:46:09Z2011https://repositorio.escuelaing.edu.co/handle/001/1893This paper presents a mathematical foundation and a rewriting logic infrastructure for the execution and property verification of synchronous set relations. The mathematical foundation is given in the language of abstract set relations. The infrastructure consists of an ordersorted rewrite theory in Maude, a rewriting logic system, that enables the synchronous execution of a set relation provided by the user. By using the infrastructure, existing algorithm verification techniques already available in Maude for traditional asynchronous rewriting, such as reachability analysis and model checking, are automatically available to synchronous set rewriting. The use of the infrastructure is illustrated with an executable operational semantics of a simple synchronous language and the verification of temporal properties of a synchronous system.Este artículo presenta una base matemática y una infraestructura lógica de reescritura para la ejecución y verificación de propiedades de relaciones de conjuntos sincrónicos. El fundamento matemático se da en el lenguaje de las relaciones abstractas de conjuntos. La infraestructura consiste en una teoría de reescritura ordenada en Maude, un sistema lógico de reescritura, que permite la ejecución sincrónica de una relación establecida proporcionada por el usuario. Mediante el uso de la infraestructura, las técnicas de verificación de algoritmos existentes ya disponibles en Maude para la reescritura asincrónica tradicional, como el análisis de accesibilidad y la verificación de modelos, están disponibles automáticamente para la reescritura sincrónica de conjuntos. El uso de la infraestructura se ilustra con una semántica operativa ejecutable de un lenguaje síncrono simple y la verificación de las propiedades temporales de un sistema síncrono.12 páginas.application/pdfengNASA Langley Research CenterHampton, Virginia.Simulation and Verification of Synchronous Set Relations in Rewriting LogicDocumento de Conferenciainfo:eu-repo/semantics/publishedVersionhttp://purl.org/coar/resource_type/c_8544http://purl.org/coar/resource_type/c_2df8fbb1http://purl.org/coar/resource_type/c_c94fTextinfo:eu-repo/semantics/conferenceObjecthttp://purl.org/redcol/resource_type/ARThttp://purl.org/coar/version/c_970fb48d4fbd8a85N/AM. AlTurki and J. Meseguer. Reduction semantics and formal analysis of Orc programs. Electronic Notes in Theoretical Computer Science, 200(3):25 – 41, 2008. Proceedings of the 3rd International Workshop on Automated Specification and Verification of Web Systems (WWV 2007).R. Bruni and J. Meseguer. Semantic foundations for generalized rewrite theories. Theoretical Computer Science, 360(1-3):386–414, 2006.C. Chira, T. F. Serbanuta, and G. Stefanescu. P systems with control nuclei: The concept. Journal of Logic and Algebraic Programming, 79(6):326 – 333, 2010. Membrane computing and programming.M. Clavel, F. Dur´an, 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.G. Dowek, C. Mu˜noz, and C. Rocha. Rewriting logic semantics of a plan execution language. Electronic Proceedings in Theoretical Computer Science, 18:77–91, 2010.T. Estlin, A. J´onsson, C. P˘as˘areanu, R. Simmons, K. Tso, and V. Verna. Plan Execution Interchange Language (PLEXIL). Technical Memorandum TM-2006- 213483, NASA, 2006.D. Lucanu. Strategy-based rewrite semantics for membrane systems preserves maximal concurrency of evolution rule actions. Electronic Notes in Theoretical Computer Science, 237:107 – 125, 2009. Proceedings of the 8th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2008).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 P. Olveczky. Formalization and correctness of the pals architec- ¨ tural pattern for distributed real-time systems. In J. Dong and H. Zhu, editors, Formal Methods and Software Engineering, volume 6447 of Lecture Notes in Computer Science, pages 303–320. Springer Berlin / Heidelberg, 2010.C. Rocha and J. Meseguer. Proving safety properties of rewrite theories. Technical report, University of Illinois at Urbana-Champaign, 2010. http://hdl.handle.net/2142/17407.C. Rocha, C. Mu˜noz, and G. Dowek. A formal library of set relations and its application to synchronous languages. Theoretical Computer Science, 412(37):4853– 4866, 2011.T. Serbanuta. A Rewriting Approach to Concurrent Programming Language Design and Semantics. PhD thesis, University of Illinois at Urbana-Champaign, December 2010. https://www.ideals.illinois.edu/handle/2142/18252.T. Serbanuta, G. Stefanescu, and G. Rosu. Defining and executing p systems with structured data in k. In D. Corne, P. Frisco, G. Paun, G. Rozenberg, and A. Salomaa, editors, Membrane Computing, volume 5391 of Lecture Notes in Computer Science, pages 374–393. Springer Berlin / Heidelberg, 2009.P. Viry. Equational rules for rewriting logic. Theoretical Computer Science, 285(2):487–517, 2002.info:eu-repo/semantics/openAccesshttp://purl.org/coar/access_right/c_abf2Relaciones de conjuntos sincrónicosReachability AnalysisAnálisis de accesibilidadSynchronous set relationsORIGINALSimulation and Verification of Synchronous Set.pdfSimulation and Verification of Synchronous Set.pdfArtículo principal.application/pdf259327https://repositorio.escuelaing.edu.co/bitstream/001/1893/1/Simulation%20and%20Verification%20of%20Synchronous%20Set.pdff960a4a90ef58ee3067422ca9708d909MD51metadata only accessLICENSElicense.txtlicense.txttext/plain; charset=utf-81881https://repositorio.escuelaing.edu.co/bitstream/001/1893/2/license.txt5a7ca94c2e5326ee169f979d71d0f06eMD52open accessTEXTSimulation and Verification of Synchronous Set.pdf.txtSimulation and Verification of Synchronous Set.pdf.txtExtracted texttext/plain45823https://repositorio.escuelaing.edu.co/bitstream/001/1893/3/Simulation%20and%20Verification%20of%20Synchronous%20Set.pdf.txt523ef17e0c4c6aa415445c6916aead2cMD53open accessTHUMBNAILSimulation and Verification of Synchronous Set.pdf.jpgSimulation and Verification of Synchronous Set.pdf.jpgGenerated Thumbnailimage/jpeg10278https://repositorio.escuelaing.edu.co/bitstream/001/1893/4/Simulation%20and%20Verification%20of%20Synchronous%20Set.pdf.jpg8ba2503b4d3bff2045770696d63c1a23MD54open access001/1893oai:repositorio.escuelaing.edu.co:001/18932022-07-01 16:40:38.976metadata only accessRepositorio Escuela Colombiana de Ingeniería Julio Garavitorepositorio.eci@escuelaing.edu.coU0kgVVNURUQgSEFDRSBQQVJURSBERUwgR1JVUE8gREUgUEFSRVMgRVZBTFVBRE9SRVMgREUgTEEgQ09MRUNDScOTTiAiUEVFUiBSRVZJRVciLCBPTUlUQSBFU1RBIExJQ0VOQ0lBLgoKQXV0b3Jpem8gYSBsYSBFc2N1ZWxhIENvbG9tYmlhbmEgZGUgSW5nZW5pZXLDrWEgSnVsaW8gR2FyYXZpdG8gcGFyYSBwdWJsaWNhciBlbCB0cmFiYWpvIGRlIGdyYWRvLCBhcnTDrWN1bG8sIHZpZGVvLCAKY29uZmVyZW5jaWEsIGxpYnJvLCBpbWFnZW4sIGZvdG9ncmFmw61hLCBhdWRpbywgcHJlc2VudGFjacOzbiB1IG90cm8gKGVuICAgIGFkZWxhbnRlIGRvY3VtZW50bykgcXVlIGVuIGxhIGZlY2hhIAplbnRyZWdvIGVuIGZvcm1hdG8gZGlnaXRhbCwgeSBsZSBwZXJtaXRvIGRlIGZvcm1hIGluZGVmaW5pZGEgcXVlIGxvIHB1YmxpcXVlIGVuIGVsIHJlcG9zaXRvcmlvIGluc3RpdHVjaW9uYWwsIAplbiBsb3MgdMOpcm1pbm9zIGVzdGFibGVjaWRvcyBlbiBsYSBMZXkgMjMgZGUgMTk4MiwgbGEgTGV5IDQ0IGRlIDE5OTMsIHkgZGVtw6FzIGxleWVzIHkganVyaXNwcnVkZW5jaWEgdmlnZW50ZQphbCByZXNwZWN0bywgcGFyYSBmaW5lcyBlZHVjYXRpdm9zIHkgbm8gbHVjcmF0aXZvcy4gRXN0YSBhdXRvcml6YWNpw7NuIGVzIHbDoWxpZGEgcGFyYSBsYXMgZmFjdWx0YWRlcyB5IGRlcmVjaG9zIGRlIAp1c28gc29icmUgbGEgb2JyYSBlbiBmb3JtYXRvIGRpZ2l0YWwsIGVsZWN0csOzbmljbywgdmlydHVhbDsgeSBwYXJhIHVzb3MgZW4gcmVkZXMsIGludGVybmV0LCBleHRyYW5ldCwgeSBjdWFscXVpZXIgCmZvcm1hdG8gbyBtZWRpbyBjb25vY2lkbyBvIHBvciBjb25vY2VyLgpFbiBtaSBjYWxpZGFkIGRlIGF1dG9yLCBleHByZXNvIHF1ZSBlbCBkb2N1bWVudG8gb2JqZXRvIGRlIGxhIHByZXNlbnRlIGF1dG9yaXphY2nDs24gZXMgb3JpZ2luYWwgeSBsbyBlbGFib3LDqSBzaW4gCnF1ZWJyYW50YXIgbmkgc3VwbGFudGFyIGxvcyBkZXJlY2hvcyBkZSBhdXRvciBkZSB0ZXJjZXJvcy4gUG9yIGxvIHRhbnRvLCBlcyBkZSBtaSBleGNsdXNpdmEgYXV0b3LDrWEgeSwgZW4gY29uc2VjdWVuY2lhLCAKdGVuZ28gbGEgdGl0dWxhcmlkYWQgc29icmUgw6lsLiBFbiBjYXNvIGRlIHF1ZWphIG8gYWNjacOzbiBwb3IgcGFydGUgZGUgdW4gdGVyY2VybyByZWZlcmVudGUgYSBsb3MgZGVyZWNob3MgZGUgYXV0b3Igc29icmUgCmVsIGRvY3VtZW50byBlbiBjdWVzdGnDs24sIGFzdW1pcsOpIGxhIHJlc3BvbnNhYmlsaWRhZCB0b3RhbCB5IHNhbGRyw6kgZW4gZGVmZW5zYSBkZSBsb3MgZGVyZWNob3MgYXF1w60gYXV0b3JpemFkb3MuIEVzdG8gCnNpZ25pZmljYSBxdWUsIHBhcmEgdG9kb3MgbG9zIGVmZWN0b3MsIGxhIEVzY3VlbGEgYWN0w7phIGNvbW8gdW4gdGVyY2VybyBkZSBidWVuYSBmZS4KVG9kYSBwZXJzb25hIHF1ZSBjb25zdWx0ZSBlbCBSZXBvc2l0b3JpbyBJbnN0aXR1Y2lvbmFsIGRlIGxhIEVzY3VlbGEsIGVsIENhdMOhbG9nbyBlbiBsw61uZWEgdSBvdHJvIG1lZGlvIGVsZWN0csOzbmljbywgCnBvZHLDoSBjb3BpYXIgYXBhcnRlcyBkZWwgdGV4dG8sIGNvbiBlbCBjb21wcm9taXNvIGRlIGNpdGFyIHNpZW1wcmUgbGEgZnVlbnRlLCBsYSBjdWFsIGluY2x1eWUgZWwgdMOtdHVsbyBkZWwgdHJhYmFqbyB5IGVsIAphdXRvci5Fc3RhIGF1dG9yaXphY2nDs24gbm8gaW1wbGljYSByZW51bmNpYSBhIGxhIGZhY3VsdGFkIHF1ZSB0ZW5nbyBkZSBwdWJsaWNhciB0b3RhbCBvIHBhcmNpYWxtZW50ZSBsYSBvYnJhIGVuIG90cm9zIAptZWRpb3MuRXN0YSBhdXRvcml6YWNpw7NuIGVzdMOhIHJlc3BhbGRhZGEgcG9yIGxhcyBmaXJtYXMgZGVsIChsb3MpIGF1dG9yKGVzKSBkZWwgZG9jdW1lbnRvLiAKU8OtIGF1dG9yaXpvIChhbWJvcykK |