AuRUS is a tool for the verification and validation of UML/OCL conceptual schemas. More specifically, it allows the user to check if a certain schema fulfills various predefined properties such as the non-redundancy of integrity constraints or the existence of a primary key for a certain class. Moreover, the user can define his own state-reachability tests.
It is possible to execute AuRUS via a web application http://folre.essi.upc.edu/aurus
You can find AuRUS in web application format at http://folre.essi.upc.edu/aurus
AuRUS can be used following these steps:
When the tool starts, it asks the user to load an .XMI file containing the conceptual schema.
AuRUS can deal with .XMI files generated by ArgoUML, a graphical UML editor. ArgoUML is an open-source tool that can be downloaded from http://argouml.tigris.org/
When the schema loads, AuRUS performs a decidability analysis over the schema. Through this analysis, AuRUS can guarantee, in certain schemas, that all the tests will finish, despite the fact that, in the general case, it is undecidable to reason on UML/OCL schemas.
Once the schema has been loaded, the tool is split into two tabs: Is the schema right? and Is it the right schema?. The first tab contains a set of predefined verification tests (class satisfiability, redundancy of constraints, etc.). The second tab presents some predefined validation tests (reflexiveness of recursive associations, missing the primary key in a class,etc.) and also allows the user to define his own state-reachability tests.
For the state-reachability tests, the user has to define the instances that are part of the state that he wishes to test.
The end of the execution of the tests is only guaranteed if the decidability analysis has determined that the schema is decidable. The reason why some tests may not end is that certain properties in a particular schema can only be proven by an infinite instantiation of the schema. Consequently, the tool is infinitely calculating the instantiation.
If, after a while, the tool does not return any result, it is highly likely that it is due to this.
A failed verification test points out a contradiction or redundancy in the conceptual schema. A failed validation test highlights a potential mistake in the representation of reality. It will require user intervention to determine if this is really the case.
In any case, AuRUS always returns either an instantiation showing the satisfiability of the test or an explanation of why it is is not possible to find it. This explanation consists of the integrity constraints that prevent the existence of this instantiation.
AuRUS is a research prototype developed by the FOLRE group at Universitat Politècnica de Catalunya-BarcelonaTech.
For any question, comment or suggestion, you can get in touch with us by sending an e-mail to: grull@essi.upc.edu o xoriol@essi.upc.edu