User manual
Contents
1. 2009 2010 Universitat Politecnica de Catalunya AuRUS USER MANUAL A glance beneath the reasoning assistant Barcelona School of Informatics Revision History Revision Description 12 02 2011 User Manual Writing 05 03 2011 07 03 2011 03 05 2011 General Formatting Table of Contents NUOdUCUON asalta sides ida ek eb ejna 4 PU DO a a EE 4 Related DOCUMENT on eg 4 Solkana E E E AE E eee ecco tees coc ae eee 4 Problem Reporting Instructions cccccscccssccsscccsecceceescececcenceaeeesueeeseeeecseeeeeeceseeeeeeeaeeegeeees 4 PPP PPP A 5 Bale jo a IPPO UU e q E T 5 Se e Un EE e E o o 5 ET SSS IV IS SS i i A E a 5 JR OO PR AP A S A E E 6 AuRUS requirements over ArgoUML design ooocccccncncncncnnoncnnnoconconononnnnononononcncnnononcnonronnnononoos 6 CUS TON made types for attributes a a bia as 7 Recursive association Special 7 OGL COrnstramtdae Ae o bt At 8 Generalization TeSt ICONS sti 8 BE UMS E EE a 9 INP E eeesaasb 13 KURUS VEririca tion eS Sian 13 AURUS validation TOS US sieni bra a EET A acer 14 era e Valida Oea EE E E EEA EEA E 16 Constants variables and not defined ooooonnnnncnnnnnnnnnnnnnnnnnnnnnnononnncccnccononononnnnnnnns 18 Negative instances and Variable Equality ooccccccccnccncnonoonoonnonnonncnnnnnnnnnos 19 Introduction AuRUS is an Automatic reasoning tool for UML OCL schemas It can verify the conceptual diagram that is ensuring the absence of redund2. Retroceder Siguiente Terminar Ayuda 10 56M USed Gf 107m total It is important to remember to apply the workarounds shown in previous sections including Doubling the classes when designing associations that are not allowed o WorksFor Employee L subordinate Department name String minsalary Integer maxsalary Integer 0 1 o 1 superior Worksin managedDep e e e ss ee ee el recruited oO HasRecruited workingTeam inspected as gos WorkingTeam Applying comments for generalizations and creating custom data types lt lt datatype gt gt Integer lt lt datatype gt gt String WorksFor Employee L incomplete subordinate O 1 superior Employee Te 4 worker name String 1 salary Integer phone String 11 After designing the core conceptual schema the OCL constraints must be edited in a note WorksFor o 1 superior Employee orker name String 1 salary Integer phone String context Department inv UniqueDep Department allinstances gt select d d2 d lt gt d2 and d2 name d name gt asset gt size 0 context Employee inv UniqueEmp Employee allinstances gt select e e2 e lt gt e2 and e2 name e name gt asset gt size J 0 context WorkingTeam inv UniqueTeam WorkingTeam alllnstances gt selectit t2 t lt gt t2 and t2 name 1 name
3. gt asset gt size 0 context Department inv MinimumSalary self minsalary gt 1000 context Department inv CorrectSalaries self minsalary lt self maxSalarv context Department inv ManagerHasNoSuperior self manager superior gt asset gt size 0 context Boss inv BossisManager self managedDep gt size gt 0 context Boss inv BossHasNoSuperior self superior gt size J 0 Audits context Boss invSuperiorOfAlWorkers self managedDep worker gt select e self subordinate gt select e2 e2 e gt size 0 gt asset gt size 0 context WorkingTeam inv InspectorNotMember self member employee gt select e self inspector gt select inslins e gt size 1 gt 0 gt ass5et gt size 0 context Member inv NotSelfRecruited self recruited lt gt self context WorkingTeam inv OneRecruited self member gt select m m recruiter workingTeam gt select w w self gt asset gt size J gt 0 gt size J gt 0 context Department inv ManagerlsWorker self worker gt select e self manager gt select m m e gt size J gt 0 gt size J gt irkingTeam gix Oo WorkingT eam Finally it should be exported as an xmi extension file et ArgoUML Editar Visualizar Crear Organizar Gi POB F Nuevo BN oo IB amp a E Nuevo Perfil ES IF l E l Orientadaap Abrir proyecto 60 a FT gt Guardar el proyecto es Po gt E Profile Configu Guardar el proyecto como gt EX untitledModel Restituir el arch
4. gt 0 gt size gt 0 context Department invManagerlsWorker self worker gt select e self manager gt select m m e gt size gt 0 gt size gt 0 The first action that should be done should be designing the basis of the including all the role names and cardinalities RBRaEABRS ET Orientada a paquetes Bl gt gt EJ Profile Configuration v E untitledModel Diagrama de clase Diagrama de caso de uso E Member Ey context Department inv UniqueDe e Integer String Sin nombre Generalization Audits HasRecruited Manages WorksFor Worksin gt Boss gt Department gt E Employee Employee Member gt E WorkingTeam a gt E 4 schema im B E Department name String minsalary Integer 1 Worksin managedDep recruited 0 HasRecruited AA workingDep worker maxSalary Integer 0 1 Manages li WorksFor 0 1 superior Employee name String salary Integer inspector phone String 1 Audits workingTeam 00 OF WorkingTeam B de Ya Por prioridad 4 16 elementos a Propiedades Documentaci n EA Alta b EJ Media Ef Baja Ninguna tarea pendiente ha sido seleccionada TIY bAs Disoram Presentaci n C digo fuente Restricciones Estereotipos Valores etiquetados Lista de control
5. instance which is consistent Again if there is no such substitution AuRUS will answer the restrictions involved in that fact Notice that you can use the same variable in other instances even in instances of other types For example you can test if there can be two employees with the same salary a which is the maxSalarv of a defined Department Nevertheless if you do not care of the value of a column you can leave the definition in blank if it does not represent an OID value this definitions would be displayed as null in the main panel 18 Negative instances and Variable Equality AuRUS permits you to define some not desirable instances checking the column called Nevative In this case the reasoner will never use them to make consistent the defined schema instance However it is not allowed to add a negative instance which uses variables that do not appear in positive instances With negative instances you can test some scheme instances like Worksin Emp Dep Department Dep DepName 500 max Not Employee Emp null 100 This test can be used to proof that it is not possible to have an employee in a department with a salary lower than the departments specification However this example is not exactly true since it can only test that property for the specific values 500 and 100 The correct test would be Worksin Emp Dep Department Dep DepName min max Not Employee Emp null sal Sal
6. instances as specified by the maximum cardinality maxassociated to the same instances as the other association ends Minimum cardinality test When there is a cardinality constraint with a lower bound 0 this check shows whether it is possible that an instance s at the other end s does not participate in the association Incomplete hierarchy test If some hierarchy is specified as incomplete it can be proven if it is really such that is if an instance may only belong to the superclass Otherwise it should be specified as complete or some other constraint should be removed or modified Overlapping hierarchy If some hierarchy is specified as overlapping it can be checked if it is really such that is if an instance may belong to more than one subclass simultaneously Otherwise it should be specified as disjoint or some other constraint should be removed or modified 13 To perform verification tests check the desired properties under the s the schema right tab and press the Check button AuRUS Sele O Schema Is the schema right Is it the right schema H Classes H Association classes H Associations H OCL constraints Are all constraints non redundant not Defined Are all classes and associations lively not Defined Are minimum cardinalities correct not Defined not Defined Are incomplete hierarchies correct not Defined Are overlapping hierarchies correct not Defined Liveliness Non redunda
7. name String working dep minSalary Real p 4 Manages maxsalarv Real managed dep manager inspector Audits HasRecruited inspected The OCL restrictions associated are the following context Department invUniqueDep Department alllnstances gt select d d2 d lt gt d2 and d2 name d name gt asSet gt size 0 context Employee invUniqueEmp Employee allinstances gt select e e2 e lt gt e2 and e2 name e name gt asSet gt size 0 contextWorking TeaminvUniqueTeam WorkingTeam allinstances gt select t t2 t lt gt t2 and t2 name t name gt asSet gt size 0 context Department invMinimumSalary self minSalary gt 1000 context Department invCorrectSalaries self minSalary lt self maxSalary context Department invManagerHasNoSuperior self manager superior gt asSet gt size 0 context Boss invBossisManager self managedDep gt size gt 0 context Boss invBossHasNoSuperior self superior gt size 0 context Boss invSuperiorOfAllWorkers self managedDep worker gt select e self subordinate gt select e2 e2 e gt size 0 gt asSet gt size 0 contextWorkingTeaminvinspectorNotMember self member employee gt select e self inspector gt select ins ins e gt size gt 0 gt asSet gt size 0 context Member invNotSelfRecruited self recruited lt gt self contextWorkingTeaminvOneRecruited self member gt select m m recruiter workingleam gt select w w self gt asSet gt size
8. this test we have to select the Interactive Validation tab and look through the Class Instantiation the Employee class After that we can push the Edit button and define the desired attributes as commented E Schema Is the schema right2 Is it the right schema Employee instantiation Classes E Association classes Et Ly Associations OCL constraints Chat A OID Negative Employee Y Predefined validation Interactive validation Instantiated elements tt Association Class Instantiation Member Association Instantiation Audits Variable equalitv Instantiation Instantiation addition 16 In this panel you can add or delete as rows as you want All the modifications will be saved in the schema instance after closing it which is displayed in the main panel Ei AuRUS L Schema H Ji Classes 4H Association classes H Ly Associations OCL constraints Variable equality Instantiation Employee 1 John 1000 17 Constants variables and not defined You can define the instances using constants variables and or omitting some columns Every String will be considered as a variable while real numbers will be interpreted as constants So in the last example the name John will be interpreted as a variable Variable values will be substituted by the reasoner for constants to find a schema
9. ancies or contradictions by performing some automatic tests like class liveliness tests or OCL Constraints redundancy tests It also helps to validate the schema that is ensuring that its representation corresponds to the real world by performing some automatic tests that must be interpreted by the specifier like class identifiers detection inclusion exclusion paths tests etc Furthermore this tool allows you to define and execute your own state reachability tests Purpose This document has been written to help to get introduced in using this tool Concretely this User Manual explains how to load a conceptual schema to the tool how to make tests and get the results Related Documents This document explains everything you need about using AURUS However if you want to Know how it works you can consult the following paper AuRUS Automated Reasoning on UML OCL Schemas Anna Queralt GuillemRull Ernest Teniente CarlesFarr Toni Urpi Conventions Throughout this document we will use some concrete vocabulary which will be written in italic We will define each concrete word only the first time it appears but you will be able to find its definition in the Glossary of the end of this manual Problem Reporting Instructions If you find any error in AuRUS you can report it to the following mail address teniente lt at gt essi upc edu Overview Decidability It is well known that reasoning on conceptual schemas is not decidab
10. ing the same class are not allowed in ArgoUML However this restriction is worked around bonding two classes with the same name Class atributes or other associations should not be duplicated as they must be only specified once The following figure shows a well constructed recursive association This ArgoUML design issue also comes up when trying to link other type of classes such as associative classes or generalizations In any case it shall be solved by the same procedure OCL constraint definition OCL constraints should be specified in a single note as it is shown in the following figure String Integer lt lt datatype gt gt Integer context Department inv UniqueDep Department alllnstances gt select d d2 d lt gt d2 and d2 name d name gt size j 0 context Employee inv UniqueEmp Employee alllnstances gt select e e2 e lt gt e2 and e2 name e name gt size 0 context WorkingTeam inv UniqueTeam WorkingTeam alllnstances gt select t t2 t lt gt t2 and t2 name 1 name gt size 0 context Department inv MinimumSalary self minsalary gt 1000 context Department inv CorrectSalaries self minSalary lt self maxSalary context Department inv ManagerHasNoSuperior self manager superior gt size 0 context Boss inv BossisManager self managedDep gt size j gt 0 inspected context Boss inv BossHasNoSuperior self superior gt size J 0 context Boss inv SuperiorOfAllWorkers self managedDep worker gt
11. ivo Importar XMI Exportar proyecto como archivo XMI 5 Importar desde c digo amp Configurar Pagina amp Imprimir P Guardar los gr ficos Guardar todos los gr ficos Notaci n pe Ey Propiedades thesisxmifinit zargo thesisxmifinitARGOasSet xmi thesisxmifinit zargo r 12 AuRUS Schema Testing AuRUS verification tests The AuRUS verification tool includes tests devoted to check the internal correctness of a schema This assessments can be performed automatically without the designer intervention aiming to answer to the question is the structural schema right Some of them correspond to well known reasoning tasks such as schema satisfiability while others correspond to additional properties that can be automatically drawn from the definition of each conceptual schema For all of them the fact that the test is not satisfiable necessarily indicates that the schema has some kind of flaw The automatic verification tests offered are Satisfiability of a Schema A schema is satisfiable if there is a non empty state of the IB in which all its integrity constraints are satisfied Redundancy of an Integrity Constraint An integrity constraint is redundant if integrity does not depend on it This situation takes place if the states of the IB that are not allowed are already prevented by the rest of constraints Maximum cardinality test This assessment shows whether it is possible to have as many
12. le that is some tests may not end for some specific diagrams However AURUS can check some properties on the schema which ensures the termination of any test This checking is known as the decidability test Notice that if this checking fails it is not possible to predict if there is or not any test that would never end Completeness AURUS was thought to ensure the completeness of any test That is giving an instance which satisfies the test goal or answering that it is not possible to find one in case it does not exists Nevertheless it may happen that the unique instances which satisfy the goal are not finite Then AuRUS will never finish the instance computation which is the cause of the never ending tests Notice that this situation will never occur if the schema is correct or the decidability test has been passed Expressiveness AuRUS deals with the most common graphic UML elements Classes n arv Associations Association Classes Hierarchies and Association Cardinalities However at the moment it is not possible to define Attribute cardinalities and all the types are interpreted as Real numbers One important point about AuRUS is the expressiveness of the allowed OCL Constraints In the current version the following type of OCL Constraints are admitted notice that aggregation functions like sum are not admitted Admitted Boolean Operators And or not includes excludes includesAll excludesAll isEmptv n
13. lt min Where sal lt min can be defined in using the variable equality instantiation option which allows you to define lt gt lt gt lt gt between variables and constants Variable Equality Instantiation Instantiated elements Variable 1 sal Instantiation addition Insert the preferred variables or select one from previous custom instantiations lt v 19
14. ncy Min card Max card Incomplete Overlapping AuRUS validation tests The AuRUS validation tool also offers a set of tests to check if the schema correctly specifies the requirements set by the designer which are not usually formalized That is why it is desirable to help the designer to analyze the schema so that he can decide whether it represents the intended domain Some standard automatic tests are offered in order to check potentially undesirable common situations Irreflexive constraint test If a recursive association can relate the same instance then an irreflexible constraint may be missing This test can be defined for each recursive association in the schema identifier constraint test If a class admits several valid instances with the same value in all its attributes then an identifier constraint may be needed to state the set of attributes that uniquely identify each instance This test can be generated 14 for each class of the schema as long as it is not an association class or a subclass since in these cases their identifiers are already known Path inclusion test If c is an instance of C the set of instances of D related to c bv means of R is a subset of the set of instances of D related to c bv means of S or the other wav around This test helps determine if there are some associations that are subset of another Path exclusion test If c is an instance of C the set of instance
15. otEmpty exists forall isUnique oclisTvpeOf lt gt lt gt lt gt Admitted Loop Expressions Select alllnstances Admitted Collection Operators size asSet Other admitted expressions oclAsType There are only two restrictions that might be considered when writing the OCL constraints it is not possible to compare the size of a collection with a variable only constants and it is not possible to work with bags only sets which means that the asSet operation should be used if the navigation path has more than one navigation Input Creation The source input normally used in AuRUS is a plain ArgoUML xmi export file The current version of ArgoUML 0 32 is based directly on the UML 1 4 specification Furthermore it provides an extensive support for OCL Object Constraint Language and XMI XML Model Interchange format ArgoUML has many features that make it special but it does not implement all the features that CASE tools provide ArgoUML is available for free and can be used in commercial settings For terms of use see the license agreement presented when ArgoUML is downloaded AuRUS requirements over ArgoUML design In the current version there are several limitations that prevent ArgoUML from creating certain types of expressions accepted by AuRUS Several workarounds have been made in order to solve this issue Generally speaking AuRUS will accept any correct and legal input genera
16. s of D related to c bv means of R excludes the set of instances of D related to c bv means of S This test helps determine if there are some associations that implv a mutual exclusion between them To perform verification tests check the desired properties under the s it the right schema tab and press the Check button AuRUS D Schema Is the schema right Is it the right schema Classes 9 Association classes 5 Associations H OCL constraints Predefined validation Interactive validation Is some identifier missing not Defined C Is some irreflexive constraint missing not Defined not Defined L 1Is some path exclusion missing not Defined l Check Identifiers Irreflexivity Path inclusion Path exclusion 15 Interactive Validation In order to completely validate your schema it is necessary to make some custom test to check if the schema represents exactly your domain This checking is made by some scheme reachability tests That is the user defines a concrete instance for the schema and the reasoner tries making that instance consistent by adding new instances to the original ones If it is not possible to make it consistent AuRUS will answer the restrictions that cause this situation However this response is not ensured in case that the decidability test would have failed For example we can check if there can be an employee called John whose salary is 1000 To perform
17. select e self subordinate gt select e2 e2 e gt size j 0 gt size 0 context WorkingT eam inv InspectorNotMember self member employee gt select e self inspector gt select inslins e gt size gt 0 gt size 0 context Member inv NotSelfRecruited self recruited lt gt self context WorkingTeam inv OneRecruited self member gt select m m recruiter workingTeam gt select w w self gt size gt 0 gt size gt e String i 7 context Department inv ManagerlsWorker self worker gt select e self manager gt select m m e gt size gt 0 gt size J gt 0 Please note that it is important not to leave a new end of line after the last constraint as the AuRUS OCL parser will interpret it as a new blank invalid restriction Generalization restrictions Generalization restrictions should be specified using a linking note and one of the following legal combinations incomplete overlapping incomplete disjoint complete overlapping complete disjoint However it is also allowed to specify only one of the requirements either incomplete complete disjoint or overlapping phone String Employee O m name String salary Integer Designing an example With all the previous limitations in mind this section will illustrate how to design a sample valid input for AuRUS The next conceptual schema will be used as an example WWorksFor Department 1 Worksin
18. ted by ArgoUML However there are some requisites to take into account All attribute types must be custom data types All association roles must be defined in a non ambiguous way Recursive associations and similar bondings are allowed but must be specified specially OCL constraints must be specified in a note format Generalization restrictions are specified linking a note Please refer tohttp areouml tigris org for further information about ArgoUML Custom made types for attributes Attribute types are defined using data types In order to ensure compatibility with the AuRUS reasoning engine all attribute types included in the conceptual schema must be custom made Firstly a new data type must be defined Finally the custom type is assigned to the selected attribute Zz 4 s ToDo item Properties 4 Documentation Presentation Source Constraints Stereotype 4 Tagged Val E Attribute 4 gt e Visibility Name INT public package protected private Type o Integer UML 1 4 Standard Elements modifiers Multiplicity NONE gt i 7 l ownerScope FAO BI Boolean UML 1 4 Standard Elements Pech bility ogee Bycicle untitledModel Ur angeabilitv Integer untitledModel o String UML 1 4 Standard Elements rt The same data type may be used as many times as needed Recursive association specification Associations with association ends bond
Download Pdf Manuals
Related Search