Execução de túneis nas formações vulcânicas da Ilha da Madeira: o caso do túnel 1 da nova ligação Vasco Gil-Fundoa à cota 500

Este trabalho pretende contribuir para um melhor conhecimento ao nível da execução de túneis em formações vulcânicas, mais especificamente na Ilha da Madeira, visto esta região ter sido nos últimos anos palco da construção de inúmeros túneis rodoviários, que forneceram novos dados, experiencias e metodologias na execução de túneis em maciços vulcânicos. Assim sendo, esta tese foca inicialmente a geologia da Ilha da Madeira com o objectivo de dar a conhecer as características litológicas das rochas que compõem os maciços vulcânicos assim como é feita uma abordagem à história e evolução dos túneis existentes na região, com realce para os vários tipos de túneis executados e para os acidentes mais comuns que acontecem durante a escavação neste tipo de maciços. Depois são abordados os estudos geológicos e geotécnicos que são indispensáveis antes do inicio da execução dos túneis e também os métodos de escavação utilizados em maciços vulcânicos. É ainda abordado o estudo das vibrações causadas pelo uso de explosivos na escavação de túneis visto ser o método mais usado na região. Por fim é relatado o acompanhamento realizado durante a execução de um túnel na Ilha da Madeira, com particular destaque ao estudo das vibrações causadas devido à detonação de explosivos.

A aplicabilidade duma ecotaxa em Porto Santo

As ilhas apresentam-se como casos muito especiais de exemplos de destinos turísticos em que nem sempre os seus recursos naturais permitem muita diversificação a nível económico, levando-as a escolher a via do turismo, como acontece no Porto Santo. Com uma população a abandonar a ilha, na sua maioria por falta de alternativas profissionais e económicas, este pequeno oásis no meio do Atlântico pertencente à Região Autónoma da Madeira,luta pelo seu lugar de destino “Sol & Mar” por excelência, mas tentado, à priori, diversificar, através de outras apostas que irão ser apontadas no capítulo 3. Será assim revelada a importância e o papel do turismo na “ilha dourada” e medir até que ponto a implementação duma ecotaxa seria bem-vinda entre os seus visitantes, e constatar a sua importância para a protecção do meio ambiente único. Numa altura em que o comportamento dos turistas e da população em geral está a mudar e a palavra sustentabilidade e ecologia começam a ter cada vez mais importância, este trabalho tem por objectivo analisar e apresentar resultados relativamente a uma alternativa inovadora para a protecção do meio ambiente daquela ilha: eventual aplicação duma ecotaxa.

Simulação do comportamento espectral de redes de período longo em fibra óptica

Esta tese é dedicada às redes de período longo, LPG’s, em fibra óptica, escritas por exposição a radiação ultravioleta (UV) ou por exposição a descargas eléctricas, e às suas aplicações em comunicações ópticas e em sistemas sensores. Numa primeira fase estudaram-se os aspectos teóricos fundamentais para a compreensão das LPG, nomeadamente os dois modelos matemáticos propostos na literatura, para a transmissão espectral de uma LPG, o modelo de duas camadas e o modelo de três camadas. Em seguida, estudou-se o deslocamento do comprimento de onda ressonante perante mudanças de parâmetros externos. Aqui, verificou-se que para variações da temperatura no exterior da LPG, o deslocamento do comprimento de onda ressonante é linear. Por outro lado, para variações de índice de refracção exterior, verificou-se que à medida que o índice exterior se aproxima dos valores do índice de refracção da bainha, o comprimento de onda ressonante tende para valores mais baixos. Por último, realizou-se um estudo da transmissão espectral de duas aplicações que envolvem LPG’s, nomeadamente dois tipos de interferómetros e filtros ópticos. Numa segunda fase, foi desenvolvida uma ferramenta de simulação destes modelos, que permitia não só a obtenção dos espectros de transmissão das LPG’s mas também a obtenção das curvas de phase matching em função do período da rede e do comprimento de onda ressonante. A aplicação permitia também a obtenção das curvas do deslocamento do comprimento de onda ressonante, perante variações do índice de refracção exterior ou da temperatura. Para além disso, essa ferramenta realiza a simulação dos espectros de transmissão de filtros ópticos e de interferómetros de Michelson e de Mach-Zehnder construídos com base em LPG’s. A última fase do trabalho, a componente laboratorial, foi realizada na Unidade de Optoelectrónica e Sistemas Electrónicos do INESC Porto, onde foram construídos e testados os dispositivos estudados anteriormente, com o intuito de validar a aplicação desenvolvida. A ferramenta de simulação demonstrou ser capaz de simular de forma adequada os diversos aspectos do comportamento das LPG’s que foram estudados. A comparação dos resultados obtidos permitiu concluir que o modelo mais correcto para o estudo das LPG’s é o modelo de três camadas, o que está de acordo com o esperado.

