Deciding Kleene Algebra Terms Equivalence in Coq

This paper presents a mechanically verified implementation of an algorithm for deciding the equivalence of Kleene algebra terms within the Coq proof assistant. The algorithm decides equivalence of two given regular expressions through an iterated process of testing the equivalence of their partial derivatives and does not require the construction of the corresponding automata. Recent theoretical and experimental research provides evidence that this method is, on average, more efficient than the classical methods based on automata. We present some performance tests, comparisons with similar approaches, and also introduce a generalization of the algorithm to decide the equivalence of terms of Kleene algebra with tests. The motivation for the work presented in this paper is that of using the libraries developed as trusted frameworks for carrying out certified program verification.

Soleus activity in post-stroke subjects: movement sequence from standing to sitting

O documento em anexo encontra-se na versão post-print (versão corrigida pelo editor).

Supporting intra-task parallelism in real-time multiprocessor systems

Os sistemas de tempo real modernos geram, cada vez mais, cargas computacionais pesadas e dinâmicas, começando-se a tornar pouco expectável que sejam implementados em sistemas uniprocessador. Na verdade, a mudança de sistemas com um único processador para sistemas multi- processador pode ser vista, tanto no domínio geral, como no de sistemas embebidos, como uma forma eficiente, em termos energéticos, de melhorar a performance das aplicações. Simultaneamente, a proliferação das plataformas multi-processador transformaram a programação paralela num tópico de elevado interesse, levando o paralelismo dinâmico a ganhar rapidamente popularidade como um modelo de programação. A ideia, por detrás deste modelo, é encorajar os programadores a exporem todas as oportunidades de paralelismo através da simples indicação de potenciais regiões paralelas dentro das aplicações. Todas estas anotações são encaradas pelo sistema unicamente como sugestões, podendo estas serem ignoradas e substituídas, por construtores sequenciais equivalentes, pela própria linguagem. Assim, o modo como a computação é na realidade subdividida, e mapeada nos vários processadores, é da responsabilidade do compilador e do sistema computacional subjacente. Ao retirar este fardo do programador, a complexidade da programação é consideravelmente reduzida, o que normalmente se traduz num aumento de produtividade. Todavia, se o mecanismo de escalonamento subjacente não for simples e rápido, de modo a manter o overhead geral em níveis reduzidos, os benefícios da geração de um paralelismo com uma granularidade tão fina serão meramente hipotéticos. Nesta perspetiva de escalonamento, os algoritmos que empregam uma política de workstealing são cada vez mais populares, com uma eficiência comprovada em termos de tempo, espaço e necessidades de comunicação. Contudo, estes algoritmos não contemplam restrições temporais, nem outra qualquer forma de atribuição de prioridades às tarefas, o que impossibilita que sejam diretamente aplicados a sistemas de tempo real. Além disso, são tradicionalmente implementados no runtime da linguagem, criando assim um sistema de escalonamento com dois níveis, onde a previsibilidade, essencial a um sistema de tempo real, não pode ser assegurada. Nesta tese, é descrita a forma como a abordagem de work-stealing pode ser resenhada para cumprir os requisitos de tempo real, mantendo, ao mesmo tempo, os seus princípios fundamentais que tão bons resultados têm demonstrado. Muito resumidamente, a única fila de gestão de processos convencional (deque) é substituída por uma fila de deques, ordenada de forma crescente por prioridade das tarefas. De seguida, aplicamos por cima o conhecido algoritmo de escalonamento dinâmico G-EDF, misturamos as regras de ambos, e assim nasce a nossa proposta: o algoritmo de escalonamento RTWS. Tirando partido da modularidade oferecida pelo escalonador do Linux, o RTWS é adicionado como uma nova classe de escalonamento, de forma a avaliar na prática se o algoritmo proposto é viável, ou seja, se garante a eficiência e escalonabilidade desejadas. Modificar o núcleo do Linux é uma tarefa complicada, devido à complexidade das suas funções internas e às fortes interdependências entre os vários subsistemas. Não obstante, um dos objetivos desta tese era ter a certeza que o RTWS é mais do que um conceito interessante. Assim, uma parte significativa deste documento é dedicada à discussão sobre a implementação do RTWS e à exposição de situações problemáticas, muitas delas não consideradas em teoria, como é o caso do desfasamento entre vários mecanismo de sincronização. Os resultados experimentais mostram que o RTWS, em comparação com outro trabalho prático de escalonamento dinâmico de tarefas com restrições temporais, reduz significativamente o overhead de escalonamento através de um controlo de migrações, e mudanças de contexto, eficiente e escalável (pelo menos até 8 CPUs), ao mesmo tempo que alcança um bom balanceamento dinâmico da carga do sistema, até mesmo de uma forma não custosa. Contudo, durante a avaliação realizada foi detetada uma falha na implementação do RTWS, pela forma como facilmente desiste de roubar trabalho, o que origina períodos de inatividade, no CPU em questão, quando a utilização geral do sistema é baixa. Embora o trabalho realizado se tenha focado em manter o custo de escalonamento baixo e em alcançar boa localidade dos dados, a escalonabilidade do sistema nunca foi negligenciada. Na verdade, o algoritmo de escalonamento proposto provou ser bastante robusto, não falhando qualquer meta temporal nas experiências realizadas. Portanto, podemos afirmar que alguma inversão de prioridades, causada pela sub-política de roubo BAS, não compromete os objetivos de escalonabilidade, e até ajuda a reduzir a contenção nas estruturas de dados. Mesmo assim, o RTWS também suporta uma sub-política de roubo determinística: PAS. A avaliação experimental, porém, não ajudou a ter uma noção clara do impacto de uma e de outra. No entanto, de uma maneira geral, podemos concluir que o RTWS é uma solução promissora para um escalonamento eficiente de tarefas paralelas com restrições temporais.

