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

WalkNRide: contextualising feedback in physical activity trackers

Increasing levels of sedentarism and obesity, along with advances in sensor technologies have instigated a market for wearable activity trackers, electronic devices that sense users’ physical activity levels with the goals of self-monitoring and behaviour change. Nowadays, activity trackers are one of the most desirable technologies, making up for a market of over $230 million in 2013. However, despite the spike of users’ interest, activity trackers have been shown to lose their appeal over time, with a recent survey suggesting that one out of three users discard the tracker in the course of the first six months of use. The question we pose is: how can we design activity tracker so that users’ interests is sustained over the long term? Our design approach focuses on contextualising physical activity. We do this through sensing users’ locations and activities (such as being still, walking or commuting through a car, bus or other means) and thus providing innovative ways of presenting feedback on users. This thesis presents the design and evaluation of WalkNRide, a physical activity tracker for Google Android. Through a longitudinal field study of WalkNRide, we attempt to inquire into the factors that drive the adoption (or non-adoption) of the tool as well as the ways in which the use of the tool contributes towards habit formation.

Motivating sustainable goal choices and providing effective feedback

Overconsumption of natural resources and the associated environmental hazards are one of today’s most pressing global issues. In the western world, individual consumption in homes and workplaces is a key contributor to this problem. Reflecting the importance of individual action in this domain, this thesis focuses on studying and influencing choices related to sustainability and energy consumption made by people in their daily lives. There are three main components to this work. Firstly, this thesis asserts that people frequently make ineffective consumption reduction goal choices and attempts to understand the rationale for these poor choices by fitting them to goalsetting theory, an established theoretical model of behavior change. Secondly, it presents two approaches that attempt to influence goal choice towards more effective targets, one of which deals with mechanisms for goal priming and the other of which explores the idea that carefully designed toys can exert influence on children’s long term consumption behavior patterns. The final section of this thesis deals with the design of feedback to support the performance of environmentally sound activities. Key contributions surrounding goals include the finding that people choose easy sustainable goals despite immediate feedback as to their ineffectiveness and the discussion and study of goal priming mechanisms that can influence this choice process. Contributions within the design of value instilling toys include a theoretically grounded framework for the design of such toys and a completed and tested prototype toy. Finally, contributions in designing effective and engaging energy consumption feedback include the finding that negative feedback is best presented verbally compared with visually and this is exemplified and presented within a working feedback system. The discussions, concepts, prototypes and empirical findings presented in this work will be useful for both environmental psychologists and for HCI researchers studying eco-feedback.

Exploring the dimensions of eco-feedback in the wild

Worldwide reports about energy usage have noted the importance of the domestic energy consumption sector in the worldwide scenario. This fact motivated and supported the birth and spread of the so-called eco-feedback devices. Such devices provide information about individual or group energy consumption behavior with the goal of reducing the impact in the environment. Motivated by the body of work which questions the long term effectiveness of eco-feedback systems, this thesis focus on evaluating in-the-wild the long term usage of eco-feedback systems. We have conducted five long term studies with different eco-feedback systems designed to evaluate different dimensions in the design of eco-feedback plus two more focused short term studies aimed at studying concrete approaches. Our summary reports on the fact that the there is a novelty effect associated with ecofeedback systems in which the usage of these devices declines significantly after a month. We did not found evidence that the novelty effect is related to location or the type of information represented, nor that the decrease in the eco-feedback usage could lead to the consumption relapsing to values previous to the introduction of the eco-feedback. Our work has also generated other contributions related to the positioning of the feedback, using metaphors for representing the consumption and presenting information about the source of the energy in the feedback.