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