Constructing and Using Multimodal Narratives to Research in Science Education: Contributions Based on Practical Classroom

This study deals with the problem of how to collect genuine and useful data about science classroom practices, and preserving the complex and holistic nature of teaching and learning. Additionally, we were looking for an instrument that would allow comparability and verifiability for teaching and research purposes. Given the multimodality of teaching and learning processes, we developed the multimodal narrative (MN), which describes what happens during a task and incorporates data such as examples of students’ work.

Adhesion and wear behaviour of NCD coatings on Si3N4 by micro-abrasion tests

Nanocrystalline diamond (NCD) coatings offer an excellent alternative for tribological applications, preserving most of the intrinsic mechanical properties of polycrystalline CVD diamond and adding to it an extreme surface smoothness. Silicon nitride (Si3N4) ceramics are reported to guarantee high adhesion levels to CVD microcrystalline diamond coatings, but the NCD adhesion to Si3N4 is not yet well established. Micro-abrasion tests are appropriate for evaluating the abrasive wear resistance of a given surface, but they also provide information on thin film/substrate interfacial resistance, i.e., film adhesion. In this study, a comparison is made between the behaviour of NCD films deposited by hot-filament chemical vapour deposition (HFCVD) and microwave plasma assisted chemical vapour deposition (MPCVD) techniques. Silicon nitride (Si3N4) ceramic discs were selected as substrates. The NCD depositions by HFCVD and MPCVD were carried out using H2–CH4 and H2–CH4–N2 gas mixtures, respectively. An adequate set of growth parameters was chosen for each CVD technique, resulting in NCD films having a final thickness of 5 m. A micro-abrasion tribometer was used, with 3 m diamond grit as the abrasive slurry element. Experiments were carried out at a constant rotational speed (80 r.p.m.) and by varying the applied load in the range of 0.25–0.75 N. The wear rate for MPCVD NCD (3.7±0.8 × 10−5 m3N−1m−1) is compatible with those reported for microcrystalline CVD diamond. The HFCVD films displayed poorer adhesion to the Si3N4 ceramic substrates than the MPCVD ones. However, the HFCVD films show better wear resistance as a result of their higher crystallinity according to the UV Raman data, despite evidencing premature adhesion failure.

Consistency and Context Management in a Multi Agent Belief Revision Testbed

