Protocols between programs and proofs

In this paper we describe a new protocol that we call the Curry-Howard protocol between a theory and the programs extracted from it. This protocol leads to the expansion of the theory and the production of more powerful programs. The methodology we use for automatically extracting “correct” programs from proofs is a development of the well-known Curry-Howard process. Program extraction has been developed by many authors, but our presentation is ultimately aimed at a practical, usable system and has a number of novel features. These include 1. a very simple and natural mimicking of ordinary mathematical practice and likewise the use of established computer programs when we obtain programs from formal proofs, and 2. a conceptual distinction between programs on the one hand, and proofs of theorems that yield programs on the other. An implementation of our methodology is the Fred system. As an example of our protocol we describe a constructive proof of the well-known theorem that every graph of even parity can be decomposed into a list of disjoint cycles. Given such a graph as input, the extracted program produces a list of the (non-trivial) disjoint cycles as promised.

A Framework supporting collaboration on the distributed design of integrated systems

The work described in this thesis aims to support the distributed design of integrated systems and considers specifically the need for collaborative interaction among designers. Particular emphasis was given to issues which were only marginally considered in previous approaches, such as the abstraction of the distribution of design automation resources over the network, the possibility of both synchronous and asynchronous interaction among designers and the support for extensible design data models. Such issues demand a rather complex software infrastructure, as possible solutions must encompass a wide range of software modules: from user interfaces to middleware to databases. To build such structure, several engineering techniques were employed and some original solutions were devised. The core of the proposed solution is based in the joint application of two homonymic technologies: CAD Frameworks and object-oriented frameworks. The former concept was coined in the late 80's within the electronic design automation community and comprehends a layered software environment which aims to support CAD tool developers, CAD administrators/integrators and designers. The latter, developed during the last decade by the software engineering community, is a software architecture model to build extensible and reusable object-oriented software subsystems. In this work, we proposed to create an object-oriented framework which includes extensible sets of design data primitives and design tool building blocks. Such object-oriented framework is included within a CAD Framework, where it plays important roles on typical CAD Framework services such as design data representation and management, versioning, user interfaces, design management and tool integration. The implemented CAD Framework - named Cave2 - followed the classical layered architecture presented by Barnes, Harrison, Newton and Spickelmier, but the possibilities granted by the use of the object-oriented framework foundations allowed a series of improvements which were not available in previous approaches: - object-oriented frameworks are extensible by design, thus this should be also true regarding the implemented sets of design data primitives and design tool building blocks. This means that both the design representation model and the software modules dealing with it can be upgraded or adapted to a particular design methodology, and that such extensions and adaptations will still inherit the architectural and functional aspects implemented in the object-oriented framework foundation; - the design semantics and the design visualization are both part of the object-oriented framework, but in clearly separated models. This allows for different visualization strategies for a given design data set, which gives collaborating parties the flexibility to choose individual visualization settings; - the control of the consistency between semantics and visualization - a particularly important issue in a design environment with multiple views of a single design - is also included in the foundations of the object-oriented framework. Such mechanism is generic enough to be also used by further extensions of the design data model, as it is based on the inversion of control between view and semantics. The view receives the user input and propagates such event to the semantic model, which evaluates if a state change is possible. If positive, it triggers the change of state of both semantics and view. Our approach took advantage of such inversion of control and included an layer between semantics and view to take into account the possibility of multi-view consistency; - to optimize the consistency control mechanism between views and semantics, we propose an event-based approach that captures each discrete interaction of a designer with his/her respective design views. The information about each interaction is encapsulated inside an event object, which may be propagated to the design semantics - and thus to other possible views - according to the consistency policy which is being used. Furthermore, the use of event pools allows for a late synchronization between view and semantics in case of unavailability of a network connection between them; - the use of proxy objects raised significantly the abstraction of the integration of design automation resources, as either remote or local tools and services are accessed through method calls in a local object. The connection to remote tools and services using a look-up protocol also abstracted completely the network location of such resources, allowing for resource addition and removal during runtime; - the implemented CAD Framework is completely based on Java technology, so it relies on the Java Virtual Machine as the layer which grants the independence between the CAD Framework and the operating system. All such improvements contributed to a higher abstraction on the distribution of design automation resources and also introduced a new paradigm for the remote interaction between designers. The resulting CAD Framework is able to support fine-grained collaboration based on events, so every single design update performed by a designer can be propagated to the rest of the design team regardless of their location in the distributed environment. This can increase the group awareness and allow a richer transfer of experiences among them, improving significantly the collaboration potential when compared to previously proposed file-based or record-based approaches. Three different case studies were conducted to validate the proposed approach, each one focusing one a subset of the contributions of this thesis. The first one uses the proxy-based resource distribution architecture to implement a prototyping platform using reconfigurable hardware modules. The second one extends the foundations of the implemented object-oriented framework to support interface-based design. Such extensions - design representation primitives and tool blocks - are used to implement a design entry tool named IBlaDe, which allows the collaborative creation of functional and structural models of integrated systems. The third case study regards the possibility of integration of multimedia metadata to the design data model. Such possibility is explored in the frame of an online educational and training platform.

