Unmanned Aerial Vehicles (UAVs) are the most dynamic growth sector of the aerospace industry today. The need to provide persistent intelligence, surveillance, and reconnaissance for military operations is driving the planned acquisition of over 5,000 UAVs over the next five years. The most pressing need is for quiet, small UAVs with endurance beyond what is capable with advanced batteries or small internal combustion propulsion systems. Fuel cell systems demonstrate high efficiency, high specific energy, low noise, low temperature operation, modularity, and rapid refuelability making them a promising enabler of the small, quiet, and persistent UAVs that military planners are seeking. Despite the perceived benefits, the actual near-term performance of fuel cell powered UAVs is unknown. Until the auto industry began spending billions of dollars in research, fuel cell systems were too heavy for useful flight applications. However, the last decade has seen rapid development with fuel cell gravimetric and volumetric power density nearly doubling every 2-3 years. As a result, a few design studies and demonstrator aircraft have appeared, but overall the design methodology and vehicles are still in their infancy. The design of fuel cell aircraft poses many challenges. Fuel cells differ fundamentally from combustion based propulsion in how they generate power and interact with other aircraft subsystems. As a result, traditional multidisciplinary analysis (MDA) codes are inappropriate. Building new MDAs is difficult since fuel cells are rapidly changing in design, and various competitive architectures exist for balance of plant, hydrogen storage, and all electric aircraft subsystems. In addition, fuel cell design and performance data is closely protected which makes validation difficult and uncertainty significant. Finally, low specific power and high volumes compared to traditional combustion based propulsion result in more highly constrained design spaces that are problematic for design space exploration. To begin addressing the current gaps in fuel cell aircraft development, a methodology has been developed to explore and characterize the near-term performance of fuel cell powered UAVs. The first step of the methodology is the development of a valid MDA. This is accomplished by using propagated uncertainty estimates to guide the decomposition of a MDA into key contributing analyses (CAs) that can be individually refined and validated to increase the overall accuracy of the MDA. To assist in MDA development, a flexible framework for simultaneously solving the CAs is specified. This enables the MDA to be easily adapted to changes in technology and the changes in data that occur throughout a design process. Various CAs that model a polymer electrolyte membrane fuel cell (PEMFC) UAV are developed, validated, and shown to be in agreement with hardware-in-the-loop simulations of a fully developed fuel cell propulsion system. After creating a valid MDA, the final step of the methodology is the synthesis of the MDA with an uncertainty propagation analysis, an optimization routine, and a chance constrained problem formulation. This synthesis allows an efficient calculation of the probabilistic constraint boundaries and Pareto frontiers that will govern the design space and influence design decisions relating to optimization and uncertainty mitigation. A key element of the methodology is uncertainty propagation. The methodology uses Systems Sensitivity Analysis (SSA) to estimate the uncertainty of key performance metrics due to uncertainties in design variables and uncertainties in the accuracy of the CAs. A summary of SSA is provided and key rules for properly decomposing a MDA for use with SSA are provided. Verification of SSA uncertainty estimates via Monte Carlo simulations is provided for both an example problem as well as a detailed MDA of a fuel cell UAV. Implementation of the methodology was performed on a small fuel cell UAV designed to carry a 2.2 kg payload with 24 hours of endurance. Uncertainty distributions for both design variables and the CAs were estimated based on experimental results and were found to dominate the design space. To reduce uncertainty and test the flexibility of the MDA framework, CAs were replaced with either empirical, or semi-empirical relationships during the optimization process. The final design was validated via a hardware-in-the loop simulation. Finally, the fuel cell UAV probabilistic design space was studied. A graphical representation of the design space was generated and the optima due to deterministic and probabilistic constraints were identified. The methodology was used to identify Pareto frontiers of the design space which were shown on contour plots of the design space. Unanticipated discontinuities of the Pareto fronts were observed as different constraints became active providing useful information on which to base design and development decisions.