Multi-agent architectures are well suited for complex inherently distributed problem solving domains. From the many challenging aspects that arise within this framework, a crucial one emerges: how to incorporate dynamic and conflicting agent beliefs? While the belief revision activity in a single agent scenario is concentrated on incorporating new information while preserving consistency, in a multi-agent system it also has to deal with possible conflicts between the agents perspectives. To provide an adequate framework, each agent, built as a combination of an assumption based belief revision system and a cooperation layer, was enriched with additional features: a distributed search control mechanism allowing dynamic context management, and a set of different distributed consistency methodologies. As a result, a Distributed Belief Revision Testbed (DiBeRT) was developed. This paper is a preliminary report presenting some of DiBeRT contributions: a concise representation of external beliefs; a simple and innovative methodology to achieve distributed context management; and a reduced inter-agent data exchange format.

Environmental Decision Support: a Distributed Artificial Intelligence Approach

Decision making in any environmental domain is a complex and demanding activity, justifying the development of dedicated decision support systems. Every decision is confronted with a large variety and amount of constraints to satisfy as well as contradictory interests that must be sensibly accommodated. The first stage of a project evaluation is its submission to the relevant group of public (and private) agencies. The individual role of each agency is to verify, within its domain of competence, the fulfilment of the set of applicable regulations. The scope of the involved agencies is wide and ranges from evaluation abilities on the technical or economical domains to evaluation competences on the environmental or social areas. The second project evaluation stage involves the gathering of the recommendations of the individual agencies and their justified merge to produce the final conclusion. The incorporation and accommodation of the consulted agencies opinions is of extreme importance: opinions may not only differ, but can be interdependent, complementary, irreconcilable or, simply, independent. The definition of adequate methodologies to sensibly merge, whenever possible, the existing perspectives while preserving the overall legality of the system, will lead to the making of sound justified decisions. The proposed Environmental Decision Support System models the project evaluation activity and aims to assist developers in the selection of adequate locations for their projects, guaranteeing their compliance with the applicable regulations.

Localização da página web da VisionSpace – do inglês ao francês

Trabalho de Projeto apresentado ao Instituto de Contabilidade e Administração do Porto para a obtenção do grau de Mestre em Tradução e Interpretação Especializadas, sob orientação do Doutor Manuel Moreira da Silva e coorientação da Mestre Isabelle Tulekian

Seasonal patterns of polycyclic aromatic hydrocarbons in digestive gland and arm of octopus (Octopus vulgaris) from the Northwest Atlantic

Among organic pollutants existing in coastal areas, polycyclic aromatic hydrocarbons (PAHs) are of great concern due to their ubiquity and carcinogenic potential. The aim of this study was to evaluate the seasonal patterns of PAHs in the digestive gland and arm of the common octopus (Octopus vulgaris) from the Northwest Atlantic Portuguese coast. In the different seasons, 18 PAHs were determined and the detoxification capacity of the species was evaluated. Ethoxyresorufin O-deethylase (EROD) and ethoxycoumarin O-deethylase (ECOD) activities were measured to assess phase I biotransformation capacity. Individual PAH ratios were used for major source (pyrolytic/petrogenic) analysis. Risks for human consumption were determined by the total toxicity equivalence approach. Generally, low levels of PAHs were detected in the digestive gland and in the arm of octopus, with a predominance of low molecular over high molecular weight compounds. PAHs exhibited seasonality in the concentrations detected and in their main emission sources. In the digestive gland, the highest total PAH levels were observed in autumn possibly related to fat availability in the ecosystem and food intake. The lack of PAH elimination observed in the digestive gland after captivity could be possibly associated to a low biotransformation capacity, consistent with the negligible/undetected levels of EROD and ECOD activity in the different seasons. The emission sources of PAHs found in the digestive gland varied from a petrogenic profile observed in winter to a pyrolytic pattern in spring. In the arm, the highest PAH contents were observed in June; nevertheless, levels were always below the regulatory limits established for food consumption. The carcinogenic potential calculated for all the sampling periods in the arm were markedly lower than the ones found in various aquatic species from different marine environments. The results presented in this study give relevant baseline data for environmental monitoring of organic pollution in coastal areas.

