<p>Za potrebe evaluacije kvaliteta vizuelizacije u svrhu prakse inkluzivnog dizajna razvijen je namenski jezik koji hendikepe vida opisuje kroz formalizam baziran na vizuelnim promenljivama. Namenski jezik se može koristiti kao dokumentacija, ili kao specifikacija hendikepa za posebno napisan simulator vizuelnih hendikepa koji se može koristiti za potrebe testiranja. Kao pandan ovoj tehnologiji razvijen je novi mehanizam za evaluaciju vizuelizacija koji kroz inovacije u metodologiji i statistici omogućava da se merodavni zaključci izvedu iz relativno malih uzoraka podataka.</p> / <p>For purposes of visualization quality evaluation as part of the practice of<br />inclusive design, a domain specific language was developed such that it<br />describes visual handicaps through a formalism based on visual variables.<br />This domain specific language can be used as documentation or as a handicap<br />specification for a specially constructed visual handicap simulator usable for<br />testing. Alongside this technology, a novel mechanism for visualization<br />evalution was developed. This mechanism allows, through innovations in<br />metholodoly and statistics, the production of trustworthy results from relatively<br />small data sets.</p>

This dissertation develops a new model transformation approach that supports engineering model integration, which is essential to support contemporary interdisciplinary system design processes. We extend traditional model transformation, which has been primarily used for software engineering, to enable model-based systems engineering (MBSE) so that the model transformation can handle more general engineering models. We identify two issues that arise when applying the traditional model transformation to general engineering modeling domains. The first is instance data integration: the traditional model transformation theory does not deal with instance data, which is essential for executing engineering models in engineering tools. The second is syntactical inconsistency: various engineering tools represent engineering models in a proprietary syntax. However, the traditional model transformation cannot handle this syntactic diversity. In order to address these two issues, we propose a new multi-layer syntactical model transformation approach. For the instance integration issue, this approach generates model transformation rules for instance data from the result of a model transformation that is developed for user model integration, which is the normal purpose of traditional model transformation. For the syntactical inconsistency issue, we introduce the concept of the complete meta-model for defining how to represent a model syntactically as well as semantically. Our approach addresses the syntactical inconsistency issue by generating necessary complete meta-models using a special type of model transformation.

Design synthesis is a fundamental engineering task that involves the creation of structure from a desired functional specification; it involves both creating a system topology as well as sizing the system's components. Although the use of computer tools is common throughout the design process, design synthesis is often a task left to the designer. At the synthesis stage of the design process, designers have an extensive choice of design alternatives that need to be considered and evaluated. Designers can benefit from computational synthesis methods in the creative phase of the design process. Recent increases in computational power allow automated synthesis methods for rapidly generating a large number of design solutions. Combining an automated synthesis method with an evaluation framework allows for a more thorough exploration of the design space as well as for a reduction of the time and cost needed to design a system. To facilitate computational synthesis, knowledge about feasible system configurations must be captured. Since it is difficult to capture such synthesis knowledge about any possible system, a design domain must be chosen. In this thesis, the design domain is hydraulic systems. In this thesis, Model-Driven Software Development concepts are leveraged to create a framework to automate the synthesis of hydraulic systems will be presented and demonstrated. This includes the presentation of a domain specific language to describe the function and structure of hydraulic systems as well as a framework for synthesizing hydraulic systems using graph grammars to generate system topologies. Also, a method using graph grammars for generating analysis models from the described structural system representations is presented. This approach fits in the context of Model-Based Systems Engineering where a variety of formal models are used to represent knowledge about a system. It uses the Systems Modeling Language developed by The Object Management Group (OMG SysML™) as a unifying language for model definition.

