JML- Based formal development of a Java card application for managing medical appointments

Although formal methods can dramatically increase the quality of software systems, they have not widely been adopted in software industry. Many software companies have the perception that formal methods are not cost-effective cause they are plenty of mathematical symbols that are difficult for non-experts to assimilate. The Java Modelling Language (short for JML) Section 3.3 is an academic initiative towards the development of a common formal specification language for Java programs, and the implementation of tools to check program correctness. This master thesis work shows how JML based formal methods can be used to formally develop a privacy sensitive Java application. This is a smart card application for managing medical appointments. The application is named HealthCard. We follow the software development strategy introduced by João Pestana, presented in Section 3.4. Our work influenced the development of this strategy by providing hands-on insight on challenges related to development of a privacy sensitive application in Java. Pestana’s strategy is based on a three-step evolution strategy of software specifications, from informal ones, through semiformal ones, to JML formal specifications. We further prove that this strategy can be automated by implementing a tool that generates JML formal specifications from a welldefined subset of informal software specifications. Hence, our work proves that JML-based formal methods techniques are cost-effective, and that they can be made popular in software industry. Although formal methods are not popular in many software development companies, we endeavour to integrate formal methods to general software practices. We hope our work can contribute to a better acceptance of mathematical based formalisms and tools used by software engineers. The structure of this document is as follows. In Section 2, we describe the preliminaries of this thesis work. We make an introduction to the application for managing medical applications we have implemented. We also describe the technologies used in the development of the application. This section further illustrates the Java Card Remote Method Invocation communication model used in the medical application for the client and server applications. Section 3 introduces software correctness, including the design by contract and the concept of contract in JML. Section 4 presents the design structure of the application. Section 5 shows the implementation of the HealthCard. Section 6 describes how the HealthCard is verified and validated using JML formal methods tools. Section 7 includes some metrics of the HealthCard implementation and specification. Section 8 presents a short example of how a client-side of a smart card application can be implemented while respecting formal specifications. Section 9 describes a prototype tools to generate JML formal specifications from informal specifications automatically. Section 10 describes some challenges and main ideas came acrorss during the development of the HealthCard. The full formal specification and implementation of the HealthCard smart card application presented in this document can be reached at https://sourceforge.net/projects/healthcard/.

Development of a novel microextraction by packed sorbent-based approach followed by ultrahigh pressure liquid chromatography as a powerful technique for quantification phenolic constituents of biological interest in wines

A novel analytical approach, based on a miniaturized extraction technique, the microextraction by packed sorbent (MEPS), followed by ultrahigh pressure liquid chromatography (UHPLC) separation combined with a photodiode array (PDA) detection, has been developed and validated for the quantitative determination of sixteen biologically active phenolic constituents of wine. In addition to performing routine experiments to establish the validity of the assay to internationally accepted criteria (linearity, sensitivity, selectivity, precision, accuracy), experiments are included to assess the effect of the important experimental parameters on the MEPS performance such as the type of sorbent material (C2, C8, C18, SIL, and M1), number of extraction cycles (extract-discard), elution volume, sample volume, and ethanol content, were studied. The optimal conditions of MEPS extraction were obtained using C8 sorbent and small sample volumes (250 μL) in five extraction cycle and in a short time period (about 5 min for the entire sample preparation step). The wine bioactive phenolics were eluted by 250 μL of the mixture containing 95% methanol and 5% water, and the separation was carried out on a HSS T3 analytical column (100 mm × 2.1 mm, 1.8 μm particle size) using a binary mobile phase composed of aqueous 0.1% formic acid (eluent A) and methanol (eluent B) in the gradient elution mode (10 min of total analysis). The method gave satisfactory results in terms of linearity with r2-values > 0.9986 within the established concentration range. The LOD varied from 85 ng mL−1 (ferulic acid) to 0.32 μg mL−1 ((+)-catechin), whereas the LOQ values from 0.028 μg mL−1 (ferulic acid) to 1.08 μg mL−1 ((+)-catechin). Typical recoveries ranged between 81.1 and 99.6% for red wines and between 77.1 and 99.3% for white wines, with relative standard deviations (RSD) no larger than 10%. The extraction yields of the MEPSC8/UHPLC–PDA methodology were found between 78.1 (syringic acid) and 99.6% (o-coumaric acid) for red wines and between 76.2 and 99.1% for white wines. The inter-day precision, expressed as the relative standard deviation (RSD%), varied between 0.2% (p-coumaric and o-coumaric acids) and 7.5% (gentisic acid) while the intra-day precision between 0.2% (o-coumaric and cinnamic acids) and 4.7% (gallic acid and (−)-epicatechin). On the basis of analytical validation, it is shown that the MEPSC8/UHPLC–PDA methodology proves to be an improved, reliable, and ultra-fast approach for wine bioactive phenolics analysis, because of its capability for determining simultaneously in a single chromatographic run several bioactive metabolites with high sensitivity, selectivity and resolving power within only 10 min. Preliminary studies have been carried out on 34 real whole wine samples, in order to assess the performance of the described procedure. The new approach offers decreased sample preparation and analysis time, and moreover is cheaper, more environmentally friendly and easier to perform as compared to traditional methodologies.

