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.

The verification of temporal KBS: SPARSE - a case study in power systems

In this paper we present VERITAS, a tool that focus time maintenance, that is one of the most important processes in the engineering of the time during the development of KBS. The verification and validation (V&V) process is part of a wider process denominated knowledge maintenance, in which an enterprise systematically gathers, organizes, shares, and analyzes knowledge to accomplish its goals and mission. The V&V process states if the software requirements specifications have been correctly and completely fulfilled. The methodologies proposed in software engineering have showed to be inadequate for Knowledge Based Systems (KBS) validation and verification, since KBS present some particular characteristics. VERITAS is an automatic tool developed for KBS verification which is able to detect a large number of knowledge anomalies. It addresses many relevant aspects considered in real applications, like the usage of rule triggering selection mechanisms and temporal reasoning.

Inexact restoration approaches to solve mathematical program with complementarity constraints

Mathematical Program with Complementarity Constraints (MPCC) finds applica- tion in many fields. As the complementarity constraints fail the standard Linear In- dependence Constraint Qualification (LICQ) or the Mangasarian-Fromovitz constraint qualification (MFCQ), at any feasible point, the nonlinear programming theory may not be directly applied to MPCC. However, the MPCC can be reformulated as NLP problem and solved by nonlinear programming techniques. One of them, the Inexact Restoration (IR) approach, performs two independent phases in each iteration - the feasibility and the optimality phases. This work presents two versions of an IR algorithm to solve MPCC. In the feasibility phase two strategies were implemented, depending on the constraints features. One gives more importance to the complementarity constraints, while the other considers the priority of equality and inequality constraints neglecting the complementarity ones. The optimality phase uses the same approach for both algorithm versions. The algorithms were implemented in MATLAB and the test problems are from MACMPEC collection.

Severe stress urinary incontinence: pelvic floor muscle training program

International guidelines recommend a first line therapy in the treatment of female stress urinary incontinence (SUI), the pelvic floor muscle (PFM) training. This case report assesses the effects of the PFM training program in treating women with severe SUI. The urodynamic parameters allow diagnosed intrinsic sphincter deficiency and urethral hypermobility. The subjective and objective parameters were assessed at the beginning and after six-month of PFM training program. This case report confirms the efficiency of the intensive training program in severe SUI. The medical implications of the PFM training as first treatment option reflect favourable individual results and additionally contribute to the selection of the non-invasive treatment, the reduction of the incidence collateral effects, low costs and that does not prevent future treatment options.

A system verification strategy based on the BST infrastructure

A good verification strategy should bring near the simulation and real functioning environments. In this paper we describe a system-level co-verification strategy that uses a common flow for functional simulation, timing simulation and functional debug. This last step requires using a BST infrastructure, now widely available on commercial devices, specially on FPGAs with medium/large pin-counts.

Estruturas de suporte de terras executadas com pneus

O aproveitamento de pneus em fim de vida revela ser uma alternativa eficaz e promissora na indústria da construção civil, na utilização deste resíduo em muros de suporte. O presente trabalho tem como principal objetivo a apresentação de uma técnica de aproveitamento de pneus em fim de vida na execução de muros de gravidade, combinando solo e pneus. Neste sentido, tomou-se como referência um estudo realizado no Brasil por Sieira, Sayão, Medeiros e Gerscovich, para avaliar a eficiência e o custo deste tipo de estruturas, comparando-o com um muro de suporte tradicional de betão simples. Inicialmente, avaliou-se a segurança do muro de solo-pneus, de acordo com a metodologia proposta no Eurocódigo 7 (NP EN 1997-1, 2010), considerando a geometria e as características dos materiais apresentados no estudo referido e usando o programa de cálculo automático Slide, da Rocscience, para a verificação da estabilidade global. Reproduziu-se a análise numérica realizada no âmbito do caso de estudo brasileiro de referência, recorrendo também a uma formulação por elementos finitos com o programa de cálculo automático Phase2, da Rocscience. Por último, utilizando uma vez mais o programa Slide, definiu-se a geometria de um muro de betão simples cuja geometria garantisse o mesmo valor do fator de segurança à estabilidade global, obtido com o muro de solo-pneus e compararam-se os custos respetivos. O presente trabalho confirmou a eficiência e o baixo custo desta solução construtiva, sendo necessários, no entanto, estudos mais detalhados que reforcem estas conclusões.

