Hardware implementation of an analog neural nonderivative optimizer

Analog neural systems that can automatically find the minimum value of the outputs of unknown analog systems, described by convex functions, are studied. When information about derivative or gradient are not used, these systems are called analog nonderivative optimizers. An electronic circuit for the analog neural nonderivative optimizer proposed by Teixeira and Zak, and its simulation with software PSPICE, is presented. With the simulation results and hardware implementation of the system, the validity of the proposed optimizer can be verified. These results are original, from the best of the authors knowledge.

Esquemas alternativos para o passo de parametrização do método da continuação baseados em parâmetros físicos

O método de fluxo de carga convencional é considerado inadequado para se obter o ponto de máximo carregamento (PMC) de sistemas de potência, devido à singularidade da matriz Jacobiana neste ponto. Os métodos da continuação são ferramentas eficientes para a solução deste tipo de problema, visto que técnicas de parametrização podem ser utilizadas para evitar a singularidade da matriz Jacobiana. Neste trabalho, novas opções para a etapa de parametrização do método da continuação são apresentadas. Mostra-se que variáveis com claro significado físico podem ser utilizadas na etapa de parametrização. As seguintes variáveis foram testadas: perda total de potência ativa e reativa, potência ativa e reativa na barra de referência, potência reativa das barras de geração, e as perdas de potência ativa e reativa nas linhas de transmissão (LT). Além de facilitar a implementação computacional do método de continuação, as técnicas de parametrização apresentadas simplificam a definição matemática e o entendimento do método por parte de engenheiros de potência, visto que os métodos de continuação existentes na literatura sempre utilizam técnicas de parametrização complexas, e de interpretação puramente geométrica. Resultados obtidos com a nova metodologia para os sistemas testes do IEEE (14, 30, 57 e 118 barras) mostram que as características de convergência do método de fluxo de carga convencional são melhoradas na região do PMC. Além disso, durante o traçado das curvas PV, as diversas técnicas de parametrização podem ser comutadas entre si possibilitando o cálculo de todos os pontos da curva com um número reduzido de iterações. Diversos testes são realizados para proporcionar a comparação do desempenho dos esquemas de parametrização propostos.

Determinação do ponto de máximo carregamento de sistemas de potência utilizando o fluxo de carga desacoplado rápido parametrizado

Os métodos de fluxo de carga por Newton-Raphson e fluxo de carga desacoplado rápido convencionais são considerados inadequados para a obtenção do ponto de máximo carregamento de sistemas de potência, devido à problemas de mal-condicionamento neste ponto crítico e na sua vizinhança. Neste ponto a matriz Jacobiana do método de Newton-Raphson torna-se singular e considera-se que não são mais válidas as hipóteses de desacoplamento P-V e Q-teta utilizadas para a formulação do método fluxo de carga desacoplado rápido. No entanto, mostra-se neste trabalho, que com pequenas modificações, as versões XB e BX do fluxo de carga desacoplado rápido tornam-se adequadas para a obtenção do ponto de máximo carregamento. Estas novas versões modificadas são comparadas entre si com o intuito de explicitar suas características, assim como da influência da atuação dos limites de geração de potência reativa e de tap's de transformadores. Os resultados obtidos para os sistemas testes do IEEE (14, 30, 57 e 118 barras) mostram que as características de convergência das versões originais são preservadas. Além disso, durante o traçado das curvas PV, os diversos métodos podem ser comutados entre si possibilitando o cálculo de todos os pontos da curva com um número reduzido de iterações.

O desempenho terminológico dos descritores em Ciência da Informação do Vocabulário Controlado do SIBi/USP nos processos de indexação manual, automática e semi-automática

The terminological performance of the descriptors representing the Information Science domain in the SIBI/USP Controlled Vocabulary was evaluated in manual, automatic and semi-automatic indexing processes. It can be concluded that, in order to have a better performance (i.e., to adequately represent the content of the corpus), current Information Science descriptors of the SIBi/USP Controlled Vocabulary must be extended and put into context by means of terminological definitions so that information needs of users are fulfilled.

Melhorando a estimação de pose com o RANSAC preemptivo generalizado e múltiplos geradores de hipóteses

The camera motion estimation represents one of the fundamental problems in Computer Vision and it may be solved by several methods. Preemptive RANSAC is one of them, which in spite of its robustness and speed possesses a lack of flexibility related to the requirements of applications and hardware platforms using it. In this work, we propose an improvement to the structure of Preemptive RANSAC in order to overcome such limitations and make it feasible to execute on devices with heterogeneous resources (specially low budget systems) under tighter time and accuracy constraints. We derived a function called BRUMA from Preemptive RANSAC, which is able to generalize several preemption schemes, allowing previously fixed parameters (block size and elimination factor) to be changed according the applications constraints. We also propose the Generalized Preemptive RANSAC method, which allows to determine the maximum number of hipotheses an algorithm may generate. The experiments performed show the superiority of our method in the expected scenarios. Moreover, additional experiments show that the multimethod hypotheses generation achieved more robust results related to the variability in the set of evaluated motion directions

