Waveshapes of continuing currents and properties of M-components in natural positive cloud-to-ground lightning

This work analyses the waveshapes of continuing currents and parameters of M-components in positive cloud-to-ground (CG) flashes through high-speed GPS synchronized videos. The dataset is composed of only long continuing currents (with duration longer than 40 ms) and was selected from more than 800 flashes recorded in Sao Jose dos Campos (45.864 degrees W, 23.215 degrees S) and Uruguaiana (29.806 degrees W, 57.005 degrees S) in Southeast and South of Brazil, respectively, during 2003 to 2007 summers. The videos are compared with data obtained by the Brazilian Lightning Location System (BrasilDAT) in order to determine the polarity of each flash and select only positive cases. There are only two studies of waveshapes of continuing currents in the literature. One is based on direct current measurements of triggered lightning, in which four different types of waveshapes were observed; and the other is based on measurements of luminosity variations in high-speed videos of CG negative lightning, in which besides the four types above mentioned two additional types were observed. The present work is an extension of the latter, using the same method but now applied to obtain the waveshapes of positive CG lightning. As far as the authors know, this is the first report on M-components in positive continuing currents. We also have used the luminosity-versus-time graphs to observe their occurrence and measure some parameters (duration, elapsed time and time between two successive M-components), whose statistics are presented and compared in detail to the data for negative flashes. We have plotted a histogram of the M-components elapsed time over the total duration of the continuing current for positive flashes, which presented an exponential decay (correlation coefficient: 0.83), similar to what has been observed for negative flashes. (C) 2008 Elsevier B.V. All rights reserved.

A metallurgical study of aluminium alloys used as aircraft components

The effects of heat treatment on morphologies and microstructures of Al 2024 and Al 7050 alloys, used as aircraft components, were studied by metallographic techniques. Light microscopy (LM) and quantitative image analysis were used to characterize the precipitate dispersion and morphology for these alloys. The application of the scanning electron microscopy (SEM) and energy dispersive spectroscopy (EDS) combined techniques for studying these multiphase systems makes it possible to distinguish and quantify the different phases in the surface structure. Xray diffraction also permitted a qualitative comparison of the structures before and after heat treatments.

Simulation Tools for Power Electronics Courses Based on Java Technologies

Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq)

Java applets para um software educacional distribuído em eletrônica de potência

Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq)

Ensino e orientação para projeto de conversores CC-CC através de aplicativos em java

Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq)

Desenvolvimento formal de aplicações para smartcards

Smart card applications represent a growing market. Usually this kind of application manipulate and store critical information that requires some level of security, such as financial or confidential information. The quality and trustworthiness of smart card software can be improved through a rigorous development process that embraces formal techniques of software engineering. In this work we propose the BSmart method, a specialization of the B formal method dedicated to the development of smart card Java Card applications. The method describes how a Java Card application can be generated from a B refinement process of its formal abstract specification. The development is supported by a set of tools, which automates the generation of some required refinements and the translation to Java Card client (host) and server (applet) applications. With respect to verification, the method development process was formalized and verified in the B method, using the Atelier B tool [Cle12a]. We emphasize that the Java Card application is translated from the last stage of refinement, named implementation. This translation process was specified in ASF+SDF [BKV08], describing the grammar of both languages (SDF) and the code transformations through rewrite rules (ASF). This specification was an important support during the translator development and contributes to the tool documentation. We also emphasize the KitSmart library [Dut06, San12], an essential component of BSmart, containing models of all 93 classes/interfaces of Java Card API 2:2:2, of Java/Java Card data types and machines that can be useful for the specifier, but are not part of the standard Java Card library. In other to validate the method, its tool support and the KitSmart, we developed an electronic passport application following the BSmart method. We believe that the results reached in this work contribute to Java Card development, allowing the generation of complete (client and server components), and less subject to errors, Java Card applications.

JCML - Java Card Modeling Language: Definição e Implementação

Formal methods should be used to specify and verify on-card software in Java Card applications. Furthermore, Java Card programming style requires runtime verification of all input conditions for all on-card methods, where the main goal is to preserve the data in the card. Design by contract, and in particular, the JML language, are an option for this kind of development and verification, as runtime verification is part of the Design by contract method implemented by JML. However, JML and its currently available tools for runtime verification were not designed with Java Card limitations in mind and are not Java Card compliant. In this thesis, we analyze how much of this situation is really intrinsic of Java Card limitations and how much is just a matter of a complete re-design of JML and its tools. We propose the requirements for a new language which is Java Card compliant and indicate the lines on which a compiler for this language should be built. JCML strips from JML non-Java Card aspects such as concurrency and unsupported types. This would not be enough, however, without a great effort in optimization of the verification code generated by its compiler, as this verification code must run on the card. The JCML compiler, although being much more restricted than the one for JML, is able to generate Java Card compliant verification code for some lightweight specifications. As conclusion, we present a Java Card compliant variant of JML, JCML (Java Card Modeling Language), with a preliminary version of its compiler

BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B

Java Card technology allows the development and execution of small applications embedded in smart cards. A Java Card application is composed of an external card client and of an application in the card that implements the services available to the client by means of an Application Programming Interface (API). Usually, these applications manipulate and store important information, such as cash and confidential data of their owners. Thus, it is necessary to adopt rigor on developing a smart card application to improve its quality and trustworthiness. The use of formal methods on the development of these applications is a way to reach these quality requirements. The B method is one of the many formal methods for system specification. The development in B starts with the functional specification of the system, continues with the application of some optional refinements to the specification and, from the last level of refinement, it is possible to generate code for some programming language. The B formalism has a good tool support and its application to Java Card is adequate since the specification and development of APIs is one of the major applications of B. The BSmart method proposed here aims to promote the rigorous development of Java Card applications up to the generation of its code, based on the refinement of its formal specification described in the B notation. This development is supported by the BSmart tool, that is composed of some programs that automate each stage of the method; and by a library of B modules and Java Card classes that model primitive types, essential Java Card API classes and reusable data structures

