Evaluación del desempeño del generador de código EVENTB2JAVA

En este documento se presenta un caso de estudio que permitió evaluar el desempeño de la herramienta EventB2Java; dicho caso consistió en modelar formalmente un módulo de inventarios que fue traducido a código Java+JML y que posteriormente se incorporó en elsoftware opensource Openbravo POS, la eval...

Full description

Autores:
Hernández Gómez , Carlos Andrés
Tipo de recurso:
Masters Thesis
Fecha de publicación:
2014
Institución:
Pontificia Universidad Javeriana Cali
Repositorio:
Vitela
Idioma:
spa
OAI Identifier:
oai:vitela.javerianacali.edu.co:11522/1919
Acceso en línea:
https://vitela.javerianacali.edu.co/handle/11522/1919
Palabra clave:
Event-B
EventB2Java
Rodin
JML
Openbravo
POS
Rights
License
https://creativecommons.org/licenses/by-nc-nd/4.0/
id Vitela2_bf7171374054ecb31c952b715f5d12dd
oai_identifier_str oai:vitela.javerianacali.edu.co:11522/1919
network_acronym_str Vitela2
network_name_str Vitela
repository_id_str
dc.title.spa.fl_str_mv Evaluación del desempeño del generador de código EVENTB2JAVA
title Evaluación del desempeño del generador de código EVENTB2JAVA
spellingShingle Evaluación del desempeño del generador de código EVENTB2JAVA
Event-B
EventB2Java
Rodin
JML
Openbravo
POS
title_short Evaluación del desempeño del generador de código EVENTB2JAVA
title_full Evaluación del desempeño del generador de código EVENTB2JAVA
title_fullStr Evaluación del desempeño del generador de código EVENTB2JAVA
title_full_unstemmed Evaluación del desempeño del generador de código EVENTB2JAVA
title_sort Evaluación del desempeño del generador de código EVENTB2JAVA
dc.creator.fl_str_mv Hernández Gómez , Carlos Andrés
dc.contributor.advisor.none.fl_str_mv Cataño, Néstor
dc.contributor.author.none.fl_str_mv Hernández Gómez , Carlos Andrés
dc.subject.none.fl_str_mv Event-B
EventB2Java
Rodin
JML
Openbravo
POS
topic Event-B
EventB2Java
Rodin
JML
Openbravo
POS
description En este documento se presenta un caso de estudio que permitió evaluar el desempeño de la herramienta EventB2Java; dicho caso consistió en modelar formalmente un módulo de inventarios que fue traducido a código Java+JML y que posteriormente se incorporó en elsoftware opensource Openbravo POS, la evaluación del desempeño se realizó comparandola versi_on original del mismo vs la medicada. En este trabajo también se mejoró elrendimiento del conjunto de clases que usa la herramienta haciendo uso de los objetosdisponibles en el SDK de Java y se presentan las reglas de traducción y el análisis previollevado a cabo para traducir de un modelo en Event-B a código Java + especificaciónen JML.
publishDate 2014
dc.date.issued.none.fl_str_mv 2014
dc.date.accessioned.none.fl_str_mv 2024-06-06T21:18:33Z
dc.date.available.none.fl_str_mv 2024-06-06T21:18:33Z
dc.type.coar.none.fl_str_mv http://purl.org/coar/resource_type/c_bdcc
dc.type.local.none.fl_str_mv Tesis/Trabajo de grado - Monografía - Maestría
dc.type.redcol.none.fl_str_mv https://purl.org/redcol/resource_type/TM
format http://purl.org/coar/resource_type/c_bdcc
dc.identifier.uri.none.fl_str_mv https://vitela.javerianacali.edu.co/handle/11522/1919
url https://vitela.javerianacali.edu.co/handle/11522/1919
dc.language.iso.none.fl_str_mv spa
language spa
dc.rights.uri.none.fl_str_mv https://creativecommons.org/licenses/by-nc-nd/4.0/
dc.rights.creativecommons.none.fl_str_mv https://creativecommons.org/licenses/by-nc-nd/4.0/
dc.rights.accessrights.none.fl_str_mv http://purl.org/coar/access_right/c_abf2
rights_invalid_str_mv https://creativecommons.org/licenses/by-nc-nd/4.0/
http://purl.org/coar/access_right/c_abf2
dc.format.extent.none.fl_str_mv 143 p.
dc.format.mimetype.none.fl_str_mv application/pdf
dc.publisher.none.fl_str_mv Pontificia Universidad Javeriana Cali
publisher.none.fl_str_mv Pontificia Universidad Javeriana Cali
institution Pontificia Universidad Javeriana Cali
bitstream.url.fl_str_mv https://vitela.javerianacali.edu.co/bitstreams/c4e1fdcd-2bdd-480f-930c-e46b2da4f186/download
https://vitela.javerianacali.edu.co/bitstreams/b3b0d3aa-6801-40d6-9023-2b3c602f1426/download
https://vitela.javerianacali.edu.co/bitstreams/fdb7b1f7-f6be-4458-a92e-151aa287a30e/download
https://vitela.javerianacali.edu.co/bitstreams/e51883b2-b211-4b57-95b9-824158f3c0e3/download
https://vitela.javerianacali.edu.co/bitstreams/a8435d8b-ab47-4d28-8a5b-0636f9f5bf5c/download
https://vitela.javerianacali.edu.co/bitstreams/e682868e-6901-4f46-ae1c-2fa8ea115ee4/download
https://vitela.javerianacali.edu.co/bitstreams/225c7028-5966-4ce7-8bc4-605e4901d186/download
bitstream.checksum.fl_str_mv b9a689b76d8da4f2f7e2973995874ea0
6463b054756890cdb78f509d9ab835e1
8a4605be74aa9ea9d79846c1fba20a33
1e785c2685cdbc48878e4ce8ee7bffd9
f9ea2c5cffc6b592d09e68a2b60a7d54
4c54d6c56fce96eb63f90c92e710821a
157553d9362ca7f8e2c982c30c53eaf0
bitstream.checksumAlgorithm.fl_str_mv MD5
MD5
MD5
MD5
MD5
MD5
MD5
repository.name.fl_str_mv Repositorio Vitela
repository.mail.fl_str_mv vitela.mail@javerianacali.edu.co
_version_ 1829956336257859584
spelling Cataño, NéstorHernández Gómez , Carlos Andrés2024-06-06T21:18:33Z2024-06-06T21:18:33Z2014https://vitela.javerianacali.edu.co/handle/11522/1919En este documento se presenta un caso de estudio que permitió evaluar el desempeño de la herramienta EventB2Java; dicho caso consistió en modelar formalmente un módulo de inventarios que fue traducido a código Java+JML y que posteriormente se incorporó en elsoftware opensource Openbravo POS, la evaluación del desempeño se realizó comparandola versi_on original del mismo vs la medicada. En este trabajo también se mejoró elrendimiento del conjunto de clases que usa la herramienta haciendo uso de los objetosdisponibles en el SDK de Java y se presentan las reglas de traducción y el análisis previollevado a cabo para traducir de un modelo en Event-B a código Java + especificaciónen JML.In this document, a case study is presented which evaluated the performance of theEventB2Java tool. In the case study, which consisted of formally modeling a moduleof inventories translated to Java + JML code and later incorporating it into the opensource Openbravos POS software, the performance evaluation was done by comparingthe original version of the code vs the modi_ed version. In this evaluation we found thatthe modi_ed version did improve the rendition of classes using the aforementioned tool.143 p.application/pdfspaPontificia Universidad Javeriana Calihttps://creativecommons.org/licenses/by-nc-nd/4.0/https://creativecommons.org/licenses/by-nc-nd/4.0/http://purl.org/coar/access_right/c_abf2Event-BEventB2JavaRodinJMLOpenbravoPOSEvaluación del desempeño del generador de código EVENTB2JAVAhttp://purl.org/coar/resource_type/c_bdccTesis/Trabajo de grado - Monografía - Maestríahttps://purl.org/redcol/resource_type/TMFacultad de Ingeniería y Ciencias. Maestría en IngenieríaPontificia Universidad Javeriana CaliMaestríaORIGINALlicencia de uso.pdflicencia de uso.pdfapplication/pdf808010https://vitela.javerianacali.edu.co/bitstreams/c4e1fdcd-2bdd-480f-930c-e46b2da4f186/downloadb9a689b76d8da4f2f7e2973995874ea0MD51Evaluación del desempeño del generador de código EventB2Java.pdfEvaluación del desempeño del generador de código EventB2Java.pdfapplication/pdf4473310https://vitela.javerianacali.edu.co/bitstreams/b3b0d3aa-6801-40d6-9023-2b3c602f1426/download6463b054756890cdb78f509d9ab835e1MD52LICENSElicense.txtlicense.txttext/plain; charset=utf-81748https://vitela.javerianacali.edu.co/bitstreams/fdb7b1f7-f6be-4458-a92e-151aa287a30e/download8a4605be74aa9ea9d79846c1fba20a33MD52TEXTlicencia de uso.pdf.txtlicencia de uso.pdf.txtExtracted texttext/plain4800https://vitela.javerianacali.edu.co/bitstreams/e51883b2-b211-4b57-95b9-824158f3c0e3/download1e785c2685cdbc48878e4ce8ee7bffd9MD511Evaluación del desempeño del generador de código EventB2Java.pdf.txtEvaluación del desempeño del generador de código EventB2Java.pdf.txtExtracted texttext/plain101534https://vitela.javerianacali.edu.co/bitstreams/a8435d8b-ab47-4d28-8a5b-0636f9f5bf5c/downloadf9ea2c5cffc6b592d09e68a2b60a7d54MD513THUMBNAILlicencia de uso.pdf.jpglicencia de uso.pdf.jpgGenerated Thumbnailimage/jpeg5339https://vitela.javerianacali.edu.co/bitstreams/e682868e-6901-4f46-ae1c-2fa8ea115ee4/download4c54d6c56fce96eb63f90c92e710821aMD512Evaluación del desempeño del generador de código EventB2Java.pdf.jpgEvaluación del desempeño del generador de código EventB2Java.pdf.jpgGenerated Thumbnailimage/jpeg3453https://vitela.javerianacali.edu.co/bitstreams/225c7028-5966-4ce7-8bc4-605e4901d186/download157553d9362ca7f8e2c982c30c53eaf0MD51411522/1919oai:vitela.javerianacali.edu.co:11522/19192024-06-25 05:13:35.322https://creativecommons.org/licenses/by-nc-nd/4.0/open.accesshttps://vitela.javerianacali.edu.coRepositorio Vitelavitela.mail@javerianacali.edu.coTk9URTogUExBQ0UgWU9VUiBPV04gTElDRU5TRSBIRVJFClRoaXMgc2FtcGxlIGxpY2Vuc2UgaXMgcHJvdmlkZWQgZm9yIGluZm9ybWF0aW9uYWwgcHVycG9zZXMgb25seS4KCk5PTi1FWENMVVNJVkUgRElTVFJJQlVUSU9OIExJQ0VOU0UKCkJ5IHNpZ25pbmcgYW5kIHN1Ym1pdHRpbmcgdGhpcyBsaWNlbnNlLCB5b3UgKHRoZSBhdXRob3Iocykgb3IgY29weXJpZ2h0Cm93bmVyKSBncmFudHMgdG8gRFNwYWNlIFVuaXZlcnNpdHkgKERTVSkgdGhlIG5vbi1leGNsdXNpdmUgcmlnaHQgdG8gcmVwcm9kdWNlLAp0cmFuc2xhdGUgKGFzIGRlZmluZWQgYmVsb3cpLCBhbmQvb3IgZGlzdHJpYnV0ZSB5b3VyIHN1Ym1pc3Npb24gKGluY2x1ZGluZwp0aGUgYWJzdHJhY3QpIHdvcmxkd2lkZSBpbiBwcmludCBhbmQgZWxlY3Ryb25pYyBmb3JtYXQgYW5kIGluIGFueSBtZWRpdW0sCmluY2x1ZGluZyBidXQgbm90IGxpbWl0ZWQgdG8gYXVkaW8gb3IgdmlkZW8uCgpZb3UgYWdyZWUgdGhhdCBEU1UgbWF5LCB3aXRob3V0IGNoYW5naW5nIHRoZSBjb250ZW50LCB0cmFuc2xhdGUgdGhlCnN1Ym1pc3Npb24gdG8gYW55IG1lZGl1bSBvciBmb3JtYXQgZm9yIHRoZSBwdXJwb3NlIG9mIHByZXNlcnZhdGlvbi4KCllvdSBhbHNvIGFncmVlIHRoYXQgRFNVIG1heSBrZWVwIG1vcmUgdGhhbiBvbmUgY29weSBvZiB0aGlzIHN1Ym1pc3Npb24gZm9yCnB1cnBvc2VzIG9mIHNlY3VyaXR5LCBiYWNrLXVwIGFuZCBwcmVzZXJ2YXRpb24uCgpZb3UgcmVwcmVzZW50IHRoYXQgdGhlIHN1Ym1pc3Npb24gaXMgeW91ciBvcmlnaW5hbCB3b3JrLCBhbmQgdGhhdCB5b3UgaGF2ZQp0aGUgcmlnaHQgdG8gZ3JhbnQgdGhlIHJpZ2h0cyBjb250YWluZWQgaW4gdGhpcyBsaWNlbnNlLiBZb3UgYWxzbyByZXByZXNlbnQKdGhhdCB5b3VyIHN1Ym1pc3Npb24gZG9lcyBub3QsIHRvIHRoZSBiZXN0IG9mIHlvdXIga25vd2xlZGdlLCBpbmZyaW5nZSB1cG9uCmFueW9uZSdzIGNvcHlyaWdodC4KCklmIHRoZSBzdWJtaXNzaW9uIGNvbnRhaW5zIG1hdGVyaWFsIGZvciB3aGljaCB5b3UgZG8gbm90IGhvbGQgY29weXJpZ2h0LAp5b3UgcmVwcmVzZW50IHRoYXQgeW91IGhhdmUgb2J0YWluZWQgdGhlIHVucmVzdHJpY3RlZCBwZXJtaXNzaW9uIG9mIHRoZQpjb3B5cmlnaHQgb3duZXIgdG8gZ3JhbnQgRFNVIHRoZSByaWdodHMgcmVxdWlyZWQgYnkgdGhpcyBsaWNlbnNlLCBhbmQgdGhhdApzdWNoIHRoaXJkLXBhcnR5IG93bmVkIG1hdGVyaWFsIGlzIGNsZWFybHkgaWRlbnRpZmllZCBhbmQgYWNrbm93bGVkZ2VkCndpdGhpbiB0aGUgdGV4dCBvciBjb250ZW50IG9mIHRoZSBzdWJtaXNzaW9uLgoKSUYgVEhFIFNVQk1JU1NJT04gSVMgQkFTRUQgVVBPTiBXT1JLIFRIQVQgSEFTIEJFRU4gU1BPTlNPUkVEIE9SIFNVUFBPUlRFRApCWSBBTiBBR0VOQ1kgT1IgT1JHQU5JWkFUSU9OIE9USEVSIFRIQU4gRFNVLCBZT1UgUkVQUkVTRU5UIFRIQVQgWU9VIEhBVkUKRlVMRklMTEVEIEFOWSBSSUdIVCBPRiBSRVZJRVcgT1IgT1RIRVIgT0JMSUdBVElPTlMgUkVRVUlSRUQgQlkgU1VDSApDT05UUkFDVCBPUiBBR1JFRU1FTlQuCgpEU1Ugd2lsbCBjbGVhcmx5IGlkZW50aWZ5IHlvdXIgbmFtZShzKSBhcyB0aGUgYXV0aG9yKHMpIG9yIG93bmVyKHMpIG9mIHRoZQpzdWJtaXNzaW9uLCBhbmQgd2lsbCBub3QgbWFrZSBhbnkgYWx0ZXJhdGlvbiwgb3RoZXIgdGhhbiBhcyBhbGxvd2VkIGJ5IHRoaXMKbGljZW5zZSwgdG8geW91ciBzdWJtaXNzaW9uLgo=