Localização de ontologias - elementos para a construção de uma abordagem

O desenvolvimento de recursos multilingues robustos para fazer face às exigências crescentes na complexidade dos processos intra e inter-organizacionais é um processo complexo que obriga a um aumento da qualidade nos modos de interacção e partilha dos recursos das organizações, através, por exemplo, de um maior envolvimento dos diferentes interlocutores em formas eficazes e inovadoras de colaboração. É um processo em que se identificam vários problemas e dificuldades, como sendo, no caso da criação de bases de dados lexicais multilingues, o desenvolvimento de uma arquitectura capaz de dar resposta a um conjunto vasto de questões linguísticas, como a polissemia, os padrões lexicais ou os equivalentes de tradução. Estas questões colocam-se na construção quer dos recursos terminológicos, quer de ontologias multilingues. No caso da construção de uma ontologia em diferentes línguas, processo no qual focalizaremos a nossa atenção, as questões e a complexidade aumentam, dado o tipo e propósitos do artefacto semântico, os elementos a localizar (conceitos e relações conceptuais) e o contexto em que o processo de localização ocorre. Pretendemos, assim, com este artigo, analisar o conceito e o processo de localização no contexto dos sistemas de gestão do conhecimento baseados em ontologias, tendo em atenção o papel central da terminologia no processo de localização, as diferentes abordagens e modelos propostos, bem como as ferramentas de base linguística que apoiam a implementação do processo. Procuraremos, finalmente, estabelecer alguns paralelismos entre o processo tradicional de localização e o processo de localização de ontologias, para melhor o situar e definir.

CPMD-mindful task assignment for NPS-F

The multiprocessor scheduling scheme NPS-F for sporadic tasks has a high utilisation bound and an overall number of preemptions bounded at design time. NPS-F binpacks tasks offline to as many servers as needed. At runtime, the scheduler ensures that each server is mapped to at most one of the m processors, at any instant. When scheduled, servers use EDF to select which of their tasks to run. Yet, unlike the overall number of preemptions, the migrations per se are not tightly bounded. Moreover, we cannot know a priori which task a server will be currently executing at the instant when it migrates. This uncertainty complicates the estimation of cache-related preemption and migration costs (CPMD), potentially resulting in their overestimation. Therefore, to simplify the CPMD estimation, we propose an amended bin-packing scheme for NPS-F allowing us (i) to identify at design time, which task migrates at which instant and (ii) bound a priori the number of migrating tasks, while preserving the utilisation bound of NPS-F.

Reabilitação sustentável em edifícios habitacionais com valor histórico

Mestrado em Engenharia Civil – Ramo Construções

Acetyl-L-Carnitine Prevents Methamphetamine-Induced Structural Damage on Endothelial Cells via ILK-Related MMP-9 Activity

Methamphetamine (METH) is a potent psychostimulant highly used worldwide. Recent studies evidenced the involvement of METH in the breakdown of the blood-brain-barrier (BBB) integrity leading to compromised function. The involvement of the matrix metalloproteinases (MMPs) in the degradation of the neurovascular matrix components and tight junctions (TJs) is one of the most recent findings in METH-induced toxicity. As BBB dysfunction is a pathological feature of many neurological conditions, unveiling new protective agents in this field is of major relevance. AcetylL-carnitine (ALC) has been described to protect the BBB function in different paradigms, but the mechanisms underling its action remain mostly unknown. Here, the immortalized bEnd.3 cell line was used to evaluate the neuroprotective features of ALC in METH-induced damage. Cells were exposed to ranging concentrations of METH, and the protective effect of ALC 1 mM was assessed 24 h after treatment. F-actin rearrangement, TJ expression and distribution, and MMPs activity were evaluated. Integrin-linked kinase (ILK) knockdown cells were used to assess role of ALC in ILK mediated METHtriggered MMPs’ activity. Our results show that METH led to disruption of the actin filaments concomitant with claudin-5 translocation to the cytoplasm. These events were mediated by MMP-9 activation in association with ILK overexpression. Pretreatment with ALC prevented METH-induced activation of MMP-9, preserving claudin-5 location and the structural arrangement of the actin filaments. The present results support the potential of ALC in preserving BBB integrity, highlighting ILK as a new target for the ALC therapeutic use.

