Proposal of a Transmission Line Model Based on Lumped Elements: An Analytic Solution

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

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

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

Structure of acetone and dimethyl sulfoxide from Monte Carlo simulations and MM2 calculations

The structure of acetone and dimethyl sulfoxide in the liquid phase is investigated using Monte Carlo simulations and MM2 calculations. The principal site - site correlations and degree of structure in both liquids have been investigated. The results showed that dimethyl sulfoxide is more structured than acetone. At short distances the dipoles of neighboring molecules are found to be in antiparallel configurations, but further apart the molecules tend to be aligned predominantly as head to tail. In both liquids there is evidence of strong methyl - oxygen interaction, important to the structure of the liquids. The contacts suggest weak hydrogen bonds between methyl hydrogen and oxygen.

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

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

Joker: um realizador de desenhos animados para linguagens formais

Using formal methods, the developer can increase software s trustiness and correctness. Furthermore, the developer can concentrate in the functional requirements of the software. However, there are many resistance in adopting this software development approach. The main reason is the scarcity of adequate, easy to use, and useful tools. Developers typically write code and test it. These tests usually consist of executing the program and checking its output against its requirements. This, however, is not always an exhaustive discipline. On the other side, using formal methods one might be able to investigate the system s properties further. Unfortunately, specification languages do not always have tools like animators or simulators, and sometimes there are no friendly Graphical User Interfaces. On the other hand, specification languages usually have a compiler which normally generates a Labeled Transition System (LTS). This work proposes an application that provides graphical animation for formal specifications using the LTS as input. The application initially supports the languages B, CSP, and Z. However, using a LTS in a specified XML format, it is possible to animate further languages. Additionally, the tool provides traces visualization, the choices the user did, in a graphical tree. The intention is to improve the comprehension of a specification by providing information about errors and animating it, as the developers do for programming languages, such as Java and C++.

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.

KitSmart: Uma biblioteca de componentes para o desenvolvimento rigoroso de aplicações Java Card com o método B

The development of smart card applications requires a high level of reliability. Formal methods provide means for this reliability to be achieved. The BSmart method and tool contribute to the development of smart card applications with the support of the B method, generating Java Card code from B specifications. For the development with BSmart to be effectively rigorous without overloading the user it is important to have a library of reusable components built in B. The goal of KitSmart is to provide this support. A first research about the composition of this library was a graduation work from Universidade Federal do Rio Grande do Norte, made by Thiago Dutra in 2006. This first version of the kit resulted in a specification of Java Card primitive types byte, short and boolean in B and the creation of reusable components for application development. This work provides an improvement of KitSmart with the addition of API Java Card specification made in B and a guide for the creation of new components. The API Java Card in B, besides being available to be used for development of applications, is also useful as a documentation of each API class. The reusable components correspond to modules to manipulate specific structures, such as date and time. These structures are not available for B or Java Card. These components for Java Card are generated from specifications formally verified in B. The guide contains quick reference on how to specify some structures and how some situations were adapted from object-orientation to the B Method. This work was evaluated through a case study made through the BSmart tool, that makes use of the KitSmart library. In this case study, it is possible to see the contribution of the components in a B specification. This kit should be useful for B method users and Java Card application developers

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

Ultrasound guidance is not necessary during easy embryo transfers

Purpose: To determine whether the use of ultrasound (US) to guide embryo transfer (ET) in a population previously defined as likely to have easy transfer would change the implantation and pregnancy rates in an ICSI program.Methods: A total of 100 patients identified as likely to have easy transfer after mock transfer were divided into two groups: Group I, US-guided ET (N = 50) and Group II, ET without the aid of US (N = 50).Results: Implantation and pregnancy rates were similar (p = 0.51, p = 0.29) for Group I (19.6%,42%) and Group II (16.3%,30%), as also was the abortion rate (p = 0.55) (Group I: 1/21; Group II: 2/15).Conclusion: As long as previous mock transfers are routinely performed during a cycle preceding assisted reproduction and the clinician considers transfer to be easy, ultrasound does not benefit the process of embryo transfer.

Time series analysis for minority game simulations of financial markets

The minority game (MG) model introduced recently provides promising insights into the understanding of the evolution of prices, indices and rates in the financial markets. In this paper we perform a time series analysis of the model employing tools from statistics, dynamical systems theory and stochastic processes. Using benchmark systems and a financial index for comparison, several conclusions are obtained about the generating mechanism for this kind of evolution. The motion is deterministic, driven by occasional random external perturbation. When the interval between two successive perturbations is sufficiently large, one can find low dimensional chaos in this regime. However, the full motion of the MG model is found to be similar to that of the first differences of the SP500 index: stochastic, nonlinear and (unit root) stationary. (C) 2002 Elsevier B.V. B.V. All rights reserved.

NOISE and ULTRAVIOLET DIVERGENCES IN SIMULATIONS of GINZBURG-LANDAU-LANGEVIN TYPE of EQUATIONS

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

SPH simulations of clumps formation by dissipative collisions of molecular clouds - II. Magnetic case

We performed computer simulations of interstellar cloud-cloud collisions using the three-dimensional smoothed particle magnetohydrodynamics method. In order to study the role of the magnetic field on the process of collision-triggered fragmentation, we focused our attention on head-on supersonic collisions between two identical spherical molecular-clouds. Two extreme configurations of the magnetic field were adopted: parallel and perpendicular to the initial clouds motion. The initial magnetic field strength was approximately 12.0 muG. In the parallel case, much more of the collision debris were retained in the shocking region than in the non-magnetic case where gas escaped freely throughout the symmetry plane. Differently from the non-magnetic case, eddy-like vortices were formed. The regions of highest vorticity and the the regions of highest density are offset. We found clumps formation only in the parallel case, however, they were larger, hotter and less dense than in the analogous non-magnetic case. In the perpendicular case, the compressed field works as a magnetic wall, preventing a stronger compression of the colliding clouds. This last effect inhibits direct contact of the two clouds. In both cases, we found that the field lines show a chaotic aspect in large scales. Also, the field magnitude is considerably amplified in the shock layer. However, the field distribution is almost coherent in the higher density regions.

SPH simulations of clumps formation by dissipative collision of molecular clouds - I. Non magnetic case

Computer experiments of interstellar cloud collisions were performed with a new smoothed-particle-hydrodynamics (SPH) code. The SPH quantities were calculated by using spatially adaptive smoothing lengths and the SPH fluid equations of motion were solved by means of a hierarchical multiple time-scale leapfrog. Such a combination of methods allows the code to deal with a large range of hydrodynamic quantities. A careful treatment of gas cooling by H, H(2), CO and H II, as well as a heating mechanism by cosmic rays and by H(2) production on grains surface, were also included in the code. The gas model reproduces approximately the typical environment of dark molecular clouds. The experiments were performed by impinging two dynamically identical spherical clouds onto each other with a relative velocity of 10 km s(-1) but with a different impact parameter for each case. Each object has an initial density profile obeying an r(-1)-law with a cutoff radius of 10 pc and with an initial temperature of 20 K. As a main result, cloud-cloud collision triggers fragmentation but in expense of a large amount of energy dissipated, which occurred in the head-on case only. Off-center collision did not allow remnants to fragment along the considered time (similar to 6 Myr). However, it dissipated a considerable amount of orbital energy. Structures as small as 0.1 pc, with densities of similar to 10(4) cm(-3), were observed in the more energetic collision.