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.

Projeto café do trabalhador como promotor de segurança alimentar e nutricional: avaliação da eficácia da unidade Natal-RN

The evaluation of public policies that promote Food Security and Nutrition (FSN) it s a multidisciplinary activity extremely relevant to the effectiveness of actions to legitimize the Human Right to Adequate Food (HRAF). This study aimed at assessing the effectiveness of the unit project Natal-RN Café do Trabalhador in promoting SAN to its users. The theoretical framework is based on the public and political and on the dimensions of the concept of FSN (quantity and quality-regularity). Through a qualitative approach, methodologically this was the work of an evaluation of efficiency of the unit Natal-RN of Café do Trabalhador project in light of the assumptions of the concept of SAN. Data collection was conducted through retrospective archival research in official documents of the project, semi-structured interviews with managers involved in its implementation (representative of the Secretary of State for Employment, Housing and Care of RN SETHAS and third party), socioeconomic questionnaire applied to the users of the unit, check the amount, regularity and quality of meals offered for 15 days (menu routine) using the descriptive form menu and form filling type checklist for verification of compliance with good practices . Methods of analysis, we used content analysis, descriptive statistics and compared to previously established parameters for the project. As categories of analysis were defined organizational arrangement, access, user, food quantity-regularity and food quality. The results show that, it was found in the category arrangement that will implement the project dismissed technical criteria for choosing the districts and the quantitative distribution of meals for each location. It was found that the valuation of the shares of the company outsources technical SETHA has not been performed. We observed in the access category, the unit has a strategic location, but lack of space in the refectory. The main obstacle to economic access for users is the lack of a register for the beneficiaries. In the category of users, it was identified that the clientele of the project it is predominantly men, with more than 51 years, low education, earning wages less 1 obtained through informal employment, which they move up through the unit transport collective, go to all days of operation due primarily to price. About the meals category quantity-regularity of food showed that the menu serves 95% of the desired needs, and that holidays and weekends are periods of disrupting the regularity of supply of meals. Regarding the category of food quality, it was found that the nutritional aspect on the menu are food sources rich in sodium, nitrates and low in fiber. In the aspect of hygiene and sanitation are the main limitations related to waste management, lack of exposure controls of food prepared and inadequacies of the physical structure. The results showed that in general and the institutional arrangement of the organs attached to the project should establish a systematic evaluation project is to establish as a promoter of and FSN overcome these obstacles

Eficiência e razão de hedge: uma análise dos mercados futuro brasileiros de boi, café, etanol, milho e soja

This research aims to investigate the Hedge Efficiency and Optimal Hedge Ratio for the future market of cattle, coffee, ethanol, corn and soybean. This paper uses the Optimal Hedge Ratio and Hedge Effectiveness through multivariate GARCH models with error correction, attempting to the possible phenomenon of Optimal Hedge Ratio differential during the crop and intercrop period. The Optimal Hedge Ratio must be bigger in the intercrop period due to the uncertainty related to a possible supply shock (LAZZARINI, 2010). Among the future contracts studied in this research, the coffee, ethanol and soybean contracts were not object of this phenomenon investigation, yet. Furthermore, the corn and ethanol contracts were not object of researches which deal with Dynamic Hedging Strategy. This paper distinguishes itself for including the GARCH model with error correction, which it was never considered when the possible Optimal Hedge Ratio differential during the crop and intercrop period were investigated. The commodities quotation were used as future price in the market future of BM&FBOVESPA and as spot market, the CEPEA index, in the period from May 2010 to June 2013 to cattle, coffee, ethanol and corn, and to August 2012 to soybean, with daily frequency. Similar results were achieved for all the commodities. There is a long term relationship among the spot market and future market, bicausality and the spot market and future market of cattle, coffee, ethanol and corn, and unicausality of the future price of soybean on spot price. The Optimal Hedge Ratio was estimated from three different strategies: linear regression by MQO, BEKK-GARCH diagonal model, and BEKK-GARCH diagonal with intercrop dummy. The MQO regression model, pointed out the Hedge inefficiency, taking into consideration that the Optimal Hedge presented was too low. The second model represents the strategy of dynamic hedge, which collected time variations in the Optimal Hedge. The last Hedge strategy did not detect Optimal Hedge Ratio differential between the crop and intercrop period, therefore, unlikely what they expected, the investor do not need increase his/her investment in the future market during the intercrop

Estudo da potencialidade da incorporação de resíduo de granito e da queima da casca do café em cerâmica vermelha

