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

Touch ‘n’ sketch: pen and fingers on a multi-touch sketch application for tablet PC’s

In many creative and technical areas, professionals make use of paper sketches for developing and expressing concepts and models. Paper offers an almost constraint free environment where they have as much freedom to express themselves as they need. However, paper does have some disadvantages, such as size and not being able to manipulate the content (other than remove it or scratch it), which can be overcome by creating systems that can offer the same freedom people have from paper but none of the disadvantages and limitations. Only in recent years has the technology become massively available that allows doing precisely that, with the development in touch‐sensitive screens that also have the ability to interact with a stylus. In this project a prototype was created with the objective of finding a set of the most useful and usable interactions, which are composed of combinations of multi‐touch and pen. The project selected Computer Aided Software Engineering (CASE) tools as its application domain, because it addresses a solid and well‐defined discipline with still sufficient room for new developments. This was the result from the area research conducted to find an application domain, which involved analyzing sketching tools from several possible areas and domains. User studies were conducted using Model Driven Inquiry (MDI) to have a better understanding of the human sketch creation activities and concepts devised. Then the prototype was implemented, through which it was possible to execute user evaluations of the interaction concepts created. Results validated most interactions, in the face of limited testing only being possible at the time. Users had more problems using the pen, however handwriting and ink recognition were very effective, and users quickly learned the manipulations and gestures from the Natural User Interface (NUI).

Sistema de divulgação dos serviços e produtos da Porto Santo Line na plataforma Android

A Porto Santo Line é a empresa responsável pela ligação marítima entre as ilhas Madeira e Porto Santo, oferecendo, para além do transporte, um conjunto de serviços e produtos que estão associado à sua actividade principal. A sua base de clientes inclui não só os residentes de ambas as ilhas, mas também muitos dos turistas que visitam o arquipélago. O posicionamento desta empresa no mercado é feito das formas tradicionais, onde se inclui uma rede de balcões e um site através do qual os clientes podem aceder aos produtos e serviços que constitui a oferta da Porto Santo Line. Num esforço de reforçar a sua presença no mercado e de intensificar a sua aposta na inovação, a empresa tem procurado encontrar novas formas e novos canais para chegar aos seus clientes. Este projecto visa dotar a Porto Santo Line de uma aplicação que estenda a sua presença no mercado, oferecendo aos seus clientes a possibilidade de aceder aos seus produtos e serviços através de equipamentos móveis. Este relatório documenta a realização deste projecto, dando principal enfase ao processo adoptado, assim como ao desenho do sistema e sua avaliação. Procurou-se igualmente evidenciar ao longo do relatório, as considerações mais relevantes na elaboração de um projecto com estas características.

FXBus: uma aplicação móvel para combater a ansiedade de perder o autocarro

Os utilizadores de transportes públicos enfrentam dificuldades no seu dia-a-dia quando usam o autocarro para deslocar-se. Essas dificuldades passam por atrasos pessoais, por enganos na consulta dos horários das carreiras, entre outros, resultando na perda do autocarro. Este trabalho consistiu no desenvolvimento de uma aplicação móvel para a plataforma Android, tendo como principal objectivo fornecer ao utilizador uma ferramenta leve, rápida e útil para utilizar quando se encontra em movimento. O público-alvo desta aplicação são os utilizadores de transportes públicos da empresa Horários do Funchal, que necessitam de realizar deslocações frequentes, e não têm acesso constante à internet, dentro e fora de casa. Realizou-se uma pesquisa, através de um inquérito divulgado nas redes sociais, aos utilizadores de transportes públicos e, posteriormente, utilizou-se essa pesquisa no processo de brainstorming para construir as ideias para as funcionalidades da aplicação. Também se pesquisaram por outras aplicações com objectivos semelhantes e compararam-se essas com a aplicação desta dissertação. Posteriormente, implementou-se o primeiro protótipo e realizaram-se mais testes com novos utilizadores, que usaram a aplicação no seu dia-a-dia. Após se terem corregido os erros encontrados pelos utilizadores na aplicação, lançou-se uma versão beta online no mercado da Google Play. Os resultados obtidos com esta aplicação comprovam não só que existe a necessidade de uma aplicação destas no mercado, mas também permitiram ainda recolher dados sobre melhoramentos que podem ser feitos na mesma. Ao desenvolver esta aplicação pôde-se compreender as necessidades e as limitações que são impostas pelo cliente, como também colocar em prática os conhecimentos adquiridos ao longo do curso.

Sistema de gestão de rondas: aplicação android para empresas de segurança privada