Problemas associados à instalação de subestações de energia em malha urbana. Caso de estudo da subestação de parceiros em Leiria

No âmbito do desenvolvimento da dissertação do Mestrado de Engenharia Eletrotécnica – Sistemas Elétricos de Energia, surgiu a oportunidade de participar no desenvolvimento de um projeto integrante numa subestação de energia. O presente caso de estudo tem em vista a resolução de condicionantes na conceção desta subestação, tais como cumprir requisitos estéticos projetando todo o tipo de equipamentos dentro de edifícios, a ventilação das salas de transformação assim como insonorização de todo o ruído produzido de forma a cumprir os limites legais e não perturbar a vizinhança. A presente subestação de energia está situada numa zona urbana da cidade de Leiria, localidade de Parceiros, dando origem ao nome Subestação de Energia de Parceiros. Esta subestação pertence ao cliente Energias de Portugal, conhecida como EDP, e visa o melhoramento da distribuição do serviço eléctrico. As tradicionais subestações de energia, com aparência bastante desenquadrada dos meios urbanos, representam um entrave ao nível da aproximação destes centros de produção energética às zonas urbanas, comprometendo a melhoria da rede elétrica. Desta forma, foi implementada a tecnologia Gas-Insolated Switchgear e permite o enquadramento destes centros energéticos em zonas urbanas, constituindo mais um edifício urbano na zona onde se insere. Esta substitui os convencionais barramentos existentes nos Parques Exteriores de Aparelhagem das subestações e apresenta-se com dimensões muito reduzidas quando comparadas com as estruturas instaladas nestes parques. Dado que esta tecnologia é desenvolvida no sentido de permitir a construção destes centros energéticos em zonas urbanas, podem ser alojadas dentro de edifícios produzindo assim vantagens ao nível estético, não perturbando a paisagem. Dado que os principais equipamentos de funcionamento na subestação de Parceiros, nomeadamente o Transformador de Potência, se encontram instalados num edifício completamente fechado, foram construídas duas salas de ventilação, na parte superior deste edifício, cada uma adjacente a uma sala de transformação. O transformador instalado possui elevadas dimensões, pesando 53000 kg e contendo 11000 kg de óleo que em estado normal de funcionamento circula por quase todo o interior da máquina a elevadas temperaturas, provocando um aquecimento elevado no interior do edifício o que condiciona o bom funcionamento do transformador. Para ultrapassar esta condicionante foi realizado um estudo de um sistema de ventilação capaz de avaliar e controlar os valores térmicos existentes e proceder à circulação de ar, que será movimentado ou bloqueado, recorrendo a um sistema autónomo, mantendo a temperatura ideal nas salas de transformação. Este autómato é o cérebro de toda a cadeia lógica que, mediante as leituras efetuadas irá dar ordens de atuação aos diversos equipamentos. Apesar dos TP estarem protegidos dentro do edifício, estes produzem um maior ruído. A necessidade da existência do referido sistema de ventilação das divisões de funcionamento destas máquinas, implica a utilização de aparelhos que, apesar da sua evolução tecnológica os torna cada vez menos ruidosos, mas geram sempre alguma perturbação, o que pode representar um problema no cumprimento do regulamento geral do ruído.

Contributo da manutenção técnica de edifícios para a sustentabilidade