Aplicações de Dispositivos de Microondas utilizando Substrato EBG/PBG para Comunicações Móveis

The modern society depends on an efficient communications system able to of transmitting and receiving information with a higher speed and reliability every time. The need for ever more efficient devices raises optimization techniques of microstrip devices, such as techniques to increase bandwidth: thicker substrates and substrate structures with EBG (Electromagnetic Band Gap) and PBG (Photonic Band Gap). This work has how aims the study of the application of PBG materials on substrates of planar structures in microstrip, more precisely in directional quadrature couplers and in rat-race and impedance of transformers. A study of the planar structures in microstrip and substrates EBG is presented. The PBG substrates can be used to optimize the radiation through the air, thus reducing the occurrence of surface waves and the resulting diffraction edge responsible for degradation of radiation pattern. Through specific programs in FORTRAN Power Station obtained the frequencies and couplings for each structure. Are used the program PACMO - Computer Aided Design in Microwave. Results are obtained of the frequency and coupling devices, ranging the frequency band used (cellular communication and Wimax systems) and the permittivity of the substrate, comparing the results of conventional material and PBG materials in the s and p polarizations.

Estudo de antenas patches de microfita miniaturizadas em banda larga para aplicação em dispositivos móveis e portáteis

This work presents techniques used to design and manufacture microstrip patch antennas for applications in portable and mobile devices. To do so, are evaluated several factors that can influence the performance of microstrip patch antennas. Miniaturization techniques are studied and employed in order to apply this type of antenna in mobile and / or mobile. The theories of microstrip patch antennas are addressed by analyzing characteristics such as constitution, kinds of patches, substrates, feeding methods, analysis methods, the main advantages and disadvantages and others. Techniques for obtaining broadband microstrip patch antennas were surveyed in literature and exemplified mainly by means of simulations and measurements. For simulations of the antennas was used the commercial software . In addition, antenna miniaturization techniques have been studied as a main concern the fundamental limits of antennas with special attention to electrically small antennas because they are directly linked to the microstrip patch antennas. Five design antennas are proposed to demonstrate the effectiveness of techniques used to obtain the microstrip patch antennas broadband and miniaturized for use in mobile devices and/or portable. For this, the proposed antennas were simulated, built and measured. The antennas are proposed to be used in modern systems of wireless communications such as DTV, GPS, IEEE 802.16, IEEE 802.11, etc. The simulations of the antennas were made in business and computer programs. The measured results were obtained with a parser Vector of networks of the Rhode and Schwarz model ZVB 14

DIRECT EXPRESSIONS FOR OGATA LEAD-LAG DESIGN METHOD USING ROOT LOCUS

Direct expressions for the design of a lead-lag continuous compensator using the root locus method and the procedure described in the 1970 and 1990 books by Ogata are presented. These results are useful in the Ogata design method because they avoid the geometrical determination of poles and zeros, making it easier to create a computer-based design.

Determination of the maximum force due to skull impact in fights between sheep of the Ovis aries species

The present article presents a means of determining the maximum impact force between two bodies from the determination of the involved impulse in the impact and the sound emitted by the shock of the bodies during this impact.It also presents a case study applied to the shock between the skulls of male sheep of the Ovis aries species. These animals do not possess horns and dispute the territorial leadership by fighting, during which the skull is used as a weapon of attack, similar to a battering ram.Initially, a revision of basic physics approaching the theory of impulse is made, which shows that the average force during an impact can be obtained by the quantity of movement of the bodies. In its turn, the quantity of movement is obtained through the average speed of approach and the mass of the bodies. The maximum force is obtained from the average force, using the approach of the Force X Time curve with the Sonorous Intensity X Time Curve.In order to study the case of a shock between two sheep, the mass of the bodies was obtained through direct weighing and the average speed of approach obtained indirectly through filming, thus making possible the calculation of the average force. The Sonorous Intensity X Time Curve was obtained through the recording of the sound of the impact during a filmed fight, with later manipulation through computer programs. With this data the maximum force exercised between the skull of the sheep during the impact was obtained, which will be used in later studies.

