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

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

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.

O discurso de outrem em retextualizações

This work investigates features that speakers use to introduce different voices during retextualization of a literary work. It presents events revealing different resources used, characterizing the discursive heterogeneity, recognized through various brands such as quotation marks, italics, etc. The material analyzed, ie, the corpus of this research, consists of 65 essays from the reading of a literary work - Jealous of Card, Moacyr Scliar - produced by students of the 8th year of high school while in the classroom. The data revealed that the resource most used by students was the indirect discourse, although there also occurred the use of other resources such as free indirect discourse and modalizations in fewer redactions. Notably, the autonym connotation was noted through the use of quotation marks, and the use of parentheses. The recurrence of the parentheses seem to be justified by the need to make clearer sentences that could raise questions to the reader, since the protocol request retextualization established a thirty lines of text, which would certainly limit the possibilities of expansion of the text

A documentação odontológica sob a ótica dos cirurgiões-dentistas de Natal-RN

The dental documentation or handbook is a collection of documents produced by the professional with diagnostic and therapeutical purpose where the inherent information to the buccal and general health of patients are registered. The register and proper filling of these documents, taking care of the ethical and legal requirements, provide to the dentist the possibility to contribute with justice in cases of human identification and makes of these documents an essential element of evidence in the ethical processes, administrative, civil and criminal against the dentists. Ahead of this fact, understanding such requirements and the importance of the dentist to register himself adequately, this research verified the knowledge of Natal (RN) City s dentists with relation to the elaboration of the dental handbook, investigating the concepts and the importance attributed to the handbook, identifying the documents more used and filed by these professionals, besides inquiring the legal value of filed documents and the filling time of these ones. The sample was constituted by 124 dentists, who had answered a questionnaire, after having been randomly selected ITom a list of professionals subscribed in the Dentistry Local Council/RN Section. The analysis of the results showed that majority of the participant citÍzens (52,3%) confers to the dental documentation the clinical importance, followed by the legal and forensic-dentistry importance; 59,3% of the searched professionals do not distinguish satisfactorily or they do not observe differences between the dental handbook and the clinical filing card, the X-rays, the dental certificates, the prescriptions, the directions and the receipts; between the documents of common use to clínical and specialist ones, the contract of rendering of services and term of ITee and cleared up consent are the documents less used by the professionals. It was still verified, that only 13,1% of the sample register the signature of the patients in the clinical filing card, making it more credibility to be presented in judgement. In the same way, copies of dental certificates and prescriptions evaluated and signed by the patients are filed respectively by only 13,5% and 9,4% ofthe searched professionals and 50% ofthe sample, keep these documents filed for an indeterminate period of time, that is, these professionals have the guard of the handbook and they do not intend to disdain it, although 85,5% of the sample does not recognize the real proprietor of the handbook. It is concluded that a great part of the dentists is unaware about the importance of the dental documentation, and neglect its elaboration, leaving themselves exposed to several kinds of penalties foreseen in the legislation