On the analysis of compensation correctness

One fundamental idea of service-oriented computing is that applications should be developed by composing already available services. Due to the long running nature of service interactions, a main challenge in service composition is ensuring correctness of transaction recovery. In this paper, we use a process calculus suitable for modelling long running transactions with a recovery mechanism based on compensations. Within this setting, we discuss and formally state correctness criteria for compensable processes compositions, assuming that each process is correct with respect to transaction recovery. Under our theory, we formally interpret self-healing compositions, that can detect and recover from faults, as correct compositions of compensable processes. Moreover, we develop an automated verification approach and we apply it to an illustrative case study.

Numerical 3D modeling of heat transfer in human tissues for microwave radiometry monitoring of Brown fat metabolismo

Background: Brown adipose tissue (BAT) plays an important role in whole body metabolism and could potentially mediate weight gain and insulin sensitivity. Although some imaging techniques allow BAT detection, there are currently no viable methods for continuous acquisition of BAT energy expenditure. We present a non-invasive technique for long term monitoring of BAT metabolism using microwave radiometry. Methods: A multilayer 3D computational model was created in HFSS™ with 1.5 mm skin, 3-10 mm subcutaneous fat, 200 mm muscle and a BAT region (2-6 cm3) located between fat and muscle. Based on this model, a log-spiral antenna was designed and optimized to maximize reception of thermal emissions from the target (BAT). The power absorption patterns calculated in HFSS™ were combined with simulated thermal distributions computed in COMSOL® to predict radiometric signal measured from an ultra-low-noise microwave radiometer. The power received by the antenna was characterized as a function of different levels of BAT metabolism under cold and noradrenergic stimulation. Results: The optimized frequency band was 1.5-2.2 GHz, with averaged antenna efficiency of 19%. The simulated power received by the radiometric antenna increased 2-9 mdBm (noradrenergic stimulus) and 4-15 mdBm (cold stimulus) corresponding to increased 15-fold BAT metabolism. Conclusions: Results demonstrated the ability to detect thermal radiation from small volumes (2-6 cm3) of BAT located up to 12 mm deep and to monitor small changes (0.5°C) in BAT metabolism. As such, the developed miniature radiometric antenna sensor appears suitable for non-invasive long term monitoring of BAT metabolism.

Análise de fadiga de uma ponte ferroviária com tabuleiro misto vigado sob ação de tráfego de mercadorias

A presente dissertação centra-se no estudo de fadiga de uma ponte ferroviária com tabuleiro misto vigado pertencente a uma via de transporte de mercadorias. O caso de estudo incide sobre a ponte ferroviária sobre o rio do Sonho, localizada na Estrada de Ferro de Carajás situada no nordeste do Brasil. Nesta linha circulam alguns dos maiores comboios de mercadoria do mundo com cerca de 3.7 km de extensão e com cargas por eixo superiores a 300 kN. Numa primeira fase apresentam-se diversas metodologias de análise da fadiga em pontes ferroviárias metálicas. É também descrita a ferramenta computacional FADBridge, desenvolvida em ambiente MATLAB, e que possibilita o cálculo sistematizado e eficiente do dano de fadiga em detalhes construtivos de acordo com as indicações dos eurocódigos. Em seguida são abordadas as metodologias numéricas utilizadas para a realização das análises dinâmicas do sistema ponte-comboio e os aspetos regulamentares a ter em consideração no dimensionamento de pontes ferroviárias. O modelo numérico de elementos finitos da ponte foi realizado com recurso ao programa ANSYS. Com base neste modelo foram obtidos os parâmetros modais, nomeadamente as frequências naturais e os modos de vibração, tendo sido também analisada a importância do efeito compósito via-tabuleiro e a influência do comportamento não linear do balastro. O estudo do comportamento dinâmico da ponte foi realizado por intermédio de uma metodologia de cargas móveis através da ferramenta computacional Train-Bridge Interaction (TBI). As análises dinâmicas foram efetuadas para a passagem dos comboios reais de mercadorias e de passageiros e para os comboios de fadiga regulamentares. Nestas análises foi estudada a influência dos modos de vibração globais e locais, das configurações de carga dos comboios e do aumento da velocidade de circulação, na resposta dinâmica da ponte. Por último, foi avaliado o comportamento à fadiga de diversos detalhes construtivos para os cenários de tráfego regulamentar e reais. Foi ainda analisada a influência do aumento da velocidade, da configuração de cargas dos comboios e da degradação da estrutura nos valores do dano por fadiga e da respetiva vida residual.

A metodologia BIM-FM aplicada a um caso prático