Implementação Hardware/Software da estimação de movimento segundo o padrão H.264

Motion estimation is the main responsible for data reduction in digital video encoding. It is also the most computational damanding step. H.264 is the newest standard for video compression and was planned to double the compression ratio achievied by previous standards. It was developed by the ITU-T Video Coding Experts Group (VCEG) together with the ISO/IEC Moving Picture Experts Group (MPEG) as the product of a partnership effort known as the Joint Video Team (JVT). H.264 presents novelties that improve the motion estimation efficiency, such as the adoption of variable block-size, quarter pixel precision and multiple reference frames. This work defines an architecture for motion estimation in hardware/software, using a full search algorithm, variable block-size and mode decision. This work consider the use of reconfigurable devices, soft-processors and development tools for embedded systems such as Quartus II, SOPC Builder, Nios II and ModelSim

Prova automática de satisfatibilidade módulo teoria aplicada ao método B

Este trabalho apresenta uma extensão do provador haRVey destinada à verificação de obrigações de prova originadas de acordo com o método B. O método B de desenvolvimento de software abrange as fases de especificação, projeto e implementação do ciclo de vida do software. No contexto da verificação, destacam-se as ferramentas de prova Prioni, Z/EVES e Atelier-B/Click n Prove. Elas descrevem formalismos com suporte à checagem satisfatibilidade de fórmulas da teoria axiomática dos conjuntos, ou seja, podem ser aplicadas ao método B. A checagem de SMT consiste na checagem de satisfatibilidade de fórmulas da lógica de primeira-ordem livre de quantificadores dada uma teoria decidível. A abordagem de checagem de SMT implementada pelo provador automático de teoremas haRVey é apresentada, adotando-se a teoria dos vetores que não permite expressar todas as construções necessárias às especificações baseadas em conjuntos. Assim, para estender a checagem de SMT para teorias dos conjuntos destacam-se as teorias dos conjuntos de Zermelo-Frankel (ZFC) e de von Neumann-Bernays-Gödel (NBG). Tendo em vista que a abordagem de checagem de SMT implementada no haRVey requer uma teoria finita e pode ser estendida para as teorias nãodecidíveis, a teoria NBG apresenta-se como uma opção adequada para a expansão da capacidade dedutiva do haRVey à teoria dos conjuntos. Assim, através do mapeamento dos operadores de conjunto fornecidos pela linguagem B a classes da teoria NBG, obtem-se uma abordagem alternativa para a checagem de SMT aplicada ao método B

CrossMDA-SPL: uma abordagem para gerência de variabilidades dirigida por modelos e aspectos

This paper proposes a systematic approach to management of variability modelsdriven and aspects using the mechanisms of approaches Aspect-Oriented Software Development (AOSD) and Model-Driven Development (MDD). The main goal of the approach, named CrossMDA-SPL, is to improve the management(gerência), modularization and isolation ou separation of the variability of the LPSs of architecture in a high level of abstraction (model) at the design and implementing phases of development Software Product Lines (SPLs), exploiting the synergy between AOSD and MDD. The CrossMDA-SPL approach defines some artifacts basis for advance the separation clear in between the mandatory (bounden) and optional features in the architecture of SPL. The artifacts are represented by two models named: (i) core model (base domain) - responsible for specify the common features the all members of the SPL, and (ii) variability model - responsible for represent the variables features of SPL. In addition, the CrossMDA-SPL approach is composed of: (i) guidelines for modeling and representation of variability, (ii) CrossMDA-SPL services and process, and (iii) models of the architecture of SPL or product instance of SPL. The guidelines use the advantages of AOSD and MDD to promote a better modularization of the variable features of the architecture of SPL during the creation of core and variability models of the approach. The services and sub-processes are responsible for combination automatically, through of process of transformation between the core and variability models, and the generation of new models that represent the implementation of the architecture of SPL or a instance model of SPL. Mechanisms for effective modularization of variability for architectures of SPL at model level. The concepts are described and measured with the execution of a case study of an SPL for management systems of transport electronic tickets

Geração de casos de teste a partir de especificações B

With the increasing complexity of software systems, there is also an increased concern about its faults. These faults can cause financial losses and even loss of life. Therefore, we propose in this paper the minimization of faults in software by using formally specified tests. The combination of testing and formal specifications is gaining strength in searches mainly through the MBT (Model-Based Testing). The development of software from formal specifications, when the whole process of refinement is done rigorously, ensures that what is specified in the application will be implemented. Thus, the implementation generated from these specifications would accurately depict what was specified. But not always the specification is refined to the level of implementation and code generation, and in these cases the tests generated from the specification tend to find fault. Additionally, the generation of so-called "invalid tests", ie tests that exercise the application scenarios that were not addressed in the specification, complements more significantly the formal development process. Therefore, this paper proposes a method for generating tests from B formal specifications. This method was structured in pseudo-code. The method is based on the systematization of the techniques of black box testing of boundary value analysis, equivalence partitioning, as well as the technique of orthogonal pairs. The method was applied to a B specification and B test machines that generate test cases independent of implementation language were generated. Aiming to validate the method, test cases were transformed manually in JUnit test cases and the application, created from the B specification and developed in Java, was tested. Faults were found with the execution of the JUnit test cases

