Made available in DSpace on 2014-12-17T15:47:44Z (GMT). No. of bitstreams: 1 BrunoEGG.pdf: 1320681 bytes, checksum: 897ca75ef7f0e564e8588d949fcc67d5 (MD5) Previous issue date: 2007-11-19 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / 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 / A tecnologia Java Card permite o desenvolvimento e execu??o de pequenas aplica??es embutidas em smart cards. Uma aplica??o Java Card ? composta por um cliente, externo ao cart?o, e por uma aplica??o contida no cart?o que implementa os servi?os dispon?veis ao cliente por meio de uma Application Programming Interface (API). Usualmente, essas aplica??es manipulam e armazenam informa??es importantes, tais como valores monet?rios ou dados confidenciais do seu portador. Sendo assim, faz-se necess?rio adotar um maior rigor no processo de desenvolvimento de uma aplica??o smart card, visando melhorar a sua qualidade e confiabilidade. O emprego de m?todos formais como parte desse processo ? um meio de se alcan?ar esses requisitos de qualidade. O m?todo formal B ?e um dentre os diversos m?todos formais para a especifica??o de sistemas. O desenvolvimento em B tem in?cio com a especifica??o funcional do sistema, continua com a aplica??o opcional de refinamentos ? especifica??o e, a partir do ?ltimo n?vel de refinamento, ? poss?vel a gera??o de c?digo para alguma linguagem de programa??o. O formalismo B conta com bom suporte de ferramentas e a sua aplica??o a Java Card mostra-se bastante adequada, uma vez que a especifica??o e desenvolvimento de APIs ?e o ponto forte de B. O m?todo BSmart aqui proposto visa promover o desenvolvimento rigoroso de aplica??es Java Card a partir da gera??o de c?digo da aplica??o com base em refinamentos da sua especifica??o formal descrita na nota??o B. O processo de desenvolvimento descrito no m?todo ? apoiado pela ferramenta BSmart, a qual constitui-se por alguns programas que automatizam cada etapa do m?todo; e por uma biblioteca de m?dulos B e classes Java Card que modelam tipos primitivos, classes essenciais da API Java Card e estruturas de dados reutiliz?veis

Made available in DSpace on 2014-12-17T15:48:00Z (GMT). No. of bitstreams: 1 SimoneOS_DISSERT_capa_ate_pag44.pdf: 4276014 bytes, checksum: c178262769ab9981c0bbfc10faf1c633 (MD5) Previous issue date: 2012-02-10 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / 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 / O desenvolvimento de aplica??es para smart cards requer um alto grau de confiabilidade. M?todos formais fornecem meios para que esta confiabilidade seja alcan?ada. O m?todo e a ferramenta BSmart fornecem uma contribui??o para que o desenvolvimento para smart cards seja feito com o aux?lio do m?todo formal B, gerando c?digo Java Card a partir de especifica??es B. Para que o desenvolvimento com o BSmart seja efetivamente rigoroso sem sobrecarregar o usu?rio do m?todo ? importante que haja uma biblioteca de componentes reutiliz?veis feitos em B. O KitSmart tem como objetivo prover esse aux?lio. Um primeiro estudo sobre a composi??o dessa biblioteca foi tema de uma monografia de gradua??o do curso de Bacharelado em Ci?ncia da Computa??o da Universidade Federal do Rio Grande do Norte, feita por Thiago Dutra em 2006. Esta primeira vers?o do kit resultou na especifica??o dos tipos primitivos permitidos em Java Card (byte, short e boolean) em B e a cria??o de componentes reutiliz?veis para o desenvolvimento de aplica??es. Esta disserta??o prov? o aperfei?oamento do KitSmart com o acr?scimo da especifica??o da API Java Card em B, e um guia para o desenvolvimento de novos componentes. A API Java Card especificada em B, al?m de estar dispon?vel para ser usada no desenvolvimento de projetos, serve como documenta??o ao especificar restri??es de uso para cada classe da API. Os componentes reutiliz?veis correspondem a m?dulos para manipula??o de estruturas espec?ficas, como data e hora, por exemplo. Estes tipos de estruturas n?o est?o dispon?veis em B ou Java Card. Os componentes reutiliz?veis para Java Card s?o gerados a partir das especifica??es verificadas formalmente em B. O guia cont?m informa??es de consulta r?pida para especifica??o de diversas estruturas e como algumas situa??es foram contornadas para adaptar a orienta??o a objetos ao M?todo B. Este trabalho foi avaliado atrav?s de um estudo de caso feito com a ferramenta BSmart que faz uso da biblioteca KitSmart. Neste estudo de caso, ? poss?vel ver a contribui??o dos componentes em uma especifica??o B. Este kit dever? ser ?til tanto para usu?rios do m?todo B como para desenvolvedores de aplica??es Java Card em geral

