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/.

A JML-Based strategy for incorporating formal specifications into the software development process

This thesis presents a JML-based strategy that incorporates formal specifications into the software development process of object-oriented programs. The strategy evolves functional requirements into a “semi-formal” requirements form, and then expressing them as JML formal specifications. The strategy is implemented as a formal-specification pseudo-phase that runs in parallel with the other phase of software development. What makes our strategy different from other software development strategies used in literature is the particular use of JML specifications we make all along the way from requirements to validation-and-verification.

Os desafios da educação hospitalar para além da escola formal: um estudo das práticas desses educadores

Orientador: Robson Luiz de França

Representações sociais de velhice em contexto de prestação formal de cuidados

Universidade da Madeira. Centro de Ciência e Tecnologia da Madeira

Avaliação do desenvolvimento neuropsicomotor em crianças na rede básica de saúde utilizando o teste de Denver II: identificação de fatores de risco materno

Alterations in the neuropsychomotor development of children are not rare and can manifest themselves with varying intensity at different stages of their development. In this context, maternal risk factors may contribute to the appearance of these alterations. A number of studies have reported that neuropsychomotor development diagnosis is not an easy task, especially in the basic public health network. Diagnosis requires effective, low-cost, and easy - to-apply procedures. The Denver Developmental Screening Test, first published in 1967, is currently used in several countries. It has been revised and renamed as the Denver II Test and meets the aforementioned criteria. Accordingly, the aim of this study was to apply the Denver II Test in order to verify the prevalence of suspected neuropsychomotor development delay in children between the ages of 0 and 12 months and correlate it with the following maternal risk factors: family income, schooling, age at pregnancy, drug use during pregnancy, gestational age, gestational problems, type of delivery and the desire to have children. For data collection, performed during the first 6 months of 2004, a clinical assessment was made of 398 children selected by pediatricians and the nursing team of each public health unit. Later, the parents or guardians were asked to complete a structured questionnaire to determine possible risk indicators of neuropsychomotor development delay. Finally the Denver II Developmental Screening Test (DDST) was applied. The data were analyzed together, using Statistical Package for Social Science (SPSS) software, version 6.1. The confidence interval was set at 95%. The Denver II Test yielded normal and questionable results. This suggests compromised neuropsychomotor development in the children examined and deserves further investigation. The correlation of the results with preestablished maternal risk variables (family income, mother s schooling, age at pregnancy, drug use during the pregnancy and gestational age) was strongly significant. The other maternal risk variables (gestational problems, type of delivery and desire to have children) were not significant. Using an adjusted logistic regression model, we obtained the estimate of the greater likelihood of a child having suspected neuropsychomotor development delay: a mother with _75 4 years of schooling, chronological age less than 20 years and a drug user during pregnancy. This study produced two manuscripts, one published in Acta Cirúrgica Brasileira , in which an analysis was performed of children with suspected neuropsychomotor development delay in the city of Natal, Brazil. The other paper (to be published) analyzed the magnitude of the independent variable maternal schooling associated to neuropsychomotor development delay, every 3 months during the first twelve months of life of the children selected.. The results of the present study reinforce the multifactorial characteristic of development and the cumulative effect of maternal risk factors, and show the need for a regional policy that promotes low-cost programs for the community, involving children at risk of neuropsychomotor development delay. Moreover, they suggest the need for better qualified health professionals in terms of monitoring child development. This was an inter- and multidisciplinary study with the integrated participation of doctors, nurses, nursing assistants and professionals from other areas, such as statisticians and information technology professionals, who met all the requirements of the Postgraduate Program in Health Sciences of the Federal University of Rio Grande do Norte

Cuidado formal em saúde bucal: percepção de senescentes

