Embora o conceito de reuso não seja novo em engenharia de software, a conscientização sobre sua importância e seu impacto no desenvolvimento de sistemas computacionais ainda não é generalizada. Uma das principais dificuldades encontradas pelas empresas de desenvolvimento é a inexistência de métodos efetivos para reuso de software. As pesquisas em engenharia de software que enfocam o reuso de software têm gerado contribuições crescentes na forma de paradigmas (como a orientação a objeto), de conceitos (como domínios e componentes) e de métodos e processos. Mais recentemente, o conceito de Padrão (Pattern) possibilitou novas formas de representações e a proposição de métodos ainda mais orientados ao reuso. Os padrões de software denominados padrões de projeto e padrões de programação (ou idiomas) têm sido bem explorados na literatura científica. Modelos de representação e exemplos são encontrados em artigos e livros especializados. O conceito de Padrão Arquitetural, entretanto, não possui a mesma maturidade. Trata-se de um conceito mais abrangente envolvendo modelos e técnicas mais extensos e complexos. Essencialmente, um Padrão Arquitetural é um modelo genérico de uma solução de software para um determinado domínio. Seu desenvolvimento permite que se possa reusar toda a arquitetura de um sistema em novos projetos semelhantes. O objetivo deste trabalho é oferecer uma contribuição para uma metodologia de identificação e descrição de Padrões Arquiteturais de Software. Para atingir este objetivo foram criadas cinco tipologias para serem empregadas como extensão da UML na descrição de casos de uso, classes, seqüências, estados e componentes. Esta descrição diferenciada visa evidenciar, nos diagramas da UML, as partes do padrão que são variantes, opcionais e múltiplas. Estas tipologias são empregadas no metamodelo desenvolvido para a descrição dos padrões arquiteturais. A utilização do metamodelo e, conseqüentemente, das tipologias é guiada pelos passos de um processo que também foi criado para servir como um roteiro para se chegar à descrição do padrão arquitetural. / Although the concept of reuse is not new in software engineering, the awareness of its importance and its impact in the development of computational systems is not generalized yet. One of the main difficulties found by development companies is the absence of effective methods for software reuse. The researches on software engineering that focuses software reuse have generated increasing contributions in the form of paradigms (such as object orientation), concepts (such as domain and component), and methods, languages and processes. More recently, the concept of Pattern allowed new representation forms and the proposal of methods even more reuse-oriented. Software patterns named as Design Patterns and Programming Patterns (or Idioms) have been well explored at scientific literature. Representation models and examples related to these patterns type are found in articles and specialized books. The concept of Architectural Pattern, however, does not have the same maturity. This is a more including concept involving more extensive and complex models and techniques. Essentially, an Architectural Pattern is a generic model of a software solution to a determined domain. Its development may allow the reuse of all the architecture of a system in new similar projects. This work aims to offer a contribution for a methodology of Software Architectural Patterns identification and description. In order to achieve this objective, five typologies have been created to be employed as UML extension in the description of use cases, classes, sequences, states and components. This differentiated description aims to evidence, in the UML diagrams, variant, optional, and multiple pattern parts. These typologies are used in the developed metamodel for the architectural patterns description. The use of the metamodel, and consequently the use of typologies, is guided by the steps of a process, which was also created to serve as a guideline to accomplish the architectural pattern description.