Beta: uma ferramenta para geração de testes de unidade a partir de especificações B

Formal methods and software testing are tools to obtain and control software quality. When used together, they provide mechanisms for software specification, verification and error detection. Even though formal methods allow software to be mathematically verified, they are not enough to assure that a system is free of faults, thus, software testing techniques are necessary to complement the process of verification and validation of a system. Model Based Testing techniques allow tests to be generated from other software artifacts such as specifications and abstract models. Using formal specifications as basis for test creation, we can generate better quality tests, because these specifications are usually precise and free of ambiguity. Fernanda Souza (2009) proposed a method to define test cases from B Method specifications. This method used information from the machine s invariant and the operation s precondition to define positive and negative test cases for an operation, using equivalent class partitioning and boundary value analysis based techniques. However, the method proposed in 2009 was not automated and had conceptual deficiencies like, for instance, it did not fit in a well defined coverage criteria classification. We started our work with a case study that applied the method in an example of B specification from the industry. Based in this case study we ve obtained subsidies to improve it. In our work we evolved the proposed method, rewriting it and adding characteristics to make it compatible with a test classification used by the community. We also improved the method to support specifications structured in different components, to use information from the operation s behavior on the test case generation process and to use new coverage criterias. Besides, we have implemented a tool to automate the method and we have submitted it to more complex case studies

Geração procedural de cenários orientada a objetivos

The game industry has been experiencing a consistent increase in production costs of games lately. Part of this increase refers to the current trend of having bigger, more interactive and replayable environments. This trend translates to an increase in both team size and development time, which makes game development a even more risky investment and may reduce innovation in the area. As a possible solution to this problem, the scientific community is focusing on the generation of procedural content and, more specifically, on procedurally generated levels. Given the great diversity and complexity of games, most works choose to deal with a specific genre, platform games being one of the most studied. This work aims at proposing a procedural level generation method for platform/adventure games, a fairly more complex genre than most classic platformers which so far has not been the subject of study from other works. The level generation process was divided in two steps, planning and viusal generation, respectively responsible for generating a compact representation of the level and determining its view. The planning stage was divided in game design and level design, and uses a goaloriented process to output a set of rooms. The visual generation step receives a set of rooms and fills its interior with the appropriate parts of previously authored geometry

Utilizando programação orientada a aspectos no projeto de sistemas hardware desenvolvidos com SystemC

New programming language paradigms have commonly been tested and eventually incorporated into hardware description languages. Recently, aspect-oriented programming (AOP) has shown successful in improving the modularity of object-oriented and structured languages such Java, C++ and C. Thus, one can expect that, using AOP, one can improve the understanding of the hardware systems under design, as well as make its components more reusable and easier to maintain. We apply AOP in applications developed using the SystemC library. Several examples will be presented illustrating how to combine AOP and SystemC. During the presentation of these examples, the benefits of this new approach will also be discussed

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

Instanciação e avaliação de um framework para a geração dinâmica de processos

One way to deal with the high complexity of current software systems is through selfadaptive systems. Self-adaptive system must be able to monitor themselves and their environment, analyzing the monitored data to determine the need for adaptation, decide how the adaptation will be performed, and finally, make the necessary adjustments. One way to perform the adaptation of a system is generating, at runtime, the process that will perform the adaptation. One advantage of this approach is the possibility to take into account features that can only be evaluated at runtime, such as the emergence of new components that allow new architectural arrangements which were not foreseen at design time. In this work we have as main objective the use of a framework for dynamic generation of processes to generate architectural adaptation plans on OSGi environment. Our main interest is evaluate how this framework for dynamic generation of processes behave in new environments

Geração de processos WS-BPEL com base em um algoritmo de reescrita de regras

Web services are computational solutions designed according to the principles of Service Oriented Computing. Web services can be built upon pre-existing services available on the Internet by using composition languages. We propose a method to generate WS-BPEL processes from abstract specifications provided with high-level control-flow information. The proposed method allows the composition designer to concentrate on high-level specifi- cations, in order to increase productivity and generate specifications that are independent of specific web services. We consider service orchestrations, that is compositions where a central process coordinates all the operations of the application. The process of generating compositions is based on a rule rewriting algorithm, which has been extended to support basic control-flow information.We created a prototype of the extended refinement method and performed experiments over simple case studies