Traditionally, the design of complex aerospace systems requires iteration among segregated disciplines such as aerodynamic modeling and trajectory optimization. Multidisciplinary design optimization algorithms have been developed to efficiently orchestrate the interaction among these disciplines during the design process. For example, vehicle capability is generally obtained through sequential iteration among vehicle shape, aerodynamic performance, and trajectory optimization routines in which aerodynamic performance is obtained from large pre-computed tables that are a function of angle of attack, sideslip, and flight conditions. This numerical approach segregates advancements in vehicle shape design from advancements in trajectory optimization. This investigation advances the state-of-the-art in conceptual hypersonic aerodynamic analysis and trajectory optimization by removing the source of iteration between aerodynamic and trajectory analyses and capitalizing on fundamental linkages across hypersonic solutions. Analytic aerodynamic relations, like those derived in this investigation, are possible in any flow regime in which the flowfield can be accurately described analytically. These relations eliminate the large aerodynamic tables that contribute to the segregation of disciplinary advancements. Within the limits of Newtonian flow theory, many of the analytic expressions derived in this investigation provide exact solutions that eliminate the computational error of approximate methods widely used today while simultaneously improving computational performance. To address the mathematical limit of analytic solutions, additional relations are developed that fundamentally alter the manner in which Newtonian aerodynamics are calculated. The resulting aerodynamic expressions provide an analytic mapping of vehicle shape to trajectory performance. This analytic mapping collapses the traditional, segregated design environment into a single, unified, mathematical framework which enables fast, specialized trajectory optimization methods to be extended to also include vehicle shape. A rapid trajectory optimization methodology suitable for this new, mathematically integrated design environment is also developed by relying on the continuation of solutions found via indirect methods. Examples demonstrate that families of optimal hypersonic trajectories can be quickly constructed for varying trajectory parameters, vehicle shapes, atmospheric properties, and gravity models to support design space exploration, trade studies, and vehicle requirements definition. These results validate the hypothesis that many hypersonic trajectory solutions are connected through fast indirect optimization methods. The extension of this trajectory optimization methodology to include vehicle shape through the development of analytic hypersonic aerodynamic relations enables the construction of a unified mathematical framework to perform rapid, simultaneous hypersonic aerodynamic and trajectory optimization. Performance comparisons relative to state-of-the-art methodologies illustrate the computational advantages of this new, unified design environment.

<p>The challenge of building scalable quantum computer lies in striking appropriate balance between designing a reliable system architecture from large number of faulty computational resources and improving the physical quality of system components. The detailed investigation of performance variation with physics of the components and the system architecture requires adequate performance simulation tool. In this thesis we demonstrate a software tool capable of (1) mapping and scheduling the quantum circuit on a realistic quantum hardware architecture with physical resource constraints, (2) evaluating the performance metrics such as the execution time and the success probability of the algorithm execution, and (3) analyzing the constituents of these metrics and visualizing resource utilization to identify system components which crucially define the overall performance.</p><p>Using this versatile tool, we explore vast design space for modular quantum computer architecture based on trapped ions. We find that while success probability is uniformly determined by the fidelity of physical quantum operation, the execution time is a function of system resources invested at various layers of design hierarchy. At physical level, the number of lasers performing quantum gates, impact the latency of the fault-tolerant circuit blocks execution. When these blocks are used to construct meaningful arithmetic circuit such as quantum adders, the number of ancilla qubits for complicated non-clifford gates and entanglement resources to establish long-distance communication channels, become major performance limiting factors. Next, in order to factorize large integers, these adders are assembled into modular exponentiation circuit comprising bulk of Shor's algorithm. At this stage, the overall scaling of resource-constraint performance with the size of problem, describes the effectiveness of chosen design. By matching the resource investment with the pace of advancement in hardware technology, we find optimal designs for different types of quantum adders. Conclusively, we show that 2,048-bit Shor's algorithm can be reliably executed within the resource budget of 1.5 million qubits.</p> / Dissertation

