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.

A modified debugging infrastructure to assist real time fault injection campaigns

Fault injection is frequently used for the verification and validation of the fault tolerant features of microprocessors. This paper proposes the modification of a common on-chip debugging (OCD) infrastructure to add fault injection capabilities and improve performance. The proposed solution imposes a very low logic overhead and provides a flexible and efficient mechanism for the execution of fault injection campaigns, being applicable to different target system architectures.

Uma aplicação Web para apoio a laboratórios remotos reconfiguráveis baseados na norma IEEE 1451.0

Nos últimos anos, o processo de ensino e aprendizagem tem sofrido significativas alterações graças ao aparecimento da Internet. Novas ferramentas para apoio ao ensino têm surgido, nas quais se destacam os laboratórios remotos. Atualmente, muitas instituições de ensino disponibilizam laboratórios remotos nos seus cursos, que permitem, a professores e alunos, a realização de experiências reais através da Internet. Estes são implementados por diferentes arquiteturas e infraestruturas, suportados por vários módulos de laboratório acessíveis remotamente (e.g. instrumentos de medição). No entanto, a sua inclusão no ensino é ainda deficitária, devido: i) à falta de meios e competências técnicas das instituições de ensino para os desenvolverem, ii) à dificuldade na partilha dos módulos de laboratório por diferentes infraestruturas e, iii) à reduzida capacidade de os reconfigurar com esses módulos. Para ultrapassar estas limitações, foi idealizado e desenvolvido no âmbito de um trabalho de doutoramento [1] um protótipo, cuja arquitetura é baseada na norma IEEE 1451.0 e na tecnologia de FPGAs. Para além de garantir o desenvolvimento e o acesso de forma normalizada a um laboratório remoto, este protótipo promove ainda a partilha de módulos de laboratório por diferentes infraestruturas. Nesse trabalho explorou-se a capacidade de reconfiguração de FPGAs para embutir na infraestrutura do laboratório vários módulos, todos descritos em ficheiros, utilizando linguagens de descrição de hardware estruturados de acordo com a norma IEEE 1451.0. A definição desses módulos obriga à criação de estruturas de dados binárias (Transducer Electronic Data Sheets, TEDSs), bem como de outros ficheiros que possibilitam a sua interligação com a infraestrutura do laboratório. No entanto, a criação destes ficheiros é bastante complexa, uma vez que exige a realização de vários cálculos e conversões. Tendo em consideração essa mesma complexidade, esta dissertação descreve o desenvolvimento de uma aplicação Web para leitura e escrita dos TEDSs. Para além de um estudo sobre os laboratórios remotos, é efetuada uma descrição da norma IEEE 1451.0, com particular atenção para a sua arquitetura e para a estrutura dos diferentes TEDSs. Com o objetivo de enquadrar a aplicação desenvolvida, efetua-se ainda uma breve apresentação de um protótipo de um laboratório remoto reconfigurável, cuja reconfiguração é apoiada por esta aplicação. Por fim, é descrita a verificação da aplicação Web, de forma a tirar conclusões sobre o seu contributo para a simplificação dessa reconfiguração.

Projeto de comportamento térmico, certificação energética e ensaios acústicos

O presente relatório incluído na Unidade Curricular de Dissertação/Projeto/Estágio do Mestrado (DIPRE) em Engenharia Civil do Instituto Superior de Engenharia do Porto (ISEP) e desenvolvido no âmbito do estágio curricular realizado na empresa Asl & Associados, tem como principais objetivos a minha integração no mercado de trabalho e obtenção de experiência profissional. Neste trabalho, serão abordados temas como as introduções teóricas ao Comportamento Térmico e Acústico de Edifícios de Habitação, estudos de casos práticos como o Projeto de Comportamento Térmico de uma grande intervenção, Certificação Energética de edifícios existentes com base no Regulamento de Desempenho Energético dos Edifícios de Habitação e Ensaios Acústicos de Edifícios de acordo com o Regulamento dos Requisitos Acústicos dos Edifícios. O projeto realizado consistiu no estudo do comportamento térmico do edifício na Avenida Marechal Gomes da Costa nº802, no Porto. Nesse estudo realizou-se a verificação das soluções construtivas, por vezes foram propostas alterações das mesmas de modo a verificar os requisitos impostos pelo REH e foi realizada a emissão do seu pré-certificado. A maior parte do período em que decorreu o estágio na empresa foi preenchida com a realização de certificados energéticos de frações autónomas e de moradias. Para a recolha da informação necessária à sua elaboração, foram efetuadas várias vistorias aos imóveis referidos. Foram também efetuados durante o estágio, ensaios acústicos a edifícios de habitação e comércio e elaborado o respetivo relatório de ensaio.

