
Alf-verifier es un conector de Eclipse para verificar la corrección de los modelos ejecutables UML. La parte estática de estos modelos está representada por un diagrama de clases UML, mientras que la parte dinámica está representada por un conjunto de operaciones descritas con el nuevo estándar OMG Alf Action Language.

Alf-verifier puede comprobar la ejecución de estas operaciones; es decir, si se garantiza que generen un estado consistente después de la ejecución. Para modelos incorrectos, el verificador Alf devuelve un feedback significativo que ayuda a reparar las inconsistencias detectadas.
El conector Alf-verifier requiere los siguientes requisitos mínimos para ejecutarse:
Alf-verifier es un conector de Eclipse que debe instalarse en vuestro ordenador según las instrucciones siguientes:
¡Una vez hecho esto, el plug-in Alf-verifier está listo para ser utilizado!
A continuación mostramos los pasos principales que se deben seguir para utilizar Alf-verifier:
El plug-in Alf-verifier está diseñado para funcionar como vista de Eclipse. Por lo tanto, lo primero que hay que hacer es decirle a Eclipse que muestre las vistas correspondientes.
Para mostrar las vistas del verificador Alf, accede a: Window > Show View > Other y selecciona bajo SeverificationTreeView tanto Alf verifier – input como Alf verifier – feedback views.

Comprueba que las dos visualizaciones estén disponibles en la sección de visualizaciones:
Alf-verifier toma como entrada un modelo ejecutable UML compuesto por:
Para crear el diagrama de clases UML, os recomendamos que utilicéis el conector UML2Tools, un conector de Eclipse para manipular modelos UML.
Para crear un nuevo diagrama de clases UML usando el plug-in UML2Tools, ve a: File > New > Other y selecciona bajo UML2.1 Diagrams la opción Class Diagram.

Ahora, podemos crear un diagrama de clases UML completo utilizando la paleta de elementos UML. Tenga en cuenta que también podemos adjuntar restricciones de integridad OCL a nuestro diagrama de clases.

Como resultado, obtenemos dos archivos:
El archivo que contiene las operaciones Alf se puede crear utilizando archivos de texto de Eclipse o cualquier otra herramienta de edición. Debe guardarse con la extensión .alf

Para ver las reglas del lenguaje de acción Alf, haz clic aquí.
Nuestro método toma como entrada los archivos .uml y .alf. Para importar estos archivos, puede ir a la pestaña Alf verifier – input y hacer clic en los botones UML class diagram y Alf operations respectivamente.

Una vez importados los dos archivos, puede elegir cuál de las operaciones debe verificarse: para ello, hay disponible un combo de selección con todas las operaciones contenidas en el archivo de operaciones .alf más una opción «all», que verificará todas las operaciones incluidas en el archivo.
Luego, puede seleccionar la propiedad que desea verificar (ejecutabilidad débil o ejecutabilidad fuerte) haciendo clic en el botón correspondiente. Tras esto, los resultados de la verificación aparecerán en la pestaña Alf-verifier Feedback.

Una vez finaliza la verificación, la pestaña Alf verifier – Feedback muestra el resultado de la verificación:

Como se puede observar, el feedback proporcionado por Alf-verifier consiste en un árbol con estos niveles:
Vea un ejemplo completo aquí.
En el siguiente video-tutorial mostramos cómo se puede utilizar Alf-verifier para verificar la ejecutabilidad de una operación basada en acciones Alf. El video-tutorial utiliza el diagrama de clases UML de un sistema de cadena de restaurantes como ejemplo de ejecución.
Alf-verifier es un prototipo de investigación desarrollado por el grupo de investigación Conceptual Modeling of Information Systems de la Universitat Oberta de Catalunya.
Para cualquier pregunta o sugerencia, no dude en ponerse en contacto con nosotros enviando un correo electrónico a eplanash@uoc.edu