Development of a scar marker for Pierce's Disease strains of Xylella fastidiosa

O objetivo deste trabalho foi desenvolver um oligonucleotídeo iniciador para reação em cadeia da polimerase (PCR) específico para as estirpes de Xylella fastidiosa que causam o mal de Pierce (PD) em videira (Vitis vinifera). Amplificações de DNA de 23 diferentes hospedeiros, usando o conjunto de oligonucleotídeos REP1-R (5'-IIIICGICGIATCCIGGC-3') e REP 2 (5'-ICGICTTATCI GGCCTAC-3') utilizando o programa: 94 ºC/2 min; 35 X (94 ºC/1 min, 45 ºC/1 min; 72 ºC/1 min and 30 s) 72 ºC/5 min, produziu um fragmento de 630 pb que diferenciou as estirpes de videiras dos demais. Entretanto, padrões de bandeamento REP não são considerados confiáveis para detecção devido ao par de oligonucleotídeos REP 1 e REP 2 corresponderem a seqüências repetitivas encontradas por todo o genoma bacteriano. Desse modo, o produto amplificado de 630 pb foi eluído do gel de agarose, purificado e seqüenciado. A informação da seqüência nucleotídica foi usada para identificar e sintetizar um oligonucleotídeo específico para o isolado de X. fastidiosa causadora do mal de Pierce denominado Xf-1 (5'-CGGGGGTGTAGGAGGGGTTGT-3'), que foi utilizado juntamente com o oligonucleotídeo REP-2 nas condições 94 ºC/2 min; 35 X (94 ºC/1 min, 62 ºC/1 min; 72 ºC/1 min and 30 s) 72 ºC/10 min. Os DNAs das estirpes de X. fastidiosa de outros hospedeiros [amêndoa (Prumus amygdalus), citros (Citrus spp.), café (Coffea arabica), olmo (Ulmus americana), amora (Morus rubra), carvalho (Quercus rubra), vinca (Catharantus roseus), ameixa (Prunus salicina) e ragweed (Ambrosia artemisiifolia)] e de bactérias Gram negativas e positivas foram submetidos a amplificação com o conjunto de oligonucleotídeos Xf-1/REP 2. Um fragmento, de aproximadamente 350 pb, foi amplificado apenas com o DNA de X. fastidiosa isolada de videira.

Weight and neuro-psycho-motor development in children discharged from neonatal intensive care unit

Background: Low birth weight affects child growth and development, requiring the intensive use of health services. There are conversely proportional associations between prematurity and academic performance around the world. In this study we evaluated factors involved in weight and neuropsychomotor profile in one and two years old discharged from Intensive Care Units (ICU).Methods/Design: We investigated 203 children from the ICU who were followed for 24 +/- 4 months. The research was conducted by collecting data from medical records of patients in a Follow-up program. We investigated the following variables: inadequate weight at one year old; inadequate weight at two years old and a severe neurological disorder at two years old.Results: We observed increase of almost 20% in the proportion of children which weighted between the 10th and 90th percentiles and decrease of around 40% of children below the 15th percentile, from one to two years old. In almost 60% of the cases neuropsychomotor development was normal at 2 years old, less than 15% of children presented abnormal development. Variables that remained influential for clinical outcome at 1 and 2 years old were related to birth weight and gestational age, except for hypoglycemia. Neurological examination was the most influential variable for severe neurological disturbance.Conclusion: Hypoglycemia was considered a new fact to explain inadequate weight. The results, new in Brazil and difficult in terms of comparison, could be used to identify risk factors and for a better approach of newborn discharged from ICUs.