Exigências funcionais em pavimentos de madeira

Durante séculos a madeira foi dos materiais mais privilegiados e usados na construção. Ainda hoje, existem construções antigas em madeira em bom estado de conservação e que, desempenham as suas funções adequadamente. Com o aparecimento do betão e do aço, os projetistas deixaram de usar este tipo de estruturas. Isto provocou um desinteresse na indústria da madeira, adiando a criação de regulamentos e normas relativamente às exigências funcionais deste tipo de estruturas. Com a necessidade da reabilitação do património edificado, verifica-se uma inversão desta tendência, devido às edificações no centro histórico serem constituídas por estruturas de madeira, essencialmente os pavimentos e coberturas. Na maioria das vezes estas estruturas apresentam um elevado nível de degradação e a solução mais rentável é demolir. Os pavimentos de madeira são então substituídos por lajes aligeiradas ou de betão armado provocando alterações estruturais inadequadas nas fachadas a manter. Pretende-se com esta dissertação mostrar as potencialidades dos pavimentos de madeira e assim incentivar ao seu uso, principalmente nas áreas a reabilitar. São analisados todos os regulamentos e normas aplicáveis às exigências estruturais, térmicas, acústicas e contra incêndio dos pavimentos de madeira. A análise da normalização aplicável vai ser sintetizada, ou seja, só vão ser referidos os aspetos a ter em conta para a verificação das exigências funcionais em pavimentos de madeira. A aplicação dos conceitos e das verificações necessárias são aplicadas a um pavimento de madeira a ser construído na parcela C4 do Quarteirão das Cardosas. Os resultados obtidos neste caso de estudo são encorajadores, e abrem uma perspetiva das potencialidades que este sistema construtivo apresenta.

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.

Implementação dos sistemas de gestão ambiental e de segurança e sua integração com o sistema de gestão da qualidade de uma empresa do setor de construção civil e transformação de agregados

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

Verificação interna periódica de esfigmomanómetros digitais

Os equipamentos de medição utilizados nos hospitais têm uma função muito importante na deteção e diagnóstico de doenças como é o caso da pressão arterial. Entre esses equipamentos encontram-se os esfigmomanómetros digitais portáteis que são em muitos casos os primeiros a serem utilizados e a fornecerem um primeiro diagnóstico da pressão arterial do doente como é no caso das urgências hospitalares. Para que os diagnósticos prescritos pelos profissionais de saúde - médicos e enfermeiros seja o mais correto é necessário conhecer as condições de trabalho em que se encontram os esfigmomanómetros digitais existentes nas unidades de saúde. Sendo os esfigmomanómetros digitais equipamentos com uma importância relevante na vida do ser humano, estes deveriam fazer parte da lista de equipamentos que estão englobados na metrologia legal, situação que neste momento ainda não foi concretizada e cada hospital toma a decisão espontânea se efetua a calibração ou verificação internamente dos seus esfigmomanómetros digitais. Pretende-se com este trabalho dar a conhecer o estado ao nível dos erros de alguns esfigmomanómetros digitais existentes nos hospitais envolvidos no trabalho e desenvolver um procedimento de verificação interna dos mesmos com auxílio de um manómetro analógico calibrado e um estetoscópio duplo – método de medição auscultatório - e comparar esses resultados com a utilização de um simulador – método de medição oscilométrico.

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.

Experiências supply-siders na UE15: a redução de impostos como política de melhoria da posição orçamental intertemporal

A Curva de Laffer postula que a partir de determinados níveis de taxas de impostos, uma redução destas pode aumentar as receitas fiscais. Tendo presentes os recentes desenvolvimentos da teoria do crescimento económico, que predizem que a política fiscal tem efeitos permanentes de longo prazo na taxa de crescimento económico, aquele argumento pode ser encarado num contexto dinâmico: a fiscalidade afecta permanentemente a taxa de crescimento económico de longo prazo, alterando as bases fiscais futuras, melhorando, em consequência, a posição orçamental de longo prazo. Neste artigo procura-se averiguar a validação de um efeito Laffer dinâmico para os Estados-Membros da União Europeia dos 15 e, em consequência, se a política fiscal pode ser gerida de forma a substituir o endividamento por reduções de impostos.

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.

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.

Estudo de campo de verificação metrológica de termómetros clínicos timpânicos