Embora o conceito de reuso não seja novo em engenharia de software, a conscientização sobre sua importância e seu impacto no desenvolvimento de sistemas computacionais ainda não é generalizada. Uma das principais dificuldades encontradas pelas empresas de desenvolvimento é a inexistência de métodos efetivos para reuso de software. As pesquisas em engenharia de software que enfocam o reuso de software têm gerado contribuições crescentes na forma de paradigmas (como a orientação a objeto), de conceitos (como domínios e componentes) e de métodos e processos. Mais recentemente, o conceito de Padrão (Pattern) possibilitou novas formas de representações e a proposição de métodos ainda mais orientados ao reuso. Os padrões de software denominados padrões de projeto e padrões de programação (ou idiomas) têm sido bem explorados na literatura científica. Modelos de representação e exemplos são encontrados em artigos e livros especializados. O conceito de Padrão Arquitetural, entretanto, não possui a mesma maturidade. Trata-se de um conceito mais abrangente envolvendo modelos e técnicas mais extensos e complexos. Essencialmente, um Padrão Arquitetural é um modelo genérico de uma solução de software para um determinado domínio. Seu desenvolvimento permite que se possa reusar toda a arquitetura de um sistema em novos projetos semelhantes. O objetivo deste trabalho é oferecer uma contribuição para uma metodologia de identificação e descrição de Padrões Arquiteturais de Software. Para atingir este objetivo foram criadas cinco tipologias para serem empregadas como extensão da UML na descrição de casos de uso, classes, seqüências, estados e componentes. Esta descrição diferenciada visa evidenciar, nos diagramas da UML, as partes do padrão que são variantes, opcionais e múltiplas. Estas tipologias são empregadas no metamodelo desenvolvido para a descrição dos padrões arquiteturais. A utilização do metamodelo e, conseqüentemente, das tipologias é guiada pelos passos de um processo que também foi criado para servir como um roteiro para se chegar à descrição do padrão arquitetural. / Although the concept of reuse is not new in software engineering, the awareness of its importance and its impact in the development of computational systems is not generalized yet. One of the main difficulties found by development companies is the absence of effective methods for software reuse. The researches on software engineering that focuses software reuse have generated increasing contributions in the form of paradigms (such as object orientation), concepts (such as domain and component), and methods, languages and processes. More recently, the concept of Pattern allowed new representation forms and the proposal of methods even more reuse-oriented. Software patterns named as Design Patterns and Programming Patterns (or Idioms) have been well explored at scientific literature. Representation models and examples related to these patterns type are found in articles and specialized books. The concept of Architectural Pattern, however, does not have the same maturity. This is a more including concept involving more extensive and complex models and techniques. Essentially, an Architectural Pattern is a generic model of a software solution to a determined domain. Its development may allow the reuse of all the architecture of a system in new similar projects. This work aims to offer a contribution for a methodology of Software Architectural Patterns identification and description. In order to achieve this objective, five typologies have been created to be employed as UML extension in the description of use cases, classes, sequences, states and components. This differentiated description aims to evidence, in the UML diagrams, variant, optional, and multiple pattern parts. These typologies are used in the developed metamodel for the architectural patterns description. The use of the metamodel, and consequently the use of typologies, is guided by the steps of a process, which was also created to serve as a guideline to accomplish the architectural pattern description.

Dans cette thèse, nous décrivons comment on peut utiliser un diagramme de séquence UML avec des contraintes de temps MARTE pour spécifier complètement le comportement des systèmes à base de composants tout en faisant abstraction des rôles fonctionnels des composants. Nous avons proposé une approche qui permet d'analyser ces spécifications d'une manière modulaire. Pour cela, nous avons attribué une sémantique opérationnelle aux diagrammes de séquence en les traduisant vers les TIOSTS qui sont des automates symbolique et temporisé. Nous avons utilisé des techniques d'exécution symbolique pour calculer les exécutions du système sous la forme d'un arbre symbolique. Nous avons défini des mécanismes de projection pour extraire l'arbre d'exécution associé à un composant sous-jacent. L'arbre résultant de la projection caractérise les comportements attendus du composant et peut être utilisé comme une référence pour valider le système bout par bout. Pour ce faire, nous nous sommes intéressés à des techniques de test. Nous avons présenté un résultat qui ramène la conformité du système à la conformité des composants qui le composent. Sur la base de ces résultats, nous avons proposé une méthodologie incrémentale de test basé sur des spécifications décrites sous la forme de diagrammes de séquence. / In this thesis, we describe how to use UML sequence diagrams with MARTE timing constraints to specify entirely the behavior of component-based systems while abstracting as much as possible the functional roles of components composing it. We have shown how to conduct compositional analysis of such specifications. For this, we have defined operational semantics to sequence diagrams by translating them into TIOSTS which are symbolic automata with timing constraints. We have used symbolic execution techniques to compute possible executions of the system in the form of a symbolic tree. We have defined projection mechanisms to extract the execution tree associated with any distinguished component. The resulting projected tree characterizes the possible behaviors of the component with respect to the context of the whole system specification. As such, it represents a constraint to be satisfied by the component and it can be used as a correctness reference to validate the system in a compositional manner. For that purpose, we have grounded our validation framework on testing techniques. We have presented compositional results relating the correctness of a system to the correctness of components. Based on these results, we have defined an incremental approach for testing from sequence diagrams.