Effect of Strength Training on Rate of Force Development in Older Women

Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq)

Effect of the juvenile hormone on the development of the mandibular gland in workers' pupae of Apis mellifera L. (Hymenoptera, Apidae)

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

Tensor3D: A computer graphics program to simulate 3D real-time deformation and visualization of geometric bodies

Tensor3D is a geometric modeling program with the capacity to simulate and visualize in real-time the deformation, specified through a tensor matrix and applied to triangulated models representing geological bodies. 3D visualization allows the study of deformational processes that are traditionally conducted in 2D, such as simple and pure shears. Besides geometric objects that are immediately available in the program window, the program can read other models from disk, thus being able to import objects created with different open-source or proprietary programs. A strain ellipsoid and a bounding box are simultaneously shown and instantly deformed with the main object. The principal axes of strain are visualized as well to provide graphical information about the orientation of the tensor's normal components. The deformed models can also be saved, retrieved later and deformed again, in order to study different steps of progressive strain, or to make this data available to other programs. The shape of stress ellipsoids and the corresponding Mohr circles defined by any stress tensor can also be represented. The application was written using the Visualization ToolKit, a powerful scientific visualization library in the public domain. This development choice, allied to the use of the Tcl/Tk programming language, which is independent on the host computational platform, makes the program a useful tool for the study of geometric deformations directly in three dimensions in teaching as well as research activities. (C) 2007 Elsevier Ltd. All rights reserved.

Molecular modeling databases: A new way in the search of protein targets for drug development

DBMODELING is a relational database of annotated comparative protein structure models and their metabolic, pathway characterization. It is focused on enzymes identified in the genomes of Mycobacterium tuberculosis and Xylella fastidiosa. The main goal of the present database is to provide structural models to be used in docking simulations and drug design. However, since the accuracy of structural models is highly dependent on sequence identity between template and target, it is necessary to make clear to the user that only models which show high structural quality should be used in such efforts. Molecular modeling of these genomes generated a database, in which all structural models were built using alignments presenting more than 30% of sequence identity, generating models with medium and high accuracy. All models in the database are publicly accessible at http://www.biocristalografia.df.ibilce.unesp.br/tools. DBMODELING user interface provides users friendly menus, so that all information can be printed in one stop from any web browser. Furthermore, DBMODELING also provides a docking interface, which allows the user to carry out geometric docking simulation, against the molecular models available in the database. There are three other important homology model databases: MODBASE, SWISSMODEL, and GTOP. The main applications of these databases are described in the present article. © 2007 Bentham Science Publishers Ltd.

Development of SCAR marker linked to stem canker resistance gene in soybean

Stem canker caused by the fungus Diaporthe phaseolorum f. sp. meridionalis is a disease that limits soybean cultivation. Phenotypic evaluations aiming at disease resistance require labor-intensive processes, as for instance handling and transport of phytopathogens. The use of DNA markers in the selective procedures eases certain phases, besides being practical, safe and reliable. A RAPD fragment of 588pb was identified among bulks of resistant and susceptible plants in the cross BR92-15454 (R) x IAC-11 (S). Through co-segregation, the distance between the resistance locus and the fragment was estimated at 7.4 ± 2.1 cM, with a Lodmax. of 23.072 (first year) and at 6.0 ± 3.4 cM with a Lodmax. of 7.806 (second year). The fragment was converted into a SCAR marker and digested with enzyme Hinc II, which made the classification in homozygous resistant, heterozygous resistant and susceptible plants possible. This SCAR marker is suitable for use in the improvement program conducted in Jaboticabal.

