Geração automática de hardware a partir de especificações formais: estendendo uma abordagem de tradução

Removing inconsistencies in a project is a less expensive activity when done in the early steps of design. The use of formal methods improves the understanding of systems. They have various techniques such as formal specification and verification to identify these problems in the initial stages of a project. However, the transformation from a formal specification into a programming language is a non-trivial task and error prone, specially when done manually. The aid of tools at this stage can bring great benefits to the final product to be developed. This paper proposes the extension of a tool whose focus is the automatic translation of specifications written in CSPM into Handel-C. CSP is a formal description language suitable for concurrent systems, and CSPM is the notation used in tools support. Handel-C is a programming language whose result can be compiled directly into FPGA s. Our extension increases the number of CSPM operators accepted by the tool, allowing the user to define local processes, to rename channels in a process and to use Boolean guards on external choices. In addition, we also propose the implementation of a communication protocol that eliminates some restrictions on parallel composition of processes in the translation into Handel-C, allowing communication in a same channel between multiple processes to be mapped in a consistent manner and that improper communication in a channel does not ocurr in the generated code, ie, communications that are not allowed in the system specification

AutoWebS: um Ambiente para Modelagem e Geração Automática de ServiçosWeb Semânticos

Typically Web services contain only syntactic information that describes their interfaces. Due to the lack of semantic descriptions of the Web services, service composition becomes a difficult task. To solve this problem, Web services can exploit the use of ontologies for the semantic definition of service s interface, thus facilitating the automation of discovering, publication, mediation, invocation, and composition of services. However, ontology languages, such as OWL-S, have constructs that are not easy to understand, even for Web developers, and the existing tools that support their use contains many details that make them difficult to manipulate. This paper presents a MDD tool called AutoWebS (Automatic Generation of Semantic Web Services) to develop OWL-S semantic Web services. AutoWebS uses an approach based on UML profiles and model transformations for automatic generation of Web services and their semantic description. AutoWebS offers an environment that provides many features required to model, implement, compile, and deploy semantic Web services

Contribuições para verificação automática de applets javacard

The widespread growth in the use of smart cards (by banks, transport services, and cell phones, etc) has brought an important fact that must be addressed: the need of tools that can be used to verify such cards, so to guarantee the correctness of their software. As the vast majority of cards that are being developed nowadays use the JavaCard technology as they software layer, the use of the Java Modeling Language (JML) to specify their programs appear as a natural solution. JML is a formal language tailored to Java. It has been inspired by methodologies from Larch and Eiffel, and has been widely adopted as the de facto language when dealing with specification of any Java related program. Various tools that make use of JML have already been developed, covering a wide range of functionalities, such as run time and static checking. But the tools existent so far for static checking are not fully automated, and, those that are, do not offer an adequate level of soundness and completeness. Our objective is to contribute to a series of techniques, that can be used to accomplish a fully automated and confident verification of JavaCard applets. In this work we present the first steps to this. With the use of a software platform comprised by Krakatoa, Why and haRVey, we developed a set of techniques to reduce the size of the theory necessary to verify the specifications. Such techniques have yielded very good results, with gains of almost 100% in all tested cases, and has proved as a valuable technique to be used, not only in this, but in most real world problems related to automatic verification

Desenvolvimento de um sistema computacional para geração automática de mapas de vulnerabilidade como ferramenta de auxílio às ações de prevenção ao derramamento de óleo em áreas costeiras

The northern portion of the Rio Grande do Norte State is characterized by intense coastal dynamics affecting areas with ecosystems of moderate to high environmental sensitivity. In this region are installed the main socioeconomic activities of RN State: salt industry, shrimp farm, fruit industry and oil industry. The oil industry suffers the effects of coastal dynamic action promoting problems such as erosion and exposure of wells and pipelines along the shore. Thus came the improvement of such modifications, in search of understanding of the changes which causes environmental impacts with the purpose of detecting and assessing areas with greater vulnerability to variations. Coastal areas under influence oil industry are highly vulnerable and sensitive in case of accidents involving oil spill in the vicinity. Therefore, it was established the geoenvironmental monitoring of the region with the aim of evaluating the entire coastal area evolution and check the sensitivity of the site on the presence of oil. The goal of this work was the implementation of a computer system that combines the needs of insertion and visualization of thematic maps for the generation of Environmental Vulnerability maps, using techniques of Business Intelligence (BI), from vector information previously stored in the database. The fundamental design interest was to implement a more scalable system that meets the diverse fields of study and make the appropriate system for generating online vulnerability maps, automating the methodology so as to facilitate data manipulation and fast results in cases of real time operational decision-making. In database development a geographic area was established the conceptual model of the selected data and Web system was done using the template database PostgreSQL, PostGis spatial extension, Glassfish Web server and the viewer maps Web environment, the GeoServer. To develop a geographic database it was necessary to generate the conceptual model of the selected data and the Web system development was done using the PostgreSQL database system, its spatial extension PostGIS, the web server Glassfish and GeoServer to display maps in Web