Simulation is a vital tool used by architects to develop new architectures. However, because of the complexity of modern architectures and the length of recent benchmarks, detailed simulation of programs can take extremely long times. This impedes the exploration of processor design space which the architects need to do to find the optimal configuration of processor parameters. Sampling is one technique which reduces the simulation time without adversely affecting the accuracy of the results. Yet, most sampling techniques either ignore the warm-up issue or require significant development effort on the part of the user.In this thesis we tackle the problem of reconciling state-of-the-art warm-up techniques and the latest sampling mechanisms with the triple objective of keeping the user effort minimum, achieving good accuracy and being agnostic to software and hardware changes. We show that both the representative and statistical sampling techniques can be adapted to use warm-up mechanisms which can accommodate the underlying architecture's warm-up requirements on-the-fly. We present the experimental results which show an accuracy and speed comparable to latest research. Also, we leverage statistical calculations to provide an estimate of the robustness of the final results.

Cryptographic protocols are implemented in hardware to ensure low-area, high speed and reduced power consumption especially for mobile devices. Elliptic Curve Cryptography (ECC) is the most commonly used public-key cryptosystem and its performance depends heavily on efficient finite field arithmetic hardware. Finding the multiplicative inverse (inversion) is the most expensive finite field operation in ECC. The two predominant algorithms for computing finite field inversion are Fermat’s Little Theorem (FLT) and Extended Euclidean Algorithm (EEA). EEA is reported to be the most efficient inversion algorithm in terms of performance and power consumption. This dissertation presents a new reformulation of EEA algorithm, which allows for speedup and optimization techniques such as concurrency and resource sharing. Modular arithmetic operations over GF(p) are introduced for small values of p, observing interesting figures, particularly for modular division. Whereas, polynomial arithmetic operations over GF(pm) are discussed adequately in order to examine the potential for processes concurrency. In particular, polynomial division and multiplication are revisited in order to derive their iterative equations, which are suitable for systolic array implementation. Consequently, several designs are proposed for each individual process and their complexities are analyzed and compared. Subsequently, a concurrent divider/multiplier-accumulator is developed, while the resulting systolic architecture is utilized to build the EEA-based inverter. The processing elements of our systolic architectures are created accordingly, and enhanced to accommodate data management throughout our reformulated EEA algorithm. Meanwhile, accurate models for the complexity analysis of the proposed inverters are developed. Finally, a novel, fast, and compact inverter over binary fields is proposed and implemented on FPGA. The proposed design outperforms the reported inverters in terms of area and speed. Correspondingly, an EEA-based inverter over ternary fields is built, showing the lowest area-time complexity among the reported inverters. / Graduate

With the current demand for mixed-signal SoCs, an increasing number of designers are looking for ADC architectures that can be easily implemented over digital substrates. Since ADC performance is strongly dependent upon physical and electrical features, it gets more difficult for them to benefit from more recent technologies, where these features are more variable. This way, analog signal acquisition is not allowed to follow an evolutionary trend compatible with Moore’s Law. In fact, such trend shall get worst, since newer technologies are expected to have more variable characteristics. Also, for a matter of economy of scale, many times a mixed-signal SoC presents a good amount of idle processing power. In such systems it is advantageous to employ more costly digital signal processing provided that it allows a reduction in the analog area demanded or the use of less expensive analog blocks, able to cope with process variations and uncertainty. Besides the technological concerns, other factors that impact the cost of the design also advise to transfer problems from the analog to the digital domain whenever possible: design automation and self-test requirements, for instance. Recent surveys indicate that the total cost in designer hours for the analog blocks of a mixed-signal system can be up to three times the cost of the digital ones. This manuscript explores the concept of bottom-up analog acquisition design, using statistical sampling as a way to reduce the analog area demanded in the design of ADCs within mixed-signal systems. More particularly, it investigates the possibility of using digital modeling and digital compensation of non-idealities to ease the design of ADCs. The work is developed around three axes: the definition of target applications, the development of digital compensation algorithms and the exploration of architectural possibilities. New methods and architectures are defined and validated. The main notions behind the proposal are analyzed and it is shown that the approach is feasible, opening new paths of future research. Keywords:

