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 to 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 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 supports Morgan’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 model element; the second group presents more elaborate 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.

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 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.

Finally, we present the development of case study in order to illustrate the overall approach. From the analysis model of a simplified manufacturing system, we systematically built a more detailed design model; each step is justified by the application of algebraic transformation laws.

Main Contributions

• Assignment of a formal semantics for UML-RT via mapping into OhCircus, which acts as a useful hidden formalism for software engineering practise.

• Proposition and proof of a comprehensive set of basic algebraic laws for UML-RT that preserve the system behaviour on both static and dynamic views.

• Presentation of larger grain laws, derived from basic laws, that might be considered as precise model refactorings and easily applied in a rigorous development.

• A notion of relative completeness, briefly presented through a strategy for reducing an arbitrary UML-RT model to a UML model, entirely based on the laws.

• Seamless application of the laws through design activities of the Rational Unified Process in the development of a case study.

Papers derived from the Master Thesis

• Rodrigo Ramos, Augusto Sampaio and Aleandre Mota. Rigorous Development with UML-RT.  19th Brazilian Contest on Dissertations and Thesis (CTD'06), SBC, 2006. (pdf) [classified among the 10 Best Computer Science Master's Thesis Nationwide in 2005 in this contest of the Brazilian Computing Society (SBC)]

• An RUP extension for rigorous modeling of concurrent systems(with R. Godoi and A. Sampaio). 19th Brazilian Symposium on Software Engineering (SBES'06), Florianópolis, Brazil (2006)(pdf) (bib) [In portuguese (English Abstract)] [To Appear]

• Transformation Laws for UML-RT, (with A. Sampaio and A. Mota) Proc. the 8th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS’06), Vol. 4037 of Lecture Notes in Computer Science (LNCS), Springer (2006) 123-138.  (pdf)

• A Semantics for UML-RT Active Classes via Mapping into Circus, (with A. Sampaio and A. Mota) Proc. 7th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS’05), Vol. 3535 of Lecture Notes in Computer Science (LNCS), Springer (2005) 99-114.  (pdf)

• Class and Capsule Refinement in UML for Real Time, (with A. Sampaio and A. Mota) Volume 95 of Electronic Notes in Theoretical Computer Science (ENTCS), Elsevier Science (2004) 23–51 [Extended Version] (pdf) (bibtex)

• Class and Capsule Refinement in UML for Real Time, (with A. Sampaio and A. Mota) Proc. 4th Brazilian Workshop on Formal Methods, Campina Grande, Brazil (2003) 16-34  (pdf) (bibtex)