Made available in DSpace on 2014-12-17T15:48:04Z (GMT). No. of bitstreams: 1 GeorgeHCD_DISSERT.pdf: 1498112 bytes, checksum: 47b708a57a0944475a3489af84029df2 (MD5) Previous issue date: 2012-08-06 / The academic community and software industry have shown, in recent years, substantial interest in approaches and technologies related to the area of model-driven development (MDD). At the same time, continues the relentless pursuit of industry for technologies to raise productivity and quality in the development of software products. This work aims to explore those two statements, through an experiment carried by using MDD technology and evaluation of its use on solving an actual problem under the security context of enterprise systems. By building and using a tool, a visual DSL denominated CALV3, inspired by the software factory approach: a synergy between software product line, domainspecific languages and MDD, we evaluate the gains in abstraction and productivity through a systematic case study conducted in a development team. The results and lessons learned from the evaluation of this tool within industry are the main contributions of this work / A comunidade acad?mica e a ind?stria de software t?m demonstrado, nos ?ltimos anos, bastante interesse em abordagens e tecnologias ligadas ? ?rea de desenvolvimento dirigido por modelos (MDD). Em paralelo a isto, continua a busca incessante da ind?stria por tecnologias que aumentem a produtividade e qualidade no desenvolvimento de produtos de software. Esta pesquisa visa explorar estas duas afirma??es, atrav?s de um trabalho que usa uma tecnologia MDD e avalia seu uso na resolu??o de um problema real no contexto de seguran?a de sistemas corporativos. Com a constru??o e uso de uma ferramenta, uma DSL visual denominada CALV3, inspirada na abordagem de F?bricas de Software: uma sinergia entre linha de produto de software, linguagens espec?ficas de dom?nio e MDD, avaliamos os ganhos em abstra??o e produtividade, atrav?s de um estudo de caso sistem?tico conduzido em uma equipe de desenvolvimento. Os resultados e li??es aprendidas com a avalia??o desta ferramenta no ?mbito industrial s?o uma das principais contribui??es deste trabalho

In Artificial Intelligence, especially in area of constraint programming, it's popular to design various modeling languages which allow solving problems on domain level and by using domain specific abstractions. Techniques known from research on Domain-Specific Languages are often useful in this effort. Functional programming languages offer new tools for designing such languages, particularly Domain-Specific Embedded Languages. This work investigates the advantages and disadvantages of using functional programming for designing and implementing a Domain-Specific Embedded Language for state space search problems.

Image processing pipelines are ubiquitous. Every image captured by a camera and every image uploaded on social networks like Google+or Facebook is processed by a pipeline. Applications in a wide range of domains like computational photography, computer vision and medical imaging use image processing pipelines. Many of these applications demand high-performance which requires effective utilization of modern architectures. Given the proliferation of camera enabled devices and social networks optimizing these emerging workloads has become important both at the data center and the embedded device scales. An image processing pipeline can be viewed as a graph of interconnected stages which process images successively. Each stage typically performs one of point-wise, stencil, sam-pling, reduction or data-dependent operations on image pixels. Individual stages in a pipeline typically exhibit abundant data parallelism that can be exploited with relative ease. However, the stages also require high memory bandwidth preventing effective uti-lization of parallelism available on modern architectures. The traditional options are using optimized libraries like OpenCV or to optimize manually. While using libraries precludes optimization across library routines, manual optimization accounting for both parallelism and locality is very tedious. Inthisthesis,wepresentthedesignandimplementationofPolyMage,adomain-specific language and compiler for image processing pipelines. The focus of the system is on au-tomatically generating high-performance implementations of image processing pipelines expressed in a high-level declarative language. We achieve such automation with: • tiling techniques to improve parallelism and locality by introducing redundant computation, v a model-driven fusion heuristic which enables a trade-off between locality and re-dundant computations, and anautotuner whichleveragesthefusionheuristictoexploreasmallsubsetofpipeline implementations and find the best performing one. Our optimization approach primarily relies on the transformation and code generation ca-pabilities of the polyhedral compiler framework. To the best of our knowledge, this is the first model-driven compiler for image processing pipelines that performs complex fusion, tiling, and storage optimization fully automatically. We evaluate our framework on a modern multicore system using a set of seven benchmarks which vary widely in structure and complexity. Experimental results show that the performance of pipeline implementations generated by our approach is: • up to 1.81× better than pipeline implementations manually tuned using Halide, a state-of-the-art language and compiler for image processing pipelines, • on average 5.39× better than pipeline implementations automatically tuned using Halide and OpenTuner, and • on average 3.3× better than naive pipeline implementations which only exploit par-allelism without optimizing for locality. We also demonstrate that the performance of PolyMage generated code is better or compa-rable to implementations using OpenCV, a state-of-the-art image processing and computer vision library.

