JCML: A specification language for the runtime verification of Java Card programs

COSTA, Umberto Souza; MOREIRA, Anamaria Martins; MUSICANTE, Matin A.; SOUZA NETO, Plácido A. JCML: A specification language for the runtime verification of Java Card programs. Science of Computer Programming. [S.l]: [s.n], 2010.

Specification and Runtime Verification of Java Card Programs

COSTA, Umberto Souza da; MOREIRA, Anamaria Martins; MUSICANTE, Martin A. Specification and Runtime Verification of Java Card Programs. Electronic Notes in Theoretical Computer Science. [S.l:s.n], 2009.

e-Pontos: Uma solução embarcada de automação comercial aplicada a clubes de fidelidade baseado em tecnologia RFID e esmart card

In practically all vertical markets and in every region of the planet, loyalty marketers have adopted the tactic of recognition and reward to identify, maintain and increase the yield of their customers. Several strategies have been adopted by companies, and the most popular among them is the loyalty program, which displays a loyalty club to manage these rewards. But the problem with loyalty programs is that customer identification and transfer of loyalty points are made in a semiautomatic. Aiming at this, this paper presents a master's embedded business automation solution called e-Points. The goal of e-Points is munir clubs allegiances with fully automated tooling technology to identify customers directly at the point of sales, ensuring greater control over the loyalty of associate members. For this, we developed a hardware platform with embedded system and RFID technology to be used in PCs tenant, a smart card to accumulate points with every purchase and a web server, which will provide services of interest to retailers and customers membership to the club

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

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

JCML: A specification language for the runtime verification of Java Card programs

COSTA, Umberto Souza; MOREIRA, Anamaria Martins; MUSICANTE, Matin A.; SOUZA NETO, Plácido A. JCML: A specification language for the runtime verification of Java Card programs. Science of Computer Programming. [S.l]: [s.n], 2010.

Specification and Runtime Verification of Java Card Programs

COSTA, Umberto Souza da; MOREIRA, Anamaria Martins; MUSICANTE, Martin A. Specification and Runtime Verification of Java Card Programs. Electronic Notes in Theoretical Computer Science. [S.l:s.n], 2009.

Desenvolvimento de um sistema Inteligente para a análise de cartas dinamométricas no método de elevação por bombeio mecânico

The artificial lifting of oil is needed when the pressure of the reservoir is not high enough so that the fluid contained in it can reach the surface spontaneously. Thus the increase in energy supplies artificial or additional fluid integral to the well to come to the surface. The rod pump is the artificial lift method most used in the world and the dynamometer card (surface and down-hole) is the best tool for the analysis of a well equipped with such method. A computational method using Artificial Neural Networks MLP was and developed using pre-established patterns, based on its geometry, the downhole card are used for training the network and then the network provides the knowledge for classification of new cards, allows the fails diagnose in the system and operation conditions of the lifting system. These routines could be integrated to a supervisory system that collects the cards to be analyzed

Comparação da análise de diferentes perfis de poços pelo método DFA

The study of complex systems has become a prestigious area of science, although relatively young . Its importance was demonstrated by the diversity of applications that several studies have already provided to various fields such as biology , economics and Climatology . In physics , the approach of complex systems is creating paradigms that influence markedly the new methods , bringing to Statistical Physics problems macroscopic level no longer restricted to classical studies such as those of thermodynamics . The present work aims to make a comparison and verification of statistical data on clusters of profiles Sonic ( DT ) , Gamma Ray ( GR ) , induction ( ILD ) , neutron ( NPHI ) and density ( RHOB ) to be physical measured quantities during exploratory drilling of fundamental importance to locate , identify and characterize oil reservoirs . Software were used : Statistica , Matlab R2006a , Origin 6.1 and Fortran for comparison and verification of the data profiles of oil wells ceded the field Namorado School by ANP ( National Petroleum Agency ) . It was possible to demonstrate the importance of the DFA method and that it proved quite satisfactory in that work, coming to the conclusion that the data H ( Hurst exponent ) produce spatial data with greater congestion . Therefore , we find that it is possible to find spatial pattern using the Hurst coefficient . The profiles of 56 wells have confirmed the existence of spatial patterns of Hurst exponents , ie parameter B. The profile does not directly assessed catalogs verification of geological lithology , but reveals a non-random spatial distribution

Perfil de imunoglobulinas e correlação de autoanticorpos com a ocorrência de diversas formas clínicas em pacientes chagásicos crônicos