Argilas modificadas como catalisadores ácidos sólidos

Important bentonitic deposits are present in Porto Santo Island, part of the Madeira Archipelago. Several locations were selected and samples were collected and characterised. The bentonite obtained at Serra de Dentro (SD) was selected for further laboratorial work. The fine fraction of SD bentonite was purified using several methods and the sodium homoionic form was prepared. This was the starting material used in the three generic types of modifications: metal exchange, acid activation and pillaring. These modifications produce materials with markedly different acidic (e.g. Brönsted and/or Lewis acidity), textural (e.g. increase of the surface area and active site accessibility) or structural (e.g. creation of permanent porous structures) properties. The wide range of materials obtained (including reference clays counterparts) was characterised in terms of chemical, structural, textural and catalytic properties. Limonene is an important raw material produced in Portugal, and its aromatisation reaction was chosen for the catalytic characterisation of the clay catalysts prepared.

Padrões de aleatoriedade na modelação do acaso

A soma de variáveis aleatórias com número de parcelas é aleatório, para além do evidente interesse conceptual e teórico, tem larga ressonância na investigação do processo de risco e em processos de ramificação. Reformulamos a teoria de Panjer (1981), que permite o cálculo iterativo do risco agregado, com o recurso a valores médios de uniformes, descrevendo uma extensão da classe de Panjer, e estudando em detalhe a equação funcional que a caracteriza. Aplicamos essas ideias na caracterização de aleatoriedade discreta, exemplificando com o comportamento das fêmeas de pássaros que investem na promiscuidade de parceiros para garantir a diversidade genética da progénie, tendo no entanto o cuidado de manter as aparências de fidelidade, para garantir a cooperação do parceiro no sucesso da ninhada. Apresentamos as transformadas de Laplace e funções geradoras numa perspectiva que leva a uma introdção natural de transformadas de Pareto, cuja relevância exemplificamos.

Estudo e avaliação das componentes térmicas na utilização de energia em edifícios

Este trabalho tem por objectivo desenvolver eimplementar metodologias relacionadas com a temática de térmica de edifícos, no sentido dequantificar e optimizar as perdas e ganhos decalor e os consumos de energia associados aosedifícios. Com base na teoria de transferência de calor e massa, foram construídos programas de cálculo numérico para simular, em regime estacionário (permanente) e não estacionário (transiente), os fluxos de calor e a distribuição das temperaturas em diferentes tipos de paredes comummente encontradas em Portugal e em particular na Região Autónoma da Madeira. Estes resultados permitiram analisar a eficácia dos diversos tipos de paredes estudadas bem como o risco de condensação em algumas dessas situações. Para além deste estudo houve a preocupação de desenvolver uma metodologia de análise económica relacionada com a espessura de isolamento a aplicar. Foram igualmente estudadas algumas medições simples de conservação de energia cuja implementação em edifícios será facilmente ustificada atendendo aos baixos períodos de retorno de investimento geralmente associados a estas medidas. Como resultado deste trabalho foi desenvolvida uma ferramenta de cálculo cuja aplicaçãovai permitir não só estimar o risco decondensação mas igualmente o campo de temperaturas no interior das paredes ao longo do período de tempo considerado, visando a optimização de soluções de isolamento térmico versus condições de conforto recomendadas.