Methodology analysis of a computational tool used in electronic circuit design

This paper considers the importance of using a top-down methodology and suitable CAD tools in the development of electronic circuits. The paper presents an evaluation of the methodology used in a computational tool created to support the synthesis of digital to analog converter models by translating between different tools used in a wide variety of applications. This tool is named MS 2SV and works directly with the following two commercial tools: MATLAB/Simulink and SystemVision. Model translation of an electronic circuit is achieved by translating a mixed-signal block diagram developed in Simulink into a lower level of abstraction in VHDL-AMS and the simulation project support structure in SystemVision. The method validation was performed by analyzing the power spectral of the signal obtained by the discrete Fourier transform of a digital to analog converter simulation model. © 2011 IEEE.

Uso e adequação de tensoestruturas à região Amazônica estudo de caso: Feira do Ver-O-Peso em Belém-Pa

A crescente utilização das tensoestruturas para os mais diversos tipos de uso, nem sempre com a devida preocupação com os aspectos climáticos locais, motivou o presente estudo, o qual avalia a adequação deste tipo de cobertura à Região Amazônica. Em particular, tem-se como objeto de estudo as tensoestruturas da feira do Ver-O-Peso, localizada na cidade de Belém-PA. Neste trabalho, a avaliação do desempenho das coberturas tensionadas utilizadas na feira baseou-se na Arquitetura Bioclimática, com ênfase no desempenho das mesmas como proteção às intempéries. Na metodologia utilizada, a adequação do projeto destas tensoestruturas ao clima da região é verificada utilizando-se os programas Analyses Bio 3.0, o SOL-AR 5.0.1 e o Tensil 2.1. Os resultados obtidos com estes programas permitiram uma análise crítica do projeto das tensoestruturas da feira do Ver-O-Peso, quanto à orientação destas estruturas com relação à direção dos ventos predominantes e incidência dos raios solares, assim como no que diz respeito ao seu desempenho térmico e luminoso. Para estudar precisamente a incidência solar nas estruturas de acordo com a posição do sol, foi desenvolvida uma maquete eletrônica, utilizando-se o programa 3 DS MAX 8. Posteriormente, algumas simulações computacionais foram realizadas considerando as coordenadas geográficas da cidade de Belém e a respectiva trajetória do sol, durante o solstício de verão, solstício de inverno e equinócio; Além das análises realizadas através destes programas, foi desenvolvida também uma pesquisa de campo, com base na aplicação de questionários aos usuários da feira (feirantes e clientes). Os resultados obtidos demonstraram a necessidade de melhoria na proteção no interior destas tensoestruturas, especialmente para as barracas localizadas na periferia da área coberta. Para isso, sugere-se a utilização de um anteparo feito com uma membrana translúcida. Este anteparo, colocado estrategicamente nas regiões mais críticas da cobertura permitiria a passagem da luz, porém diminuindo os efeitos da radiação direta e criaria uma proteção mais eficaz para as chuvas, sem agredir esteticamente o projeto original.

Modelo dinâmico de um túnel de vento de sopro

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES)

Aplicação e análise da utilização do software Eberick em um projeto residencial popular

Due to new technologies in civil engineering and the competition of the market, the demand for computer programs for the elaboration of structural projects of reinforced concrete is raising in a quick and efficient manner. This paper presents a study based on Eberick, a structural calculation software, and this software was applied to a low cost residence project. By performing structural calculation manually, it is possible to compare and analyze the criteria that Eberick uses for the design and detailing of structural elements like columns, beams and slabs. As the software functionality becomes clear, the engineer will use it careful and safely, exploring all of its resources and advantages

Arte reversa: aplicando a engenharia reversa na arte

This study aimed to examine the reverse engineering and respond to a concern about the possible application of this concept in art, breaking down barriers and breaking paradigms. Using 3D scanning, the art of computer aided design and manufacturing – CAD/CAM, machining by computer numerical control - CNC, engineering, and applying this methodology in the arts especially in sculpture, it is possible to dematerialize a artwork, virtualizes it in 3D programs, make speeches, and process a new work, a new art elsewhere. By the example of surgeries at a distance, the artist, or technical author could produce their works, and materialize them anywhere. In other words, do the reverse gear. It discusses the relationship between art and technology, the role of the author, the viewer, which can interfere with the interactivity that case by stating that art, exists only in the look and feel of the viewer.

