Caracteres (em Java)

O professor apresenta a utilização de caracteres nas linguagens de programação Java e C++. Ilustra como utilizar e tratar conjuntos de caracteres nas linguagens de programação.

Interface com o Usuário (em Java)

O professor apresenta interfaces orientadas a objetos na linguagem de programação Java. Ilustra como e quando são utilizadas as interfaces orientadas a objetos em Java.

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

Conversores DC-DC comutados de elevado rendimento para sensores de imagem

Nesta tese de mestrado em engenharia telecomunicações e redes de energia, fez-se um estudo sobre conversores DC-DC comutados de elevado rendimento para sensores de imagem. Onde o principal objetivo é que se desenvolva, em ambiente industrial, um conversor DC-DC de alto rendimento que seja capaz de criar uma tensão inferior à sua alimentação. De salientar que o conversor foi implementado, quase na totalidade, sob a forma de circuito integrado, na tecnologia CMOS 0,35 μm. A implementação deste trabalho foi realizada por meio de um estágio na empresa de sensores de imagem Awaiba. No desenvolvimento do conversor DC-DC inicializou-se o estudo com um regulador de condensadores comutados, com uma arquitetura simples, em que se verificou, através de simulações realizadas num software específico para circuitos integrados - Design Arquitect-IC, que este regulador, apesar de estabilizar a tensão de saída na pretendida, não apresentava alto rendimento, ficando pelos 62%. Na sequência do estudo, na tentativa de melhorar as características do regulador de condensadores comutados, desenvolveu-se um conversor DC-DC com um filtro passa baixo na saída. Verificou-se, através de simulação que este conversor apresentava um rendimento de 92%, onde a sua tensão de alimentação é de 3,3 V e consegue regular na sua saída uma tensão variável entre 1,4 V e 2,2 V, suportando uma corrente máxima de 200 mA. É de referir que o conversor desenvolvido apresenta um tempo de resposta de 20 μs quando ocorre um consumo de corrente com variação em escalão. Sendo um conversor adequado para alimentar sensores de imagem e com elevado rendimento.

Compressão de imagem e vídeo com controlador ARM

Este trabalho foi desenvolvido num estágio na empresa ABS GmbH sucursal em Portugal, e teve como foco a compressão de imagem e vídeo com os padrões JPEG e H.264, respetivamente. Foi utilizada a plataforma LeopardBoard DM368, com um controlador ARM9. A análise do desempenho de compressão de ambos os padrões foi realizada através de programas em linguagem C, para execução no processador DM368. O programa para compressão de imagem recebe como parâmetros de entrada o nome e a resolução da imagem a comprimir, e comprime-a com 10 níveis de quantização diferentes. Os resultados mostram que é possível obter uma velocidade de compressão até 73 fps (frames per second) para a resolução 1280x720, e que imagens de boa qualidade podem ser obtidas com rácios de compressão até cerca de 22:1. No programa para compressão de vídeo, o codificador está configurado de acordo com as recomendações para as seguintes aplicações: videoconferência, videovigilância, armazenamento e broadcasting/streaming. As configurações em cada processo de codificação, o nome do ficheiro, o número de frames e a resolução do mesmo representam os parâmetros de entrada. Para a resolução 1280x720, foram obtidas velocidades de compressão até cerca de 68 fps, enquanto para a resolução 1920x1088 esse valor foi cerca de 30 fps. Foi ainda desenvolvida uma aplicação com capacidades para capturar imagens ou vídeos, aplicar processamento de imagem, compressão, armazenamento e transmissão para uma saída DVI (Digital Visual Interface). O processamento de imagem em software permite melhorar dinamicamente as imagens, e a taxa média de captura, compressão e armazenamento é cerca de 5 fps para a resolução 1280x720, adequando-se à captura de imagens individuais. Sem processamento em software, a taxa sobe para cerca de 23 fps para a resolução 1280x720, sendo cerca de 28 fps para a resolução 1280x1088, o que é favorável à captura de vídeo.

JCML: A specification language for the runtime verification of Java Card programs

COSTA, Umberto Souza; MOREIRA, Anamaria Martins; MUSICANTE, Matin A.; SOUZA NETO, Plácido A. JCML: A specification language for the runtime verification of Java Card programs. Science of Computer Programming. [S.l]: [s.n], 2010.

Specification and Runtime Verification of Java Card Programs

COSTA, Umberto Souza da; MOREIRA, Anamaria Martins; MUSICANTE, Martin A. Specification and Runtime Verification of Java Card Programs. Electronic Notes in Theoretical Computer Science. [S.l:s.n], 2009.

O city marketing em Natal/RN e a construção da imagem da cidade

The growing importance of tourism in overall economic activity worldwide has favored the intensification of competition among cities that seek to create environments attractive to tourists and potential investors. It has been common practice to import characteristics of the business environment in the public management of cities. The city marketing is a key tool used by public leaders to promote a linkage between the tourism image and urban image and involves, in addition to promoting the image of the city, the planning of interventions in urban space, trying to formulate a positive image of the city able to facilitate the deployment of capital. This research seeks to understand the nature of city marketing as part of contemporary urban management and analyzes how is its application in decisions concerning the promotion of tourism in Natal/RN. The approach of this research is qualitative, exploratory and descriptive, in which respondents were the main leaders of two of the official tourism site, the Empresa Potiguar de Promoção Turística and the Secretaria Municipal de Turismo e Desenvolvimento Econômico. It was found that there is a strong articulation of public power with private enterprise in the design and conduct of the actions of urban marketing, that from the survey data show that the behavior of target markets provide guidelines for taking strategic decisions relating to tourism. Sun and sea are some key elements explored to form the image of Natal and to authorize the sale of the city as a tropical paradise. However, there is an increase in the diversification of tourism products, seeking to increase flow to the segments of ecotourism, adventure, business and culture. It s also growing the use of local culture as a tourism product, however, the cultural representation focuses on superficial values and does not bring to light the social and historical richness that the city has. Public authorities use the city marketing strategies as a means able to maximize the attractiveness of Natal urban space to investors, business groups and tourists. It can be observed that urban managers seek solutions that can continuously increase the tours, which often manifests in interventions that focus the tourist areas of the city, in oposition of those who do not contribute to a positive reading of the city, which ultimately generate the worsening of spacial and social inequalities