Ações promotoras de saúde e independência para pessoas idosas são indispensáveis. Compreender essa construção no cotidiano da provisão dos cuidados talvez estimule o desenvolvimento de capacitações ao bem estar nesta população. O objetivo deste estudo foi Identificar a repercussão da provisão do cuidado formal em saúde bucal na percepção de senescentes. Desenvolvemos uma pesquisa de base qualitativa com abordagem fenomenológica, onde realizamos entrevistas semiestruturadas e individuais com 30 pessoas de idade superior a 50 anos (22 mulheres e 08 homens), em um Centro de Convivência na cidade de Natal/Rio Grande do Norte, no nordeste do Brasil. Os relatos obtidos foram analisados em cinco estágios: transcrição dos discursos sem preocupação interpretativa; limpeza de erros linguísticos e repetições; leitura repetitiva e exaustiva para apreensão do sentido das informações coletadas; seleção das unidades significativas dos discursos, correspondendo aos trechos relevantes no horizonte do fenômeno em estudo; e compreensão da ideografia elaborada pelos participantes por grupos temáticos simbólicos. Assim, identificamos as essências temáticas de: determinante social e iniquidade em saúde bucal; e provisão de cuidados de saúde bucal e mal-estar físico, mental e social. Concluímos que a prestação de cuidados agregando abordagem humanístico-ética pode levar a vivências dignificantes no processo de envelhecimento, destacadamente quando estimula a promoção da segurança pessoal. O âmago desse trabalho descortina uma vertente multidisciplinar que perpassa a saúde, a educação e a ética

Criteria for analysis of the structure of electronic scientific journals

This paper is the result of the Masters dissertation studying the role and history of scientific communication, especially the changes that have occurred after the appearance of electronic communication and computer networks. This study showed that hypertext systems are increasingly being used in the scientific and academic world in the production of electronic journals; this makes it possible for the user to rapidly access information in their area. However, these systems need to be improved to help the user during search and access to information. Both printed journals migrating to electronic media, and the exclusively electronic journals should present the current quality indicators. The attempt was made to discover whether characteristics related to printed journals are being maintained in their electronic counterparts. For this, a prototype model was developed to analyze the structure of electronic scientific journals; it composes 14 criteria expressing aspects of quality for these journals. It includes elements of Website Information Architecture and those already in place in printed scientific journals in order to ensure that basic functions - archiving and dissemination - are maintained in electronic publishing. Each criterion consists of variables, which measure the maintenance of these functions both in the migrating printed journals and the exclusively electronic ones. This prototype model was used to analyze Ciência da Informação On-line and DataGramaZero - Revista de Ciência da Informação. Results indicate that this model is able to find out if the basic functions of archiving and dissemination are being maintained in electronic journals. Therefore, its implementation is justified in electronic journals. The model can help librarians, authors, and users of electronic journals to identify quality journals, and assist editors in developing their projects. The material from the study may be included in the preservice and inservice education of Information Science professionals and to support editors of scientific journals.

Uma análise sociodemográfica dos cuidadores formais de idosos institucionalizados no município de Natal/RN, 2012

The aging population and individual have been the subject of a multitude of studies nowadays. This is probably due to the impact of this phenomenon in various sectors of society, like social security, social assistance and public health. The process of aging of the individual imply the demand for specific services, considering the limitations and vulnerabilities of the individual at that stage of life cycle. The growth of the elderly contingent in the last decades raises challenges for policymakers, the family and also for the society at large. In this scenario, long-stay institutions for the elderly (LSIEs) appear as an option to aid and support the elderly and their family, assisting in all or part in the activities of daily living and self-care. Inside these LSIEs we find the professional responsible for the direct care of the elderly, the formal caregiver. In this context, this dissertation presents two main objectives: an analysis of the phenomenon of population aging in a given brazilian municipality Natal / RN, based on the Demographic Censuses of 2000 e 2010; and a social, demographic and economic characterization of the Formal caregiver for the institutionalized elderly in the municipality, evaluating aspects of his quality of life and also analyzing the institutions where they are inserted. Furthermore, we intend to identify demographic, socioeconomic and quality of life factors that are correlated with caregivers quitting the job. The data used in the second part of this work comes from the research project named Long-Stay Institutions for Elderly: abandonment or a family need? . This survey interviewed 92 caregivers in eleven LSIEs in Natal/RN. In the data treatment logistic regressions, cluster analysis and statistical tests were used. The survey revealed that aging in Natal is more pronounced in the older, more traditional districts: Petrópolis, Lagoa Seca and Tirol. It also allowed a broad characterization of the formal caregivers in LSIEs. Most of these professionals are female. The educational level is predominantly complete high school and more. Most caregivers reported being married or in union, or have ever been in a union. Family monthly income is under three times the minimum wage. The mean age is of 37.4 years. The mean time of work as a caregiver was 5.93 years. The associations showed that being woman, not being single, having caregiving training and physical limitations (regarding quality of life) are related to wanting to quit the caregiving job. As for the characterization of the LSIEs, it was found that the philanthropic ones are older and have most (62.5%) of the institutionalized elderly. The institutions managers gave social interaction and affinity with the elderly as the main criteria with which to evaluate and hire caregivers. It is intended with this study to contribute to improving the quality of life of the elderly and their caregiver, providing information on aspects of institutionalization of elderly both in the philanthropic and particular institutions, in Natal/RN; this dissertation may also be used as a starting point for later works