Introdução: O dano miocárdico na doença de Chagas resulta tanto da ação parasitária quanto da resposta imune do hospedeiro humano. O mimetismo molecular entre proteínas do Trypanosoma cruzi e vários antígenos do hospedeiro tem sido amplamente descrito gerando células T CD8+ e anticorpos autorreativos. Entretanto, a geração dos autoanticorpos e seu papel na imunopatogenia da doença de Chagas ainda não têm sido elucidados, o que nos levou, neste trabalho, a avaliar a produção de imunoglobulina G total (IgGt) e seus isotipos anti-T. cruzi, proteínas cardíacas e sua possível associação com as diferentes formas clínicas da doença de Chagas. Métodos: A produção de IgGt e isotipos foi mensurada pelo método de ELISA no soro de pacientes com as formas clínicas indeterminada (IND, n=72), cardíaca (CARD, n=47) e digestiva/cardio-digestiva (DIG/CARD-DIG, n=12) da doença de Chagas, usando como antígenos as formas epimastigota e tripomastigota do T. cruzi e proteínas cardíacas humana (miosina e troponina T). As amostras de indivíduos não infectados saudáveis (CONT, n= 30) e pacientes com cardiomiopatia isquêmica (ISCH, n=15) foram usadas como controle. Os títulos de autoanticorpos foram correlacionados com parâmetros da função cardíaca obtidos por exames eletrocardiográficos, radiográficos e ecocardiográficos. Resultados: Neste estudo foram incluídos 131 indivíduos sem diferença significativa relativa à idade ou sexo. Destes, 55% foram classificados como IND, 35,9% CARD e 9,1% DIG/CARD-DIG. Os títulos de IgGt foram mais elevados em pacientes com as formas clínicas IND, CARD e DIG/CARD-DIG do que em indivíduos CONT e ISCH usando os antígenos as formas tripomastigotas e epimastigotas do T. cruzi e, proteínas cardíacas humanas. Os pacientes com formas clínicas CARD e DIG/CARD-DIG mostraram a produção mais elevada de IgG total dirigida contra antígenos de tripomastigota e epimastigota do que os IND. Os grupos de pacientes IND e CARD apresentaram uma similar produção de IgG total específica direcionada à miosina e troponina T, e mais elevada do que em indivíduos CONT e ISCH. Há uma correlação negativa entre a produção de anticorpos anti-proteínas cardíacas com a fração de ejeção do ventrículo esquerdo (FEVE) em pacientes chagásicos crônicos. Os pacientes foram agrupados em baixo e alto produtores de autoanticorpos e comparados com a fração de ejeção demonstrando que em pacientes alto produtores de anti-troponina T (p=0.042) e miosina (p=0.013) a FEVE foi mais baixa do que os baixo produtores. A maioria dos pacientes chagásicos produz simultaneamente autoanticorpos direcionados à ambas proteínas cardíacas (r=0.9508, p=0.0001). Conclusões: Estes resultados indicam que os autoanticorpos anti- troponina T e miosina cardíaca parecem induzir redução FEVE e deve ser associado com o desenvolvimento de cardiomiopatia chagásica

Análise de qualidade da atenção à criança na estratégia saúde da família: o óbito infantil evitável como referência

