AURUS
Introducció
AuRUS és una eina per la verificació i validació d'esquemes conceptuals UML/OCL. En concret, permet provar si un esquema compleix diferents propietats predefinides com la no redundància de restriccions o l'existència d'una clau primària per tota classe. A més a més, l'usuari pot definir els seus propis tests d'assoliment d'estat.
Podeu executar AuRUS a través de l'aplicació web http://folre.essi.upc.edu/aurus
Característiques principals
- Decidibilitat: raonar sobre esquemes UML/OCL és, en general, indecidible, pel que alguns dels tests executats poden no acabar mai. No obstant, el raonament sobre un esquema conceptual concret sí pot ser decidible. AuRUS testeja els esquemes conceptuals per comprovar si compleixen una sèrie de propietats que n'asseguren la decidibilitat i així, assegurar l'acabament de tots els seus tests.
- Expressivitat: l'AuRUS no renúncia a l'expressivitat de l'UML/OCL. En concret, admet classes, associacions, associacions n-àries, classes associatives, restriccions de cardinalitat mínima/màxima, etc. Consulteu el manual d'usuari(en anglès) per més detalls.
- Completesa: Si l'anàlisi de decidibilitat conclou que l'esquema és decidible, l'AuRUS retorna per cada test, o bé la instanciació que prova el test, o bé una explicació.
- Explicacions: Si un test falla, l'AuRUS és capaç d'argumentar quines restriccions UML/OCL són les que impedeixen trobar la instanciació que prova el test. D'aquesta manera, l'AuRUS guia a l'usuari sobre com poder corregir l'esquema conceptual.
Instal·lació
Ús
Podeu trobar l'AuRUS en format d'aplicació web a la direcció http://folre.essi.upc.edu/aurus
L'AuRUS s'utilitza seguint els següents passos:
- Càrrega de l'esquema conceptual
- Selecció dels tests automàtics a provar o definició del test manual
- Execució del/s test/s
- Anàlisi dels resultats
Càrrega de l'esquema conceptual
Al iniciar l'eina, es demana que carregueu un fitxer .XMI que contingui l'esquema conceptual.
AuRUS accepta els fitxers .XMI generats per l'editor gràfic ArgoUML. ArgoUML és una eina opensource que podeu obtenir gratuïtament a la següent direcció http://argouml.tigris.org/
Al carregar-se l'esquema, l'AuRUS realitza un anàlisi de decidibilitat sobre aquest. Mitjançant aquesta anàlisi, l'AuRUS és capaç de garantir, en certs esquemes, l'acabament de tots els tests malgrat la indecidibilitat del raonament en UML/OCL en el cas general.
Selecció dels tests automàtics a provar o definició del test manual
Un cop carregat l'esquema, es mostren dues pestanyes: Is the schema right? i Is the right schema?. La primera pestanya conté una sèrie de tests predefinits de verificació (satisfactibilitat de classes, redundància de restriccions, etc) la segona, us deixa escollir entre utilitzar uns tests predefinits de validació (reflexivitat d'associacions recursives, absència de clau primària en classes, etc) o definir un test d'assoliment d'estat.
En el cas del test d'assoliment d'estat, es requereix que definiu les instàncies que configuren l'estat que voleu posar a prova.
Execució dels tests
L'acabament dels tests només està garantit si l'anàlisi de decidibilitat ha determinat que l'esquema és decidible. La font de no acabament dels tests rau en què certes propietats en un determinat esquema només es poden provar mitjançant una instanciació infinita de l'esquema, pel que l'eina es queda infinitament calculant la instanciació.
Si passada una llarga estona no se us retorna cap resultat, és possible que us trobeu en un d'aquests casos.
Anàlisi dels resultats
Un test de verificació fallit indica una contradicció i/o redundància a l'esquema conceptual. Un test de validació fallit assenyala una possible modelització incorrecte de la realitat que requereix la intervenció de l'usuari per ser contrastat.
En qualsevol cas, l'AuRUS sempre retorna o bé una instanciació que prova el test o bé una explicació de perquè no es pot trobar tal instanciació. Aquesta explicació consta de les restriccions d'integritat que impedeixen l'existència de tal instanciació.
Quant a
Documentació
Documentació bàsica
- Manual d'usuari (en anglès)
Publicacions relacionades
- 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 és un prototip de recerca desenvolupat pel grup FOLRE a la Universitat Politècnica de Catalunya-BarcelonaTech.
Per qualsevol dubte o suggeriment, poseu-vos en contacte amb nosaltres a través dels correus: grull@essi.upc.edu o xoriol@essi.upc.edu