Expansão canavieira e ocupação formal em empresas sucroalcooleiras do Centro-Sul do Brasil, entre 2007 e 2009

Considerando-se a região Centro-Sul do Brasil e com base nos dados do Ministério do Trabalho e Emprego e do Ministério da Agricultura, Pecuária e Abastecimento, comparou-se a evoluçãoda produção sucroalcooleira comonúmero e tipos de pessoas formalmente ocupadas em empresas do setor, de 2007 a 2009. Nas empresas dedicadas ao cultivo da cana-de-açúcar, o número de pessoas ocupadas caiu nesses três anos, enquanto aumentava nas empresas dedicadas à produção de açúcareetanol.Quantoàscategoriasdeocupação,constatou-seaumentononúmero de pessoas ocupadas em atividades industriais, administrativas, de apoio ou não sucroalcooleiras, enquanto diminuíam as pessoas ocupadas na agricultura. Neste caso, houve redução dos trabalhadores canavieiros não qualificados e crescimento dos trabalhadores da mecanização agrícola, fatos associados à intensificação da adoção da colheita mecânica de cana-de-açúcar. Não ocorreu mudança expressiva na sazonalidade de emprego dos trabalhadores canavieiros não qualificados, que permaneceu muito alta. O aumento mais intenso da produção do que do número de pessoas ocupadas refletiu em indicadores de produtividade, com crescimento da relação da produção de cana-de-açúcar, tanto com o total de pessoas ocupadas, quanto com o número de trabalhadores canavieiros não qualificados. Também foi constatada redução significativa na relação desse grupo de trabalhadores com a área colhida com cana-de-açúcar.

Emprego formal na região nordeste brasileira: seus efeitos na inclusão social

This work aims to study the problem of the formal job in the Brazilian Northeast region and its effect in the social inclusion, taking for base the analysis of variables defined in the Atlas of Social Exclusion, which is based on the 2000 Brazilian Census, choosing the county as unit of analysis. As methodological options, an exploratory data analysis was performed, followed by multivariate statistical techniques, such as weighted multiple regression analysis, cluster analysis and exploratory analysis of spatial data. The results pointed out to low rates of formal job for the active age population as well as low indexes of social inclusion in the Northeast region of Brazil. A strong association of the formal job with the indicators of social inclusion under investigation, was evidenced (schooling, inequality, poverty, youth and income form government transfers), as well as a strong association of the formal job with the new index of social inclusion (IIS), modified from the IES. At the Federative Units, in which better levels of formal job had been found, good indexes of social inclusion are also observed. Highlights for the state of the Rio Grande do Norte, with the best conditions of life, and for the states of the Maranhão and Piauí, with the worst conditions. The situation of the Northeast region, facing the indicators under study, is very precarious, claiming for the necessity of emphasizing programs and governmental actions, specially directed to the raise of formal job levels of the region, reflecting, thus, in improvements on the income inequality, as well as in the social inclusion of the population of Northeastern natives.