O crescente aumento da consciencialização da importância da fase de operação e manutenção, bem como a amplificação que a metodologia Building Information Modelling (BIM) tem obtido nos últimos anos, sugere uma necessidade de alterar a atual abordagem da gestão das instalações de forma a dotá-la das mais recentes inovações tecnológicas como seja a utilização do BIM. Os Building Information Models apresentam as características ideais para a integração da gestão das instalações, não só pela visualização do edifício, mas sobretudo pela potencialidade que a base de dados oferece, com informação referente a cada um dos componentes presentes e suas relações. O âmbito deste trabalho envolve assim a integração da gestão das instalações com o modelo BIM criado, representativo do edifício em estudo. Este trabalho começa com as definições do âmbito e dos objetivos que são propostos no Capítulo 1. No Capítulo 2, é elaborada uma pesquisa sobre o estado da arte atual de cada uma das metodologias BIM e FM, de forma a tomar conhecimento dos seus conceitos principais. Foi feito também um levantamento no campo do BIM-FM de forma a apurar as atuais soluções tecnológicas existentes, a forma como é feita a sua troca de informação e também alguns casos em que esta metodologia foi aplicada. Com base na informação recolhida sobre as metodologias e também nos casos práticos estudados, é realizado no Capítulo 3, capítulo central deste trabalho, a aplicação prática. A realização desta aplicação é dividida por 3 fases principais. Numa primeira fase é especificada e recolhida a informação necessária de ser obtida para a realização do modelo e a posterior aplicação do FM. A escolha da informação a recolher é feita ponderando todos os fatores existentes, mas de forma a cumprir os requisitos pedidos. Numa segunda fase, assente na compilação de informação recolhida anteriormente, realiza-se o modelo do edifício. A modelação, de forma a seguir o método de trabalho BIM é realizada por especialidades, sendo numa primeira fase realizada a especialidade de arquitetura e posteriormente, utilizando esse modelo como base, é feita a modelação das especialidades de águas, águas residuais, AVAC e eletricidade. Esta escolha foi também estimulada pela organização do software utilizado para a modelação, por módulos. Na última fase da aplicação do caso prático a informação inserida na fase de modelação do edifício é exportada para o software de FM, neste caso em específico, o IBM Maximo. Para a exportação destes dados foi utilizado o formato Construction Operations Building Information Exchange (COBie), de forma a garantir a integridade e conformidade da informação transferida. No Capítulo 4 deste trabalho são abordadas as especificidades relativas à informação existente, à modelação e à troca de dados entre o software de modelação e o software utilizado na gestão do edifício. São também sugeridos alguns temas para futuros desenvolvimentos com o intuito de ampliação dos campos de FM com o uso do modelo. O BIM-FM é um tema emergente na atualidade do BIM, sendo a sua utilização encarada como uma mais-valia ao processo BIM. A compilação da informação durante a fase de projeto e execução, aliada à existência do modelo torna a implementação do FM com o modelo BIM como uma sequência natural.

A behavioral analysis tool for models of software systems

Trabalho apresentado no âmbito do Mestrado em Engenharia Informática, como requisito parcial para obtenção do grau de Mestre em Engenharia Informática

Remote operation of embedded controllers designed using IOPT Petri-nets

