Alf Verifier

Introducció

The Alf-verifier is an Eclipse plug-in for verifying the correctness of UML executable models. The static part of such models is represented by a UML class diagram, while the dynamic part is represented by a set of operations described using the new OMG standard Alf Action Language.

The Alf-verifier can check the executability of such operations, i.e. whether they are guaranteed to generate a consistent state after executing. For incorrect models, the Alf-verifier returns a meaningful feedback that helps repairing the detected inconsistencies.

Main features

  • The Alf-verifier is a release of a research prototype concieved as an Eclipse plug-in.
  • The Alf-verifier allows specifying a UML executable model by a UML class diagram (to specify the static part of the model) and a set of Alf-action-based operations (to specify the dynamic part of the model).
  • The Alf-verifier can help the designers to improve the quality of her UML executable models by checking the executability of the operations belonging to the dynamic model. An operation is weakly executable when there is a chance that a user may successfully execute it; and an operation is strongly executable when it is always successfully executed.
  • For non-executable operations, the Alf-verifier is able to provide a meaningful feedback by identifying the source of the inconsistency and suggesting possible corrections to repair them.

Instal·lació

Requirements

The Alf-verifier plug-in requires the following minimal requirements to be run:

 

Installation instructions

The Alf-verifier is an Eclipse plug-in that needs to be installed in your computer according to the following instructions:

  1. Download the Alf-verifier jar file from here.
  2. Unzip the file in the \eclipse\plugins folder.
  3. Restart your Eclipse.

Once this is done the Alf-verifier plug-in is ready to be used!

Ús

In the following we show the main steps must be followed to use the Alf-verifier:

Showing the Alf-verifier views

The Alf-verifier plug-in is designed to work as an Eclipse view. Therefore, the first thing to be done is telling Eclipse to show the corresponding views.

To show the Alf-verifier views, go to: Window > Show View > Other and select under SeverificationTreeView both the Alf verifier – input and the Alf verifier - feedback views.

Check the two views are available in the views section:

Creating a UML/Alf executable model

The Alf-verifier takes as input a UML executable model composed by:

  • A structural model represented as a UML class diagram.
  • A behavioural model represented as a set of operations described in Alf action language.

Creating a UML class diagram

In order to create the UML class diagram, we recommend using the UML2Tools plug-in, an Eclipse plug-in for manipulating UML models.

To create a new UML Class Diagram using UML2Tools plug-in, go to: File > New > Other and select under UML2.1 Diagrams the Class Diagram option.

Now, we can create a complete UML class diagram using the palette of UML elements. Note that we can also attach OCL integrity constraints to our class diagram.

As a result, we obtain two files:

  • A .uml file: Containing information about the class diagram.
  • A .umlclass file: Containing information on the graphical representation of the class diagram.

Creating Alf operations

The file containing the Alf operations can be created using Eclipse text files or other any editing tool. It must be saved with extension .alf

To see the rules of the Alf action language, go here.

Importing .uml and .alf files to Alf-verifier

Our method takes as input the .uml and the .alf files. In order to import these files, you can go to the Alf verifier – input tab and click on UML class diagram and  Alf operations button respectively.

Once the two files has been imported, you can choose which of the operations should be verifier: in order to do this a select combo is available with all the operations contained in .alf operations file plus an “all” option, which will verify all the operations included in the file.

Then, you can select the property you want to verify (weak executability or strong executability) by clicking at the corresponding button. After that, the results of the verification will appear in Alf-verifier Feedback tab.

Feedback

Once the verification ends, the Alf verifier – Feedback tab shows the result of the verification:

As can be observed, the feedback provided by Alf-verifier consists of a tree with these levels:

  • Level 1: Operation : Show the name of the operation being verified.
  • Level 2: Execution path : Show the i-th execution path of the operation, where an execution path is a consecutive sequence of actions that can be followed during the execution of the operation.
  • Level 3: Instruction : Show the j-th instruction of the i-th execution path.
  • Level 4: Violated constraints : Show the constraints the j-th sentence may violate.
  • Level 5: Solving proposals:
    • Level 5.1: Queries : Only when it is necessary, show the (basic) queries that the user may manually resolve to help during the verification process.
    • Level 5.2: Code : Show one or several alternative code blocks to be added to the operation in order to ensure the violated constraints will not be violated.

Example

See a complete example here.

Video-tutorial

In the following video-tutorial we show how the Alf-verifier can be used in order to verify the executability of an Alf-action-based operation. The video-tutorial uses the UML class diagram of a restaurant chain system as a running example.

Alf-verifier: Example of Use

Quant a

Documentació

Basic documentation

  • Alf-verifier: Installation Guide
    This documentation contains the instructions to install the Alf-verifier plug-in.
  • Alf-verifier: User Guide
    This documentation contains the instructions to make use of of the Alf-verifier through an example to illustrate the whole verification process.

Video-tutorial

Related publications

  • Elena Planas: Lightweight and Static Verification of UML Executable Models. PhD Thesis. Advised by: Dr. Jordi Cabot and 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. Pag. 378-382 (2012)
  • Elena Planas, Jordi Cabot, Cristina Gómez: Lightweight Verification of Executable Models. In: Proceedings of Conceptual Modeling (ER). LNCS vol. 6998. Pag. 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. Pag. 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). Pag. 62-71 (2008)

Contacte

The Alf-verifier is a research prototype developed by the Conceptual Modeling of Information Systems Research Group at the Open University of Catalonia.

For any question or suggestion, feel free to contact us by sending an email to eplanash@uoc.edu

Treball Futur

Suggeriments