Automated reasoning on UML conceptual schemas with derived information and queries

Context: It is critical to ensure the quality of a software system in the initial stages of development, and several approaches have been proposed to ensure that a conceptual schema correctly describes the user's requirements. Objective: The main goal of this paper is to perform automated reasoning on UML schemas containing arbitrary constraints, derived roles, derived attributes and queries, all of which must be specified by OCL expressions. Method: The UML/OCL schema is encoded in a first order logic formalisation, and an existing reasoning procedure is used to check whether the schema satisfies a set of desirable properties. Due to the undecidability of reasoning in highly expressive schemas, such as those considered here, we also provide a set of conditions that, if satisfied by the schema, ensure that all properties can be checked in a finite period of time. Results: This paper extends our previous work on reasoning on UML conceptual schemas with OCL constraints by considering derived attributes and roles that can participate in the definition of other constraints, queries and derivation rules. Queries formalised in OCL can also be validated to check their satisfiability and to detect possible equivalences between them. We also provide a set of conditions that ensure finite reasoning when they are satisfied by the schema under consideration. Conclusion: This approach improves upon previous work by allowing automated reasoning for more expressive UML/OCL conceptual schemas than those considered so far. (c) 2013 Elsevier B.V. All rights reserved.