Made available in DSpace on 2016-06-02T19:06:01Z (GMT). No. of bitstreams: 1 4765.pdf: 5526051 bytes, checksum: eca7635e3ad1f0a28a9f3871c97aac57 (MD5) Previous issue date: 2012-11-12 / Universidade Federal de Sao Carlos / Autonomous mobile robots are machines capable of executing repetitive/dangerous tasks more efficiently. Most of them have an embedded software which is responsible for their execution. Over the last years, the complexity of these applications has continuously growing and they are presenting challenges that are uncommon to traditional information systems development. Therefore, any technique that can support their development is a great contribution. A technique that improves the productivity is to use domain-specific languages (DSLs). These are modeling and programming languages whose constructs are concepts and abstractions of a particular domain. It frees developers from worrying about generic programming concepts (classes, objects, attributes, etc.) and allows them to focus on the problem to be solved. As creating a DSL is not a trivial task and pointing the idiosyncrasies of mobile robots, this dissertation presents an approach for engineering DSLs to mobile robots. The aim is to make the activity of creating DSLs to this domain more systematic and controlled. In this approach, an application is taken as input and a series of domain statements is extracted from it. These statements are classified into categories and each one of them are analized in order to extract commonalities and variabilities, wich are transformed into components of a DSL. An important characteristic of the approach is that it asks for just one application to reach a first version of a running DSL. We suggest that the same DSL can be evolved just by applying the approach again using another application as input. So new components could be created and the existing ones could be modified. We also present a generic language model providing a foundation architecture that allows one to easily create new DSLs by extending it. Two proofs of concept are presented in order to exemplify the application of our approach. / Robôs móveis autônomos são máquinas com potencial para realizar atividades repetitivas ou de alta periculosidade com mais eficácia. Muitos possuem um software embarcado responsável pelo seu funcionamento. Nos últimos anos, a complexidade dessas aplicações robóticas embarcadas tem crescido continuamente e apresentam desafios que são incomuns ao desenvolvimento dos tradicionais sistemas de informação. Portanto, toda técnica que dê suporte a esse tipo de desenvolvimento pode contribuir significativamente. Uma técnica que permite o aumento de produtividade é a utilização de linguagens específicas de domínio (DSLs). Essas são linguagens de modelagem e programação cujas construções são conceitos e abstrações de um domínio de aplicação em particular. Isso desobriga o desenvolvedor de se preocupar com conceitos genéricos de programação (classes, objetos, atributos, etc.) para focar-se no problema a ser resolvido. Como o desenvolvimento de uma DSL não é uma tarefa trivial e tendo em vista as idiossincrasias dos robôs móveis autônomos, esta dissertação apresenta uma abordagem para construção de DSLs para robôs móveis. O objetivo é deixar mais sistemática e controlada a criação de DSLs para esse domínio. Nessa abordagem, uma aplicação é tomada como entrada e dela extraem-se declarações a respeito do domínio. Essas declarações são categorizadas e, para cada categoria, são levantadas partes comuns e variáveis. Então, essas partes são transformadas em componentes de uma DSL. Uma característica importante da abordagem apresentada é que uma versão inicial da DSL pode ser alcançada tendo apenas uma aplicação como base. Sugere-se que essa mesma DSL possa evoluir pela reaplicação da abordagem tendo uma nova aplicação como entrada. Dessa forma, novos componentes podem ser criados e os existentes, modificados. Também é apresentado um modelo genérico de linguagem que fornece uma arquitetura básica, permitindo que novas DSLs sejam facilmente construídas pela extensão da mesma. Duas provas de conceito são apresentadas com a intenção de exemplificar a aplicação da abordagem.