Context. Automation of conversion of business rules into source code in software development project can reduce time and effort in phase of development. In this thesis we discuss automatic conversion of behavioral business rules defined in Semantics of Business Vocabulary and Rules (SBVR) standard, to fragments of Unified Modeling Language diagrams: activity, sequence and state machine. It is conversion from Computation Independent Model (CIM) into Platform Independent Model (PIM) levels defined by Model Driven Architecture (MDA). PIM in MDA can be further transformed into Platform Specific Model which is prepared for source code generation. Objectives. Aim of this thesis is to initially explore field of automatic conversion of behavioral business rules - conversion from SBVR representation to fragments of UML diagrams. It is done by fulfilment of objectives defined as following: -To find out properties of SBVR behavioral rule which ensure that the rule can be automatically converted to parts of UML behavioral diagrams (activity, sequence, state machine). -To propose mapping of SBVR contructs to constructs of UML behavioral diagrams. -To prepare guidelines which help to specify SBVR behavioral business rules in such way that they can be automatically transformed into fragments of selected UML behavioral diagrams. Methods. Expert opinion and case study were applied. Business analysts from industry and academia were asked to convert set of SBVR behavioral business rules to UML behavioral diagrams: activity, sequence and state machine. Analysis of the set of business rules and their conversions to UML diagrams was basis for fulfilment of objectives. Results. 2 syntax and 3 semantic properties were defined. Conversion rules which define mapping for SBVR behavioral business rules constructs to UML constructs were defined: 5 rules for conversion to activity diagram, 6 for conversion to sequence diagram, 5 for conversion to state machine diagram. 6 guidelines which are intended to help in specification of behavioral business rules that can be automatically transformed into UML diagrams according to the presented conversion rules, were defined. Conclusions. Research performed in this thesis is initial study of automatic conversion of behavioral business rules from SBVR notation to UML behavioral diagrams notation. Validation of defined properties, conversion rules and guidelines can be done in industry as future work. Re-execution of research for larger and more diverse set/sets of behavioral business rules taken from industry projects, sufficiently broad access to business analysts from industry and academia could help to improve results.