Sistema de interrogação de sensores bioquímicos

Este documento reporta as fases de concepção, desenvolvimento e teste de uma unidade autónoma de interrogação de sensores bioquímicos, de custo reduzido e de fácil utilização, baseado na espectroscopia no domínio das frequências. Com este protótipo, é possível efectuar medições de concentrações bioquímicas de diferentes compostos, de acordo com a cabeça sensora utilizada. Devido ao número e à complexidade dos equipamentos de bancada necessários num esquema tradicional, este tipo de medições pode implicar um custo bastante elevado. Daí a importância deste projecto no desenvolvimento de uma alternativa que seja economicamente viável, utilizando novas técnicas de medição. Inicialmente este projecto começou por uma pesquisa significativa dos componentes electrónicos necessários para o desenvolvimento do sistema, seguindo-se uma escolha detalhada do material, de acordo com as características desejadas para o sistema. Um dos factores mais relevantes deste trabalho foi a introdução da instrumentação virtual, utilizada para controlar por intermédio de uma placa de aquisição de dados (DAQ), as componentes electrónicas do sistema e na implementação de um “lock-in” virtual, sendo este responsável pela recuperação dos sinais “enterrados” no ruído de fundo. O sistema desenvolvido é composto pelos seguintes módulos: O módulo de alimentação, que fornece as tensões e correntes para o funcionamento do sistema, o módulo de geração e modulação utilizado para gerar o sinal modulador e fornecer corrente ao LED, o módulo de detecção e amplificação, que recebe e eleva o nível do sinal emitido pela amostra, e por fim, o módulo de controlo e processamento, que recolhe esse sinal através da DAQ e processa-o por intermédio do “lock-in” virtual. Para avaliar o desempenho do sistema de interrogação foi estudada a resposta de um complexo de rutênio luminescente a diferentes temperaturas. São apresentados resultados em que o sistema desenvolvido é comparado com um sistema padrão e caracterizado face aos parâmetros do “lock-in” virtual, demonstrando-se as suas possibilidades e limitações.

Sistema automático de prevenção de úlceras por pressão

As úlceras por pressão são um problema de saúde pública que tem vindo a centrar a atenção da comunidade científica da área da saúde. Em consonância, a prevenção constitui um aspecto fulcral do seu controlo. Esta dissertação centra-se na prevenção deste flagelo, desenvolvendo um protótipo para estudo da prevenção das úlceras por pressão através de sistemas de sensores. Um olhar sobre a temperatura corporal e a pressão, enquanto factores etiológicos, levou à construção de um sistema de monitorização destas variáveis. O sistema de monitorização é constituído pela matriz de sensores, pelo circuito de aquisição de dados da matriz, por um microcontrolador que percorre cada um dos nós da matriz, por um sistema de transmissão sem fios e um software de visualização dos dados da matriz. A matriz de sensores, aplicada numa superfície de contacto, cadeira ou cama, está associada a um computador e a um nó sensor sem fios, para que a informação relativa a cada doente possa ser visualizada local e remotamente. Local, porque os dados de temperatura e pressão podem ser acedidos na unidade de cuidados e remotamente, pois a informação enviada sem fios através de um nó XBee, pode ser acedida num computador central, noutra sala, permitindo a monitorização, interpretação e registo dos dados. São apresentadas, neste trabalho, as matrizes de temperatura, uma com 64 sensores (8x8), que serviu de base à construção do circuito de aquisição de dados, outra com 256 sensores (16x16) de temperatura e ainda uma matriz de pressão. Para a matriz de sensores de pressão de 16x16, foram construídos manualmente cada um dos 256 sensores. Foi criado o software de visualização dos dados, obtidos da matriz, utilizando o MatLab, através do qual o utilizador final do sistema poderá aceder aos dados gráfica e numericamente. A aplicação do sistema desenvolvido permitirá medir, em situação de contacto, as alterações da temperatura da pele e pressão, factores estes associados à detecção precoce de úlceras de pressão.

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