Sanitário solar: a transdisciplinaridade como ferramenta de projeto, design e desenvolvimento sustentável

The appropriate use of computer aided technologies, allied to the concepts and design guidelines, grounded in biology, stimulated the development of a solar toilet, able to convert human waste into compost, rich in nutrients for use in gardens, farms and small farms. This transdisciplinary approach is presented as a necessary tool to be used in academia, integrating and developing activities previously disconnected. The solar toilet also called green bathroom, combines the most modern concepts and technologies of computer-aided design, design, selection of materials and microbiological control, reaching biologically correct and safe composting of waste, ensuring the viability of the project terms of cost, deployment, use and environmental safety, such as supporting sustainable development. It is also planned to install a pilot project in a small community with the aim of assessing its implementation and use as a complementary activity and university extension.

Design of a Wireless Vision Sensor for Object Tracking in Wireless Vision Sensor Networks

The integration of CMOS cameras with embedded processors and wireless communication devices has enabled the development of distributed wireless vision systems. Wireless Vision Sensor Networks (WVSNs), which consist of wirelessly connected embedded systems with vision and sensing capabilities, provide wide variety of application areas that have not been possible to realize with the wall-powered vision systems with wired links or scalar-data based wireless sensor networks. In this paper, the design of a middleware for a wireless vision sensor node is presented for the realization of WVSNs. The implemented wireless vision sensor node is tested through a simple vision application to study and analyze its capabilities, and determine the challenges in distributed vision applications through a wireless network of low-power embedded devices. The results of this paper highlight the practical concerns for the development of efficient image processing and communication solutions for WVSNs and emphasize the need for cross-layer solutions that unify these two so-far-independent research areas.

DESIGN AND IMPLEMENT DYNAMIC PROGRAMMING BASED DISCRETE POWER LEVEL SMART HOME SCHEDULING USING FPGA

With the development and capabilities of the Smart Home system, people today are entering an era in which household appliances are no longer just controlled by people, but also operated by a Smart System. This results in a more efficient, convenient, comfortable, and environmentally friendly living environment. A critical part of the Smart Home system is Home Automation, which means that there is a Micro-Controller Unit (MCU) to control all the household appliances and schedule their operating times. This reduces electricity bills by shifting amounts of power consumption from the on-peak hour consumption to the off-peak hour consumption, in terms of different “hour price”. In this paper, we propose an algorithm for scheduling multi-user power consumption and implement it on an FPGA board, using it as the MCU. This algorithm for discrete power level tasks scheduling is based on dynamic programming, which could find a scheduling solution close to the optimal one. We chose FPGA as our system’s controller because FPGA has low complexity, parallel processing capability, a large amount of I/O interface for further development and is programmable on both software and hardware. In conclusion, it costs little time running on FPGA board and the solution obtained is good enough for the consumers.

DESIGN AND IMPLEMENTATION OF HOME USE PORTABLE SMART ELECTRONICS

The widespread of low cost embedded electronics makes it easier to implement the smart devices that can understand either the environment or the user behaviors. The main object of this project is to design and implement home use portable smart electronics, including the portable monitoring device for home and office security and the portable 3D mouse for convenient use. Both devices in this project use the MPU6050 which contains a 3 axis accelerometer and a 3 axis gyroscope to sense the inertial motion of the door or the human hands movement. For the portable monitoring device for home and office security, MPU6050 is used to sense the door (either home front door or cabinet door) movement through the gyroscope, and Raspberry Pi is then used to process the data it receives from MPU6050, if the data value exceeds the preset threshold, Raspberry Pi would control the USB Webcam to take a picture and then send out an alert email with the picture to the user. The advantage of this device is that it is a small size portable stand-alone device with its own power source, it is easy to implement, really cheap for residential use, and energy efficient with instantaneous alert. For the 3D mouse, the MPU6050 would use both the accelerometer and gyroscope to sense user hands movement, the data are processed by MSP430G2553 through a digital smooth filter and a complementary filter, and then the filtered data will pass to the personal computer through the serial COM port. By applying the cursor movement equation in the PC driver, this device can work great as a mouse with acceptable accuracy. Compared to the normal optical mouse we are using, this mouse does not need any working surface, with the use of the smooth and complementary filter, it has certain accuracy for normal use, and it is easy to be extended to a portable mouse as small as a finger ring.