Objetivando implementar um sistema embarcado baseado principalmente em software, duas abordagens ortogonais estão sendo propostas: Desenvolvimento Baseado em Plataformas, que maximiza o reuso; Desenvolvimento Baseado em Modelos, que aumenta o nível de abstração utilizando conceitos de orientação a objetos e UML para modelar uma aplicação. Porém, com o aumento do nível de abstração, engenheiros de software não possuem a idéia exata do impacto de suas decisões de modelagem em questões importantes, como desempenho, e consumo de energia e de memória para uma plataforma embarcada específica. Neste trabalho, propõe-se estimar a memória de dados e de programa, o desempenho e o consumo de energia, diretamente de especificações em UML, como intuito de realizar a exploração do espaço de projeto já nos estágios iniciais do processo de desenvolvimento. Resultados experimentais apresentam erros reduzidos, quando componentes da plataforma são reutilizados e seus custos já são conhecidos para uma plataforma alvo. Aplicações reais foram modeladas de diferentes formas e demonstram a eficiência da abordagem de estimativa para o estagio inicial de exploração do espaço de projeto, permitindo ao desenvolvedor avaliar e comparar diferentes soluções de modelagem. Os valores estimados utilizados na exploração do espaço de projeto podem alcançar taxas de erros inferiores a 5%. / In order to quickly implement an embedded system that is mainly based on software, two orthogonal approaches have been proposed: Platform-based Design, which maximizes the reuse of components; and Model Driven Development, which rises the abstraction level by using object-oriented concepts and UML for modeling an application. However, with this increasing of the abstraction level, software engineers do not have an exact idea of the impact of their modeling decisions on important issues such as performance, energy, and memory footprint for a given embedded platform. This work proposes to estimate data and program memory, performance, and energy directly from UML model specifications to explore the design space in the early steps of development process. Experimental results show a very small estimation error when platform components are reused and their costs on the target platform are already known. Real-life applications are modeled in different ways and demonstrate the effectiveness of the estimates in an early design space exploration, allowing the designer to evaluate and compare different modeling solutions. The estimated values used in the design space exploration can achieve errors as low as 5%.

A abordagem de desenvolvimento dirigido por modelos (DDM) propõe que modelos (e transformações entre modelos) assumam o papel principal no desenvolvimento de sistemas. Entretanto, não há uma notação consensual para modelagem de persistência baseada em arcabouços de mapeamento objeto-relacional: enquanto a UML não possui recursos específicos para a modelagem de persistência, o modelo entidade-relacionamento não expressa os conceitos dinâmicos existentes na UML. Este trabalho propõe o perfil UML MD-JPA (Model Driven JPA) para a modelagem de persistência baseada na já difundida API de persistência Java (JPA), buscando a modelagem dos elementos persistentes e transientes de forma mais coerente e integrada. São especificadas as principais características do perfil MD-JPA, assim como a maneira pela qual modelos que adotam este perfil podem ser transformados em implementação Java, através de transformações de modelos propostas em uma abordagem DDM. Por fim, uma ferramenta de código livre foi desenvolvida para disponibilizar para comunidade os resultados deste trabalho. / The model driven development (MDD) approach proposes that models (and modelto- model transformations) play the main role on system development. However, there is not a consensual notation to model persistence based upon object relational mapping frameworks: while UML lacks specific resources for persistence modeling, the entityrelationship model does not make reference to the dynamic concepts existing in UML. This work proposes MD-JPA, a UML profile for persistence modeling based on the well-known Java Persistence API (JPA), pursuing the modeling of transient and persistent elements in a more coherent and integrated way. This work describes the main characteristics of MD-JPA as well as the way that models that adopt such profile can them be used to generate a Java implementation by the application of the proposed model transformations on a MDD approach. Finally, an open source tool was developed to make the results of this work available to the community.