Development of an instrumentation system embedded on FPGA for real time measurement of mechanical vibrations in rotating machinery

The real-time monitoring of events in an industrial plant is vital, to monitor the actual conditions of operation of the machinery responsible for the manufacturing process. A predictive maintenance program includes condition monitoring of the rotating machinery, to anticipate possible conditions of failure. To increase the operational reliability it is thus necessary an efficient tool to analyze and monitor the equipments, in real-time, and enabling the detection of e.g. incipient faults in bearings. To fulfill these requirements some innovations have become frequent, namely the inclusion of vibration sensors or stator current sensors. These innovations enable the development of new design methodologies that take into account the ease of future modifications, upgrades, and replacement of the monitored machine, as well as expansion of the monitoring system. This paper presents the development, implementation and testing of an instrument for vibration monitoring, as a possible solution to embed in industrial environment. The digital control system is based on an FPGA, and its configuration with an open hardware design tool is described. Special focus is given to the area of fault detection in rolling bearings. © 2012 IEEE.

Resistance training for explosive and maximal strength: Effects on early and late rate of force development

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

Planting coconuts in Indian villages: ethnoecological aspects and evaluation of a "sustainable development" project

Apesar de cientistas e tomadores de decisão abraçarem o conceito geral de "desenvolvimento sustentável", há pouco acordo sobre como se atingir esta meta em situações específicas. Assim, projetos de desenvolvimento sustentável são amplamente criticados por etno-cientistas quanto à forma como são inter-culturalmente formulados. Aqui reportamos um caso controverso de plantio de coco-da-Bahia em aldeias Kayapó do sul do Pará, e fazemos a nossa autocrítica. Nós partimos da premissa de que o reflorestamento e o estado geral de saúde/nutrição caminham lado a lado. Portanto, o desenvolvimento da cultura de cocos por si só deve contribuir para a conservação da floresta no longo prazo e, simultaneamente, contribuir para o bom estado nutricional do povo Kayapó que protege a floresta da ameaça de práticas não-sustentáveis. Nós buscamos descobrir como que o comportamento dos Kayapó afeta o desenvolvimento da cultura de cocos quando amparada com suporte externo. Nós apresentamos resultados de duas viagens de campo para a terra Kayapó, onde detectamos fatores sócio-ecológicos relevantes para o sucesso de nosso projeto de apoio à cultura de coqueiros nas aldeias indígenas. Primeiro, em novembro de 2007, nós visitamos as aldeias Kikretum, Moikarakô e Aukre (dentre 10 aldeias que receberam mudas de coqueiros de nosso programa de apoio) para entregar um segundo carregamento de mudas de coqueiro (o primeiro carregamento aconteceu em abril de 2006). E descrevemos quantitativamente um aspecto do comportamento dos dispersores de sementes de coco (os Kayapó). Especificamente, como as palmeiras pré-existentes nas aldeias são distribuídas dentre as famílias dos índios e como este carregamento sobreviveu a fatores etno-ecológicos. Segundo, em julho de 2008 nós visitamos as aldeias Kokraimoro e Pykararankre e estimamos a posição dos coqueiros pré-existentes e dos novos em relação a outras árvores cultivadas, fazendo uso de censos partindo do centro das aldeias para seus limites exteriores. Nas três aldeias indígenas visitadas em 2007, virtualmente todos os coqueiros pré-existentes pertenciam a poucas famílias e a distribuição de frutos era, na maior parte dos casos, altamente concentrada dentre os membros destas famílias. Entretanto, assumindo que todos os coqueiros jovens que sobreviveram ao primeiro ano chegarão à maturidade (do primeiro carregamento em abril de 2006), eles representam um aumento considerável no numero projetado de coqueiros adultos nas três aldeias visitadas (48, 195 e 101% em Kikretum, Moikarakô e Aukre, respectivamente). E uma redução substancial na desigualdade de acesso aos cocos. Na expedição de 2008, encontramos que os índios geralmente plantam coqueiros bem próximos das suas casas onde a competição com outras árvores cultivadas podem limitar o desenvolvimento das palmeiras.

Intervention program efficacy for spelling difficulties

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