CodeSkelGen: a program skeleton generator

Existent computer programming training environments help users to learn programming by solving problems from scratch. Nevertheless, initiating the resolution of a program can be frustrating and demotivating if the student does not know where and how to start. Skeleton programming facilitates a top-down design approach, where a partially functional system with complete high level structures is available, so the student needs only to progressively complete or update the code to meet the requirements of the problem. This paper presents CodeSkelGen - a program skeleton generator. CodeSkelGen generates skeleton or buggy Java programs from a complete annotated program solution provided by the teacher. The annotations are formally described within an annotation type and processed by an annotation processor. This processor is responsible for a set of actions ranging from the creation of dummy methods to the exchange of operator types included in the source code. The generator tool will be included in a learning environment that aims to assist teachers in the creation of programming exercises and to help students in their resolution.

Distributed, Agent-Based Intelligent System for Demand Response Program Simulation in Smart Grids

A distributed, agent-based intelligent system models and simulates a smart grid using physical players and computationally simulated agents. The proposed system can assess the impact of demand response programs.

Lean and quality management integration: improvement program implementation in a service company

Lean Thinking is an important pillar in the success of any program of continuous improvement process. Its tools are useful means in the analysis, control and organization of important data for correct decision making in organizations. This project had as main objective the design of a program of quality improvement in Eurico Ferreira, S.A., based on the evaluation of customer satisfaction and the implementation of 5S. Subsequently, we have selected which business area of the company to address. After the selection, there was an initial diagnostic procedure, identifying the various points of improvement to which some tools of Lean Thinking have been applied, in particular Value Stream Mapping and 5S methodology. With the first, we were able to map the current state of the process in which all stakeholders were represented as well as the flow of materials and information throughout the process. The 5S methodology allowed to act on the wastage, identifying and implementing various process improvements.

Sistema pericial para auditoria de registos clínicos

O registo clinico é um documento hospitalar confidencial, nele é registado todo o percurso clinico de um determinado paciente. Esse percurso é registado através da atribuição de códigos descritos num sistema de classificação, também denominados de dados da codificação. Os dados da codificação são armazenados electronicamente numa Base de Dados, e é a partir dela que certas medidas, tais como facturação hospitalar, financiamentos hospitalares anuais, tratamentos médicos, ou até mesmo dados epidemiológicos, são adotadas. Portanto torna-se fundamental a garantia da qualidade na área da codificação clinica, para isso é necessário recorrer a processos de auditorias aos registos clínicos. O processo de auditoria é uma atividade independente de avaliação, cujo objetivo visa acrescentar valor e melhorar os objetos e processos da auditoria. Atualmente uma ferramenta denominada de Programa Auditor é utilizada, contudo essa ferramenta demonstra uma tecnologia já ultrapassada. A Tese que se pretende defender é a de que, através de Sistemas Periciais, é possível realizar auditorias internas aos registos clínicos. Pretende-se ainda demonstrar que dos Sistemas Periciais e um benefício para os peritos na área, pois diminui a probabilidade de erros e torna o processo de verificação menos moroso. Neste contexto, o objetivo desta Dissertação prende-se em definir e implementar um Sistema Pericial que permita a auditoria de registos clínicos hospitalares. O Sistema Pericial dever a ainda ser capaz de traduzir o raciocínio do perito, detectando assim diversos tipos de erros que traduzem num registo clínico não conforme. Por sua vez, foi desenvolvido um protótipo de um Sistema Pericial para auditoria de registos clínicos em linguagem PROLOG. Este mesmo protótipo serviu de base à realização de uma experiência que permitiu comparar com o programa Auditor e verificar a sua aplicabilidade no dia-a-dia hospitalar.

An Exercise Program Improves Health-Related Quality of Life of Workers

