Interactive interface for stress relief

Every time more we hear in our everyday statements like "I'm stressed!", "Don´t worry me more than I am." But in what sense can we use technology to combat these congestions that we deal with daily? Well, one way would be to use technology to create objects, systems or applications that can spoil us and preferably be imperceptible by the user and, for this we have the ubiquitous computing and nurturant technologies. The ubiquitous computing is increasingly discussed as well as ways to make your computer more subtle in the view of the user, which is subject of research and development. The use of technology as a source of relaxation and spoil us is a strand that is being explored in the context of nurturant technologies. Accordingly, this thesis is focused on the development of an object and several applications with which we can interact. The object and applications have the purpose to spoil us and help us relax after a long day at work or in some situation more stressful. The object developed employs technologies like the use of accelerometers and the applications developed employs communications between computers and Web cameras. This thesis begins with a brief introduction to the areas of research and others that we can include in this thesis, such as ubiquitous computing and the nurturant technologies, providing yet general information on stress and ways to mitigate it. Later is described some of the work already done and that influenced this thesis as well as the prototypes developed and the experiences performed, ending with a general conclusion and future work.

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

Interactive music visualization: implementation, realization and evaluation

This thesis describes all process of the development of music visualization, starting with the implementation, followed by realization and then evaluation. The main goal is to have to knowledge of how the audience live performance experience can be enhanced through music visualization. With music visualization is possible to give a better understanding about the music feelings constructing an intensive atmosphere in the live music performance, which enhances the connection between the live music and the audience through visuals. These visuals have to be related to the live music, furthermore has to quickly respond to live music changes and introduce novelty into the visuals. The mapping between music and visuals is the focus of this project, in order to improve the relationship between the live performance and the spectators. The implementation of music visualization is based on the translation of music into graphic visualizations, therefore at the beginning the project was based on the existent works. Later on, it was decided to introduce new ways of conveying music into visuals. Several attempts were made in order to discover the most efficient mapping between music and visualization so people can fully connect with the performance. Throughout this project, those attempts resulted in several music visualizations created for four live music performances, afterwards it was produced an online survey to evaluate those live performances with music visualization. In the end, all conclusions are presented based on the results of the online survey, and also is explained which music elements should be depicted in the visuals, plus how those visuals should respond to the selected music elements.