Desenvolvimento Rigoroso com UML-RT
Universidade Federal de Pernambuco, (April 2005)Abstract
As other object-oriented visual methods, UML has tremendously influenced the software engineering modeling practice with rich structuring mechanisms. Despite its strengths, the rigorous development of non-trivial applications (those applications that, due their complexity, need to emphasise the specification and verification of their components) do not seem feasible without a formal semantics. The reason is that well-known model transformations might not preserve behaviour. This problem is even more serious in a model driven development, where transformations are as important as models, and involve different model views. Similar limitations can be found during the development with UML-RT. This language is a conservative UML profile that includes active objects (objects with an execution flow independent of the rest of the system) to describe concurrent and distributed applications. In this kind of development, transformations have to simultaneously handle both static and dynamic model views, represented by the diagrams and properties of the model. For these reasons, this work proposes a semantics for UML-RT via mapping into OhCircus, a formal object oriented language that combines CSP, Z and specification statements, and also support Morgan^a€™s refinement calculus. From this semantics and the laws of OhCircus, we are able to propose and prove model transformation laws that preserve the system behaviour. Two groups of laws are proposed: the first one embodies a comprehensive set of laws that govern small changes in the main model views, like introducing or removing a modelo element; the second group presents more elaborated laws derived from the composition of these basic laws, like decomposing a capsule into parallel component capsules. The derived laws can be taken as precise model refactorings that are easily applied in a rigourous development, without the developer directly dealing with the formalism that supports them. Finally, the comprehensiveness of the set of laws is particularly discussed through the main steps of a reduction strategy of UML-RT models into a UML model extended with a single capsule responsible for all the interactions with the environment; This capsule is also responsible for maintaining the active behaviour of the modeled system. This extended UML model can be regarded as a normal form, and, therefore, our strategy can be regarded as a contribution to a completeness strategy captured by normal form reduction.