AURUS
Introducció
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
Main features
- Decidability: Reasoning on UML/OCL schemas is, in the general case, undecidable. Consequently, some of the tests may never finish. However, reasoning on a certain conceptual schema can be decidable. AuRUS tests the conceptual schemas to check if they fulfill certain properties that guarantee their decidability and, therefore, ensure that all the tests finish in finite time.
- Expressivity: AuRUS does not sacrifice the UML/OCL expressivity. In particular, it allows classes, associations, n-ary associations, association classes, minimum/maximum cardinality constraints, etc. Check the user manual for more details..
- Completeness: If the decidability analysis concludes that the schema is decidable, then AuRUS will return, for each test, either the instantiation proving that the test is satisfiable, or an explanation.
- Explanation: If a test fails, AuRUS is capable of determining which UML/OCL restrictions prevent it from finding an instantiation that satifies the test. In this way, AuRUS guides the user to correct the conceptual schema.
Instal·lació
Ús
You can find AuRUS in web application format at http://folre.essi.upc.edu/aurus
AuRUS can be used following these steps:
- Load the conceptual schema
- Select automatic tests or define new manual test
- Test execution
- Result analysis
Load the conceptual schema
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.
Select automatic tests or define new manual test
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.
Tests' execution
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.
Results' analysis
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.
Quant a
Documentació
Basic documentation
Related publications
- Queralt, A., Teniente, E.: Verification and validation of UML conceptual schemas with OCL constraints. ACM Transactions on Software Engineering and Methodology (TOSEM) (2012)
- Queralt, A., Rull, G., Teniente, E., Farré, C., & Urpí, T: AuRUS: automated reasoning on UML/OCL schemas. In Conceptual Modeling–ER (2010).
Contacte
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