Este trabalho propõe uma nova abordagem para o desenvolvimento de sistemas embarcados, através da combinação da abstração e propriedades de verificação de modelos da linguagem declarativa Alloy com a ampla aceitação de Java na indústria. A abordagem surge no contexto de que a automação de software no domínio embarcado tornou-se extremamente necessária, uma vez que atualmente a maior parte do tempo de desenvolvimento é gasta no projeto de software de produtos tão restritos em termos de recursos. As ferramentas de automação de software embarcado devem atender a demanda por produtividade e manutenibilidade, mas respeitar restrições naturais deste tipo de sistema, tais como espaço de memória, potência e desempenho. As ferramentas de automação de projeto lidam com produtividade e manutenibilidade ao permitir especificações de alto nível, tarefa difícil de atender no domínio embarcado devido ao comportamento misto de muitas aplicações embarcadas. Abordagens que promovem meios para verificação formal também são atrativas, embora geralmente sejam difíceis de usar, e por este motivo não são de grande auxílio na tarefa de reduzir o tempo de chegada ao mercado do produto. Através do uso de Alloy, baseada em lógica de primeira-ordem, é possível obter especificações em altonível e verificação formal de modelos com uma única linguagem. Este trabalho apresenta a poderosa abstração proporcionada pela linguagem Alloy em aplicações embarcadas, assim como regras para obter automaticamente código Java a partir de modelos Alloy. A geração de código Java a partir de modelos Alloy, combinada a uma ferramenta de estimativa, provê exploração de espaço de projeto, atendendo assim as fortes restrições do projeto de software embarcado, o que normalmente não é contemplado pela engenharia de software tradicional. / This work proposes a new approach for embedded software development, by combining the abstraction and model verification properties of the Alloy declarative language with the broad acceptance in industry of Java. The approach comes into play since software automation in the embedded domain has become a major need, as currently most of the development time is spent designing software for such hardconstrained resources products. Design automation tools for embedded systems must meet the demand for productivity and maintainability, but constraints such as memory, power and performance must still be considered. Design automation tools deal with productivity and maintainability by allowing high-level specifications, which is hard to accomplish on the embedded domain due to the mixed behavior nature of many embedded applications. Approaches that provide means for formal verification are also attractive, but their usage is usually not straightforward, and for this reason they are not that helpful in dealing with time-tomarket constraints. By using Alloy, based in first-order logic, it is possible to obtain high-level specifications and formal model verification with a single language. This work shows the powerful abstraction provided by the Alloy language for embedded applications, as well as rules for obtaining automatically Java code from Alloy models. The Java source code generation from Alloy models, combined with an estimation tool, provides design space exploration to match tight embedded software design constraints, what is usually not taken into account by standard software engineering techniques.