Made available in DSpace on 2016-06-02T19:06:19Z (GMT). No. of bitstreams: 1 6469.pdf: 4680875 bytes, checksum: 348ed33838e264f70033e8383aeaa100 (MD5) Previous issue date: 2014-10-27 / The integrated network management system aims to manage the telecommunications network, regardless of network elements technology in order to identify the causes of problems, providing a more assertive decision making to remedy these problems and make the network available and operational. Thus, can to cater to the market that is increasingly demanding with the level of quality telecommunications products and services. Given this need, integrated networks management system belongs to a real company needs to respond quickly to customers' expectations with respect to requests for new functions system, and perform technology upgrades periodically. However, the integrated network management system development use centered-source technologies, and it requires great effort and hinders reuse. In this context, this master's project presents a proposal to facilitate the integrated network management system development using the techniques of MDD (Model Driven Development). MDD emphasizes the use of models in software development. These models specify the rules of business domain at a high level of abstraction, i.e., regardless of the programming language and to run the software platform. With appropriate computational tools transformations of models in the source code are performed. The use of MDD can provide software reuse procedurally, enabling faster development, lower cost, produce a flexible software and enable faster modifications. To apply MDD approach, a Domain Specific Language (DSL) for the configuration management of integrated network management system setting is designed to facilitate the inclusion of a new technology to be managed by the system, while providing faster development and with fewer errors of code. To evaluate the proposal, an experiment was conducted with the participation of software developers that know the system and work in this real company. The results showed that according to the descriptive analyses there was a reduction in the time spent in application development when it was used DSL compared to the specialization of classes. However, hypotheses tests showed no such reduction. The insertion of errors in the code occurred only in applications developed using specialization classes. The use of DSL provided a broader view of the business rule and you do not need knowledge of the programming language, once the code was automatically generated. / Um sistema de gerenciamento integrado de redes tem o objetivo de gerenciar uma rede de telecomunicações, independentemente da tecnologia dos elementos de rede, a fim de identificar as causas de problemas, proporcionando a tomada de decisão mais assertiva para saná-los e deixar a rede disponível e operacional. Dessa forma, o mercado que está cada vez mais exigente com o nível de qualidade dos produtos e serviços de telecomunicações é atendido. Diante dessa necessidade, o sistema de gerenciamento integrado de redes de uma empresa real precisa atender rapidamente às expectativas dos clientes com relação às solicitações de novas funções do sistema, assim como realizar atualizações tecnológicas periodicamente. Porém, o desenvolvimento do sistema de gerenciamento integrado de redes dessa empresa utiliza tecnologias centradas em código-fonte, o que implica em grande esforço e dificulta a sua reutilização. Neste contexto, este projeto de mestrado apresenta uma proposta para facilitar o desenvolvimento do sistema de gerenciamento integrado de redes utilizando as técnicas de MDD (Desenvolvimento Dirigido a Modelos). MDD enfatiza a utilização de modelos no desenvolvimento do software. Esses modelos especificam as regras de negócio de domínio em um alto nível de abstração, ou seja, independentemente da linguagem de programação e da plataforma de execução do software. Com ferramentas computacionais adequadas são realizadas as transformações dos modelos em código-fonte. A utilização de MDD pode proporcionar reúso de software de forma processual, possibilitar um desenvolvimento mais rápido, com menor custo, produzir um software flexível e possibilitar modificações mais rapidamente. Para aplicar a abordagem de MDD, uma linguagem específica de domínio (DSL) para a gerência de configuração do sistema de gerenciamento integrado de redes foi desenvolvida. Tem como objetivo facilitar a inclusão de uma nova tecnologia a ser gerenciada pelo sistema e ao mesmo tempo proporcionar um desenvolvimento mais rápido, com menos erros de código. Para avaliar a proposta foi realizado um experimento com a participação dos atuais desenvolvedores de software de uma empresa real. Os resultados obtidos mostraram que, segundo a análise descritiva, houve redução do tempo gasto no desenvolvimento das aplicações quando foi utilizada a DSL em comparação com o desenvolvimento baseado em especialização das classes. Porém, os testes das hipóteses não apresentaram tal redução. A inserção de erros no código ocorreu somente nas aplicações desenvolvidas utilizando especialização das classes. O uso da DSL proporcionou uma visão mais ampla da regra de negócio e não exigiu conhecimento da linguagem de programação, pois o código foi gerado automaticamente.

