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.
The Alf-verifier plug-in requires the following minimal requirements to be run:
The Alf-verifier is an Eclipse plug-in that needs to be installed in your computer according to the following instructions:
Once this is done the Alf-verifier plug-in is ready to be used!
In the following we show the main steps must be followed to use the Alf-verifier:
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:
The Alf-verifier takes as input a UML executable model composed by:
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:
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.
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.
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:
See a complete example here.
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.