La mise à jour dynamique des programmes consiste en la modification de ceux-ci sans en arrêter l'exécution. Cette caractéristique est primordiale pour les applications critiques en continuelles évolutions et nécessitant une haute disponibilité. Le but de notre travail est d'effectuer la vérification formelle de la correction de la mise à jour dynamique d'applications Java Card à travers l'étude du système EmbedDSU. Pour ce faire, nous avons premièrement établi la correction de la mise à jour du code en définissant une sémantique formelle des opérations de mise à jour sur le code intermédiaire Java Card en vue d'établir la sûreté de typage des mises à jour. Nous avons ensuite proposé une approche pour vérifier la sémantique du code mis à jour à travers la définition d'une transformation de prédicats. Nous nous sommes ensuite intéressés à la vérification de la correction concernant la détection de points sûrs de la mise à jour. Nous avons utilisé la vérification de modèles. Cette vérification nous a permis de corriger d'abord un problème d'inter blocage dans le système avant d'établir d'autres propriétés de correction : la sûreté d'activation et la garantie de mise à jour. La mise à jour des données est effectuée à travers les fonctions de transfert d'état. Pour cet aspect, nous avons proposé une solution permettant d'appliquer les fonctions de transfert d’état tout en préservant la consistance du tas de la machine virtuelle Java Card et en permettant une forte expressivité dans leurs écritures. / Dynamic Software Updating (DSU) consists in updating running programs on the fly without any downtime. This feature is interesting in critical applications that are in continual evolution and that require high availability. The aim of our work is to perform formal verification the correctness of dynamic software updating in Java Card applications by studying the system EmbedDSU. To do so, we first established the correctness of code update. We achieved this by defining formal semantics for update operations on java Card bytecode in order to ensure type safety. Then, we proposed an approach to verify the semantics of updated programs by defining a predicate transformation. Afterward, we were interested in the verification of correction concerning the safe update point detection. We used model checking. This verification allowed us first to fix a deadlock situation in the system and then to establish other correctness properties: activeness safety and updatability. Data update is performed through the application of state transfer functions. For this aspect, we proposed a solution to apply state transfer functions with the preservation of the Java Card virtual machine heap consistency and by allowing a high expressiveness when writing state transfer functions.

Made available in DSpace on 2014-12-17T14:13:51Z (GMT). No. of bitstreams: 1 JocelineCFS_TESE.pdf: 9953676 bytes, checksum: 9e87c154e4492433b05652a1e5ae5096 (MD5) Previous issue date: 2013-10-29 / Conselho Nacional de Desenvolvimento Cient?fico e Tecnol?gico / O objetivo deste estudo foi analisar o efeito do treinamento f?sico aer?bico (TFA) na modula??o auton?mica card?aca, avaliado pela variabilidade da frequ?ncia card?aca (VFC), em mulheres com s?ndrome dos ov?rios polic?sticos (SOP). Participaram do estudo 30 mulheres na faixa et?ria entre 18 e 34 anos, com diagn?stico de SOP de acordo com o Consenso de Rotterdam, e foram divididas em dois grupos: 1) grupo treinamento (GT; n=15) que conclu?ram programa de treinamento aer?bico durante 16 semanas, tr?s vezes por semana e 40 minutos por sess?o; e 2) grupo controle (GC; n=15) que n?o participaram do treinamento. A VFC foi analisada antes e ap?s o per?odo de estudo, sendo analisada pelos m?todos linear e n?o-linear. Para avaliar o efeito do treinamento sobre as vari?veis da an?lise da VFC foi ajustado um modelo de an?lise de covari?ncia multivariado (MANCOVA) tendo como covari?veis o IMC (?ndice de massa corporal), a Insulina e a Testosterona e como fator explicativo o grupo (tratamento, controle). As caracter?sticas cl?nicas quanto ao peso, circunfer?ncia de cintura, IMC, press?o arterial, frequ?ncia card?aca, VO2 m?x (consumo m?ximo de oxig?nio), insulina de jejum e testosterona, n?o apresentaram diferen?a estatisticamente significativa (p>0.05) entre os grupos pr?-interven??o. Tanto a FC (frequ?ncia card?aca) como a press?o arterial sist?lica de repouso, apresentaram diminui??o estatisticamente significativa no grupo treinado ap?s as 16 semanas (p=0.016; p=0.001 respectivamente). Observaram-se aumentos significativos no RMSSD ( raiz quadrada da somat?ria dos quadrados das diferen?as entre os intervalos R-R normais adjacentes) - (p < 0,0001) e no SDNN (desvio-padr?o da m?dia de todos os intervalos RR normais) - (p = 0,002). Na an?lise espectral no dom?nio da frequ?ncia foi encontrado aumento significativo no AF (alta frequ?ncia) em unidades absolutas (p < 0,0001), a vari?vel AFun (alta frequ?ncia em unidades normalizadas) tamb?m apresentou um aumento significativo (p < 0,001), enquanto que BFun (baixa frequ?ncia em unidades normalizadas) demonstrou diminui??o significativa (p < 0,001). Na an?lise das vari?veis pelo m?todo n?o-linear foram encontradas diferen?as significativas na ES (Entropia de Shannon), 0V% (porcentagem de padr?es sem varia??o) e 2VD% (porcentagem de padr?es com duas varia??es diferentes) (p<0,05), caracterizando uma melhora na modula??o auton?mica da frequ?ncia card?aca do grupo treinado. O TFA melhorou a VFC em repouso de mulheres com SOP, caracterizado pelo aumento na modula??o parassimp?tica e redu??o da modula??o simp?tica na frequ?ncia card?aca. Os resultados refor?am a import?ncia da abordagem interdisciplinar na avalia??o e tratamento de mulheres com SOP, com vistas ? redu??o de morbidade relacionada ao sistema cardiovascular