Apesar das novas e efetivas técnicas de engenharia de software, os projetos de desenvolvimento de sistemas estão propensos a ter os mesmos problemas que acometem o software de apoio à gestão. Entrega com atraso, acima do orçamento e não suprindo as reais necessidades dos usuários finais ou da organização que está financiando o desenvolvimento do sistema, são os principais problemas. Esse último problema é o que mais afeta o desenvolvimento de sistemas e é um desafio para que o desenvolvimento personalizado seja uma solução real para várias empresas. Este trabalho apresenta uma proposta de método de gestão que auxilie a comunicação entre as atividades associadas à engenharia de requisitos e as atividades associadas à modelagem dos processos de negócio. Essa abordagem concerne à gestão e tratamento de requisitos de sistemas baseando-se em técnicas de engenharia de processos de negócios e de engenharia de requisitos, no processo unificado de desenvolvimento de software e na utilização de linguagens semi-formais e formais de modelagem, UML e SysML respectivamente. O método pretende mitigar os efeitos dos problemas de comunicação existentes entre os diversos integrantes de um projeto, com especial atenção para a comunicação entre a equipe de requisitos do projeto e os stakeholders responsáveis pela aceitação e aprovação do sistema. A pesquisa, com o apoio da apresentação de dois casos que ilustram o método de gestão proposto, permite concluir que é possível tornar mais efetiva e produtiva a comunicação entre os diversos envolvidos com o projeto, podendo resultar em um processo mais eficiente para a aceitação dos requisitos junto aos stakeholders. / Despite new and effective software engineering techniques, system development projects are likely to have the same problems that affect the management support software. Delivery delay, above budget and not fitting the real needs of end users or the organization that is funding the system development, are the most common problems. The latter problem is the one that most affects the systems development and is a challenge for the custom development to be a real solution to several companies. This work presents a proposal for a management method to help the communication between the activities associated with the engineering requirements and the activities associated with business processes modeling. This approach, concerns to the systems requirements treatment and management, is based on business processes engineering and requirements engineering, in software development unified process and in the use of semi-formal and formal modeling languages as UML and SysML, respectively. The method seeks to mitigate the effects of the communication problems among the project members, with special attention to the communication between the project requirements team and the stakeholders responsible for the system acceptance and adoption. The research, supported by the presentation of two cases which illustrates the proposed management method, has concluded that it is possible to make more effective and productive communication among members related with the project, which may result a more efficient process for the stakeholders requirement acceptance.

Syftet med denna rapport är att analysera DHL express behov av ärendehantering. Unified process och unified modelling language har använts för att kartlägga vilka nyckelfunktioner som skulle kunna ingå och vilka krav som DHL har på ärendehantering. Utifrån resultatet av unified process har en prototyp byggts upp för att demonstrera hur ärendehanteringen ser ut praktiskt / The purpose of this report is to analyse DHL Express need for information management in Växjö. Unified process and Unified modelling language have been used to capture the requirements and to make an analysis in order to map key functions for an information management system. From the result of the Unified process a prototype has been built to demonstrate practically the functions in an information management system.

