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

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

RR3D: Uma solução para renderização remota de imagens médicas tridimensionais

The visualization of three-dimensional(3D)images is increasigly being sed in the area of medicine, helping physicians diagnose desease. the advances achived in scaners esed for acquisition of these 3d exames, such as computerized tumography(CT) and Magnetic Resonance imaging (MRI), enable the generation of images with higher resolutions, thus, generating files with much larger sizes. Currently, the images of computationally expensive one, and demanding the use of a righ and computer for such task. The direct remote acess of these images thruogh the internet is not efficient also, since all images have to be trasferred to the user´s equipment before the 3D visualization process ca start. with these problems in mind, this work proposes and analyses a solution for the remote redering of 3D medical images, called Remote Rendering (RR3D). In RR3D, the whole hedering process is pefomed a server or a cluster of servers, with high computational power, and only the resulting image is tranferred to the client, still allowing the client to peform operations such as rotations, zoom, etc. the solution was developed using web services written in java and an architecture that uses the scientific visualization packcage paraview, the framework paraviewWeb and the PACS server DCM4CHEE.The solution was tested with two scenarios where the rendering process was performed by a sever with graphics hadwere (GPU) and by a server without GPUs. In the scenarios without GPUs, the soluction was executed in parallel with several number of cores (processing units)dedicated to it. In order to compare our solution to order medical visualization application, a third scenario was esed in the rendering process, was done locally. In all tree scenarios, the solution was tested for different network speeds. The solution solved satisfactorily the problem with the delay in the transfer of the DICOM files, while alowing the use of low and computers as client for visualizing the exams even, tablets and smart phones

Análise da relação causal entre imagem de destinos, qualidade, satisfação e fidelidade: um estudo de acordo com a percepção do turista nacional no destino turístico Natal

This dissertation aims to analyze the causal relationship between the quality of tourist services, satisfaction with the attributes and globally, fidelity and image of tourist destinations. Therefore, it was conducted an exploratory, descriptive research with quantitative analytical approach. Data collection was performed by a questionnaire addressed to tourists at the Augusto Severo International Airport and Bus station of Natal, the main points of entry and exit of tourists. The composition was simple random sampling by reaching the final number of 400 tourists interviewed. Among the main results, is an assessment of the quality of the components of the destination. It was noted that nine are the dimensions of perceived quality of tourism products and services of ―Sun and Sand‖ segment, that is, Beaches and Facilities, Public Equipment, Catering Services, Transportation, Hotel Equipment, Hotel Services, Entertainment & Attractions, Access to the Hotel and Hospitality. Moreover, it was concluded that the Preview Tourism Destination Image has little direct influence in the Consumer Satisfaction, and only indirectly in the Post-Purchase Behavior. While the Complex Tourism Destination Image exerts strong and direct influence on both factors, in the Customer Satisfaction Process and Loyalty, the dimensions of quality also claimed to be strongly influences both factors

Desenvolvimento e validação de técnica quantitativa de análise de imagem para avaliação do teste do cometa corado pela prata

INTRODUÇÃO: O ensaio do cometa ou técnica da eletroforese de células isoladas é largamente empregado para avaliação de danos e reparo do DNA em células individuais. O material pode ser corado por técnicas de fluorescência ou por sal de prata. Este último apresenta vantagens técnicas, como o tipo de microscópio utilizado e a possibilidade de armazenamento das lâminas. A análise dos cometas pode ser feita de modo visual, porém há a desvantagem da subjetividade dos resultados, que pode ser minimizada por análise digital automatizada. OBJETIVOS: Desenvolvimento e validação de método de análise digital de cometas corados por sal de prata. MÉTODOS: Cinquenta cometas foram fotografados de maneira padronizada e impressos em papel. Além de medidas manualmente, essas imagens foram classificadas em cinco categorias por três avaliadores, antes e depois de pré-processadas automaticamente pelo software ImageJ 1.38x. As estimativas geradas pelos avaliadores foram comparadas quanto sua correlação e reprodutibilidade. em seguida, foram desenvolvidos algoritmos de análise digital das medidas, com base em filtros estatísticos de mediana e de mínimo. Os valores obtidos foram comparados com os estimados manual e visualmente após o pré-processamento. RESULTADOS: As medidas manuais das imagens pré-processadas apresentaram maior correlação intraclasse do que as imagens preliminares. Os parâmetros automatizados apresentaram alta correlação com as medidas manuais pré-processadas, sugerindo que este sistema aumenta a objetividade da análise, podendo ser utilizado na estimativa dos parâmetros dos cometas. CONCLUSÃO: A presente análise digital proposta para o teste do cometa corado pela prata mostrou-se factível e de melhor reprodutibilidade que a análise visual.

Comportamento da sutura palatina mediana em crianças submetidas à expansão rápida da maxila: avaliação mediante imagem de tomografia computadorizada

OBJETIVO: o presente estudo, de caráter prospectivo, objetivou avaliar a imagem da sutura palatina mediana em crianças submetidas à expansão rápida da maxila por meio de tomografia computadorizada, após a fase de contenção. METODOLOGIA: a amostra constou de 17 crianças de ambos os gêneros, na faixa etária compreendida entre 5 anos e 2 meses e 10 anos e 5 meses no início do tratamento, provenientes da Clínica de Ortodontia Interceptiva da Sociedade de Promoção Social do Fissurado Lábio-Palatal da Universidade de São Paulo (PROFIS-USP), Bauru/SP. Tomografias computadorizadas foram implementadas para avaliar o comportamento da sutura palatina mediana em diferentes momentos do tratamento. RESULTADOS E CONCLUSÕES: constatou-se que, após um período médio de 8 a 9 meses de contenção com o aparelho expansor, a sutura palatina mediana mostrou-se completamente ossificada, desde a região da espinha nasal anterior até a espinha nasal posterior. Tal informação esclarece o comportamento da sutura palatina mediana frente à expansão rápida da maxila e reitera o senso comum quanto ao caráter biológico do procedimento.