Heutzutage sind wir von Geräten umgeben, die sowohl Hardware wie auch Software- Komponenten beinhalten. Diese Geräte unterstützen ein breites Spektrum an verschiedenen Domänen, so zum Beispiel Telekommunikation, Luftfahrt, Automobil und andere. Derartige Systeme sind überall aufzufinden und werden als Eingebettete Systeme bezeichnet, da sie zur Informationsverarbeitung in andere Produkte eingebettet werden, wobei die Informationsverarbeitung des eingebetteten Systems jedoch nicht die bezeichnende Funktion des Produkts ist. Die ständig zunehmende Komplexität moderner eingebettete Systeme erfordert die Verwendung von mehreren Komponenten um die Funktionen von einem einzelnen System zu implementieren. Eine solche Steigerung der Funktionalität führt jedoch ebenfalls zu einem Wachstum in der Entwurfs-Komplexität, die korrekt und effizient beherrscht werden muss. Neben hohen Anforderungen bezüglich Leistungsaufnahme, Performanz und Kosten hat auch Time-to-Market-Anforderungen großen Einfluss auf den Entwurf von Eingebetteten Systemen. Design Space Exploration (DSE) beschreibt die systematische Erzeugung und Auswertung von Entwurfs-Alternativen, um die Systemleistung zu optimieren und den gestellten Anforderungen an das System zu genügen. Bei der Entwicklung von Eingebetteten Systemen, speziell beim Platform-Based Design (PBD) führt die zunehmende Anzahl von Design-Entscheidungen auf mehreren Abstraktionsebenen zu einer Explosion der möglichen Kombinationen von Alternativen, was auch für aktuelle DSE Methoden eine Herausforderung darstellt. Jedoch vermag üblicherweise nur eine begrenzte Anzahl von Entwurfs-Alternativen die zusätzlich formulierten nicht-funktionalen Anforderungen zu erfüllen. Darüber hinaus beeinflusst jede Entwurfs- Entscheidung weitere Entscheidungen und damit die resultierenden Systemeigenschaften. Somit existieren Abhängigkeiten zwischen Entwurfs-Entscheidungen und deren Reihenfolge auf dem Weg zur Implementierung des Systems. Zudem gilt es zwischen einer spezifischen Heuristik für eine bestimmte DSE, welche zu verbesserten Optimierungsresultaten führt, sowie globalen Verfahren, welche ihrerseits zur Flexibilität hinsichtlich der Anwendbarkeit bei verschiedenen DSE Szenarien beitragen, abzuwägen. Um die genannten Herausforderungen zu lösen wird eine Modellgetriebene Entwicklung (englisch Model-Driven Engineering, kurz MDE) Methodik für DSE vorgeschlagen. Für diese Methodik wird ein DSE-Domain-Metamodell eingeführt um relevante DSEKonzepte wie Entwurfsraum, Entwurfs-Alternativen, Auswertungs- und Bewertungsverfahren, Einschränkungen und andere abzubilden. Darüber hinaus modelliert das Metamodell verschiedenen DSE-Frage- stellungen, was zur Verbesserung der Flexibilität der vorgeschlagenen Methodik beiträgt. Zur Umsetzung von DSE-Regeln, welche zur Steuerung, Einschränkung und Generierung der Ent- wurfs-Alternativen genutzt werden, finden Modell-zu-Modell-Transformationen Anwendung. Durch die Fokussierung auf die Zuordnung zwischen den Schichten in einem PBDAnsatz wird eine neuartige Entwurfsraumabstraktion eingeführt, um multiple Entwurfsentscheidungen als singuläres DSE Problem zu repräsentieren. Diese auf dem Categorial Graph Product aufbauende Abstraktion entkoppelt den Explorations-Algorithmus vom Entwurfsraum und ist für Umsetzung in automatisierte Werkzeugketten gut geeignet. Basierend auf dieser Abstraktion profitiert die DSE-Methode durch die eingeführte MDEMethodik als solche und ermöglicht nunmehr neue Optimierungsmöglichkeiten sowie die Verbesserung der Integration von DSE in Entwicklungsprozesse und die Spezifikation von DSE-Szenarien. / Atualmente dispositivos contendo hardware e software são encontrados em todos os lugares. Estes dispositivos prestam suporte a uma varieadade de domínios, como telecomunicações, automotivo e outros. Eles são chamados “sistemas embarcados”, pois são sistemas de processamento montados dentro de produtos, cujo sistema de processamento não faz parte da funcionalidade principal do produto. O acréscimo de funções nestes sistemas implica no aumento da complexidade de seu projeto, o qual deve ser adequadamente gerenciado, pois além de requisitos rigorosos em relação à dissipação de potência, desempenho e custos, a pressão sobre o prazo para introdução de um produto no mercado também dificulta seu projeto. Exploração do espaço de projeto (DSE) é a atividade sistemática de gerar e avaliar alternativas de projetos, com o objetivo de otimizar suas propriedades. No desenvolvimento de sistemas embarcados, especialmente em Projeto Baseado em Plataformas (PBD), metodologias de DSE atuais são desafiadas pelo crescimento do número de decisões de projeto, o qual implica na explosão da combinação de alternativas. Porém, somente algumas destas resultam em projetos que atedem os requisitos nãofuncionais. Além disso, as decisões influenciam umas às outras, de forma que a ordem em que estas são tomadas alteram a implementação final do sistema. Outro desafio é o balanço entre flexibilidade da metodologia e seu desempenho, pois métodos globais de otimização são flexíveis, mas apresentam baixo desempenho. Já heurísticas especialmente desenvolvidas para o cenário de DSE em questão apresentam melhor desempenho, porém dificilmente são aplicáveis a diferentes cenários. Com o intuito de superar os desafios é proposta uma metodologia de projeto dirigido por modelos (MDE) adquada para DSE. Um metamodelo do domínio de DSE é definido para representar conceitos como espaço de projeto, métodos de avaliação e restrições. O metamodelo também representa diferentes problemas de DSE aprimorando a flexibilidade da metodologia. Regras de transformações de modelos implementam as regras de DSE, as quais são utilizadas para restringir e guiar a geração de projetos alternativos. Restringindo-se ao mapeamento entre camadas no PBD é proposta uma abstração para representar o espaço de projeto. Ela representa múltiplas decisões de projeto envolvidas no mapeamento como um único problema de DSE. Esta representação é adequada para a implementação em ferramentas automática de DSE e pode beneficiar o processo de DSE com uma abordagem de MDE, aprimorando a especificação de cenários de DSE e sua integração no processo de desenvolvimento. / Nowadays we are surrounded by devices containing hardware and software components. These devices support a wide spectrum of different domains, such as telecommunication, avionics, automobile, and others. They are found anywhere, and so they are called Embedded Systems, as they are information processing systems embedded into enclosing products, where the processing system is not the main functionality of the product. The ever growing complexity in modern embedded systems requires the utilization of more components to implement the functions of a single system. Such an increasing functionality leads to a growth in the design complexity, which must be managed properly, because besides stringent requirements regarding power, performance and cost, also time-to-market hinders the design of embedded systems. Design Space Exploration (DSE) is the systematic generation and evaluation of design alternatives, in order to optimize system properties and fulfill requirements. In embedded system development, specifically in Platform-Based Design (PBD), current DSE methodologies are challenged by the increasing number of design decisions at multiple abstraction levels, which leads to an explosion of combination of alternatives. However, only a reduced number of these alternatives leads to feasible designs, which fulfill non-functional requirements. Moreover, each design decision influences subsequent decisions and system properties, hence there are inter-dependencies between design decisions, so that the order decisions are made matters to the final system implementation. Furthermore, there is a trade-off between heuristics for specific DSE, which improves the optimization results, and global optimizers, which improve the flexibility to be applied in different DSE scenarios. In order to overcome the identified challenges an MDE methodology for DSE is proposed. For this methodology a DSE Domain metamodel is proposed to represent relevant DSE concepts such as design space, design alternatives, evaluation method, constraints and others. Moreover, this metamodel represents different DSE problems, improving the flexibility of the proposed framework. Model transformations are used to implement DSE rules, which are used to constrain, guide, and generate design candidates. Focusing on the mapping between layers in a PBD approach, a novel design space abstraction is provided to represent multiple design decisions involved in the mapping as a single DSE problem. This abstraction is based on Categorical Graph Product, decoupling the exploration algorithm from the design space and being well suited to be implemented in automatic exploration tools. Upon this abstraction, the DSE method can benefit from the MDE methodology, opening new optimization opportunities, and improving the DSE integration into the development process and specification of DSE scenarios.

