VirtualLabs@UMa: uma plataforma personalizável para a realização de actividades experimentais

Os presentes métodos de estudo complementar fora de aulas adequam-se a um contexto mais teórico onde alunos, necessitam somente de manuais escolares ou acesso a um computador para complementar os seus estudos e atingirem os objectivos. O mesmo não se enquadra para cadeiras ou contextos mais práticos como por exemplo química ou biologia. Nestes contextos normalmente necessitamos de um laboratório ou localização específica onde se encontra as condições mínimas para a realização destes exercícios ou ensino. Actualmente existem laboratórios virtuais que vêem suplantar esta necessidade, mas os nossos estudos indicam que estes não são capazes de se adaptar a novas actividades sendo necessário desenvolver um laboratório específico para cada actividade. Neste contexto, a principal contribuição desta dissertação de mestrado é a proposta e o desenvolvimento de uma aplicação de Realidade Virtual, que seja capaz de adaptar-se facilmente às novas actividades laboratoriais de forma a personalizar as tarefas a serem realizadas pelos alunos, e que possa ser acedido através da plataforma Moodle. A aplicação desenvolvida proporciona aos alunos uma melhor percepção da forma como a actividade será realizada e prepara-os para realiza-la com sucesso num ambiente real.

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

Implementação de um sistema autónomo para a geração de visualizações 3D de dados ambientais

Este trabalho foi realizado na Universidade da Madeira, no âmbito do Mestrado em Engenharia Informática, tendo como título “Implementação de um sistema autónomo para a geração de visualizações 3D de dados ambientais”. A visualização 3D tem vindo a ganhar terreno em áreas como o entretenimento, medicina, arquitetura e desenho de equipamentos, entre outros. Relativamente à visualização de dados ambientais (oceano e atmosfera) em 3D, esta é uma área pouco explorada. Como tal, foi proposto o estudo e criação de um sistema autónomo capaz de gerar imagens 3D de dados ambientais e disponibilizar as mesmas na web. O estudo iniciou-se com testes às ferramentas que permitem a visualização 3D de dados ambientais, de forma a escolher a que mais se adequa ao sistema a implementar. Após diversos testes às várias ferramentas, a que mais se destacou foi o IDV (Integrated Data Visualization), pelas suas funcionalidades e capacidade de ser executado de forma automática. A implementação do sistema foi efetuada ao longo de diversas etapas: pré-processamento dos dados; escolha das visualizações a disponibilizar na web; escrita do script responsável pelo processo; criação das páginas web para visualização das imagens e implementação de todo o sistema em ambiente Linux. Este sistema foi desenvolvido tendo em conta a adição de novas visualizações, assim como a alteração das visualizações existentes. A possibilidade de adicionar/alterar visualizações de forma simples também foi tida em conta, de forma a não ser necessário reestruturar todo o sistema.

tCAD: a 3D modeling application on a depth enhanced tabletop computer

Tabletop computers featuring multi-touch input and object tracking are a common platform for research on Tangible User Interfaces (also known as Tangible Interaction). However, such systems are confined to sensing activity on the tabletop surface, disregarding the rich and relatively unexplored interaction canvas above the tabletop. This dissertation contributes with tCAD, a 3D modeling tool combining fiducial marker tracking, finger tracking and depth sensing in a single system. This dissertation presents the technical details of how these features were integrated, attesting to its viability through the design, development and early evaluation of the tCAD application. A key aspect of this work is a description of the interaction techniques enabled by merging tracked objects with direct user input on and above a table surface.

3D reconstruction through photographs

Humans can perceive three dimension, our world is three dimensional and it is becoming increasingly digital too. We have the need to capture and preserve our existence in digital means perhaps due to our own mortality. We have also the need to reproduce objects or create small identical objects to prototype, test or study them. Some objects have been lost through time and are only accessible through old photographs. With robust model generation from photographs we can use one of the biggest human data sets and reproduce real world objects digitally and physically with printers. What is the current state of development in three dimensional reconstruction through photographs both in the commercial world and in the open source world? And what tools are available for a developer to build his own reconstruction software? To answer these questions several pieces of software were tested, from full commercial software packages to open source small projects, including libraries aimed at computer vision. To bring to the real world the 3D models a 3D printer was built, tested and analyzed, its problems and weaknesses evaluated. Lastly using a computer vision library a small software with limited capabilities was developed.