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

Factores determinantes na definição da estratégia de uma companhia aérea

Considerando a gestão estratégica como um meio de alcançar uma performance superior face aos seus competidores, torna-se, então, necessário identificar as fontes de rentabilidade para o negócio, para formular e implementar uma estratégia que delas retire os maiores proveitos. A análise estratégica proporciona um conjunto de conceitos, modelos e técnicas de avaliação, que permitem aos gestores tomarem decisões mais adequadas às necessidades percebidas. Na realidade as transformações sucessivas verificadas no ambiente competitivo e a um ritmo cada vez mais crescente colocam às empresas a exigência de responder apropriadamente ao mercado, de forma a garantirem a sustentabilidade e o sucesso da sua actividade. Esta conjuntura não é estranha à indústria do turismo, que tem assistido à emergência de novos modelos de negócio, à mudança das preferências dos consumidores, ao incremento da tecnologia e, em alguns sectores, à desregulamentação, com implicações directas ao nível da gestão. O presente trabalho de investigação centra o seu estudo na fase de formulação da estratégia, particularizando para o sector de transporte aéreo, pretendendo reconhecer os elementos intervenientes no sector de transporte aéreo, perceber as relações de interdependência estabelecidas entre estes e identificar, classificar e compreender os factores relevantes para as decisões estratégicas. Analisa-se o problema da identificação dos factores determinantes na definição da estratégia de uma companhia aérea, procurando verificar se estes são de ordem económica, política, tecnológica e sócio-demográfica ou se por outro lado são de natureza dos destinos turísticos. Para tal, recorreu-se à revisão bibliográfica sobre o estado da arte, dando enquadramento teórico ao presente estudo, à elaboração e análise de entrevistas realizadas aos dirigentes das companhias aéreas portuguesas a operar para a Madeira, que permitiram adquirir um maior conhecimento da visão da indústria. Deste processo proveio que as empresas pertencentes ao sector de transporte aéreo, à semelhança das empresas de outros sectores, consideram que a estratégia assume um papel determinante para o sucesso da sua actividade, pelo facto das companhias aéreas desenvolverem a sua acção no longo prazo e necessitarem da análise periódica de elementos com influência no seu negócio. Conclui-se que os factores determinantes na definição da estratégia de uma companhia aérea são de ordem económica, política, tecnológica e sócio-demográfica, porquanto são os elementos que darão sustentabilidade às transportadoras de aceder ao destino.

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

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