Made available in DSpace on 2014-12-17T14:56:06Z (GMT). No. of bitstreams: 1 JailtonCP_DISSERT.pdf: 2190503 bytes, checksum: ee26df46d54432b596d1d87d4b66b75c (MD5) Previous issue date: 2012-07-27 / 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 / Em praticamente todos os mercados verticais e em cada regi?o do planeta, os comerciantes de fidelidade adotaram a t?tica de reconhecimento e recompensa para identificar, manter e aumentar o rendimento de seus clientes. V?rias estrat?gias t?m sido adotadas pelas empresas, e a mais popular entre elas ? o programa de fidelidade, que exibe um clube de fidelidade para gerenciar essas recompensas. Mas o problema com os programas de fidelidade ? que a identifica??o dos clientes e a transmiss?o dos pontos de fidelidade s?o feitas de forma semiautom?tica. Visando isto, o presente trabalho de mestrado apresenta uma solu??o embarcada de automa??o comercial intitulada e-Pontos. O objetivo do e-Pontos ? munir os clubes de fidelidades com ferramental tecnol?gico totalmente automatizado para identificar os clientes diretamente nos pontos de vendas, garantindo um maior controle dos pontos de fidelidade dos membros associados. Para isso, foi desenvolvida uma plataforma de hardware com sistema embarcado e tecnologia RFID que ser? utilizada nos PCs dos lojistas, um smart card para acumular os pontos a cada compra e um servidor web, o qual disponibilizar? servi?os de interesse para os lojistas e os clientes conveniado ao clube

This diploma thesis consists of two basic parts. The theoretical part, which you hold in your hands just now, and the practical part, which you can find in reduced ver-sion in the image supplement of this work and whose originals will be presented by the day of the diploma thesis defence session. In practical part of my work I have created a full collection of the whist cards using coloured lino-cut technology. In the theoretical concomitant of the art part I wrote about the history and the pre-sent of card games. You can find there informations about origin of cards, about their journey and spreading to the continental Europe, about cards in the Czech countries and about contemporary world of cards. I also wrote about kinds of cards, especially whist cards (they have separate chapter), about card games (games played in our area and games played with whist cards above all), about technology of card production and about their players. I dedicated one whole chapter to talk about practical realization of my whist cards collection, where I cleared up the choice of the theme, creation of con-crete figures and colours used.