La recherche en santé génère des publications scientifiques de plus en plus nombreuses. Or cette production scientifique n'est pas systématiquement intégrée dans la santé publique. Chercheurs et décideurs politiques ont des fonctionnements et des contraintes qui ne facilitent pas naturellement les échanges et l'application des connaissances (AC) issues de la recherche dans les politiques de santé. Cette thèse porte sur cet écart entre recherche et politiques de santé et analyse les facteurs déterminants du succès ou de l'échec du transfert des connaissances entre recherche et politiques de santé au Cambodge. Le premier chapitre définit le processus d'application des connaissances (AC) et passe en revue les rares interventions d'AC rapportées dans la littérature. Cette revue montre que l'AC n'est pas un concept nouveau, même s'il demeure peu maîtrisé et peu développé. Dans ce chapitre, nous passons également en revue les outils utilisés pour modéliser des processus et des recherches en santé. Nous concluons que l'UML (langage unifié de modélisation) apparait comme le meilleur outil de modélisation disponible pour analyser le processus d'AC. Le deuxième chapitre décrit une intervention d'AC que nous avons mise en place, puis analyse son impact et les déterminants de son succès partiel, utilisant pour cela les outils UML. La plupart des barrières étaient liées soit à une désynchronisation entre la production de connaissances, soit à la prise de décisions politiques et au manque de connaissance mutuelle entre chercheurs et décideurs. Parmi les facteurs favorisants, on a relevé le rôle déterminant d'un acteur qui était à la fois ‘décideur' et chercheur, ainsi que les bénéfices liés à l'intervention vecteurs de communication entre chercheurs et décideurs. Le troisième chapitre analyse tout d'abord quantitativement et qualitativement la production scientifique de la recherche en santé au Cambodge et montre que cette production scientifique ne couvre qu'en partie les priorités de santé publique du Cambodge même si plus de 85% des articles publiés sur la santé au Cambodge étaient accessibles gratuitement. L'étude suivante permet d'identifier les principales sources d'information des décideurs politiques ayant contribué à la préparation de la première loi nationale de lutte contre l'antibio-résistance. Nous montrons que la littérature scientifique n'est pas, au Cambodge comme ailleurs, un média approprié pour communiquer avec des autorités sanitaires. Finalement, en dernier chapitre, nous intégrons les diverses conclusions des précédents chapitres dans l'analyse des déterminants de l'AC, en tirons un modèle générique UML (diagramme de classes), que nous vérifions ensuite sur quatre projets de recherche conduits également au Cambodge dont trois ont réussi leur transfert de connaissances. Ce modèle qui pourrait être utilisable au Cambodge ou dans d'autres pays à ressources limitées. Nous concluons que si les principes de l'AC peuvent se résumer en quelques règles, ils se heurtent à de nombreuses barrières lorsqu'ils sont déclinés opérationnellement. L'AC est un processus complexe, itératif, dynamique et très contexte-dépendant. Un certain nombre de barrières à l'AC identifiées au Cambodge sont strictement identiques à celles rencontrées en Occident. Parmi les facteurs favorisants de l'AC, nous montrons que le rapprochement entre chercheurs et institutions nationales ou provinciales de santé est un atout majeur. / Health research generates a growing body of scientific literature. However this scientific production is not systematically integrated into public health. Researchers and policy makers have operations and constraints that do not naturally facilitate exchanges and knowledge translation (KT) from research into health policy. This thesis focuses on the gap between research and health policy and analyzes the determinants of success or failure of KT between research and health policies in Cambodia.The first chapter defines the KT process and reviews the scarce KT interventions reported in the literature. This review shows that KT is not a new concept, even though it remains somewhat under applied. In this chapter, we also look at the tools used to model processes and health research. We conclude that the UML (unified modeling language) appears to be the best modeling tool available to analyze the KT process.The second chapter describes a KT intervention we implemented and subsequently analyzes its impact and the determinants of its partial success, using UML tools. Most of identified barriers were related to either a lack of synchronization between the production of knowledge and the health policy making, or to some lack of mutual understanding between researchers and policymakers. Among the contributing factors, we identified the key roles of an actor who was both policymaker and researcher, and of organizations which acted as communication vectors between researchers and policymakers.The third chapter first includes the quantitative and qualitative analysis of the health research scientific production in Cambodia. It shows that even though more than 85% of articles published were accessible free of charge they do not cover all public health priorities of Cambodia. The following study identifies the main sources of information for policy makers who contributed to the preparation of the first national health policy against antibiotic resistance. We show that, as elsewhere, the scientific literature is not an appropriate medium to communicate with the Cambodian health authorities.Finally in the last chapter we integrate the various findings from previous chapters into the analysis of the determinants of KT. From this analysis we draw a generic UML model (class diagram), that we test on four research projects also conducted in Cambodia. This model may be used in Cambodia or in other countries with limited resources.We conclude that if the principles of the CA can be summarized in a few simple rules, they face many barriers when they are operationally implemented. KT is a dynamic, complex , iterative, and highly context –dependent process. A number of barriers to KT identified in Cambodia are identical to those found in the West. Among the facilitating factors for KT, we show that the connection between research institutions and national or provincial health is a major asset.

