Verificación de modelos independientes de la plataforma: un caso de estudio
El lenguaje UML ha sido ampliamente aceptado como el lenguaje estándar de modelado en la industria. El lenguaje OCL es una parte integral de UML, y fue introducido para definir restricciones adicionales que no se pueden expresar en este. Las expresiones OCL son concisas y precisas, y no presentan la...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | |
| Formato: | Tesis Tesis de grado |
| Lenguaje: | Español |
| Publicado: |
2017
|
| Materias: | |
| Acceso en línea: | http://sedici.unlp.edu.ar/handle/10915/67013 |
| Aporte de: |
| Sumario: | El lenguaje UML ha sido ampliamente aceptado como el lenguaje estándar de modelado en la industria. El lenguaje OCL es una parte integral de UML, y fue introducido para definir restricciones adicionales que no se pueden expresar en este. Las expresiones OCL son concisas y precisas, y no presentan las ambigüedades del lenguaje natural. Sin embargo, al ser una notación de diseño, OCL no es ejecutable: está definido sobre el modelo, por lo que sus restricciones no se reflejan en el código fuente.
Por otro lado, JML es un lenguaje de especificación formal que puede ser utilizado para especificar clases Java. A diferencia de OCL, las expresiones JML están escritas de forma que pueden ser compiladas y analizadas en tiempo de ejecución.
En este trabajo se propone transformar de forma automática las restricciones OCL a especificaciones escritas en el .onguaje JML. De esta forma se podrán verificar las restricciones en tiempo de ejecución, y se podrá hacer un análisis estático de estas mediante el uso de probadores de teoremas implementados para JML. |
|---|