A Novel Run-Time Monitoring Architecture for Safe and Efficient Inline Monitoring

20th International Conference on Reliable Software Technologies - Ada-Europe 2015 (Ada-Europe 2015), Madrid, Spain.

A Novel Runtime Monitoring Architecture

Poster presented in 28th GI/ITG International Conference on Architecture of Computing Systems (ARCS 2015). 25 to 28, Mar, 2015, Poster Session. Porto, Portugal.

A Generic and Compositional Framework for Multicore Response Time Analysis

23rd International Conference on Real-Time Networks and Systems (RTNS 2015). 4 to 6, Nov, 2015, Main Track. Lille, France. Best Paper Award Nominee

Monitoring for a decidable fragment of MTLD

The 15th International Conference on Runtime Verification (RV'15). 22-25 September. Vienna, Austria.

Abstract Timers and their Implementation onto the ARM Cor tex-M family of MCUs

Presented at Embed with Linux Workshop (EWiLi 2015). 4 to 9, Oct, 2015. Amsterdam, Netherlands.

Run-time Monitoring Architecture for RealTime Systems

Presented at INForum - Simpósio de Informática (INFORUM 2015). 7 to 8, Sep, 2015. Portugal.

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.

Análise da interoperabilidade aplicada ao projeto BIM de Estruturas Metálicas

O BIM – Building Information Modeling – é um conceito de controlo e gestão de informação desenvolvida, entre diferentes especialidades e intervenientes envolventes, durante o ciclo de vida das construções. A utilização das tecnologias BIM, no ramo da Engenharia Mecânica e Civil, tem sido uma aposta constante, e cada vez mais concisa, nos projetos de construção. A justificação para a adoção destas metodologias mais eficientes, em substituição dos processos convencionais, prende-se com o facto desses processos convencionais, ainda hoje, apresentarem muitas dificuldades e problemas associados, por exemplo, à falta de comunicação entre os intervenientes e ao ineficiente controlo na gestão de projetos. O objetivo desta dissertação centra-se na análise da interoperabilidade de softwares BIM, ou seja, na verificação da viabilidade de exportação de dados dos modelos produzidos, entre as ferramentas BIM. Para este campo de ação contribuirá a análise da passagem de informação, relativa ao modelo de uma Nave Industrial modelada, em alguns dos softwares BIM, correntemente mais utilizados. O conhecimento adquirido com a modelação do caso de estudo do presente trabalho irá permitir identificar algumas lacunas existentes ao nível da falta de recomendações práticas que sirvam de orientação na modelação recorrendo a ferramentas informáticas BIM-compatíveis. Assim, a base deste trabalho consiste na criação de uma série de recomendações ou de um roteiro de modelação em específico para a disciplina de estruturas enquanto área de aplicação concreta do estudo efetuado. Nesse sentido, a proposta deste trabalho é de apresentar alguns critérios de modelação onde são definidos os elementos a modelar em cada fase do projeto.

Projeto de estruturas do edifício administrativo de um polo logístico em Viana-Angola

O objetivo deste trabalho consiste em efetuar o dimensionamento estrutural de um edifício em betão armado, contemplando as diferentes fases, desde a conceção inicial, com a definição do modelo estrutural e escolha criteriosa dos elementos e soluções constituintes, até à fase final de dimensionamento, considerando para além das cargas gravíticas, a ação do vento e a ação sísmica. No âmbito deste trabalho considerou-se o dimensionamento de elementos estruturais nomeadamente, sapatas, paredes, pilares, vigas e lajes, com a verificação de segurança à flexão simples, flexão composta, esforço transverso e punçoamento, consoante a necessidade de cada elemento. Para tal, foi desenvolvido uma folha de cálculo automático (Macro) que permite a verificação da capacidade resistente de secções, à flexão simples e ao esforço transverso, quer em elementos com ou sem armadura de esforço transverso. Os esforços atuantes que estiveram na origem das verificações estruturais foram calculados com base na aplicação de um programa tridimensional de elementos finitos, nomeadamente o programa de cálculo ROBOT STRUCTURAL ANALYSIS. Os Critérios Gerais de Dimensionamento considerados, com base na regulamentação em vigor em Portugal – RSA, REBAP e Eurocódigos, bem como as Hipóteses de Cálculo consideradas na verificação aos estados limites últimos dos elementos estruturais são detalhadamente enunciados ao longo do trabalho. Os desenhos de elementos estruturais dimensionados, bem como os desenhos de dimensionamento do edifício encontram-se em Anexo.

Avaliação de Riscos para a Segurança da Informação no ISEP Aplicação ao Processo de Notas

Desde que existe informação, há necessidade de criar um sistema que permita gerir e garantir que a informação está segura e que cumpre os requisitos básicos de segurança. Como tal, é necessário desenvolver técnicas e mecanismos para que os requisitos sejam testados e melhorados continuamente. Com esta necessidade em vista, apareceram padrões que dão resposta a um conjunto vasto de problemas, em diferentes sistemas e aplicações diversas. Estes tornaram-se guias de reflexão para quem os analisava, de arquitetura para quem os implementava e modelos para quem os geria. O padrão ISO 27001 dá resposta aos cuidados a ter para se conseguir um sistema de gestão da segurança da informação eficaz e eficiente. Esta norma preocupa-se com os detalhes de aplicação até à forma como é implementado e arquitetado o sistema. Os processos, atividades, fluxos de trabalho são essenciais para que esta norma seja cumprida. É necessário um bom escrutínio dos processos e suas atividades, assim como um fluxo de trabalho bem definido com papéis e responsabilidades de cada ator. É necessário também assegurar a forma como é gerido, a sua verificação e melhoria contínua. Foi aplicado no ISEP um exercício com o qual se pretendeu verificar se os processos e outros aspetos seguiam estes cuidados e se estavam de acordo com a norma. Durante o exercício foram verificados processos dentro de um certo âmbito, todas as suas atividades, papéis e responsabilidades, verificação de recursos, aplicação de controlos e aplicação de uma análise de risco. Esta análise tem como objetivo verificar o nível de segurança dos recursos, algo que a norma ISO 27001 propõe mas não especifica em que moldes. No final deste exercício pretendeu-se melhorar o sistema de gestão de informação do ISEP em vertentes tais como a documentação, a qual especifica quais os passos realizados no decorrer do mesmo.

Projeto e desenvolvimento de células robotizadas para soldadura e cladding

A utilização de equipamentos robóticos para o processo de soldadura por arco elétrico teve um forte crescimento nas décadas de 80 e 90, altura em que o custo e fiabilidade da tecnologia passou a permitir a integração de robôs em linhas de produção ou em células de fabrico. Depressa cresceram as exigências de uma produção com qualidade repetitiva e facilmente ajustável, e as restrições ao uso de processos manuais ou de tecnologias com pouca flexibilidade. Desde o início do século XXI que a renovação de uma estação de fabrico de peças soldadas para produção em série, especialmente no setor automóvel, parece forçada à integração de robôs industriais, que assim se tornaram símbolos de produtividade. A KAMAZ encontra-se atualmente a renovar alguns dos seus processos de fabrico, incluindo as áreas de soldadura por arco ou cladding. Esta Dissertação aborda o trabalho elaborado, depois de contratualizada com a ABB Rússia a instalação de novas células de fabrico robotizado nesta empresa. Este projeto tem início com o levantamento das necessidades, a verificação do processo existente, e a procura da solução tecnológica que se adapte a essas condições e cumpra os requisitos acordados. São realizadas modelações e simulações off-line em 3D, usando o software RobotStudio da ABB, que permitiram testar cada solução e analisar a sua adequação e viabilidade. Para maior garantia de se obter a qualidade esperada na fusão e deposição do material por processo com arco elétrico revestido a gás, foram realizados testes reais utilizando equipamento robótico em condições baseadas nos testes feitos no ambiente virtual. Por último, são ajustadas as localizações dos postos de trabalho ao layout existente e é feito o balanceamento do tempo de operação manual com o tempo do processo robotizado. Este projeto de Tese termina com a aceitação do cliente para a solução encontrada e para os resultados dos testes reais de ambos os processos.

Aplicação de um software de cálculo automático na verificação aos estados limites de utilização em estruturas de Betão Armado

Actualmente e cada vez mais, são concebidos e utilizados programas de cálculo automático de Engenharia na realização de projectos de edifícios, que proporcionam aos engenheiros uma possibilidade avançada e rápida de execução, simulação e análise de edifícios para estruturas complexas e de elevada dimensão. Contudo, será necessário que os resultados deverão ser fiáveis de modo a não existirem consequências no comportamento real da estrutura a longo prazo. O presente relatório de estágio, refere-se à verificação aos estados limites de utilização (tensões, fendilhação e deformação) segundo o Eurocódigo 2, de uma estrutura porticada em betão armado, nomeadamente de um pórtico central pertencente a essa mesma estrutura recorrendo ao programa de cálculo automático da Autodesk o Robot Structural Analysis Professional 2014. O objectivo principal do presente trabalho consiste na comparação de resultados referente aos estados limites últimos e de utilização, pelos diferentes módulos de dimensionamento Required e Provided Reinforcement presentes no programa Robot. É destacado no final do relatório, considerando uma disposição de armadura optada analiticamente para o pórtico, uma análise comparativa de resultados referente aos estados limites de utilização entre o comando Typical Reinforcement do módulo Provided Reinforcement e por expressões analíticas. Refere-se contudo que, o procedimento do método analítico teve como base de cálculo uma aplicação desenvolvida para a verificação de elementos de betão armado aos estados limites de utilização segundo o Eurocódigo 2, com o nome de XD-Conserv tendo sido também comparado os resultados finais do mesmo.

Avaliação numérica e experimental da carga admissível de vigas compostas para monocarris de sistemas de elevação

Este trabalho foi realizado com o apoio, e em colaboração da empresa Flexcrane, que constrói e comercializa soluções flexíveis de pontes rolantes para cargas ligeiras. Com cargas máximas de 2 toneladas estas pontes e seus caminhos de rolamento são construídas essencialmente enformados a frio. O objetivo deste trabalho é a verificação numérica e experimental das cargas que este tipo de estrutura suporta, nas suas diferentes configurações. Numa aproximação por engenharia inversa, com a realização deste trabalho, foi possível determinar a carga admissível das vigas compostas utilizadas, assim como o seu comportamento quando em carga. Para obtenção destes resultados foram realizadas simulações computacionais recorrendo ao método de elementos finitos, utilizando para isso o software Ansys Workbench e ainda ensaios experimentais que permitiram validar os resultados obtidos numericamente e consolidar o conhecimento sobre o comportamento desta solução comercial. Por ser de construção modular, são possíveis diferentes combinações para o produto final, por esta razão foram estudados numericamente diferentes configurações possíveis, com e sem reforços. Foi realizada a validação experimental para a configuração mais usual, fazendo recurso a um dispositivo para ensaio de estruturas e componentes, pertencente ao Isep. Foi ainda utilizada a técnica extensométrica para avaliar as tensões em pontos selecionados e compara-los com os obtidos numericamente. Concluiu-se pelo ótimo desempenho dos produtos Flexcrane.