Alf Verifier

A continuació mostrem els passos principals que s’ha de seguir per utilitzar l’Alf-verifier:

Mostrant les vistes del verificador Alf

El plug-in Alf-verifier està dissenyat per funcionar com a vista d'Eclipsi. Per tant, el primer que cal fer és dir-li a Eclipse que mostri les vistes corresponents.

Per mostrar les vistes del verificador Alf, accedeix a: Window > Show View > Other i selecciona sota SeverificationTreeView ambdos Alf verifier – input i el Alf verifier - feedback views.

Comproveu que les dues visualitzacions estiguin disponibles a la secció de visualitzacions:

Creant el model executable de UML/Alf 

L'Alf-verifier pren com a entrada un model executable UML compost per:

• Un model estructural representat com a diagrama de classes UML.
• Un model de comportament representat com un conjunt d’operacions descrit en el llenguatge d’acció Alf.

Creació d'un diagrama de classes UML

Per crear el diagrama de classes UML, us recomanem que utilitzeu el connector UML2Tools, un connector Eclipse per manipular models UML.

Per crear un nou diagrama de classes UML usant UML2Tools plug-in, ves a: File > New > Other i selecciona sota UML2.1 Diagrams l'opcio Class Diagram.

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