Avalição de reusabilidade de aplicações web baseadas em frameworks orientados a ações e a componentes: estudo de Caso sobre os Frameworks Apache Struts e JavaServer Faces

Over the years the use of application frameworks designed for the View and Controller layers of MVC architectural pattern adapted to web applications has become very popular. These frameworks are classified into Actions Oriented and Components Oriented , according to the solution strategy adopted by the tools. The choice of such strategy leads the system architecture design to acquire non-functional characteristics caused by the way the framework influences the developer to implement the system. The components reusability is one of those characteristics and plays a very important role for development activities such as system evolution and maintenance. The work of this dissertation consists to analyze of how the reusability could be influenced by the Web frameworks usage. To accomplish this, small academic management applications were developed using the latest versions of Apache Struts and JavaServer Faces frameworks, the main representatives of Java plataform Web frameworks of. For this assessment was used a software quality model that associates internal attributes, which can be measured objectively, to the characteristics in question. These attributes and metrics defined for the model were based on some work related discussed in the document

JFloat: uma biblioteca de ponto flutuante para a linguagem Java com suporte a arredondamento direcionado

This work presents JFLoat, a software implementation of IEEE-754 standard for binary floating point arithmetic. JFloat was built to provide some features not implemented in Java, specifically directed rounding support. That feature is important for Java-XSC, a project developed in this Department. Also, Java programs should have same portability when using floating point operations, mainly because IEEE-754 specifies that programs should have exactly same behavior on every configuration. However, it was noted that programs using Java native floating point types may be machine and operating system dependent. Also, JFloat is a possible solution to that problem

Uma abordagem dirigida por modelos para desenvolvimento de middlewares auto-adaptativos para transmissão de fluxo de dados baseado em restrições de QoS

The use of middleware technology in various types of systems, in order to abstract low-level details related to the distribution of application logic, is increasingly common. Among several systems that can be benefited from using these components, we highlight the distributed systems, where it is necessary to allow communications between software components located on different physical machines. An important issue related to the communication between distributed components is the provision of mechanisms for managing the quality of service. This work presents a metamodel for modeling middlewares based on components in order to provide to an application the abstraction of a communication between components involved in a data stream, regardless their location. Another feature of the metamodel is the possibility of self-adaptation related to the communication mechanism, either by updating the values of its configuration parameters, or by its replacement by another mechanism, in case of the restrictions of quality of service specified are not being guaranteed. In this respect, it is planned the monitoring of the communication state (application of techniques like feedback control loop), analyzing performance metrics related. The paradigm of Model Driven Development was used to generate the implementation of a middleware that will serve as proof of concept of the metamodel, and the configuration and reconfiguration policies related to the dynamic adaptation processes. In this sense was defined the metamodel associated to the process of a communication configuration. The MDD application also corresponds to the definition of the following transformations: the architectural model of the middleware in Java code, and the configuration model to XML

JCircus 2.0: Uma extensão da ferramenta de tradução de Circus para Java

This dissertation aims at extending the JCircus tool, a translator of formal specifications into code that receives a Circus specification as input, and translates the specification into Java code. Circus is a formal language whose syntax is based on Z s and CSP s syntax. JCircus generated code uses JCSP, which is a Java API that implements CSP primitives. As JCSP does not implement all CSP s primitives, the translation strategy from Circus to Java is not trivial. Some CSP primitives, like parallelism, external choice, communication and multi-synchronization are partially implemented. As an aditional scope, this dissertation will also develop a tool for testing JCSP programs, called JCSPUnit, which will also be included in JCircus new version. The extended version of JCircus will be called JCircus 2.0.

Java-XSC : módulo complexo e complexo intervalar

This work aims to develop modules that will increase the computational power of the Java-XSC library, and XSC an acronym for "Language Extensions for Scientific Computation . This library is actually an extension of the Java programming language that has standard functions and routines elementary mathematics useful interval. in this study two modules were added to the library, namely, the modulus of complex numbers and complex numbers of module interval which together with the modules original numerical applications that are designed to allow, for example in the engineering field, can be used in devices running Java programs

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

BTS:uma ferramenta de suporte ao desenvolvimento sistemático de sistemas confiáveis baseados em componentes

The component-based development of systems revolutionized the software development process, facilitating the maintenance, providing more confiability and reuse. Nevertheless, even with all the advantages of the development of components, their composition is an important concern. The verification through informal tests is not enough to achieve a safe composition, because they are not based on formal semantic models with which we are able to describe precisally a system s behaviour. In this context, formal methods provide ways to accurately specify systems through mathematical notations providing, among other benefits, more safety. The formal method CSP enables the specification of concurrent systems and verification of properties intrinsic to them, as well as the refinement among different models. Some approaches apply constraints using CSP, to check the behavior of composition between components, assisting in the verification of those components in advance. Hence, aiming to assist this process, considering that the software market increasingly requires more automation, reducing work and providing agility in business, this work presents a tool that automatizes the verification of composition among components, in which all complexity of formal language is kept hidden from users. Thus, through a simple interface, the tool BST (BRIC-Tool-Suport) helps to create and compose components, predicting, in advance, undesirable behaviors in the system, such as deadlocks