A UML é uma notação gráfica utilizada na modelagem de sistemas orientados a objetos, em diferentes domínios da computação. Por ser simples de utilizar, em relação a outras formas de modelagem, a UML é amplamente difundida entre os desenvolvedores de software, tanto na academia quanto na indústria. Entre as suas vantagens, encontram-se: (i) a representação visual das relações entre classes e entidades, pois ao se utilizar de diagramas, a UML facilita o entendimento e a visualização das relações dentro do sistema modelado; (ii) a legibilidade e usabilidade, sem que seja necessário a leitura do código do sistema, uma vez que um desenvolvedor pode compreender quais partes do código são redundantes ou reutilizadas; e (iii) uma ferramenta de planejamento, ao auxiliar na definição do que deve ser feito, antes que a implementação comece de fato, além de poder produzir código e reduzir o tempo de desenvolvimento. Todavia, a UML possui desvantagens, tais como: (i) ambiguidade entre elementos UML diferentes, devido a sobreposição dos diagramas; e (ii) falta de uma semântica clara, o qual geralmente faz com que a semântica da linguagem de programação seja adotada. Para mitigar essas desvantagens, pesquisadores buscam atribuir uma semântica formal à UML. Esse tipo de semântica é encontrado em modelos formais, onde o sistema modelado é livre de ambiguidades e possui uma semântica clara e precisa. Por sua vez, os modelos formais não são simples de serem criados e compreendidos por desenvolvedores. O grau de conhecimento em formalismo necessário para utilizar tal modelo é alto, o que faz com que seu uso seja menos difundido, comparado com a notação gráfica não formal da UML. Apesar dos esforços dos pesquisadores, as técnicas de formalização semântica da UML apresentam, no geral, um problema pouco abordado: apesar de utilizar a UML para modelar o sistema, o artefato final dessas técnicas é um trace formal. Considerando o conhecimento comum de um desenvolvedor de software, esse trace dificulta a análise dos problemas, encontrados pelos model checkers, e a correção dos mesmos no modelo UML. Com o objetivo de auxiliar o desenvolvedor na compreensão dos resultados formais (o trace citado), esta tese de doutorado apresenta uma abordagem baseada em Model-driven Architecture (MDA) capaz de representar as informações dos resultados formais dentro de um modelo UML. Por meio de transformações do modelo UML, essas representações, definidas utilizando a abordagem, auxiliam o desenvolvedor a visualizar o fluxo de execução do model checker dentro do modelo UML. Assim, acredita-se que as vantagens obtidas pela formalização semântica da UML podem ser mais difundidas e utilizadas pelos desenvolvedores, principalmente na indústria. / UML is a graphical notation used for modeling object-oriented software systems in different domains in computer science. Being simple to use, compared to other modeling techniques, UML is widespread among software developers, both in academia and industry. Among its advantages are: (i) the visual representation of the relationships between classes and entities, as when using diagrams, UML facilitates understanding and visualization of relationships within the modeled system; (ii) readability and usability without having to read the system code, since a developer can understand which parts of the code are redundant or reusable; and (iii) a planning tool, helping to define what needs to be done before the implementation actually begins, as well as being able to produce code and reduce development time. However, the UML also has disadvantages, such as: (i) ambiguity between different UML elements due to overlapping diagrams; and (ii) lack of clear semantics, which generally causes the semantics of the programming language to be adopted. To mitigate these disadvantages, researchers seek to assign a formal semantics to the UML. This type of semantics is found in formal models, where the modeled system is free of ambiguity and has a clear and precise semantics. On the other hand, formal models are not simple to create and understand by developers. The degree of formalism knowledge required to use such a model is high, which makes their use less widespread, compared to UML non-formal graphical notation. Despite the researchers efforts, in general the techniques that formalize the UML semantics has a problem that is forgotten: although using the UML to model the system, the final artifact of these techniques is a formal trace. Considering the common knowledge of a software developer, this trace makes it difficult to analyze the problems encountered by model checkers and to correct them in the UML model. In order to assist the developer in understanding the formal results (the trace above), this thesis presents an approach based on Model-driven Architecture (MDA) capable of representing the information of the formal results in the UML model. Through UML model transformations, these representations, set using the approach, help the developer to visualize the execution flow of the model checker within the UML model. Thus, we believe that the advantages obtained by formalizing the UML semantics may be more widespread and used by developers, especially in industry.