WebSketch

Actualmente o desenvolvimento de aplicações baseadas na Web é uma área em crescimento exponencial, graças aos benefícios que estas trouxeram consigo. Com a crescente utilização da Web e a sua evolução como plataforma, surgiram novas tecnologias que vieram revolucionar o desenvolvimento de aplicações sobre esta plataforma. Com interfaces mais ricas e consequentemente mais dinâmicas, este tipo de aplicações assemelham-se às típicas aplicações Desktop com a diferença que estão a ser executadas em um ambiente completamente distinto, um ambiente partilhado e de fácil acesso, sendo o browser a aplicação universal de acesso a qualquer aplicação Web. Designadas serviços, as aplicações Web fornecem funcionalidades semelhantes às das aplicações Desktop, sendo na maioria das vezes software gratuito. Sendo a Google a grande pioneira nesta área, outras grandes entidades viram aqui a oportunidade de distribuir o seu software de uma forma fácil e barata, ficando esta de imediato disponível a milhões de utilizadores. Embora as aplicações Web se assemelhem às aplicações Desktop, ao seu processo de desenvolvimento surgem um conjunto de novos desafios provocados pelo facto de estas se encontrarem em um ambiente completamente distinto.

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.

Inexpensive solution for real-time video and image stitching

Image stitching is the process of joining several images to obtain a bigger view of a scene. It is used, for example, in tourism to transmit to the viewer the sensation of being in another place. I am presenting an inexpensive solution for automatic real time video and image stitching with two web cameras as the video/image sources. The proposed solution relies on the usage of several markers in the scene as reference points for the stitching algorithm. The implemented algorithm is divided in four main steps, the marker detection, camera pose determination (in reference to the markers), video/image size and 3d transformation, and image translation. Wii remote controllers are used to support several steps in the process. The built‐in IR camera provides clean marker detection, which facilitates the camera pose determination. The only restriction in the algorithm is that markers have to be in the field of view when capturing the scene. Several tests where made to evaluate the final algorithm. The algorithm is able to perform video stitching with a frame rate between 8 and 13 fps. The joining of the two videos/images is good with minor misalignments in objects at the same depth of the marker,misalignments in the background and foreground are bigger. The capture process is simple enough so anyone can perform a stitching with a very short explanation. Although real‐time video stitching can be achieved by this affordable approach, there are few shortcomings in current version. For example, contrast inconsistency along the stitching line could be reduced by applying a color correction algorithm to every source videos. In addition, the misalignments in stitched images due to camera lens distortion could be eased by optical correction algorithm. The work was developed in Apple’s Quartz Composer, a visual programming environment. A library of extended functions was developed using Xcode tools also from Apple.

Meta, tracer - MOF with traceability

The following document proposes a traceability solution for model-driven development. There as been already previous work done in this area, but so far there has not been yet any standardized way for exchanging traceability information, thus the goal of this project developed and documented here is not to automatize the traceability process but to provide an approach to achieve traceability that follows OMG standards, making traceability information exchangeable between tools that follow the same standards. As such, we propose a traceability meta-model as an extension of MetaObject Facility (MOF)1. Using MetaSketch2 modeling language workbench, we present a modeling language for traceability information. This traceability information then can be used for tool cooperation. Using Meta.Tracer (our tool developed for this thesis), we enable the users to establish traceability relationships between different traceability elements and offer a visualization for the traceability information. We then demonstrate the benefits of using a traceability tool on a software development life cycle using a case study. We finalize by commenting on the work developed.