Low back problems are associated with decreased quality of life. Specific exercises can improve quality of life, resulting in better professional performance and functionality. The purpose of this study was to evaluate the effect of following a 21-month exercise program on the quality of life of warehouse workers. The population included 557 male warehouse workers from a food distribution company in Oporto, Portugal. Upon application of the selection criteria, 249 workers were deemed eligible, which were randomized into two groups (125 in the intervention group and 124 in the control group). Then, subjects were asked to volunteer for the study, the sample being formed by 229 workers (112 in the intervention group and 117 in the control group). All subjects completed the SF-36 questionnaire prior to beginning the program and on the 11th and 21st months following it. The exercises were executed in the company facilities once a day for 8 min. Data were analyzed using SPSS® 17.0 for Windows®. After 11 months of following the exercise program, there was an increase in all scores for the experimental group, with statistically significant differences in the dimensions physical functioning (0.019), bodily pain (0.010), general health (0.004), and rolephysical (0.037). The results obtained at the end of the study (21 months) showed significant improvements in the dimensions physical functioning (p = 0.002), rolephysical (p = 0.007), bodily pain (p = 0.001), social functioning (p = 0.015), role-emotional (p = 0.011), and mental health (p = 0.001). In the control group all dimensions showed a decrease in mean scores. It can be concluded that the implementation of a low back specific exercise program has changed positively the quality of life of warehouse workers.

Reformulação de um Sistema de Gestão de Consumos de Energia

Atualmente a energia é considerada um vetor estratégico nas diversas organizações. Assim sendo, a gestão e a utilização racional da energia são consideradas instrumentos fundamentais para a redução dos consumos associados aos processos de produção do sector industrial. As ações de gestão energética não deverão ficar pela fase do projeto das instalações e dos meios de produção, mas sim acompanhar a atividade da Empresa. A gestão da energia deve ser sustentada com base na realização regular de diagnósticos energéticos às instalações consumidoras e concretizada através de planos de atuação e de investimento que apresentem como principal objetivo a promoção da eficiência energética, conduzindo assim à redução dos respetivos consumos e, consequentemente, à redução da fatura energética. Neste contexto, a utilização de ferramentas de apoio à gestão de energia promovem um consumo energético mais racional, ou seja, promovem a eficiência energética e é neste sentido que se insere este trabalho. O presente trabalho foi desenvolvido na Empresa RAR Açúcar e apresentou como principais objetivos: a reformulação do Sistema de Gestão de Consumos de Energia da Empresa, a criação de um modelo quantitativo que permitisse ao Gestor de Energia prever os consumos anuais de água, fuelóleo e eletricidade da Refinaria e a elaboração de um plano de consumos para o ano de 2014 a partir do modelo criado. A reformulação do respetivo Sistema de Gestão de Consumos resultou de um conjunto de etapas. Numa primeira fase foi necessário efetuar uma caraterização e uma análise do atual Sistema de Gestão de Consumos da Empresa, sistema composto por um conjunto de sete ficheiros de cálculo do programa Microsoft Excel©. Terminada a análise, selecionada a informação pertinente e propostas todas as melhorias a introduzir nos ficheiros, procedeu-se à reformulação do respetivo SGE, reduzindo-se o conjunto de ficheiros de cálculo para apenas dois ficheiros, um onde serão efetuados e visualizados todos os registos e outro onde serão realizados os cálculos necessários para o controlo energético da Empresa. O novo Sistema de Gestão de Consumos de Energia será implementado no início do ano de 2015. Relativamente às alterações propostas para as folhas de registos manuais, estas já foram implementadas pela Empresa. Esta aplicação prática mostrou-se bastante eficiente uma vez que permitiu grandes melhorias processuais nomeadamente, menores tempos de preenchimento das mesmas e um encurtamento das rotas efetuadas diariamente pelos operadores. Através do levantamento efetuado aos diversos contadores foi possível identificar todas as áreas onde será necessário a sua instalação e a substituição de todos os contadores avariados, permitindo deste modo uma contabilização mais precisa de todos os consumos da Empresa. Com esta reestruturação o Sistema de Gestão de Consumos tornou-se mais dinâmico, mais claro e, principalmente, mais eficiente. Para a criação do modelo de previsão de consumos da Empresa foi necessário efetuar-se um levantamento dos consumos históricos de água, eletricidade, fuelóleo e produção de açúcar de dois anos. Após este levantamento determinaram-se os consumos específicos de água, fuelóleo e eletricidade diários (para cada semana dos dois anos) e procedeu-se à caracterização destes consumos por tipo de dia. Efetuada a caracterização definiu-se para cada tipo de dia um consumo específico médio com base nos dois anos. O modelo de previsão de consumos foi criado com base nos consumos específicos médios dos dois anos correspondentes a cada tipo de dia. Procedeu-se por fim à verificação do modelo, comparando-se os consumos obtidos através do modelo (consumos previstos) com os consumos reais de cada ano. Para o ano de 2012 o modelo apresenta um desvio de 6% na previsão da água, 12% na previsão da eletricidade e de 6% na previsão do fuelóleo. Em relação ao ano de 2013, o modelo apresenta um erro de 1% para a previsão dos consumos de água, 8% para o fuelóleo e de 1% para a eletricidade. Este modelo permitirá efetuar contratos de aquisição de energia elétrica com maior rigor o que conduzirá a vantagens na sua negociação e consequentemente numa redução dos custos resultantes da aquisição da mesma. Permitirá também uma adequação dos fluxos de tesouraria à necessidade reais da Empresa, resultante de um modelo de previsão mais rigoroso e que se traduz numa mais-valia financeira para a mesma. Foi também proposto a elaboração de um plano de consumos para o ano de 2014 a partir do modelo criado em função da produção prevista para esse mesmo ano. O modelo apresenta um desvio de 24% na previsão da água, 0% na previsão da eletricidade e de 28% na previsão do fuelóleo.