Alma-Ata declaration bring the Primary Attention to the Health (PAH) as first level of health attention for individuals, family and community, which considers infant group as priority. Several initiatives that gave bases to integral attention to the children health formalized in the principles of Unique Health System. Family Health Strategy (FHS) comes to strengthen this attention, instituting new ways of work organization and professional practices that gave impact in their quality indicators. One of them is children mortality, showing decline in their values. Though, studies indicates persistence of avoidable infant deaths. In Natal RN, this reality is also perceptible leading to inquietudes, mainly at the space of services production, it means, which motivated the accomplishment of the present study intending to analyse the way that the organizational and structural processes as long as the professional practices in FHS interfered in the quality of children s health attention who died by avoidable death in the year of 2007 in municipal district of Natal-RN. It treats, therefore, to an exploratory and descriptive survey of cases study type, thar had as primary sources the oficial documents of MH, the family prontuary, pregnant card, child card and testimony obt ined from instrument of research elaborated based in investigation form of infant death by MH, applied to 10 mothers of children who had avoidable death. In analysis it was appealed silmultaneous triangulation of methods and sources, allowing a bigger aproximation from obtained informations. To elucidate the cases, the aspects studied were analyzed to the light of explicative model of Social Determinants of Health. Among individual and family aspects were highlighted the related to age, schooling, family habits and customs and mother s economic condition, besides of pregnancy age, newborn weight and associated diseases, which don t differ from literature about the theme. Reffering to the factors organizational and structural processes and professionals practice, highlihgted, the treatment given by the professionals, the territorialization and adscription of areas, the difficulty of having access to the services or sleepers and the reference and counterreference. But also, the ausence or few greet, the lack of communication, few assiduity and ponctuality by professionals in service, among others. In a general way mothers considers the attendance received in the hospital good and very good , opnions that in the Basic Attention weren t so favorable, in spite of many of predictible actions in this level have been performed in the studied cases. It is observed, therefore, that the social determinants of health has a strong influence in ocurrence of infant deaths, what implicates in a large actuation by Infant Mortality Committee from municipal district. This way, it becomes fundamental the reflection and evaluation about the effectiveness and execution by the processes of vigilance to health in FHUs; the rethink about the social determinants of health in a wide and articulate way to the services quality, to permanent education, to management in service, to the given attention and to the way how it is installed the popular participation and social control. To the professionals it is presented the great challenge to review their daily practice, their values, behaviors and commitment, which ones must be guided by logical of sharing, work in team, humanescence and alterity, not only by the accomplishment of a professional duty

Uma contribuição crítica para o redesenho de cadeiras de rodas adaptadas para crianças e adolescentes com paralisia cerebral

This work was aimed at making a critical analysis of the product wheelchair, both for using four different models, which were objects of study of the dissertation of Cláudia Regina Cabral Galvão, entitled Critical Analysis of the Mobility Products Seated a wheelchair - Used by Children and Adolescents with Cerebral Palsy in Natal / RN and other municipalities of Rio Grande do Norte . This product is considered an instrument in the social rehabilitation of great importance for people with physical disabilities. This study aims to position the issue and develop comments on technical up grading of certain models according to the needs of the user. Describes features of four models in search searched through catalogs in order to know its advantages and disadvantages of use. Were presented the definitions of ergonomics and ergonomic aspects to be considered on a design, the study of anthropometry and its recommendations. Discussions the methodology of project design in two parts: the first, on the structuring of design problem (formulation, analysis, synthesis and evaluation.) And the second on the project (design and development, implementation and evaluation and solution). With that review will include the possibilities for a new redesign of the wheelchair, based on forms of adaptation in order to achieve the target that was compressed by the average population studied. Seeks to that this project makes an improvement in quality of life of people in wheelchairs by including these people in society but also the improvement of rehabilitation

Detecção e classificação de modos de operação do bombeio mecânico via cartas dinamométricas

The precision and the fast identification of abnormalities of bottom hole are essential to prevent damage and increase production in the oil industry. This work presents a study about a new automatic approach to the detection and the classification of operation mode in the Sucker-rod Pumping through dynamometric cards of bottom hole. The main idea is the recognition of the well production status through the image processing of the bottom s hole dynamometric card (Boundary Descriptors) and statistics and similarity mathematics tools, like Fourier Descriptor, Principal Components Analysis (PCA) and Euclidean Distance. In order to validate the proposal, the Sucker-Rod Pumping system real data are used

Desenvolvimento de um laminado compósito híbrido a base de fibras de vidro/licurí

This research work is based, in search of reinforcement s vegetable alternative to polymer composites. The idealization of making a hybrid composite reinforced with vegetable fibers licuri with synthetic fibers is a pioneer in this area. Thus was conceived a hybrid composite laminate consisting of 05 (five) layers being 03 (three) webs of synthetic fibers of glass and E-02 (two) unidirectional fabrics of vegetable fibers licuri. In the configuration of the laminate layers have alternating distribution. The composite laminate was manufactured in Tecniplas Commerce & Industry LTD, in the form of a card through the manufacturing process of hand lay up. Licuri fibers used in making the foil were the City of Mare Island in the state of Bahia. After cooking and the idealization of the hybrid composite laminate, the objective of this research work has focused on evaluating the performance of the mechanical properties (ultimate strength, stiffness and elongation at break) through uniaxial tensile tests and three point bending. Comparative studies of the mechanical properties and as well as among other types of laminated hybrid composites studied previously, were performed. Promising results were found with respect to the mechanical properties of strength and stiffness to the hybridization process idealized here. To complement the entire study were analyzed in terms of macroscopic and microscopic characteristics of the fracture for all tests.