Submitted by Nayara Passos (nayara.passos@ufpe.br) on 2015-03-12T14:23:54Z No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) TESE Leandro Marques do Nascimento.pdf: 4935348 bytes, checksum: 593ec08be509bd200bc5ec59fccb17d6 (MD5) / Made available in DSpace on 2015-03-12T14:23:54Z (GMT). No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) TESE Leandro Marques do Nascimento.pdf: 4935348 bytes, checksum: 593ec08be509bd200bc5ec59fccb17d6 (MD5) Previous issue date: 2014 / CNPq, INES / É possível se observar um alto crescimento no número de aplicações Web sendo desenvolvidas. Isto está acontecendo principalmente porque a Web está entrando em uma nova fase, chamada Web programável, onde diversos sistemas baseados na Web estão disponibilizando suas APIs publicamente. Com o objetivo de lidar com a complexidade dessa Web emergente, este trabalho define a noção de uma Máquina Social (Social Machine - SM) e vislumbra uma linguagem que permite descrever redes de tais máquinas. Para começar, nós definimos uma Máquina Social como sendo “um componente conectável e programável que encapsula (WI) um sistema de processamento de informação (IPS) e define um conjunto de serviços requeridos (RS) e providos (PS), dinamicamente disponível sob certas restrições (C), as quais são determinadas por, dentre outras coisas, seus relacionamentos (Rel) com terceiros”. Em outras palavras, uma SM é uma máquina conectada, normalmente à Web, que dinamicamente provê e/ou requer um conjunto de serviços de acordo com os seus relacionamentos estabelecidos. Qualquer aplicação na Web pode ser vista como uma SM. Para que seja possível a aplicação prática do conceito de Máquina Social previamente mencionado, nós definimos SMADL, uma linguagem para descrição arquitetural de SMs, como uma tentativa de ser uma forma completamente diferente de se programar a Web, misturando conceitos de linguagens de descrição arquitetural (ADLs) e linguagens específicas de domínio (DSLs). Como uma ADL, a linguagem permite a descrição de máquinas sociais (e redes de tais) em termos de relacionamentos (Rel) como abstrações de alto nível, sem a necessidade de se especificar os detalhes de comunicação (protocolos) e/ou métodos de autenticação. Como uma DSL, ela permite a criação e integração de serviços Web usando uma sintaxe de tipos dinâmicos, integrada à máquina virtual Java e à IDE Eclipse. Cada elemento do conceito de uma SM é diretamente mapeado na linguagem. Em poucas palavras, SMADL pode ser definida como uma linguagem dirigida a relacionamentos que pode ser usada para descrever interações entre qualquer número de máquinas de inúmeras formas, como um meio de representar máquinas interagindo na Web realmente e, obviamente, como um meio de representar interações com outras máquinas sociais também. Vários outros esforços já foram feitos para definir ADLs e alguns deles foram, de alguma forma, aplicados no domínio da Web. Entretanto, há uma clara falta de base fundamental que provenha abstrações de alto nível tais como o modelo de máquinas sociais provê. SMADL foi implementada em duas versões, uma textual e outra visual. Ambas as versões foram avaliadas através de um estudo de caso e uma pesquisa baseada na opinião de especialista e indicaram ser boas soluções para problemas práticos. / We are experiencing a high growth in the number of Web applications being developed. This is happening mainly because the Web is going into a new phase, called programmable Web, where several Web-based systems make their APIs publicly available. In order to deal with the complexity of this emerging Web, we define the notion of a Social Machine and envisage a language that can describe networks of such. To start with, we define a Social Machine (SM) as a “connectable and programmable building block that wraps (WI) an information processing system (IPS) and defines a set of required (RS) and provided services (PS), dynamically available under constraints (C) which are determined by, among other things, its relationships (Rel) with others”. In other words, a SM is a connected machine, usually to the Web, which dynamically provides and/or requires a set of services according to its established relationships. Any application in the Web can be seen as a SM. In order to make feasible the practical application of the aforementioned Social Machine concept, we define SMADL – the Social Machines Architecture Description Language – as an attempt to be a completely different way to program the Web, mixing concepts from Architecture Description Languages (ADLs) and Domain-Specific Languages (DSLs). As an ADL, it allows the description of Social Machines (and networks of such) in terms of relationships (Rel) as high-level abstractions, without the need to specify details of communication (protocols) and/or authentication methods. As a DSL, it allows the implementation and integration of Web services using a dynamically typed syntax, fully integrated to the Java Virtual Machine and Eclipse IDE. Every element of the SM concept is directly mapped into the language. In few words, SMADL can be defined as a relationship-driven language which can be used to describe the interactions between any number of machines in a multitude of ways, as a means to represent real machines interacting in the real Web and, obviously, as a means to represent interactions with other social machines too. Several other efforts have been done to define ADLs, and a few of them were someway applied to the Web domain. However, there is a clear lack of fundamental base to provide high-level abstractions that the Social Machine concept does. SMADL has been implemented in two versions, one textual and one visual. Both versions have been evaluated through a case study and an expert’s opinion survey and demonstrated to be good solutions for practical problems.