A manutenção, durante vários anos, traduziu-se num conceito paliativo de instalações e equipamentos, o que se veio a revelar como uma atitude negligente perante o Homem e o Ambiente. As preocupações ambientais estão na ordem do dia e têm sido muitas as vozes que se têm levantado para que o consumo de energia seja mais equilibrado e para que as emissões de CO2 diminuam de forma a preservar o Planeta. De acordo com a resolução do Conselho Europeu, em 2007 (1), foi apresentado um pacote de propostas que visam a sustentabilidade e estimulam a Eficiência Energética (EE), com o objectivo de reduzir os consumos energéticos dos edifícios, quer estes sejam novos ou reabilitados. Segundo a Direcção Geral de Energia e Geologia os edifícios são responsáveis por 60% dos consumos de energia eléctrica, consumo esse que pode ser reduzido em mais de 50%, através de medidas de EE, traduzindo-se numa redução de 400 milhões de toneladas de CO2 por ano. (2) Para além de medidas de EE, também as práticas de manutenção preventiva podem contribuir para a diminuição dos consumos energéticos e de emissões de CO2. Segundo o Institute for Building Efficiency práticas de manutenção preventiva em equipamentos de Aquecimento Ventilação e Ar Condicionado (AVAC) reduzem os consumos energéticos de 10 a 20% e, em contrapartida, a negligência na execução da manutenção pode aumentar os consumos energéticos de 30 a 60%. (3) Uma outra análise de valores a ter em conta, é a Intensidade Energética (IE). Leia-se IE como sendo o valor global da energia consumida num país a dividir pelo seu produto interno bruto. A contribuição do sector dos serviços para a IE nacional era de 17% no ano de 2005. (4) Se a estes dados acrescentarmos que 70% dessa energia é consumida por equipamentos AVAC (5) e que práticas de manutenção reduzem esses valores entre 10 a 20%, pode concluir-se que a redução de custos energéticos associada à manutenção preventiva é efectiva e significativa. Apresentando um cenário ideal e hipotético, se ao contributo do sector dos serviços, para a IE nacional, se isolar o valor referente a equipamentos de AVAC, obtem-se uma IE de aproximadamente 12%. Se adicionalmente se considerar uma taxa de redução, relativa à execução da manutenção, entre 10 e 20%, Portugal obteria uma IE, relativamente aos consumos energéticos em edificios de serviços, não de 17% mas sim entre 14,6% e 15,8%. Neste trabalho pretende-se comprovar que um plano de actividades de manutenção equilibrado, monitorizado, e gerido de forma eficaz e funcional, é uma ferramenta fundamental no cumprimento de objectivos e metas europeias traçadas, que se reúnem num objectivo comum de preservação do planeta. A adopção deste tipo de medidas contribuirá para a racionalização dos consumos energéticos e para o aumento da vida útil dos equipamentos, bem como para a melhoria do desempenho económico e financeiro das organizações, tal como se poderá ler mais à frente neste trabalho. Será também analisado um caso prático, verificando a eficácia das medidas tomadas durante as intervenções preventivas de manutenção, sendo que para isso será estudado o comportamento de um equipamento, antes e após a realização de tarefas de manutenção preventiva. Tentar-se-á, junto de gestores de edifícios, recolher a opinião que têm sobre a importância da manutenção. Ao longo de toda a pesquisa foi possível consolidar a hipótese formulada inicialmente no que concerne ao contributo da manutenção para a sustentabilidade, quer através da revisão da literatura, quer nos testes efectuados a equipamentos. Foi possível confirmar que um plano de manutenção ajustado, monitorizado e cumprido é uma ferramenta na diminuição dos consumos energéticos, aumento da vida útil de equipamentos e por sua vez na diminuição de emissões de CO2. Verificou-se também que o controlo de poluentes e ventilação adequada dos edifícios são uma ferramenta essencial para a qualidade do ar interior, parâmetros facilmente controlados nas actividades de manutenção. O contributo das opiniões recolhidas entre os gestores de edifícios, para este estudo, foi também bastante importante, uma vez que todos eles reconhecem o papel importante da manutenção, mas nem todos estão sensibilizados para o seu papel na sustentabilidade do planeta. Nesta dissertação é deixado um alerta: o crescimento da população mundial e a consequente utilização de recursos naturais que são finitos, não sendo controlado de uma forma sustentada, pode resultar na destruição de um planeta único. O papel negativo do Homem nas alterações climáticas é inequívoco e é necessário melhorar a sua relação com o Ambiente. Cada ser humano está inserido na sua comunidade e dentro dela tem a sua função, cabe a cada um exercer esta responsabilidade nas suas actividades do dia-a-dia.