Simulação de sistema de desenfumagem de parques de estacionamento recorrendo ao programa OpenFOAM

Os parques de estacionamento cobertos estão obrigados por legislação a terem sistemas de desenfumagem. Assim, nesta dissertação desenvolve-se um procedimento computacional para a analise e verificação de funcionamento de sistemas de desenfumagem com ventiladores de impulso para parques de estacionamento, recorrendo ao software de mecânica dos fluidos computacional OpenFOAM. Actualmente nos sistemas de desenfumagem de parques de estacionamento estão a ser aplicados ventiladores de impulso. Este tipo de ventiladores não estão contemplados pela legislação em vigor. Assim, para serem utilizados é necessário verificar se estes podem substituir as redes de condutas. A verificação do funcionamento de sistemas de desenfumagem com ventiladores de impulso e efectuada com recurso a programas de simulação de mecânica dos fluidos computacional. O software OpenFOAM não tem tutoriais para ventiladores de impulso. Assim, foi executado um procedimento para validação dos ventiladores de impulso. A validação consistiu em reproduzir-se uma experiência executada por Giesen et al. (2011). Executaram-se várias simulações com diferentes modelos de turbulência, verificando-se que o programa buoyantpimplefoam do software OpenFOAM ao utilizar o modelo de turbulência k -ɛ simulou quase na perfeição os ventiladores de impulso. O desenvolvimento do procedimento computacional foi executado para um parque de estacionamento com uma geometria bastante complexa. O parque de estacionamento foi criado com um software em 3D e posteriormente inserido numa malha j a criada com as dimensões exteriores do parque. Foram estipuladas as condições de fronteira e executou-se uma simulação de seiscentos segundos com parâmetros determinados previamente. O processamento da simulação teve a duração de aproximadamente oito dias. Dos resultados obtidos concluiu-se que o procedimento computacional apresentado simula adequadamente sistemas de desenfumagem em parques de estacionamento.

Effects of a home-based exercise program in body composition, abdominal fat and lipid profile in patients with coronary artery disease

