EB2Python - Traducción automática de especificaciones Event-B en Rodin a Python
Event-B es un método formal para el modelado y análisis de sistemas basado en el enfoque de corrección por construcción. Presenta un conjunto de teorías como la elección para la notación de modelado, el refinamiento para representar diferentes niveles de abstracción en los modelos y un sistema de pr...
- Autores:
-
Losada Calderón, Hernán Felipe
- Tipo de recurso:
- Trabajo de grado de pregrado
- Fecha de publicación:
- 2018
- Institución:
- Escuela Colombiana de Ingeniería Julio Garavito
- Repositorio:
- Repositorio Institucional ECI
- Idioma:
- spa
- OAI Identifier:
- oai:repositorio.escuelaing.edu.co:001/789
- Acceso en línea:
- https://catalogo.escuelaing.edu.co/cgi-bin/koha/opac-detail.pl?biblionumber=21462
https://repositorio.escuelaing.edu.co/handle/001/789
- Palabra clave:
- Algoritmos
Python lenguaje de programación
Modelos Event-B
Algorithms
Python programming language
Event-B models
- Rights
- openAccess
- License
- Derechos Reservados - Escuela Colombiana de Ingeniería Julio Garavito
| id |
ESCUELAIG2_2f5c6e566f07dc9b33cb08366781167d |
|---|---|
| oai_identifier_str |
oai:repositorio.escuelaing.edu.co:001/789 |
| network_acronym_str |
ESCUELAIG2 |
| network_name_str |
Repositorio Institucional ECI |
| repository_id_str |
|
| dc.title.spa.fl_str_mv |
EB2Python - Traducción automática de especificaciones Event-B en Rodin a Python |
| title |
EB2Python - Traducción automática de especificaciones Event-B en Rodin a Python |
| spellingShingle |
EB2Python - Traducción automática de especificaciones Event-B en Rodin a Python Algoritmos Python lenguaje de programación Modelos Event-B Algorithms Python programming language Event-B models |
| title_short |
EB2Python - Traducción automática de especificaciones Event-B en Rodin a Python |
| title_full |
EB2Python - Traducción automática de especificaciones Event-B en Rodin a Python |
| title_fullStr |
EB2Python - Traducción automática de especificaciones Event-B en Rodin a Python |
| title_full_unstemmed |
EB2Python - Traducción automática de especificaciones Event-B en Rodin a Python |
| title_sort |
EB2Python - Traducción automática de especificaciones Event-B en Rodin a Python |
| dc.creator.fl_str_mv |
Losada Calderón, Hernán Felipe |
| dc.contributor.advisor.spa.fl_str_mv |
Rocha Niño, Hernán Camilo (dir) Garzón, Wilmer ( Co dir) |
| dc.contributor.author.spa.fl_str_mv |
Losada Calderón, Hernán Felipe |
| dc.subject.spa.fl_str_mv |
Algoritmos Python lenguaje de programación Modelos Event-B |
| topic |
Algoritmos Python lenguaje de programación Modelos Event-B Algorithms Python programming language Event-B models |
| dc.subject.keywords.spa.fl_str_mv |
Algorithms Python programming language Event-B models |
| description |
Event-B es un método formal para el modelado y análisis de sistemas basado en el enfoque de corrección por construcción. Presenta un conjunto de teorías como la elección para la notación de modelado, el refinamiento para representar diferentes niveles de abstracción en los modelos y un sistema de prueba para verificar la consistencia dichos modelos. Este documento presenta una algoritmo para generar programas en el lenguaje de programación Python a partir de modelos Event-B correctos. El algoritmo presentado aquí es la composición de reglas de traducción; incluye soporte para relaciones, expresiones numéricas y enumeraciones. El código puede ser generado para ejecución secuencial o concurrente (por medio de hilos). Un ejemplo ilustra la traducción de código y su ejecución como programa en el lenguaje de programación Python. |
| publishDate |
2018 |
| dc.date.accessioned.spa.fl_str_mv |
2018-08-01T20:46:37Z |
| dc.date.available.spa.fl_str_mv |
2018-08-01T20:46:37Z |
| dc.date.issued.spa.fl_str_mv |
2018 |
| dc.date.accessioned.none.fl_str_mv |
2021-10-01T16:04:36Z |
| dc.date.available.none.fl_str_mv |
2021-10-01T16:04:36Z |
| dc.type.spa.fl_str_mv |
Trabajo de grado - Pregrado |
| 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_7a1f |
| dc.type.content.spa.fl_str_mv |
Text |
| dc.type.driver.spa.fl_str_mv |
info:eu-repo/semantics/bachelorThesis |
| dc.type.redcol.spa.fl_str_mv |
http://purl.org/redcol/resource_type/TP |
| format |
http://purl.org/coar/resource_type/c_7a1f |
| status_str |
publishedVersion |
| dc.identifier.uri.spa.fl_str_mv |
https://catalogo.escuelaing.edu.co/cgi-bin/koha/opac-detail.pl?biblionumber=21462 |
| dc.identifier.uri.none.fl_str_mv |
https://repositorio.escuelaing.edu.co/handle/001/789 |
| url |
https://catalogo.escuelaing.edu.co/cgi-bin/koha/opac-detail.pl?biblionumber=21462 https://repositorio.escuelaing.edu.co/handle/001/789 |
| dc.language.iso.spa.fl_str_mv |
spa |
| language |
spa |
| dc.rights.spa.fl_str_mv |
Derechos Reservados - Escuela Colombiana de Ingeniería Julio Garavito |
| dc.rights.coar.fl_str_mv |
http://purl.org/coar/access_right/c_abf2 |
| dc.rights.uri.spa.fl_str_mv |
https://creativecommons.org/licenses/by-nc/4.0/ |
| dc.rights.accessrights.spa.fl_str_mv |
info:eu-repo/semantics/openAccess |
| dc.rights.creativecommons.spa.fl_str_mv |
Atribución-NoComercial 4.0 Internacional (CC BY-NC 4.0) |
| rights_invalid_str_mv |
Derechos Reservados - Escuela Colombiana de Ingeniería Julio Garavito https://creativecommons.org/licenses/by-nc/4.0/ Atribución-NoComercial 4.0 Internacional (CC BY-NC 4.0) http://purl.org/coar/access_right/c_abf2 |
| eu_rights_str_mv |
openAccess |
| dc.format.mimetype.spa.fl_str_mv |
application/pdf |
| dc.publisher.spa.fl_str_mv |
Escuela Colombiana de Ingeniería Julio Garavito |
| dc.publisher.program.spa.fl_str_mv |
Ingeniería de Sistemas |
| institution |
Escuela Colombiana de Ingeniería Julio Garavito |
| bitstream.url.fl_str_mv |
https://repositorio.escuelaing.edu.co/bitstream/001/789/1/Losada%20Calder%c3%b3n%2c%20Hern%c3%a1n%20Felipe%20-%202018.pdf https://repositorio.escuelaing.edu.co/bitstream/001/789/2/Autorizaci%c3%b3n.pdf https://repositorio.escuelaing.edu.co/bitstream/001/789/3/license.txt https://repositorio.escuelaing.edu.co/bitstream/001/789/8/Losada%20Calder%c3%b3n%2c%20Hern%c3%a1n%20Felipe%20-%202018.pdf.txt https://repositorio.escuelaing.edu.co/bitstream/001/789/10/Autorizaci%c3%b3n.pdf.txt https://repositorio.escuelaing.edu.co/bitstream/001/789/9/Losada%20Calder%c3%b3n%2c%20Hern%c3%a1n%20Felipe%20-%202018.pdf.jpg https://repositorio.escuelaing.edu.co/bitstream/001/789/11/Autorizaci%c3%b3n.pdf.jpg |
| bitstream.checksum.fl_str_mv |
f7cf9ca4680b3d4e0a308f95fa5e5f45 968eb709f89a8bb72c2211dede7d5c24 5a7ca94c2e5326ee169f979d71d0f06e 33354c01e2da30fc2553173eec92cbd3 e1c06d85ae7b8b032bef47e42e4c08f9 60a6f3f893da33cc443fe8d4c7d309b6 e7ed9dda95128dcf40c6b3cb3aae509a |
| bitstream.checksumAlgorithm.fl_str_mv |
MD5 MD5 MD5 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_ |
1814355588004446208 |
| spelling |
Rocha Niño, Hernán Camilo (dir)b8aaae70974a7a0f1fa29d074693f986300Garzón, Wilmer ( Co dir)44e045e5b08ab2ac6edef12490ab2678300Losada Calderón, Hernán Felipec44a2fd7dcc6189bb3dece63c3a7c36d6002018-08-01T20:46:37Z2021-10-01T16:04:36Z2018-08-01T20:46:37Z2021-10-01T16:04:36Z2018https://catalogo.escuelaing.edu.co/cgi-bin/koha/opac-detail.pl?biblionumber=21462https://repositorio.escuelaing.edu.co/handle/001/789Event-B es un método formal para el modelado y análisis de sistemas basado en el enfoque de corrección por construcción. Presenta un conjunto de teorías como la elección para la notación de modelado, el refinamiento para representar diferentes niveles de abstracción en los modelos y un sistema de prueba para verificar la consistencia dichos modelos. Este documento presenta una algoritmo para generar programas en el lenguaje de programación Python a partir de modelos Event-B correctos. El algoritmo presentado aquí es la composición de reglas de traducción; incluye soporte para relaciones, expresiones numéricas y enumeraciones. El código puede ser generado para ejecución secuencial o concurrente (por medio de hilos). Un ejemplo ilustra la traducción de código y su ejecución como programa en el lenguaje de programación Python.Event-B is a formal method for system-level modeling and analysis based on the correct-by-construction approach. It features set theory as the choice for modeling notation, refinement to represent different abstraction levels in the models, and a proof system to verify the consistency of such models. This document presents an algorithm to generate Python programs from correct Event-B models. The algorithm, presented here as the composition of translation rules, includes support for most of the language's constructs, including relations, numerical expressions, and enumerations. An implmentation in the Python programming language of the translation algorithm is showcased with the help of a running example and a concise case study.PregradoIngeniero(a) de Sistemasapplication/pdfspaEscuela Colombiana de Ingeniería Julio GaravitoIngeniería de SistemasDerechos Reservados - Escuela Colombiana de Ingeniería Julio Garavitohttps://creativecommons.org/licenses/by-nc/4.0/info:eu-repo/semantics/openAccessAtribución-NoComercial 4.0 Internacional (CC BY-NC 4.0)http://purl.org/coar/access_right/c_abf2AlgoritmosPython lenguaje de programaciónModelos Event-BAlgorithmsPython programming languageEvent-B modelsEB2Python - Traducción automática de especificaciones Event-B en Rodin a PythonTrabajo de grado - Pregradoinfo:eu-repo/semantics/publishedVersionhttp://purl.org/coar/resource_type/c_7a1fTextinfo:eu-repo/semantics/bachelorThesishttp://purl.org/redcol/resource_type/TPhttp://purl.org/coar/version/c_970fb48d4fbd8a85ORIGINALLosada Calderón, Hernán Felipe - 2018.pdfDocumento trabajo de gradoapplication/pdf730299https://repositorio.escuelaing.edu.co/bitstream/001/789/1/Losada%20Calder%c3%b3n%2c%20Hern%c3%a1n%20Felipe%20-%202018.pdff7cf9ca4680b3d4e0a308f95fa5e5f45MD51open accessAutorización.pdfAutorización de Publicación en Repositorio Institucional de la Escuelaapplication/pdf888401https://repositorio.escuelaing.edu.co/bitstream/001/789/2/Autorizaci%c3%b3n.pdf968eb709f89a8bb72c2211dede7d5c24MD52metadata only accessLICENSElicense.txttext/plain1881https://repositorio.escuelaing.edu.co/bitstream/001/789/3/license.txt5a7ca94c2e5326ee169f979d71d0f06eMD53open accessTEXTLosada Calderón, Hernán Felipe - 2018.pdf.txtLosada Calderón, Hernán Felipe - 2018.pdf.txtExtracted texttext/plain46140https://repositorio.escuelaing.edu.co/bitstream/001/789/8/Losada%20Calder%c3%b3n%2c%20Hern%c3%a1n%20Felipe%20-%202018.pdf.txt33354c01e2da30fc2553173eec92cbd3MD58open accessAutorización.pdf.txtAutorización.pdf.txtExtracted texttext/plain2https://repositorio.escuelaing.edu.co/bitstream/001/789/10/Autorizaci%c3%b3n.pdf.txte1c06d85ae7b8b032bef47e42e4c08f9MD510metadata only accessTHUMBNAILLosada Calderón, Hernán Felipe - 2018.pdf.jpgLosada Calderón, Hernán Felipe - 2018.pdf.jpgGenerated Thumbnailimage/jpeg6244https://repositorio.escuelaing.edu.co/bitstream/001/789/9/Losada%20Calder%c3%b3n%2c%20Hern%c3%a1n%20Felipe%20-%202018.pdf.jpg60a6f3f893da33cc443fe8d4c7d309b6MD59open accessAutorización.pdf.jpgAutorización.pdf.jpgGenerated Thumbnailimage/jpeg13451https://repositorio.escuelaing.edu.co/bitstream/001/789/11/Autorizaci%c3%b3n.pdf.jpge7ed9dda95128dcf40c6b3cb3aae509aMD511metadata only access001/789oai:repositorio.escuelaing.edu.co:001/7892021-10-01 16:20:30.328open accessRepositorio Escuela Colombiana de Ingeniería Julio Garavitorepositorio.eci@escuelaing.edu.coU0kgVVNURUQgSEFDRSBQQVJURSBERUwgR1JVUE8gREUgUEFSRVMgRVZBTFVBRE9SRVMgREUgTEEgQ09MRUNDScOTTiAiUEVFUiBSRVZJRVciLCBPTUlUQSBFU1RBIExJQ0VOQ0lBLgoKQXV0b3Jpem8gYSBsYSBFc2N1ZWxhIENvbG9tYmlhbmEgZGUgSW5nZW5pZXLDrWEgSnVsaW8gR2FyYXZpdG8gcGFyYSBwdWJsaWNhciBlbCB0cmFiYWpvIGRlIGdyYWRvLCBhcnTDrWN1bG8sIHZpZGVvLCAKY29uZmVyZW5jaWEsIGxpYnJvLCBpbWFnZW4sIGZvdG9ncmFmw61hLCBhdWRpbywgcHJlc2VudGFjacOzbiB1IG90cm8gKGVuICAgIGFkZWxhbnRlIGRvY3VtZW50bykgcXVlIGVuIGxhIGZlY2hhIAplbnRyZWdvIGVuIGZvcm1hdG8gZGlnaXRhbCwgeSBsZSBwZXJtaXRvIGRlIGZvcm1hIGluZGVmaW5pZGEgcXVlIGxvIHB1YmxpcXVlIGVuIGVsIHJlcG9zaXRvcmlvIGluc3RpdHVjaW9uYWwsIAplbiBsb3MgdMOpcm1pbm9zIGVzdGFibGVjaWRvcyBlbiBsYSBMZXkgMjMgZGUgMTk4MiwgbGEgTGV5IDQ0IGRlIDE5OTMsIHkgZGVtw6FzIGxleWVzIHkganVyaXNwcnVkZW5jaWEgdmlnZW50ZQphbCByZXNwZWN0bywgcGFyYSBmaW5lcyBlZHVjYXRpdm9zIHkgbm8gbHVjcmF0aXZvcy4gRXN0YSBhdXRvcml6YWNpw7NuIGVzIHbDoWxpZGEgcGFyYSBsYXMgZmFjdWx0YWRlcyB5IGRlcmVjaG9zIGRlIAp1c28gc29icmUgbGEgb2JyYSBlbiBmb3JtYXRvIGRpZ2l0YWwsIGVsZWN0csOzbmljbywgdmlydHVhbDsgeSBwYXJhIHVzb3MgZW4gcmVkZXMsIGludGVybmV0LCBleHRyYW5ldCwgeSBjdWFscXVpZXIgCmZvcm1hdG8gbyBtZWRpbyBjb25vY2lkbyBvIHBvciBjb25vY2VyLgpFbiBtaSBjYWxpZGFkIGRlIGF1dG9yLCBleHByZXNvIHF1ZSBlbCBkb2N1bWVudG8gb2JqZXRvIGRlIGxhIHByZXNlbnRlIGF1dG9yaXphY2nDs24gZXMgb3JpZ2luYWwgeSBsbyBlbGFib3LDqSBzaW4gCnF1ZWJyYW50YXIgbmkgc3VwbGFudGFyIGxvcyBkZXJlY2hvcyBkZSBhdXRvciBkZSB0ZXJjZXJvcy4gUG9yIGxvIHRhbnRvLCBlcyBkZSBtaSBleGNsdXNpdmEgYXV0b3LDrWEgeSwgZW4gY29uc2VjdWVuY2lhLCAKdGVuZ28gbGEgdGl0dWxhcmlkYWQgc29icmUgw6lsLiBFbiBjYXNvIGRlIHF1ZWphIG8gYWNjacOzbiBwb3IgcGFydGUgZGUgdW4gdGVyY2VybyByZWZlcmVudGUgYSBsb3MgZGVyZWNob3MgZGUgYXV0b3Igc29icmUgCmVsIGRvY3VtZW50byBlbiBjdWVzdGnDs24sIGFzdW1pcsOpIGxhIHJlc3BvbnNhYmlsaWRhZCB0b3RhbCB5IHNhbGRyw6kgZW4gZGVmZW5zYSBkZSBsb3MgZGVyZWNob3MgYXF1w60gYXV0b3JpemFkb3MuIEVzdG8gCnNpZ25pZmljYSBxdWUsIHBhcmEgdG9kb3MgbG9zIGVmZWN0b3MsIGxhIEVzY3VlbGEgYWN0w7phIGNvbW8gdW4gdGVyY2VybyBkZSBidWVuYSBmZS4KVG9kYSBwZXJzb25hIHF1ZSBjb25zdWx0ZSBlbCBSZXBvc2l0b3JpbyBJbnN0aXR1Y2lvbmFsIGRlIGxhIEVzY3VlbGEsIGVsIENhdMOhbG9nbyBlbiBsw61uZWEgdSBvdHJvIG1lZGlvIGVsZWN0csOzbmljbywgCnBvZHLDoSBjb3BpYXIgYXBhcnRlcyBkZWwgdGV4dG8sIGNvbiBlbCBjb21wcm9taXNvIGRlIGNpdGFyIHNpZW1wcmUgbGEgZnVlbnRlLCBsYSBjdWFsIGluY2x1eWUgZWwgdMOtdHVsbyBkZWwgdHJhYmFqbyB5IGVsIAphdXRvci5Fc3RhIGF1dG9yaXphY2nDs24gbm8gaW1wbGljYSByZW51bmNpYSBhIGxhIGZhY3VsdGFkIHF1ZSB0ZW5nbyBkZSBwdWJsaWNhciB0b3RhbCBvIHBhcmNpYWxtZW50ZSBsYSBvYnJhIGVuIG90cm9zIAptZWRpb3MuRXN0YSBhdXRvcml6YWNpw7NuIGVzdMOhIHJlc3BhbGRhZGEgcG9yIGxhcyBmaXJtYXMgZGVsIChsb3MpIGF1dG9yKGVzKSBkZWwgZG9jdW1lbnRvLiAKU8OtIGF1dG9yaXpvIChhbWJvcykK |