Alf Verifier

Showing Alf-verifier views:

Mostrant les vistes del verificador Alf

The Alf-verifier plug-in is designed to function as an Eclipse view. Therefore, the first thing to do is to tell Eclipse to show the corresponding views.

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

Check that both views are available in the views section:

Creating the UML/Alf executable model/Alf

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

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

Creating a UML class diagram

To create the UML class diagram, we recommend using the UML2Tools connector, an Eclipse connector for manipulating UML models.

To create a new UML class diagram using the 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