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...
- 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/