The industrial production of ornamental rocks and the burning of coffee husk generate waste that is discarded into the environment. However, with the study of the incorporation of these residues in ceramic products, may be found an alternative to reducing environmental impacts and detrimental effects on human health caused by its indiscriminate disposal of waste in nature. Thus, this work aimed to study the addition of ashes of the coffee husk and granite residue in matrix of red ceramic. The raw materials were dry milled and sieved to mesh 100. To characterize the raw materials were carried out analyzes of X-ray diffraction (XRD), X-ray fluorescence (XRF), particle size analysis (PSA), differential thermal analysis (DTA) and thermogravimetric analysis (TG). Six formulations were prepared where the clay content was kept constant (70%wt) and ashes contents and granite residue varied from 10, 15, 20 and 30%. Dilatometrics analyzes were performed at four selected formulations, containing them: 100% clay (A100); 70% clay and 30% ashes (A70C30); 70% clay and 30% granite residue (A70G30); and 70% clay, 15% granite residue and 15% ashes (A70G15C15). The samples were prepared by uniaxial compaction with pressure of 25 MPa, and fired at temperatures of 800°C, 850ºC, 900ºC, 950ºC, 1000ºC and 1100°C. Assays were performed to determine the linear shrinkage of burning (LSB), water absorption (WA), apparent porosity (AP), density (D) and tensile bending. Also were performed analyzes of X-ray diffraction (XRD) and scanning electron microscopy (SEM) of the samples fired. The formulations incorporating granite residue and/or ashes reached the required limits of water absorption according to NBR 15270-1 and NBR 15310 and tensile bending according to classical literature (SANTOS, 1989) necessary for the production of tiles and ceramic block for masonry sealing

Adição de subprodutos da cinza da casca de café (coffea canephora) em massa cerâmica para porcelanato

To produce porcelain tiles fluxing agents are used in order to obtain a liquid phase during firing. This liquid phase fills the pores decreasing porosity, water absorption and contributes to material densification. In the porcelain tiles industry, feldspar is the main flux material used, with quantities ranging between 35 and 50%. Studies focus on the discovery of materials with flux characteristics that can reduce the consumption of feldspar by porcelain tiles industry. In this context, the coffee husk ashes, a residue obtained when coffee husks are burned to produce heat for the dryers during the processing of the green fruit, have as main chemical constituents potassium, calcium and magnesium, giving them characteristics of fluxing material. Brazil is the largest coffee producer in the world and is responsible for over 30% of the world s production. In this work a physical treatment of coffee husk ash was carried out in order to eliminate the organic matter and, after this, two by-products were obtained: residual wastes R1 and R2. Both residues were added separately as single fluxes and also in association with feldspar in mixtures with raw materials collected in a porcelain industry located in Dias d Ávila-Ba. The addition of these residues aimed to contribute to the reduction of the consumption of feldspar in the production of porcelain tiles. Specimens were produced with dimensions of 60 mm x 20 mm x 6 mm in an uniaxial die with compacting pressure of 45 MPa. The samples were heated to a temperature of 1200 °C, for 8 minutes. Tests were performed to characterize the raw materials by XRF, XRD, particle size analysis, DTA and TGA and, additionally, the results of the physical properties of water absorption, apparent porosity, linear shrinkage, density, dilatometry, flexural strength and SEM of sintered body were analyzed. Additions of less than 8% of the residue R1 contributed to the decrease of porosity, but the mechanical strength of the samples was not satisfactory. Additions of 5% the R2 residue contributed significantly to decrease the water absorption and apparent porosity, and also to increase the mechanical strength. Samples with addition of feldspar associated with the R2 residue, in proportions of 6.7% of R2 and 6.7% of feldspar, led to results of water absorption of 0.12% and mechanical strength of 46 MPa, having parameters normalized to the manufacture of porcelain stoneware tiles

Uma perspectiva de extensão do modelo de aceitação de tecnologia para explicar o uso de linguagens de desenvolvimento WEB: pesquisa com desenvolvedores Pyton e Java

The spread of the Web boosted the dissemination of Information Systems (IS) based on the Web. In order to support the implementation of these systems, several technologies came up or evolved with this purpose, namely the programming languages. The Technology Acceptance Model TAM (Davis, 1986) was conceived aiming to evaluate the acceptance/use of information technologies by their users. A lot of studies and many applications have used the TAM, however, in the literature it was not found a mention of the use of such model related to the use of programming languages. This study aims to investigate which factors influence the use of programming languages on the development of Web systems by their developers, applying an extension of the TAM, proposed in this work. To do so, a research was done with Web developers in two Yahoo groups: java-br and python-brasil, where 26 Java questionnaires and 39 Python questionnaires were fully answered. The questionnaire had general questions and questions which measured intrinsic and extrinsic factors of the programming languages, the perceived usefulness, the perceived ease of use, the attitude toward the using and the programming language use. Most of the respondents were men, graduate, between 20 and 30 years old, working in the southeast and south regions. The research was descriptive in the sense of its objectives. Statistical tools, descriptive statistics, main components and linear regression analysis were used for the data analysis. The foremost research results were: Java and Python have machine independence, extensibility, generality and reliability; Java and Python are more used by corporations and international organizations than supported by the government or educational institutions; there are more Java programmers than Python programmers; the perceived usefulness is influenced by the perceived ease of use; the generality and the extensibility are intrinsic factors of programming languages which influence the perceived ease of use; the perceived ease of use influences the attitude toward the using of the programming language

Avaliação dos textos informativos em três embalagens de café