Avaliação da variação da temperatura corporal, e a monitorização da mesma é bastante importante na prática clínica sendo, por vezes, a base de muitas decisões clínicas. Atualmente, os termómetros digitais, em particular os timpânicos são amplamente utilizados, em contexto hospitalar e domiciliário. Muitos estudos têm sido efetuados para determinar a validade das medições obtidas através de termómetros timpânicos. Os defensores destes termómetros afirmam que, se forem utilizados de forma adequada e periodicamente calibrados, a avaliação da temperatura corporal com este tipo de termómetros é eficaz, cómoda, rápida, pouco invasiva emais higiénica reduzindo o número de infeções cruzadas (FarnellMaxwell &Tan, Rhodes& Philips, 2005). A Metrologia como a ciência das medições e suas aplicações ((VIM1: 2.2) (INSTITUTO PORTUGUÊS DA QUALIDADE, 2012)), abrange todos os aspetos teóricos e práticos que asseguram a exatidão e precisão exigida num processo, procurando garantir a qualidade de produtos e serviços através da calibração de instrumentos de medição e da realização de ensaios, sendo a base fundamental para a competitividade das empresas. Só após o ano 1990, com a publicação dos resultados doHarvardMedical Practice Study (T A BRENNAN, 2004), sobre adventos adversos na área da saúde, começaram a surgir preocupação com o risco do uso de equipamentos e instrumentos sem a adequada avaliação metrológica. Neste estudo concluiu-se que 3,7 % dos pacientes hospitalizados sofriam eventos adversos devido ao uso inadequado de equipamento médico, sendo que 13,6% destes eram mortais. Pegando nesta realidade e sabendo que o não controlo de Equipamento de Monitorização e Medição é uma das causas de obtenção de 36%de não conformidades - 7.6 (NP EN ISO 9001:2008), em Auditorias da Qualidade em Serviços de Saúde (Luís Marinho – Centro Hospitalar São João), fez todo o sentido o estudo e trabalho desenvolvido. Foi efetuado um estudo, no que se refere a normalização em vigor e verificou-se que a nível metrológico muito trabalho terá que ser realizado no serviço nacional de saúde por forma este fornecer o suporte material fiável ao sistema de medições, essencial aos mais diversos sectores da saúde. Sabendo-se que os ensaios/calibrações são necessários e não são negligenciáveis na estrutura de custos das instituições de saúde, e por isso são vistas como mais uma fonte de despesas, é intenção com a realização deste trabalho, contribuir em parte para superação deste tema. Este trabalho passou pela execução/realização de um procedimento de calibração para termómetros timpânicos, tendo a necessidade de desenvolver/projetar um corpo negro. A amostra em estudo é constituída por cinco termómetros timpânicos hospitalares em uso dos diferentes serviços do CHSJ2, seleccionados completamente ao acaso. Um termómetro clínico no mínimo terá que ser calibrado a temperatura 35 ºC e 42 ºC. A calibração deverá ser realizada anualmente e por entidade acreditada. O erro máximo admissível é de ± 0,2 ºC (nas condições ambientais de funcionamento). Sem a confirmação metrológica, não é possível garantir a qualidade do produto ou serviço. A Metrologia na área da saúde desperta a exigência por produtos e serviços de qualidade. Esta tencionará ser encarada como um pilar de sustentabilidade para a qualidade na saúde, sendo absolutamente necessária a implementação de novos procedimentos e atitudes.

Global and Partitioned Multiprocessor Fixed Priority Scheduling with Deferred Pre-emption

This article introduces schedulability analysis for global fixed priority scheduling with deferred preemption (gFPDS) for homogeneous multiprocessor systems. gFPDS is a superset of global fixed priority pre-emptive scheduling (gFPPS) and global fixed priority non-pre-emptive scheduling (gFPNS). We show how schedulability can be improved using gFPDS via appropriate choice of priority assignment and final non-pre-emptive region lengths, and provide algorithms which optimize schedulability in this way. Via an experimental evaluation we compare the performance of multiprocessor scheduling using global approaches: gFPDS, gFPPS, and gFPNS, and also partitioned approaches employing FPDS, FPPS, and FPNS on each processor.

Logic-based schedulability analysis for compositional hard real-time embedded systems

Over the past decades several approaches for schedulability analysis have been proposed for both uni-processor and multi-processor real-time systems. Although different techniques are employed, very little has been put forward in using formal specifications, with the consequent possibility for mis-interpretations or ambiguities in the problem statement. Using a logic based approach to schedulability analysis in the design of hard real-time systems eases the synthesis of correct-by-construction procedures for both static and dynamic verification processes. In this paper we propose a novel approach to schedulability analysis based on a timed temporal logic with time durations. Our approach subsumes classical methods for uni-processor scheduling analysis over compositional resource models by providing the developer with counter-examples, and by ruling out schedules that cause unsafe violations on the system. We also provide an example showing the effectiveness of our proposal.