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.

Avaliação da sobrecarga do cuidador informal no desempenho de suas funções à pessoa idosa dependente, no Concelho de Santana

O processo de cuidar do idoso dependente é multidimensional e executado por cuidadores formais e informais. Sempre foi uma função designada à família onde havia divisão de tarefas entre os diversos membros,. O objetivo do estudo foi avaliar a sobrecarga dos cuidadores informais no desempenho de suas funções à pessoa idosa dependente, no concelho de Santana; estimando o nível de dependência dos idosos e determinando a satisfação, as dificuldades, o coping e a sobrecarga dos cuidadores. A população acessível foi constituída por 69 cuidadores informais. O estudo foi, transversal, descritivo - correlacional. O formulário inclui questões de caracterização sociodemográfica e escalas: de satisfação, de dificuldades em cuidar, e de estratégias de coping (Nolan et cols,1998), de percepção da sobrecarga do cuidador (adaptação de Zarit et cols,1983) validadas para Portugal (Sequeira 2007). Utilizou-se a Escala de Barthel (Mahoney; Barthel,1965) para determinar a dependência dos idosos. Dos resultados realçamos: a maioria dos cuidadores é mulher, casada, com escolaridade até o 6º ano, baixo nível sócio económico sendo familiar do idoso cuidado. Dos cuidadores, 38% são-no entre um a quatro anos e 72,5% cuidam 12 horas/dia A etapa do ciclo vital familiar dos cuidadores é o fim da vida (76,8% ). Dos idosos cuidados, 68% era muito dependente. Dificuldades no cuidar incluíram: restrições sociais, exigências e reações ao cuidar e estratégias de coping mais limitadas. Os cuidadores tendiam sentir-se satisfeitos com o cuidado. Não sofrem sobrecarga 36,3 % mas, 63,7% refere-a ligeira e intensa. Nos homens realçou-se a intensa e nas mulheres a ausência de sobrecarga. Ela foi mais significativa entre os analfabetos, os que sentiam dificuldades, os mais carenciados economicamente e que não gozavam de férias. Evidencia-se a importância da intervenção junto aos cuidadores informais por parte da rede formal de apoio para prevenção da sobrecarga.

Educação informal e movimentos populares: a importância do ensino da música no resgate da cidadania de crianças assistidas pela ONG Orquestra Cidadã como uma forma de inovação pedagógica

A presente pesquisa faz parte de nosso estudo realizado junto a Orquestra Cidadã Meninos do Coque e tem por objetivo principal refletir acerca de como o ensino da música com vistas ao resgate da cidadania de crianças e adolescentes assistidos pelo projeto da referida orquestra pode ser visto sob a égide da inovação pedagógica. Para isso, num primeiro momento, em seu arcabouço teórico, que compreendido pelos capítulos segundo e terceiro, inicialmente traçamos nossas considerações sobre a prática pedagógica e a educação não formal, visando à questão da inovação e da formação para cidadania; e, logo em seguida adentramos na questão do ensino de música e a construção da cidadania, tendo-se por foco o trabalho realizado pela Orquestra Cidadã Meninos do Coque. Já num segundo momento, tratamos das questões metodológicas (capítulo quarto), cuja base foi a etnopesquisa orientado por Macedo (2006), a qual teve como instrumentos a observação participante, o uso de entrevistas e de questionários semiestruturados, além da análise documental, cujos resultados são apresentados no capítulo quinto, o qual traz como título “Educação informal e movimentos populares: a importância do ensino da música no resgate da cidadania de crianças assistidas pela ONG Orquestra Cidadã como uma forma de inovação pedagógica” diante do qual pudemos perceber o caráter inovador do trabalho empreendido pela orquestra em estudo, que na busca de atingir os objetivos pretendidos expande sua metodologia para a realidade de seus alunos e com isso alcança saltos de desenvolvimento, trazendo para as crianças e jovens um novo olhar sobre si mesmos e sobre o seu futuro.