O presente trabalho tem o objetivo de apresentar uma investigação sobre o nível de clareza dos textos informativos dos rótulos de embalagens de café torrado e moído, considerando os aspectos lingüísticos e ergonômicos presentes nos rótulos do produto. Lingüisticamente analisar se a linguagem utilizada nos rótulos é adequada para a compreensão das informações pelo consumidor, ainda expor como a lingüística preconiza a organização e estruturação dos textos a partir da classificação do gênero textual. Do ponto de vista da ergonomia a pesquisa pretende identificar a conformidade ergonômica presente nas informações dos rótulos das embalagens de café. Devido à evolução das atividades comerciais, a embalagem passou ao longo do tempo a acumular funções, transformando-se em um considerável veículo de comunicação, informação e sedução do seu público consumidor, por isso, a adoção de normas adequadas relativas às informações pode evitar que o consumidor desenvolva conceitos inadequados ou até mesmo empregue erroneamente um produto alimentício em sua dieta. A engenharia de produção considera importante a inserção de melhores práticas de produção e gestão do produto nas empresas, com vistas ao aumento de sua competitividade, compatibilizando as características ergonômicas do produto embalagem, com as necessidades do consumidor enquanto parte integrante do processo de desenvolvimento do produto. A pesquisa propõe, então, um roteiro para avaliação dos rótulos de embalagens, utilizando para isso um questionário com questões fechadas e uma aberta, aplicados em consumidores de café torrado e moído no momento da compra em quatro supermercados de Natal. Os principais resultados da investigação demonstram que os aspectos lingüísticos dos textos informativos foram considerados bons, enquanto os aspectos ergonômicos informacionais analisados podem vir a contribuir para uma melhoria visual das informações contidas nos rótulos das embalagens das marcas de café investigadas

Análise de desempenho de sistemas distribuídos de grande porte na plataforma Java

The lava Platform is increasing1y being adopted in the development of distributed sys¬tems with higb user demando This kind of application is more complex because it needs beyond attending the functional requirements, to fulfil1 the pre-established performance parameters. This work makes a study on the Java Vutual Machine (JVM), approaching its intemal aspects and exploring the garbage collection strategies existing in the literature and used by the NM. It also presents a set of tools that helps in the job of optimizing applications and others that help in the monitoring of applications in the production envi¬ronment. Doe to the great amount of technologies that aim to solve problems which are common to the application layer, it becomes difficult to choose the one with best time response and less memory usage. This work presents a brief introduction to each one of tbe possible technologies and realize comparative tests through a statistical analysis of the response time and garbage collection activity random variables. The obtained results supply engineers and managers with a subside to decide which technologies to use in large applications through the knowledge of how they behave in their environments and the amount of resources that they consume. The relation between the productivity of the technology and its performance is also considered ao important factor in this choice

Incorporação de cinzas da casca de café na produção de placas cerâmicas para revestimento

Brazil is the world s leading coffee producer. In 2008, 45.99 million of 60 kg bags of benefited coffee were produced. In the process of improvement 50% is grain and 50% is husk, thus, 1.38 million tons of coffee husk are produced annually. The husk is used as combustible in the drying and improvement ovens in the coffee farms, generating ash as residue. These ashes contain a high concentration of alkaline metals and earth metals, mainly K2O and CaO. This work studies the use of this residue in the ceramic tiles industry, as fluxing agents in substitution to the feldspar. Ten mixtures with equal ratios of clay and kaolin, proceeding from Bahia and the residue (varying from 30 to 5%) were defined and produced in uniaxial tool die of 60x20mm with approximately 5 mm of thickness and 45MPa compacting pressure. The samples were fired in four different temperatures: 1100 °C, 1150 °C, 1185 °C and 1200 °C during 60 minutes and characterized by means of X-ray fluorescence, X-ray diffraction, gravimetric thermal analysis and differential thermal analysis. The results of water absorption, apparent porosity, linear shrinkage, XRD, dilatometry, flexural strength and SEM were also analysed. The test specimen with addition of 10% of ash fired in 1200 °C resulted in 0.18% water absorption and 40.77 MPa flexural strength, being classified as porcelain stoneware tiles according to ABNT, UNI and ISO norms

Além das xícaras: a construção do Café São Luiz como lugar de memória em Natal (1950-1980)

This research stands in discussions involving the relationship between memory, history and space. We will work with the Café São Luiz in the neighborhood of Cidade Alta in Natal, an place which remains open and founded in 1953. The place was opened in the district of greater movement of the 1950s, a zone of concentration of commerce and leisure. In consequence an impulse of memory, the Café São Luiz was represented by different statements, which they built a space that serves to support memory and identity of a group. The speeches elaborate the Café São Luiz as a monument, a place of memory according to Pierre Nora. Among these discourses of construction of the Café São Luiz stands out the 1982 book titled Na Calçada do Café São Luiz by José Luiz Silva. This research aims to discuss the construction of the Café São Luiz as a place of memory, questioning their representations, traversing the authorship of speeches over the place

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.