Método para determinação de distribuição de tamanho de microbolhas (DTMB) em sistemas flotação (FAD) para tratamento de águas utilizando a análise de imagem digital

Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)

Avaliação da simetria da imagem do ramo da mandíbula em radiografias panorâmicas

Os métodos radiográficos panorâmicos apresentam ampliação das imagens de estruturas anatômicas da face, com variação de uma região para outra. Atualmente, este tipo de técnica tem sido utilizado para mensurações verticais, horizontais e angulares. A área e o perímetro da imagem bilateral do ramo da mandíbula foram medidos em radiografias panorâmicas obtidas pelo sistema elipsopantomográfico, de crianças dos dois sexos, com idade cronológica entre 8 e 10 anos. Os desenhos, em papel vegetal, da imagem de cada ramo foram capturados através de scanner e as medidas foram feitas em microcomputador com aplicativo específico. Duas formas de separar a imagem do ramo da mandíbula, bilateralmente, foram propostas: no gônio e através de uma tangente à parte mais profunda da borda anterior da imagem do ramo que tocava a base. Os resultados obtidos permitiram evidenciar que houve simetria entre os lados, expressa pelas medidas de área e perímetro das imagens do ramo da mandíbula.

Locais de implante de microchips de identificação eletrônica de leitões: seleção e validação por análise de imagem

Nas últimas décadas, a produção de suínos, pressionada por uma crescente demanda por alimentos, tem-se caracterizado pela maior concentração de animais em grandes unidades de produção, dificultando o registro dos dados individuais. Os sistemas automáticos de identificação eletrônica podem auxiliar a detecção de doenças, a avaliação de respostas fisiológicas, o controle de ingestão de alimentos, a atividade física e ainda o impacto ambiental causado pelo sistema de produção, promovendo melhor controle da propriedade. Transponders injetáveis, brincos eletrônicos e o monitoramento por meio da análise de imagem estão sendo utilizados no processo de identificação. O objetivo desta pesquisa foi avaliar os diferentes locais de implante subcutâneo de microchips em leitões, verificando-se possíveis infecções e/ou rejeições, migrações dos microchips em relação ao local de implante e sua validação em relação à análise de imagem.

Geografia: o olhar e a imagem pictórica

Este artigo objetiva apresentar, de forma introdutória, a possibilidade e a necessidade de diálogo entre a linguagem pictórica e o discurso científico da Geografia. Para tal, apresenta alguns elementos do alfabeto das pinturas de imagens a partir tanto da semiótica quanto da gestalt, analisadas por Fayga Ostrower e Donis Dondis. O exercício interpretativo dá-se a partir do conceito de paisagem aplicado sobre as imagens elaboradas artisticamente por grandes pintores da humanidade, contextualizando-as a partir dos elementos técnicos e tecnológicos que existiam na época e no lugar, e da forma como esses interferem nos processos de elaboração e interpretação das obras. Para exemplificar isso, utilizam-se três pinturas elaboradas em diferentes períodos, a partir da Europa medieval até o mundo moderno, apresentando, assim, os aspectos gerais que levavam à mudança de leitura espacial do território produzido a partir da consolidação do mundo urbano, industrial e baseado na lógica da mercadoria.

Análise do uso da terra na microbacia do Arroio do Meio - Santa Maria - RS, por Sistema de Informações Geográficas e imagem de satélite

O objetivo desse trabalho foi verificar a viabilidade do uso de um Sistema de Informações Geográficas (SIG) e a imagem de satélite para a análise do uso atual da terra e localização de áreas onde possam estar ocorrendo conflitos entre capacidade e uso do solo, na microbacia hidrográfica do Arroio do Meio. Foram utilizadas técnicas de geoprocessamento, como álgebra entre mapas, consulta ao banco de dados e reclassificação de imagens. Uma microbacia foi escolhida como objeto deste estudo, por ser considerada por muitos autores como sendo uma das melhores unidades para o planejamento e desenvolvimento sócioeconômico dos habitantes do meio rural. Na microbacia estudada, foram encontrados 555ha cobertos com florestas, compreendendo 24% da área total. As lavouras com área de 1.314ha ocupam a maior parte da microbacia (56%). Os campos de pastagens cobrem 184ha, ou seja, 8% da área total. As áreas alagadas representam 11% da área da microbacia, tendo respectivamente 265ha. Foram detectados ainda, 31ha sombreados (1%) onde não se determinou com exatidão o uso da terra. Nas áreas com declividade superior a 47%, foram detectados 32ha sem cobertura de florestas, perfazendo 1,4% da área da microbacia. em declives superiores a 30%, existem 71ha (3%) sendo usados para a agricultura. A área ocupada com Chernossolos e Neossolos Litólicos, unidade de mapeamento Ciríaco-Charrua em declividade maior que 30% sem cobertura florestal é de 14ha (0,6%). de acordo com a declividade e o solo, as áreas de conflito alcançam 5% da área total, o que demonstra que, na maior parte da microbacia, a terra está sendo usada de acordo com sua capacidade.