AURUS
Introducció
AuRUS es una herramienta para la verificación y validación de esquemas conceptuales UML/OCL. En concreto, permite probar si un esquema cumple diferentes propiedades predefinidas com la no redundancia de restricciones o la existencia de una clave primaria para tota clase. Además, el usuario puede definir sus propios tests de asolimiento de estado.
Podéis ejecutar AuRUS mediante la aplicación web http://folre.essi.upc.edu/aurus
Características principales
- Decidibilidad: Razonar sobre esquemas UML/OCL es, en general, indecidible, por lo que algunos de los tests executados pueden no terminar nunca. No obstante, el razonamiento sobre un esquema conceptual concreto sí puede ser decidible. AuRUS testea los esquemas conceptuales para comprobar si cumplen una serie de propiedades que aseguran la decidibilidad y así, asegurar la finalización de todos sus tests.
- Expresividad: AuRUS no renuncia a la expressividad del UML/OCL. En concreto, admite clases, asociaciones, asociaciones n-arias, clases asociativas, restricciones de cardinalidad mínima/máxima, etc. Consultad el manual de usuario (en inglés) para más detalles.
- Completitud: Si el análisis de decidibilidad concluye que el esquema es decidible, AuRUS responde por cada test con la instanciación que prueba el test, o bien con una explicación.
- Explicaciones: Si un test falla, AuRUS es capaz de argumentar qué restricciones UML/OCL son las que impiden encontrar la instanciación que prueba el test. De esta forma, AuRUS guía al usuario sobre cómo poder corregir el esquema conceptual.
Instal·lació
Ús
Podéis probar AuRUS en formato de aplicación web en la dirección http://folre.essi.upc.edu/aurus
AuRUS se utilitza mediante los siguientes pasos:
- Carga del esquema conceptual
- Selección de los tests automáticos a probar o definición del test manual
- Ejecución de los tests
- Análisis de los resultados
Carga del esquema conceptual
Al iniciar la herramienta, se pide que carguéis un fichero .XMI que contenga el esquema conceptual..
AuRUS acepta los ficheros .XMI generados por el editor gráfico ArgoUML. . ArgoUML es una herramienta opensource que podéis obtener gratuitamente en la siguiente dirección http://argouml.tigris.org/
Al cargar el esquema, AuRUS realiza un análisis de decidibilidad sobre éste. Mediante dicho análisis, AuRUS es capaz de garantizar, en ciertos esquemas, la terminación de todos los tests a pesar de la indecidibilidad del razonamiento en UML/OCL en el caso general.
Selección de los tests automáticos a probar o definición del test manual
Una vez cargado el esquema, se muestran dos pestañas: Is the schema right? y Is it the right schema?. La primera pestaña contiente una serie de tests predefinidos de verifación (satisfactibilidad de clases, redundancia de restricciones, etc) la segunda, os permite elegir entre utilizar unos tests predefinidos de validación (reflexividad de asociaciones recursivas, absencia de clave primaria en clases, etc) o definir un test de asolimiento de estado.
En el caso del test de asolimiento de estado, se requiere que defináis las instancias que configuran el estado que queréis poner a prueba.
Ejecución de los tests
La terminación de los tests solo está garantizado si el análisis de decidibilidad determinó que el esquema es decidible. La fuente de no terminación de los tests radica en que ciertas propiedades en un determinado esquema solo se pueden probar mediante una instanciación infinita del esquema, por lo que la herramienta se queda infinitamente calculando la instanciación.
Si al cabo de un largo rato no se os devuelve ningún resultado, es posible que os encontréis en uno de estos casos.
Análisis de los resultados
Un test de verificación fallido indica una contradicción y/o redundancia en el esquema conceptual. Un test de validación fallido señala una posible modelización incorrecta de la realidad que requiere la intervención del usuario para ser contrastada.
En cualquier caso, AuRUS siempre responde o bien con una instanciación que prueba el test o bien con una explicación de por qué no se puede hallar tal instanciación. Dicha explicación consta de las restricciones de integridad que impiden la existencia de dicha instanciación.
Quant a
Documentació
Documentación básica
- Manual del usuario (en inglés)
Publicaciones relacionadas
- Queralt, A., Teniente, E.: Verification and validation of UML conceptual schemas with OCL constraints. ACM Transactions on Software Engineering and Methodology (TOSEM) (2012)
- Queralt, A., Rull, G., Teniente, E., Farré, C., & Urpí, T: AuRUS: automated reasoning on UML/OCL schemas. In Conceptual Modeling–ER (2010).
Contacte
AuRUS es un prototipo de investigación desarrollado por el grupo FOLRE en la Universitat Politècnica de Catalunya-BarcelonaTech.
Para cualquier duda o sugerencia, os podéis poner en contacto con nosotros a través de los correos: grull@essi.upc.edu o xoriol@essi.upc.edu