With the current demand for mixed-signal SoCs, an increasing number of designers are looking for ADC architectures that can be easily implemented over digital substrates. Since ADC performance is strongly dependent upon physical and electrical features, it gets more difficult for them to benefit from more recent technologies, where these features are more variable. This way, analog signal acquisition is not allowed to follow an evolutionary trend compatible with Moore’s Law. In fact, such trend shall get worst, since newer technologies are expected to have more variable characteristics. Also, for a matter of economy of scale, many times a mixed-signal SoC presents a good amount of idle processing power. In such systems it is advantageous to employ more costly digital signal processing provided that it allows a reduction in the analog area demanded or the use of less expensive analog blocks, able to cope with process variations and uncertainty. Besides the technological concerns, other factors that impact the cost of the design also advise to transfer problems from the analog to the digital domain whenever possible: design automation and self-test requirements, for instance. Recent surveys indicate that the total cost in designer hours for the analog blocks of a mixed-signal system can be up to three times the cost of the digital ones. This manuscript explores the concept of bottom-up analog acquisition design, using statistical sampling as a way to reduce the analog area demanded in the design of ADCs within mixed-signal systems. More particularly, it investigates the possibility of using digital modeling and digital compensation of non-idealities to ease the design of ADCs. The work is developed around three axes: the definition of target applications, the development of digital compensation algorithms and the exploration of architectural possibilities. New methods and architectures are defined and validated. The main notions behind the proposal are analyzed and it is shown that the approach is feasible, opening new paths of future research. Keywords:

Este trabalho propõe uma nova abordagem para o desenvolvimento de sistemas embarcados, através da combinação da abstração e propriedades de verificação de modelos da linguagem declarativa Alloy com a ampla aceitação de Java na indústria. A abordagem surge no contexto de que a automação de software no domínio embarcado tornou-se extremamente necessária, uma vez que atualmente a maior parte do tempo de desenvolvimento é gasta no projeto de software de produtos tão restritos em termos de recursos. As ferramentas de automação de software embarcado devem atender a demanda por produtividade e manutenibilidade, mas respeitar restrições naturais deste tipo de sistema, tais como espaço de memória, potência e desempenho. As ferramentas de automação de projeto lidam com produtividade e manutenibilidade ao permitir especificações de alto nível, tarefa difícil de atender no domínio embarcado devido ao comportamento misto de muitas aplicações embarcadas. Abordagens que promovem meios para verificação formal também são atrativas, embora geralmente sejam difíceis de usar, e por este motivo não são de grande auxílio na tarefa de reduzir o tempo de chegada ao mercado do produto. Através do uso de Alloy, baseada em lógica de primeira-ordem, é possível obter especificações em altonível e verificação formal de modelos com uma única linguagem. Este trabalho apresenta a poderosa abstração proporcionada pela linguagem Alloy em aplicações embarcadas, assim como regras para obter automaticamente código Java a partir de modelos Alloy. A geração de código Java a partir de modelos Alloy, combinada a uma ferramenta de estimativa, provê exploração de espaço de projeto, atendendo assim as fortes restrições do projeto de software embarcado, o que normalmente não é contemplado pela engenharia de software tradicional. / This work proposes a new approach for embedded software development, by combining the abstraction and model verification properties of the Alloy declarative language with the broad acceptance in industry of Java. The approach comes into play since software automation in the embedded domain has become a major need, as currently most of the development time is spent designing software for such hardconstrained resources products. Design automation tools for embedded systems must meet the demand for productivity and maintainability, but constraints such as memory, power and performance must still be considered. Design automation tools deal with productivity and maintainability by allowing high-level specifications, which is hard to accomplish on the embedded domain due to the mixed behavior nature of many embedded applications. Approaches that provide means for formal verification are also attractive, but their usage is usually not straightforward, and for this reason they are not that helpful in dealing with time-tomarket constraints. By using Alloy, based in first-order logic, it is possible to obtain high-level specifications and formal model verification with a single language. This work shows the powerful abstraction provided by the Alloy language for embedded applications, as well as rules for obtaining automatically Java code from Alloy models. The Java source code generation from Alloy models, combined with an estimation tool, provides design space exploration to match tight embedded software design constraints, what is usually not taken into account by standard software engineering techniques.