Este é um relatório submetido como requisito parcial, para obtenção de grau de mestre em Engenharia Informática pela universidade da Madeira, em parceria com o Miti (Madeira Interactive Technologies Institute) e teve como base, o desenvolvimento de uma aplicação para equipamentos móveis com sistema operativo android. O objetivo principal foi, criar uma aplicação alternativa aos atuais sistemas existentes, para gestão e controlo de inspeções de segurança, efetuadas por funcionários de empresas de segurança privada (vigilantes) a instalações de clientes, atividade denominada por rondas. O principal problema encontrado e para o qual pretendia ser encontrada uma solução, não foi a falta de um sistema deste tipo, pois existem vários no mercado, mas sim, o elevado custo de aquisição dos atuais sistemas, aliado ao facto das suas limitações em termos de funcionalidades disponibilizadas tendo em conta esse elevado custo, e ainda a utilização de um equipamento dedicado e limitado exclusivamente a essa função. Conseguiu ser encontrada uma alternativa viável, versátil e prática, que para além de ser mais users friendly (termo utilizado para aplicações desenvolvidas tendo como foco o seu utilizador), disponibiliza aos seus utilizadores uma variedade de novas funcionalidades. Trata-se de uma alternativa muito mais económica mas igualmente eficaz, cumprindo assim o seu objetivo principal. Dadas as restrições temporais para o desenvolvimento deste projeto, são dadas no final deste documento, algumas ideias para uma possível evolução deste sistema, no sentido de o tornar ainda mais inovador.

XpressTrades: aplicação Android para troca de itens

As pessoas que gostam de comprar videojogos e livros, ao final de algum tempo, verificam que têm muitos destes itens armazenados e que já não os utilizam. Se estas pessoas não tiverem o intuito de criar uma coleção desses itens, irão, provavelmente se desfazer deles, por exemplo deitando-os fora. Neste contexto, apresenta-se uma aplicação para dispositivos móveis que possuam o sistema operativo Android, designada de XpressTrades. Esta aplicação visa resolver o problema descrito acima, tornando as trocas de jogos e de livros mais fácil, ajudando os seus utilizadores a reutilizarem os seus itens e a os utilizarem como moeda de troca. Juntamente com esta aplicação foi desenvolvida uma Web API, utilizando a framework ASP.NET, a qual é utilizada pela aplicação para esta poder funcionar. Embora este projeto de mestrado se tenha focado no desenvolvimento de uma aplicação especificamente para a troca de jogos e de livros, a aplicação foi desenhada e desenvolvida de forma modular e está preparada para ser estendida à troca de qualquer tipo de itens. A aplicação XpressTrades reúne diversas particularidades que tornarão as trocas de itens mais rápidas e eficientes. Algumas delas são: a apresentação da lista de proprietários ordenados por distância em relação ao utilizador e a apresentação de uma lista de itens recomendados com base no histórico de visualizações de itens realizadas pelo utilizador, ou seja, com base nos seus interesses. Relativamente à metodologia utilizada no desenvolvimento deste projeto, dado que a ideia surgiu do autor deste trabalho, recorreu-se primeiramente a inquéritos para se averiguar se as pessoas realmente revelavam interesse neste projeto e investigou-se também a existência de aplicações semelhantes. Seguidamente, utilizou-se a técnica de brainstorming para gerar as ideias e criou-se protótipos de baixa fidelidade para testar a interface de utilizador. Na fase de implementação, seguiu-se o seguinte ciclo para cada funcionalidade: prototipagem, testes com os utilizadores e correções dos erros detetados nos testes.

A multimodal tablet-based interface for designing and reviewing 3D engineering models

The ability to view and interact with 3D models has been happening for a long time. However, vision-based 3D modeling has only seen limited success in applications, as it faces many technical challenges. Hand-held mobile devices have changed the way we interact with virtual reality environments. Their high mobility and technical features, such as inertial sensors, cameras and fast processors, are especially attractive for advancing the state of the art in virtual reality systems. Also, their ubiquity and fast Internet connection open a path to distributed and collaborative development. However, such path has not been fully explored in many domains. VR systems for real world engineering contexts are still difficult to use, especially when geographically dispersed engineering teams need to collaboratively visualize and review 3D CAD models. Another challenge is the ability to rendering these environments at the required interactive rates and with high fidelity. In this document it is presented a virtual reality system mobile for visualization, navigation and reviewing large scale 3D CAD models, held under the CEDAR (Collaborative Engineering Design and Review) project. It’s focused on interaction using different navigation modes. The system uses the mobile device's inertial sensors and camera to allow users to navigate through large scale models. IT professionals, architects, civil engineers and oil industry experts were involved in a qualitative assessment of the CEDAR system, in the form of direct user interaction with the prototypes and audio-recorded interviews about the prototypes. The lessons learned are valuable and are presented on this document. Subsequently it was prepared a quantitative study on the different navigation modes to analyze the best mode to use it in a given situation.