Classificação automática de padrões projetados por um sistema de luz estruturada

One of the main problems in Computer Vision and Close Range Digital Photogrammetry is 3D reconstruction. 3D reconstruction with structured light is one of the existing techniques and which still has several problems, one of them the identification or classification of the projected targets. Approaching this problem is the goal of this paper. An area based method called template matching was used for target classification. This method performs detection of area similarity by correlation, which measures the similarity between the reference and search windows, using a suitable correlation function. In this paper the modified cross covariance function was used, which presented the best results. A strategy was developed for adaptative resampling of the patterns, which solved the problem of deformation of the targets due to object surface inclination. Experiments with simulated and real data were performed in order to assess the efficiency of the proposed methodology for target detection. The results showed that the proposed classification strategy works properly, identifying 98% of targets in plane surfaces and 93% in oblique surfaces.

Extração semi-automática de rodovias em um par de imagens aéreas digitais utilizando geometria epipolar e programação dinâmica

The purpose of this paper is to introduce a methodology for semi-automatic road extraction from aerial digital image pairs by using dynamic programming and epipolar geometry. The method uses both images from where each road feature pair is extracted. The operator identifies the corresponding road featuresand s/he selects sparse seed points along them. After all road pairs have been extracted, epipolar geometry is applied to determine the automatic point-to-point correspondence between each correspondent feature. Finally, each correspondent road pair is georeferenced by photogrammetric intersection. Experiments were made with rural aerial images. The results led to the conclusion that the methodology is robust and efficient, even in the presence of shadows of trees and buildings or other irregularities.

Orientação semi-automática de imagens CBERS usando rodovias como controle de campo

In this paper is proposed a methodology for semiautomatic CBERS image orientation using roads as ground control. It is based on an iterative strategy involving three steps. In the first step, an operator identifies on the image the ground control roads and supplies along them a few seed points, which could be sparsely and coarsely distributed. These seed points are used by the dynamic programming algorithm for extracting the ground control roads from the image. In the second step, it is established the correspondences between points describing the ground control roads and the corresponding ones extracted from the image. In the last step, the corresponding points are used to orient the CBERS image by using the DLT (Direct Linear Transformation). The two last steps are iterated until the convergence of the orientation process is verified. Experimental results showed that the proposed methodology was efficient with several test images. In all cases the orientation process converged. Moreover, the estimated orientation parameters allowed the registration of check roads with pixel accuracy or better.

Estudio Económico de América Latina y el Caribe 2008-2009: políticas para la generación de empleo de calidad

Incluye Bibliografía

Generación, difusión y uso del conocimiento científico-tecnológico en Iberoamérica: diagnóstico y potencialidad de la vinculación entre universidades y empresas

Incluye bibliografía

Influencia de la separación de residuos sólidos urbanos para reciclaje en el proceso de incineración con generación de energía

This work analyses the recuperation of the energy of Municipal Solid Waste (MSW) through the incineration process. It considers the up to date tendency of segregation (separation) of plastic, paper and cardboard, glass and metals and their influence in the fluxes of mass and energy in the incineration system of MSW. For its development was used information related to the generation of MSW in Bauru city and the Combust software. The results so obtained allowed the estimation of the Caloric power of the typical MSW and also of this residue when one considers the separations of paper/cardboard and plastic for recycling.

Generación y protección del conocimiento: propiedad intelectual, innovación y desarrollo económico

Incluye Bibliografía

La propiedad intelectual y la nueva generación de acuerdos de libre comercio: el tratado entre Chile y Estados Unidos de Norteamérica

Incluye Bibliografía

El desafío de las TIC en Argentina: crear capacidades para la generación de empleo

Incluye bibliografía

DOCPAL resúmenes sobre población en América Latina: 112-001

Contiene resúmenes bibliográficos de documentos sobre población y temas relacionados que se producen en América Latina y el Caribe, publicados entre 1984-1987.