Alf Verifier

Introducción

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.

Principales características

  • Alf-verifier es el lanzamiento de un prototipo de investigación concebido como un plug-in de Eclipse.
  • El verificador Alf permite especificar un modelo ejecutable UML mediante un diagrama de clases UML (para especificar la parte estática del modelo) y un conjunto de operaciones basadas en acciones Alf (para especificar la parte dinámica del modelo).
  • Alf-verifier puede ayudar a los diseñadores a mejorar la calidad de sus modelos ejecutables UML controlando la ejecución de las operaciones pertenecientes al modelo dinámico. Una operación es débilmente ejecutable cuando existe la posibilidad de que un usuario pueda ejecutarla correctamente; y una operación es fuertemente ejecutable cuando siempre se ejecuta con éxito.
  • Para operaciones no ejecutables, el verificador Alf puede proporcionar un feedback significativo identificando la fuente de la inconsistencia y sugiriendo posibles correcciones para repararlas.

 

 

Instalación

Requerimientos

El conector Alf-verifier requiere los siguientes requisitos mínimos para ejecutarse:

Instrucciones de instalación 

Alf-verifier es un conector de Eclipse que debe instalarse en vuestro ordenador según las instrucciones siguientes:

  1. Descarga el archivo jar del verificador Alf aquí.
  2. Descomprime el archivo en la carpeta \eclipse\plugins.
  3. Reinicia tu Eclipse.

¡Una vez hecho esto, el plug-in Alf-verifier está listo para ser utilizado!

Uso

A continuación mostramos los pasos principales que se deben seguir para utilizar Alf-verifier:

Mostrando las vistas del verificador Alf

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:

Creando el modelo ejecutable de UML/Alf 

Alf-verifier toma como entrada un modelo ejecutable UML compuesto por:

  • Un modelo estructural representado como diagrama de clases UML.
  • Un modelo de comportamiento representado como un conjunto de operaciones descrito en el lenguaje de acción Alf.

Creación de un diagrama de clases UML

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:

  • Un archivo .uml: que contiene información sobre el diagrama de clases.
  • Un archivo .umlclass: que contiene información sobre la representación gráfica del diagrama de clases.

Creación de operaciones Alf

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

Importación de archivos .uml y .alf a Alf-verifier

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.

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:

  • Nivel 1: Operation: Muestra el nombre de la operación que se está verificando.
  • Nivel 2: Execution path: Muestra el i-ésimo camino de ejecución de la operación, donde un camino de ejecución es una secuencia consecutiva de acciones que se pueden seguir durante la ejecución de la operación.
  • Nivel 3: Instruction: Muestra la j-ésima instrucción del i-ésimo camino de ejecución.
  • Nivel 4: Violated constraints: Muestra las restricciones que la j-ésima sentencia puede violar.
  • Nivel 5: Solving proposals:
    • Nivel 5.1: Queries: Solo cuando sea necesario, muestra las consultas (básicas) que el usuario puede resolver manualmente para ayudar durante el proceso de verificación.
    • Nivel 5.2: Code: Muestra uno o varios bloques de código alternativos para añadir a la operación con el fin de asegurar que las restricciones no sean violadas.

Ejemplo

Vea un ejemplo completo aquí.

Video-tutorial

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: Ejemplo de uso

Información

Documentación

Documentación básica

  • Alf-verifier: Installation Guide
    Esta documentación contiene las instrucciones para instalar el conector Alf-verifier.
  • Alf-verifier: User Guide
    Esta documentación contiene las instrucciones para hacer uso del verificador Alf mediante un ejemplo para ilustrar todo el proceso de verificación.

Video-tutorial

Publicaciones relacionadas

  • Elena Planas: Lightweight and Static Verification of UML Executable Models. PhD Thesis. Dirigida por: Dr. Jordi Cabot y Dra. Cristina Gómez. Universitat Politècnica de Catalunya (2013)
  • Elena Planas, David Sanchez-Mendoza, Jordi Cabot, Cristina Gómez: Alf-Verifier: An Eclipse Plugin for Verifying Alf/UML Executable Models. In: Proceedings of Conceptual Modeling Workshops (ER). LNCS vol. 7518. Pág. 378-382 (2012)
  • Elena Planas, Jordi Cabot, Cristina Gómez: Lightweight Verification of Executable Models. In: Proceedings of Conceptual Modeling (ER). LNCS vol. 6998. Pág. 467-475 (2011)
  • Elena Planas: A Framework for Verifying UML Behavioral Models. In: Proceedings of CAiSE – Doctoral Consortium (2009)
  • Elena Planas, Jordi Cabot, Cristina Gómez: Verifying Action Semantics Specifications in UML Behavioral Models. In: Proceedings of International Conference on Advanced Information Systems (CAiSE). LNCS vol. 5565. Pág. 125-140 (2009)
  • Elena Planas, Jordi Cabot, Cristina Gómez: Verifying Action Semantics Specifications in UML Behavioral Models (Extended Version). LSI-09-6-R LSI Research Report, Universitat Politècnica de Catalunya (2009)
  • Elena Planas, Jordi Cabot, Cristina Gómez: Verificación de la ejecutabilidad de operaciones definidas con Action Semantics. In: Actas de los Talleres de las Jornadas de Ingeniería del Software y Bases de Datos – Desarrollo de Software Dirigido por Modelos (DSDM). Pág. 62-71 (2008)

Contacto

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

Trabajo futuro

Sugerimientos