Introduction: Coronary artery disease and aging seems to be associated with a sedentary lifestyle, contributing to increased abdominal fat and consequently metabolic complications. The exercise can break this cycle by stimulating lipolysis and the use of fatty acids. In Europe there is still a lack of cardiac rehabilitation programmes in hospitals, therefore, this study aims to demonstrate the advantages of implementing home-based exercise programmes, as well as, their effects on cardiovascular prevention. This study analyzed the effects of a home-based exercise programme, in patients with coronary artery disease (myocardial infarction for 1 year), in body composition, abdominal fat, lipid profile. Methods: An ongoing randomized controlled trial with a sample of 20 participants were randomly allocated to intervention (n = 10) and control groups (n = 10). Intervention group performed a specific exercise programme during 8 weeks, consisting of ten home based exercises taking into account flexibility, muscle endurance and strength as well as cardiovascular endurance. Skinfolds thickness were measure to calculate the percentage of total fat: Skinfolds used were suprailiac, abdominal horizontal and vertical. Body mass index calculation and blood tests for lipidic profile were performed. Results: After eight weeks the intervention group decreased significantly the percentage of total fat (p < 0.05), the suprailiac skinfold (p < 0.05), the abdominal horizontal and vertical skinfold (p < 0.05) when compared with control group. In the intervention group it was observed after 8 weeks a significant decrease in body mass index, LDL-cholesterol and triglycerides. Conclusions: Home-based exercise programme influenced body composition, abdominal fat and lipid profile. These results highlight the importance of implementing home based exercises that are easy and cheap to implement in cardiac patients, in order to promote health and reduce cardiovascular risk factors.

Desenvolvimento de ferramentas BIM no âmbito do cálculo estrutural em situação de incêndio

Este trabalho insere-se no âmbito de um estágio curricular realizado no gabinete de projetos SE2P, durante o qual foram desenvolvidas ferramentas de cálculo estrutural em situação de incêndio, integradas numa metodologia de trabalho que segue os princípios inerentes à tecnologia BIM (Building Information Modeling). Em particular foi implementado um procedimento de análise ao fogo segundo os modelos simplificados prescritos pelos Eurocódigos. Estes modelos garantem a segurança estrutural, permitindo, de forma rápida e eficiente, a determinação das necessidades de proteção passiva para diferentes cenários, tendo em vista a obtenção da solução mais económica. Esta dissertação, para além da apresentação do trabalho desenvolvido em regime de estágio curricular, objetivou dotar o leitor de um documento que introduza os principais conceitos relativos ao cálculo estrutural em situação de incêndio, indicando as várias opções de análise e respetivas vantagens e desvantagens, ajudando a definir a sua adequabilidade ao projeto em estudo. Neste contexto é efetuada uma introdução geral ao fenómeno do fogo e às medidas mais correntes de proteção, indicando-se os documentos normativos aplicáveis tanto ao cálculo estrutural como aos materiais de proteção. É também abordada a interação entre as várias normas que devem ser consultadas quando é efetuada uma análise ao fogo, e quais se aplicam a cada fase da análise. Efetua-se uma clara distinção entre a análise do comportamento térmico e mecânico, indicando-se as principais propriedades dos materiais em função do tipo de análise e a forma como são afetadas pela temperatura. No campo da análise do comportamento térmico faz-se essencialmente referência aos modelos de cálculo simplificados do desenvolvimento da temperatura em elementos metálicos e vigas mistas, com e sem proteção passiva. No que concerne ao campo da análise do comportamento mecânico são descritos os modelos de cálculo simplificados para a verificação da segurança estrutural atendendo às ações e combinações em situação de incêndio e à perda de resistência a temperaturas elevadas. Relativamente ao trabalho desenvolvido na SE2P, relativo ao desenvolvimento de ferramentas de cálculo e a sua implementação na análise ao fogo, realiza-se uma descrição detalhada de todo o processo, e da forma como se integra no conceito BIM, utilizando informações provenientes da modelação das estruturas e introduzindo novos dados ao modelo. Realizou-se também a aplicação de todo o procedimento de análise e das ferramentas desenvolvidas, a um caso de estudo baseado num edifício de habitação. Este caso de estudo serviu também para criar cenários de otimização utilizando-se referências de preços de mercado para o aço, sua transformação em fábrica e sistemas de proteção passiva, demonstrando-se a dificuldade em encontrar caminhos rápidos e diretos de decisão no processo de otimização.