This paper presents a new communication architecture to enable the remote control, monitoring and debug of embedded-system controllers designed using IOPT Petri nets. IOPT Petri nets and the related tools (http://gres.uninova.pt) have been used as a rapid prototyping and development framework, including model-checking, simulation and automatic code generation tools. The new architecture adds remote operation capabilities to the controllers produced by the automatic code generators, enabling quasi-real-time remote debugging and monitoring using the IOPT simulator tool. Furthermore, it enables the creation of graphical user interfaces for remote operation and the development of distributed systems where a Petri net model running on a central system supervises the actions of multiple remote subsystems. © 2015 IEEE.

Fast unsupervised extraction of endmembers spectra from hyperspectral data

Linear unmixing decomposes an hyperspectral image into a collection of re ectance spectra, called endmember signatures, and a set corresponding abundance fractions from the respective spatial coverage. This paper introduces vertex component analysis, an unsupervised algorithm to unmix linear mixtures of hyperpsectral data. VCA exploits the fact that endmembers occupy vertices of a simplex, and assumes the presence of pure pixels in data. VCA performance is illustrated using simulated and real data. VCA competes with state-of-the-art methods with much lower computational complexity.

Estratégia e implementação da certificação de sistemas de gestão de investigação, desenvolvimento e inovação (NP 4457) nas empresas em Portugal

Dissertação de Mestrado em Gestão Integrada da Qualidade, ambiente e Segurança

Toward a Run-Time Verification Framework for Real-Time Safety-Critical Systems

Presented at SEMINAR "ACTION TEMPS RÉEL:INFRASTRUCTURES ET SERVICES SYSTÉMES". 10, Apr, 2015. Brussels, Belgium.

Modeling assembly program with constraints. A contribution to WCET problem

Dissertação para obtenção do Grau de Mestre em Lógica Computacional

Development Process and Cognitive Testing of CARATkids - Control of Allergic Rhinitis and Asthma Test for Children

Background: Allergic rhinitis and asthma (ARA) are chronic inflammatory diseases of the airways that often coexist in children. The only tool to assess the ARA control, the Control of Allergic Rhinitis and Asthma Test (CARAT) is to be used by adults. We aimed to develop the Pediatric version of Control of Allergic Rhinitis and Asthma Test (CARATkids) and to test its comprehensibility in children with 4 to 12 years of age. Methods: The questionnaire development included a literature review of pediatric questionnaires on asthma and/or rhinitis control and two consensus meetings of a multidisciplinary group. Cognitive testing was carried out in a cross-sectional qualitative study using cognitive interviews. Results: Four questionnaires to assess asthma and none to assess rhinitis control in children were identified. The multidisciplinary group produced a questionnaire version for children with 17 questions with illustrations and dichotomous (yes/no) response format. The version for caregivers had 4-points and dichotomous scales. Twenty-nine children, 4 to 12 years old, and their caregivers were interviewed. Only children over 6 years old could adequately answer the questionnaire. A few words/expressions were not fully understood by children of 6 to 8 years old. The drawings illustrating the questions were considered helpful by children and caregivers. Caregivers considered the questionnaire complete and clear and preferred dichotomous over the 4-points scales. The proportion of agreement between children and their caregivers was 61%. The words/expressions that were difficult to understand were amended. Conclusion: CARATkids, the first questionnaire to assess a child’s asthma and rhinitis control was developed and its content validity was assured. Cognitive testing showed that CARATKids is well-understood by children 6 to 12 years old. The questionnaire’s measurement properties can now be assessed in a validation study.

A proof system for lock-free concurrency

Dissertação para obtenção do Grau de Mestre em Engenharia Informática

Continuidade de cuidados numa Unidade de Saúde Familiar : o efeito nos custos

RESUMO - Caracterização do problema: O sistema de saúde português atingiu um patamar de ineficiência tal que urge ser reestruturado de forma a torná-lo sustentável. De forma a atingir este nível de sustentabilidade, uma série de soluções podem ser consideradas das quais destacamos a integração de cuidados. Este conceito exige que os diferentes níveis de saúde sigam um único caminho, trabalhando de forma coordenada e contínua. A integração de cuidados pode ser implementada através de várias tipologias entre as quais se destaca a integração clínica que por sua vez é composta pela continuidade de cuidados. Assim, ao medir a continuidade de cuidados, quantifica-se de certa forma a integração de cuidados. Objetivos: Avaliar o impacto da continuidade de cuidados nos custos. Metodologia: Os dados foram analisados através de estatísticas descritivas para verificar o seu grau de normalidade. Posteriormente foram aplicados testes t-student para analisar a existência de diferenças estatisticamente significativas entre as médias das diferentes variáveis. Foi então estudado o grau de associação entre variáveis através da correlação de spearman. Por fim, foi utilizado o modelo de regressão log-linear para verificar a existência de uma relação entre as várias naturezas de custos e os índices de continuidade. Com base neste modelo foram simulados dois cenários para estimar o impacto da maximização da continuidade de cuidados nas várias naturezas de custos. Conclusões: No geral, verifica-se uma relação muito ligeira entre a continuidade de cuidados e os custos. Mais especificamente, uma relação mais duradoura entre o médico e o doente resulta numa poupança de custos, independentemente da tipologia. Analisando a densidade da relação, observa-se uma relação positiva entre a mesma e os custos totais e o custo com Meios Complementares de Diagnóstico e Terapêutica (MCDT). Contudo verifica-se uma relação médico-doente negativa entre a densidade e os custos com medicamentos e com pessoal. Ao analisar o impacto da continuidade de cuidados nos custos, conclui-se que apenas a duração da relação médico-doente tem um impacto negativo em todas as categorias de custos, exceto o custo com medicamentos. A densidade de cuidados tem um impacto negativo apenas no custo com pessoal, influenciando positivamente as outras categorias de custos. Extrapolando para o nível nacional se o nível de densidade de uma relação fosse maximizado, existiria uma poupança de 0,18 euros, por ano, em custos com pessoal.

The ambivalence of two-part tariffs for bottleneck access

Two-part tariffs, when used at the retail level, increase efficiency by lowering the price of marginal units. The same potential for higher efficiency exists for two-part tariffs at wholesale level for a given market structure, but the fixed part of the wholesale tariff can negatively affect the latter. In a simulated competition model of next-generation telecommunications access networks that has been calibrated with engineering cost data, we show that the latter effects strongly outweigh the former. That is, substituting a cost-based linear wholesale access tariff with revenue-equivalent two-part tariffs reduces the number of access seekers and therefore leads to higher prices and lower welfare and consumer surplus.

Local Development Initiatives in Metropolitan Areas' Suburban Municipalities: a comparative case-study between Amadora (Lisbon-PT) and Diadema (São Paulo-BR)

MARQUES, B.P. e CARVALHO, R. (2010) "Local Development Initiatives in Metropolitan Areas' Suburban Municipalities: a comparative case-study between Amadora (Lisbon-PT) and Diadema (São Paulo-BR)", in Actas do 16.º Congresso da APDR, Funchal, pp. 1053-1083, ISBN 978-989-96353-1-9.