A SIM, Subscriber Identity Module, is the removable circuit board found in a modern cellular phone. It carries the network identity information and is a type of smart card which can also be found on payment cards (EMV), ID cards and so on. A smart card is basically a small computer, providing a safe and controlled execution environment. Historically smart card software was very hardware dependent and mostly developed by the manufacturers themselves. With the introduction of the open Java Card standard created by Sun Microsystems (Oracle) this was meant to change. However, information still remains scattered and is hard to obtain. This paper is meant to serve both as an introduction to the field and also as a good foundation for future studies. It begins with a theoretical discussion about smart card hardware and software architectures, network standards in the context of SIM cards, typical applications, coming trends and technologies and ends off with an overview of the Java Card standard. The following section discusses the supplied example SIM card application coupled with an introduction how to use the Gemalto Developer Suite for application development and testing. The paper ends with an extensive appendix section going in depth about some of the more important subjects.

This master thesis deals with the usage of smart cards in the area of digital signature. The descriptive part of this work outlines the basic principles of digital signature, smart cards typology and current most important application areas of smart cards. The first aim of the analytic part of this work is to evaluate actual situation on the smart cards market and to estimate future market trends. The second aim is to provide summary of new technological trends and areas, in which the usage of smart cards can be expected. These new technological trends and areas are described on the basis of survey, which was realized in the company OKsystem. Part of this work serves information about practical solution OKsmart and the analysis of its future development trends.

This thesis deals with problems of identification cards at the University of Economics, Prague. Its primary goal is to consider and evaluate the possibility of a transfer of the ID card management into the ISIS system. The thesis consists of four parts. The first one offers a complex analysis of the ID card management at the University. The second one analyses two ID card management systems: the NESA system, which is being used at the University now, and the ISIS system, which could also be used for the ID card management. The third part includes a proposal of adjustments in the ISIS system, which would make its ID card management implementation comply with the University's needs. The proposal describes general features of the system, relations to its environs and a graphical user interface. Finally the last part covers the actual state of the project and its differences from the proposal offered in the thesis. Information sources for the thesis were legal norms, University regulations and internal documents as well as the author's knowledge and experience gained through several years of the NESA system maintenance and numerous consultations with the University ID card management staff and ISIS developers. The main assets of this thesis lay in the comprehensive view of the ID card management at the University along with the proposal of the new ID card management system, which is to be integrated into ISIS.

Le montant annuel de la fraude européenne à la carte de paiement se monte à plus d’1,5 milliard d’euros. Cette manne aiguise l’appétit des groupes criminels qui exploitent la moindre faille de la monétique (écosystème de la carte de paiement). Les cinq principaux acteurs de la monétique (porteurs, émetteurs, accepteurs, acquéreurs et systèmes de paiement) s’appuient pourtant sur des systèmes et réseaux normalisés dont la sécurité est encadrée par des standards internationaux contraignants. Néanmoins, la fraude monétique ne cesse de progresser alors que les moyens de lutte (étatiques, collaboratifs ou individuels) restent limités.Après étude de la fraude monétique, cette thèse propose différentes actions (passives,réactives et proactives) visant à améliorer la lutte contre la fraude monétique. D’abord,il convient de mieux connaître la fraude en étudiant la provenance des données volées et plus seulement leur usage. Ensuite l’expertise de ces fraudes doit être améliorée, en développant par exemple une captation du progrès scientifique. Une expertise qui doit être en partie transmise aux enquêteurs afin qu’ils puissent conduire leurs enquêtes. Enquêtes qui peuvent être dynamisées par des opérations réactives associant investigateurs et sachants techniques. Enfin, de manière proactive, les enquêtes et analyses de demain doivent être facilitées par les technologies monétiques conçues aujourd’hui. / Every year, payment card fraud exceeds 1.5 billion euros in Europe. Organised crime groups are exploiting any vulnerability possible to take a piece of this lucrative activity. Even though the five principal entities in the payment card industry (cardholders, issuers,acceptors, acquirers and payment system providers) are implementing binding security measures through out standardized systems and networks, fraud continues to increase. Efforts by the state, industry collaboration, and individuals have been unsuccessful in decreasing criminal advances. Having analysed the elements of payment card fraud, this thesis proposes several actions (passive, reactive and proactive) to help improve the fight against this fraud. First, itis relevant to gain knowledge of the source of the card details and not to focus only on its reuse. Next, forensic assessment has to be improved, for example by developing an increased scientific understanding of the technology. Such an expertise should then be passed on to investigators through effective training and knowledge transfer. Investigations should also be made more dynamic with reactive operations conducted in concert by investigators and technicians. Finally, in an ideal proactive spirit, future investigations and assessments should be oriented and facilitated by studying and influencing current payment card technology developments.