Submitted by Luiz Felipe Barbosa (luiz.fbabreu2@ufpe.br) on 2015-03-12T14:30:39Z No. of bitstreams: 2 Dissertacao Robson Santos Silva.pdf: 2657380 bytes, checksum: e8bfe7912e7136af0fbf6082153115fd (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Approved for entry into archive by Daniella Sodre (daniella.sodre@ufpe.br) on 2015-03-13T12:57:10Z (GMT) No. of bitstreams: 2 Dissertacao Robson Santos Silva.pdf: 2657380 bytes, checksum: e8bfe7912e7136af0fbf6082153115fd (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Made available in DSpace on 2015-03-13T12:57:10Z (GMT). No. of bitstreams: 2 Dissertacao Robson Santos Silva.pdf: 2657380 bytes, checksum: e8bfe7912e7136af0fbf6082153115fd (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) Previous issue date: 2013-08-23 / It is well-known that model-driven engineering (MDE) is a software development methodology that focuses on creating and exploiting (specific) domain models. Domain models (conceptually) capture all the topics (for instance, entities and their attributes, roles, and relationships as well as more specific constraints) related to a particular problem. It is common to use domain-specific languages (DSL) to describe the concrete elements of such models. MDE tools can easily build domain-specific languages (DSL), capturing syntactic as well as static semantic information. However, we still do not have a clear way of capturing the dynamic semantics of a DSL as well as checking the domain properties prior to generating the implementation code. Formal methods are a well-known solution for providing correct software, where we can guarantee the satisfaction of desired properties. Unfortunately the available formal methods tools focus almost exclusively on semantics whereas human-machine interaction is "left to the user". Several industries, and in particular the safety-critical industries, use mathematical representations to deal with their problem domains. Historically, such mathematical representations have a graphical appeal. For example, Markov chains and fault-trees are used in safety assessment processes to guarantee that airplanes, trains, and other safety-critical systems work within allowed safety margins. In general, due to the difficulty to obtain correct software, such industries use Commercial Off-The-Shelf (COTS) software or build them specifically to satisfy their needs with a related testing campaign effort. Such DSLs are difficult to capture, using just MDE tools for instance, because they have specific semantics to provide the desired (core) information for the industries that use them. In this sense, given a DSL (L) composed of a syntax and static semantics (SSL), and dynamic semantics (DSL) parts, our work proposes a rigorous methodology for combining the easiness of MDE tools, to capture SSL, with the correctness assured by formal methods, to capture DSL as well and check its properties. This combination is specifically handled in the following way, we capture all aspects of L using formal methods, check the desired properties and adjust if necessary. After that, we automatically translate part of it in terms of constructs of a MDE tool, from which we can build a user-friendly (GUI) front-end very easily (automatically). Finally, we link the front-end code to the automatically synthesized code from the formal dynamic semantics back-end. Although we require the use of a formal methods tool, the distance from the mathematical representations used in industry and the formal methods notation is very close. With this proposed methodology we intend that safety-critical industries create their domain specific software as easy as possible and with the desired static and dynamic properties formally checked. / A Engenharia Dirigida a Modelos ou (MDE—Model-Driven Engineering) é uma metodologia de desenvolvimento de software que se concentra na criação e manipulação de modelos específicos de domínio. É comum o uso de linguagens específicas de domínio (DSL) para descrever os elementos concretos de tais modelos. Ferramentas de MDE podem facilmente construir linguagens específicas de domínio (DSL), capturando seus aspectos sintáticos assim como sua semântica estática. No entanto, ainda não possuem uma forma clara de capturar a semântica dinâmica de uma DSL, assim como a verificação de propriedades de domínio antes da geração de código executável. Métodos formais são tidos como uma solução para prover software correto, onde podemos garantir que desejadas propriedades são satisfeitas. Infelizmente, as ferramentas de métodos formais disponíveis concentram-se quase que exclusivamente na semântica enquanto que a interação homem-computador é "deixada para o usuário". Indústrias em que a segurança é crítica, usam representações matemáticas para lidar com os seus domínios de problemas. Historicamente, essas representações matemáticas têm um apelo gráfico. Por exemplo, Cadeias de Markov e Árvores de Falha. Em geral, devido à dificuldade em obter softwares formalmente verificados, essas indústrias utilizam sistemas comerciais prontos para uso (Commercial Off-the-shelf - COTS) ou os constróem especificamente para satisfazerem as suas necessidades com um esforço considerável em testes. Tais DSLs são difíceis de capturar, usando apenas ferramentas MDE por exemplo, porque possuem uma semântica particular para prover as informações específicas desejadas para as indústrias que as utilizam. Neste sentido, dada uma DSL (L), composta por sintaxe e semântica estática (SSL), e semântica dinâmica (DSL), este trabalho propõe uma metodologia rigorosa para combinar a facilidade de ferramentas MDE em capturar SSL, com a corretude assegurada por métodos formais para capturar DSL e verificar suas propriedades. Esta combinação é especificamente tratada da seguinte maneira: captura-se todos os aspectos de L utilizando métodos formais, verificam-se as propriedades desejadas e as ajustam caso necessário. Em seguida, parte de L é traduzida automaticamente em termos de artefatos para uma ferramenta MDE, a partir da qual é possível construir uma interface amigável (front-end) facilmente (automaticamente). Por fim, o código do front-end é integrado com o código sintetizado automaticamente a partir da semântica dinâmica formal (back-end).