Metodologia de Verificação Funcional para Circuitos Analógicos

This work proposes a new methodology to verify those analog circuits, providing an automated tools to help the verifiers to have a more truthful result. This work presents the development of new methodology for analog circuits verification. The main goal is to provide a more automated verification process to certify analog circuits functional behavior. The proposed methodology is based on the golden model technique. A verification environment based on this methodology was built and results of a study case based on the validation of an operational amplifier design are offered as a confirmation of its effectiveness. The results had shown that the verification process was more truthful because of the automation provided by the tool developed

Desenvolvimento da modelagem de turbulência e interação fluido-estrutura para as vibrações induzidas por vórtices de cilindro rígido.

Esta tese apresenta o desenvolvimento e aplicação de modelos de turbulência, transição laminar-turbulenta e de interações fluido-estrutura ao escoamento externo em cilindro rígido estacionário e em vibrações induzidas por vórtices. Tais desenvolvimentos foram realizados no código ReFRESCO, baseado em técnicas de dinâmica de fluidos computacional (CFD). Realizou-se um estudo quanto ao desempenho do modelo k- SST em extensa faixa de números de Reynolds, segundo o qual se identificaram as deficiências de modelagem para este escoamento. A modelagem adaptativa das escalas (SAS) e o modelo de transição por correlações locais (LCTM), ambos combinados ao SST, melhoraram a aderência aos resultados experimentais para este escoamento, em uma contribuição original deste trabalho. A aplicação de técnicas de verificação e validação possibilitou a estimação de incertezas e erros para os modelos e números de Reynolds e também de identificada como outra contribuição deste trabalho. A combinação da modelagem em SST, SAS e LCTM com movimentos impostos de realizada para números de Reynolds moderados, diferentes frequências e amplitudes de vibração, algo que poucas publicações abordam em detalhes. Com relação aos movimentos livres, este trabalho traz contribuições com a aplicação dos modelos SST e SAS ao estudo de vibrações induzidas por vórtices em dois graus de liberdade, baixa razão de massa e números de Reynolds moderados, mais altos do que normalmente observados na literatura. Por fim, a investigação da importância relativa de efeitos da turbulência aos casos de movimentos livres e impostos, com relação ao caso de cilindro estacionário, comprovou a conjetura formulada na parte inicial deste trabalho, no que tange à escolha do modelo de turbulência em determinadas aplicações. Tal escolha mostrou-se menos decisiva no caso do cilindro em movimento imposto e ainda menos nos movimentos livres, em comparação ao caso estacionário, uma vez que a resposta em movimentos do corpo filtra grande parte dos efeitos turbulentos de ordem superior. Esta observação mostra-se relevante, uma vez que pode permitir simplificações na modelagem e aplicação de ferramentas de CFD em uma classe importante de projetos de engenharia.

Uma abordagem para avaliação e tratamento de exceções propagadas no uso de serviços Web em .Net

High dependability, availability and fault-tolerance are open problems in Service-Oriented Architecture (SOA). The possibility of generating software applications by integrating services from heterogeneous domains, in a reliable way, makes worthwhile to face the challenges inherent to this paradigm. In order to ensure quality in service compositions, some research efforts propose the adoption of verification techniques to identify and correct errors. In this context, exception handling is a powerful mechanism to increase SOA quality. Several research works are concerned with mechanisms for exception propagation on web services, implemented in many languages and frameworks. However, to the extent of our knowledge, no works found evaluates these mechanisms in SOA with regard to the .NET framework. The main contribution of this paper is to evaluate and to propose exception propagation mechanisms in SOA to applications developed within the .NET framework. In this direction, this work: (i)extends a previous study, showing the need to propose a solution to the exception propagation in SOA to applications developed in .NET, and (ii) show a solution, based in model obtained from the results found in (i) and that will be applied in real cases through of faults injections and AOP techniques.

Verificação à fadiga de pontes rodoviárias mistas (aço-concreto)

As pontes rodoviárias mistas (aço-concreto) estão sujeitadas às ações dinâmicas variáveis, por exemplo, devido ao tráfego de veículos sobre a superfície irregular do pavimento. Estas ações dinâmicas podem gerar a nucleação de fraturas ou mesmo a sua propagação sobre a estrutura. A correta consideração desses aspectos objetivou o desenvolvimento de uma metodologia de análise, com a finalidade de avaliar os níveis dos esforços e tensões oriundos do tráfego dos veículos sobre a superfície irregular do pavimento e, bem como, proceder uma verificação à fadiga de obras de arte rodoviárias em aço e mistas (aço-concreto). Para tal, as técnicas para a contagem de ciclos de tensão e a aplicação das regras de dano acumulado foram analisadas através de curvas do tipo S-N, associadas a diversas normas de projeto. A ponte rodoviária mista (aço-concreto) investigada neste estudo é constituída por quatro vigas de aço longitudinais e por um tabuleiro de concreto armado. O modelo numérico-computacional, desenvolvido para a análise dinâmica da ponte, foi concebido com base em técnicas usuais de discretização através do método dos elementos finitos. Simulam-se as almas das vigas de aço e as lajes de concreto do tabuleiro através de elementos finitos de casca. As mesas dessas vigas, transversinas e os enrijecedores são modelados por elementos de viga tridimensionais. Os veículos são representados a partir de sistemas "massa-mola-amortecedor". O tráfego dessas viaturas é considerado mediante a simulação de comboios semi-infinitos, deslocando-se com velocidade constante sobre a ponte. As conclusões da presente investigação versam acerca da vida útil de serviço dos elementos estruturais de pontes mistas (aço-concreto).

Uma proposta metodológica de integração de técnicas de análise espectral e de inteligência computacional, baseadas em conhecimento, para o reconhecimento de padrões em imagens multiespectrais

Somente no ano de 2011 foram adquiridos mais de 1.000TB de novos registros digitais de imagem advindos de Sensoriamento Remoto orbital. Tal gama de registros, que possui uma progressão geométrica crescente, é adicionada, anualmente, a incrível e extraordinária massa de dados de imagens orbitais já existentes da superfície da Terra (adquiridos desde a década de 70 do século passado). Esta quantidade maciça de registros, onde a grande maioria sequer foi processada, requer ferramentas computacionais que permitam o reconhecimento automático de padrões de imagem desejados, de modo a permitir a extração dos objetos geográficos e de alvos de interesse, de forma mais rápida e concisa. A proposta de tal reconhecimento ser realizado automaticamente por meio da integração de técnicas de Análise Espectral e de Inteligência Computacional com base no Conhecimento adquirido por especialista em imagem foi implementada na forma de um integrador com base nas técnicas de Redes Neurais Computacionais (ou Artificiais) (através do Mapa de Características Auto- Organizáveis de Kohonen SOFM) e de Lógica Difusa ou Fuzzy (através de Mamdani). Estas foram aplicadas às assinaturas espectrais de cada padrão de interesse, formadas pelos níveis de quantização ou níveis de cinza do respectivo padrão em cada uma das bandas espectrais, de forma que a classificação dos padrões irá depender, de forma indissociável, da correlação das assinaturas espectrais nas seis bandas do sensor, tal qual o trabalho dos especialistas em imagens. Foram utilizadas as bandas 1 a 5 e 7 do satélite LANDSAT-5 para a determinação de cinco classes/alvos de interesse da cobertura e ocupação terrestre em três recortes da área-teste, situados no Estado do Rio de Janeiro (Guaratiba, Mangaratiba e Magé) nesta integração, com confrontação dos resultados obtidos com aqueles derivados da interpretação da especialista em imagens, a qual foi corroborada através de verificação da verdade terrestre. Houve também a comparação dos resultados obtidos no integrador com dois sistemas computacionais comerciais (IDRISI Taiga e ENVI 4.8), no que tange a qualidade da classificação (índice Kappa) e tempo de resposta. O integrador, com classificações híbridas (supervisionadas e não supervisionadas) em sua implementação, provou ser eficaz no reconhecimento automático (não supervisionado) de padrões multiespectrais e no aprendizado destes padrões, pois para cada uma das entradas dos recortes da área-teste, menor foi o aprendizado necessário para sua classificação alcançar um acerto médio final de 87%, frente às classificações da especialista em imagem. A sua eficácia também foi comprovada frente aos sistemas computacionais testados, com índice Kappa médio de 0,86.

Verificação à fadiga estrutural de ponte em concreto armado.

As pontes rodoviárias de concreto armado estão sujeitas à ações dinâmicas variáveis devido ao tráfego de veículos sobre o tabuleiro. Estas ações dinâmicas nem sempre são corretamente consideradas pelos projetistas. Deste modo, a correta consideração destes aspectos mostra-se de fundamental importância, de forma a se avaliar os esforços dinâmicos oriundos do tráfego de veículos sobre o tabuleiro. De acordo com este contexto, a ponte rodoviária investigada nesta dissertação é constituída por duas vigas longitudinais, três transversinas, sendo uma central e duas sobre os apoios, e por um tabuleiro em concreto armado. O modelo computacional, desenvolvido para a análise dinâmica da ponte, foi concebido com base no emprego de técnicas usuais de discretização através do método dos elementos finitos. Os veículos são representados a partir de sistemas do tipo "massa-mola-amortecedor". O tráfego destes veículos é considerado mediante a simulação de comboios semi-infinitos, deslocando-se com velocidade constante sobre a ponte. As técnicas para a contagem de ciclos de tensões e a aplicação das regras de dano acumulado foram analisadas através das curvas S-N de diversas normas e recomendações internacionais vigentes que versam sobre o tema. As conclusões deste trabalho de pesquisa se referem à análise da resposta dinâmica bem como da vida útil de serviço da obra de arte rodoviária de concreto armado investigada, quando submetida às ações dinâmicas provenientes do tráfego de veículos pesados sobre o tabuleiro.

Análise dinâmica e verificação à fadiga de obras de arte rodoviárias mistas (aço-concreto) submetidas ao tráfego de veículos sobre o pavimento irregular.

As pontes rodoviárias metálicas e mistas (aço-concreto) são submetidas a um grande número de carregamentos repetitivos de diferentes magnitudes, ao longo do tempo. Estas ações dinâmicas podem causar a nucleação de fraturas ou mesmo a propagação destas sobre o sistema estrutural. A depender da magnitude, estes efeitos podem comprometer o sistema estrutural e a sua confiabilidade, além de reduzir a vida útil das pontes. Assim sendo, neste trabalho de pesquisa foi investigada a resposta dinâmica de uma ponte mista (aço-concreto), simplesmente apoiada, com vão de 40,0 m, submetida ao tráfego de veículos sobre a superfície irregular do pavimento. Para tal um modelo numérico representativo do sistema estrutural foi desenvolvido com base no emprego do programa ANSYS, por meio do uso de técnicas usuais de discretização, via método dos elementos finitos. Um estudo paramétrico foi desenvolvido para identificar, de forma qualitativa e quantitativa, o efeito das irregularidades do pavimento sobre o comportamento dinâmico da ponte mista investigada. Em seguida, a verificação do projeto à fadiga do sistema misto foi realizada, com base no emprego do algoritmo de contagem de ciclos Rainflow e em curvas S-N associadas às principais normas de projeto sobre o tema. As conclusões deste trabalho de pesquisa alertam aos engenheiros estruturais para a possibilidade concreta acerca do aumento do dano por fadiga, relacionado às ações dinâmicas de veículos trafegando sobre o tabuleiro de pontes em aço e mistas (aço-concreto).

Desenvolvimento de um modelo integrado de planejamento financeiro e verificação de sua aplicabilidade na indústria de candies do Rio Grande do Sul

Este estudo apresenta o desenvolvimento do modelo integrado de planejamento financeiro como uma peça gerencial de administração financeira. O modelo foi construído com o intuito de reunir e adaptar à realidade brasileira diferentes contribuições teóricas em uma estrutura única, através de uma sistematização de procedimentos e análises fundamentais que possibilitem o processo reflexivo e potencializem a capacidade analítica dos gestores financeiros. A esta estrutura foi acrescida a etapa “desenvolvimento e implementação”, onde há uma preocupação com as possíveis barreiras e oportunidades relacionadas à implementação na íntegra do modelo proposto. Posteriormente, foi verificada a aplicabilidade do modelo concebido em três empresas do setor alimentício, subsetor de candies, do Rio Grande do Sul. Para esta investigação, ligada à aplicação prática do planejamento financeiro nas empresas do setor analisado, foi empregada a pesquisa qualitativa, através do método de estudo de casos. O estudo evidenciou a insuficiente utilização de técnicas financeiras como instrumentos de suporte dos processos analítico e decisório, em especial do processo de planejamento financeiro, nas empresas analisadas. A investigação demonstra que o processo de planejamento financeiro tem ainda muito o que contribuir para uma otimização da gestão financeira das empresas estudadas.

Custo unitário básico (CUB) : verificação e validação do modelo de cálculo

O custo unitário básico (CUB), foi criado em função da Lei n° 4.591 (BRASIL, 1964), que encarregou a Associação Brasileira de Normas Técnicas (ABNT), através do Banco Nacional de Habitação (BNH), de definir critérios e normas para cálculo de custos unitários de construção pelos Sindicatos das Indústrias da Construção Civil (SINDUSCON) nos Estados da Federação, para uso dos incorporadores imobiliários nas tratativas iniciais quando da viabilização junto ao Sistema Financeiro de Habitações. Com a publicação da Norma Brasileira NB 140 (ASSOCIAÇÃO BRASILEIRA DE NORMAS TÉCNICAS, 1965), ficou definido a metodologia de cálculo dos CUB para projetos-padrão de prédios habitacionais. A finalidade destes CUB é auxiliar na avaliação dos custos de incorporações imobiliárias, antes do lançamento, quando os incorporadores não dispõem dos projetos completos. A metodologia de cálculo destes CUB sofreu uma única reformulação ao longo destes quase quarenta anos, quando da edição da NBR 12.721 (ASSOCIAÇÃO BRASILEIRA DE NORMAS TÉCNICAS, 1992). Em 1999, recebeu anexo complementar, que não fez qualquer atualização na metodologia de cálculo dos CUB, apenas estendeu a apuração destes custos para edifícios comerciais, galpões industriais e casas populares Este trabalho realizou a verificação e validação do modelo de cálculo dos CUB para prédios habitacionais, fazendo comparações entre os valores apurados pela técnica recomendada na Norma e os obtidos diretamente nos orçamentos discriminados que deram origem à metodologia de cálculo dos CUB, utilizando preços unitários de insumos no período de janeiro de 1993 a dezembro de 2000. Ao final concluiu-se que o modelo de cálculo dos CUB necessita de uma profunda reformulação para readquirir a propriedade fundamental de sua caracterização que é a de substituir o cálculo dos custos com o uso do orçamento discriminado dos projetos-padrão.

Investigação de técnicas de visualização para representação de autômatos finitos com saída

Atualmente, a World Wide Web (WWW) já se estabeleceu como um dos meios de divulgação mais difundidos. Sendo um meio de publicação de custo relativamente baixo, muitas iniciativas foram desenvolvidas no sentido de estendê-la e transformá-la também numa ferramenta de apoio. Assim, uma série de pesquisas foi realizada no sentido de promover e facilitar o gerenciamento das informações da WWW, que são estruturadas, em sua maioria, como conjuntos de documentos inter-relacionados. Grafos são estruturas utilizadas para a representação de objetos e seus múltiplos relacionamentos. Nesse sentido, pode-se afirmar que hiperdocumentos podem ser modelados através de grafos, onde uma página representa um nodo e um link para outra página é representado por uma aresta. Considerando estas características, e dada a crescente complexidade dos materiais publicados na WWW, desenvolveu-se, ao longo da última década, o uso de técnicas e recursos de Visualização de Grafos com larga aplicação na visualização da estrutura e da navegação na WWW. Técnicas de visualização de grafos são aplicáveis especificamente para representar visualmente estruturas que possam ser modeladas por meio de objetos relacionados, sendo investigadas técnicas para a abstração de modo a facilitar tanto o processo de compreensão do contexto da informação, quanto a apreensão dos dados relacionados. Este trabalho tem como objetivo a investigação de técnicas de Visualização de Grafos aplicadas a autômatos finitos com saída. Este direcionamento se deve ao fato de alguns autores utilizar a abordagem de autômatos finitos com saída para as estruturas de hiperdocumentos. Se for considerado que um documento da WWW (ou o estado de um autômato) é composto por fragmentos de informação (ou saídas) tais como trechos de texto, imagens, animações, etc e que este documento é relacionado a outros por meio de links (ou transições), tem-se a verificação de sua representatividade por meio destas estruturas. Em trabalho anterior, no âmbito do PPGC da UFRGS, a ferramenta Hyper-Automaton foi desenvolvida com o objetivo de estender o uso da Internet no sentido de prover uma ferramenta de apoio à publicação de materiais instrucionais. Por adotar a notação de autômatos finitos com saída, possibilita, além da criação e gerenciamento de hiperdocumentos, a reutilização de fragmentos de informação sem que haja qualquer interferência de um autômato que utilize este fragmento sobre outro. O Hyper-Automaton foi selecionado como caso de estudo motivador deste trabalho. As técnicas aqui desenvolvidas têm como intuito diminuir a complexidade visual da informação, assim como permitir a navegação através dos autômatos finitos com saída de forma que seja possível visualizar detalhes como as saídas e informações relacionadas a cada uma delas, mantendo a visualização do contexto da informação. Foram analisadas técnicas de agrupamento como forma de redução da complexidade visual, e técnicas do tipo foco+contexto, como alternativa para prover a visualização simultânea do contexto e dos detalhes da informação.

Subsídios à previsão de safra da soja no Rio Grande do Sul usando técnicas de geoprocessamento e sensoriamento remoto

Informações sobre as condições de crescimento e expectativa de produção de culturas são importantes para a economia brasileira, visto que permitem um planejamento adequado da economia agrícola, contornando problemas de escassez e administrando com vantagens o excesso de produtos. Neste contexto, as tecnologias de sensoriamento remoto e geoprocessamento permitem a obtenção de informações precisas, em tempo hábil e com baixo custo. O presente trabalho teve como principal objetivo gerar subsídios para o aprimoramento do sistema atual de acompanhamento e previsão da safra de soja no Brasil, incorporando técnicas de sensoriamento remoto e geoprocessamento. Como objetivos específicos, buscou-se avaliar a acurácia da classificação digital de imagens LANDSAT para estimativa da área cultivada com soja e verificar a influência de aspectos regionais, tais como condições climáticas, de ocupação e de manejo, sobre a evolução temporal do índice de vegetação por diferença normalizada (NDVI), obtidos de imagens NOAA, visando o monitoramento da cultura da soja em projetos de previsão de safras. A estimativa de área cultivada com soja foi realizada através da classificação digital não supervisionada. Como verdade terrestre foram selecionadas 24 lavouras de soja, individualizadas na imagem com diferentes tamanhos e de diferentes regiões de uso e cobertura do solo, as quais foram quantificadas usando GPS de precisão topográfica. A verificação da acurácia da estimativa foi feita através de análise de regressão linear, sendo testada a significância do coeficiente de determinação. O monitoramento da cultura da soja foi realizada usando imagens decendiais de máximo NDVI. Nestas imagens, foram selecionadas 18 janelas amostrais, sendo extraídos os valores de NDVI e expressos na forma de perfis espectrais. Os resultados mostraram que a estimativa de área das lavouras cultivadas com soja, obtida através do processo de classificação digital não supervisionada em imagens LANDSAT, foi acurada e precisa para pequenas, médias e grandes lavouras, mostrando-se ser uma técnica eficiente para ser utilizada em projetos de previsão de safras de soja na região estudada. A evolução temporal do NDVI, obtida de imagens NOAA, apresentou sensibilidade quanto às diferenças de uso e cobertura do solo, demonstrando que as escalas espacial e temporal das imagens NOAA são adequadas para o acompanhamento em nível regional da evolução temporal da biomassa. Existe, ainda, potencial de uso de imagens NDVI para inferir sobre a área cultivada com soja em projetos de previsão de safras em escalas regionais, desde que a cultura seja predominante no pixel.

Estimativa da evapotranspiração regional por meio de técnicas de sensoriamento remoto integradas a modelos de balanço de energia : aplicação no estado do Rio Grande do Sul

A evapotranspiração (ET) abrange todos os processos que envolvem a mudança de fase líquida ou sólida para vapor de água. Globalmente, suas principais componentes são a evaporação nos oceanos, corpos d’água e solo e a transpiração pela cobertura vegetal. O conhecimento da ET da superfície terrestre para a atmosfera é muito importante para a resolução de inúmeras questões relacionadas aos recursos hídricos. Dentre essas questões, destacam-se planejamento de bacias hidrográficas e, em especial, o manejo da irrigação. Esse tipo de informação é igualmente relevante para estudos climáticos uma vez que, por meio da ET, ocorre redistribuição de umidade e calor da superfície para a atmosfera.As metodologias convencionais de estimativa da ET, em geral, apresentam muitas incertezas. Essas incertezas aumentam muito quando o interesse é o comportamento espacial da mesma. A única tecnologia que permite acessar esse tipo de informação, de forma eficiente e econômica, é o sensoriamento remoto. Por meio de dados derivados de imagens de satélite é possível calcular o balanço de energia de uma região e acessar as reais taxas de ET. A literatura internacional apresenta alguns modelos para estimar a ET por meio de sensoriamento remoto. A verificação dessas estimativas é feita por medidas dos termos do balanço de energia realizadas por sensores colocados em torres meteorológicas. Esse tipo de informação, no entanto, é de alto custo e de difícil aquisição. Após revisão de literatura, foram escolhidos os algoritmos SEBAL (Surface Energy Balance Algorithm for Land) e SSEBI (Simplified Surface Energy Balance Index). O primeiro foi adotado por ser um dos mais utilizados e o segundo pela sua simplicidade.Dessa maneira, a partir de 44 imagens de satélite, praticamente livres de cobertura de nuvens, do sensor AVHRR (Advanced Very High Resolution Radiometer), a bordo do satélite NOAA-14, e dados climatológicos de algumas estações, foram geradas séries de coberturas de ET real para o Estado do Rio Grande do Sul em nível diário, durante o ano de 1998. Para efeito de simplificação, na análise dos resultados foram escolhidas algumas áreas representativas das principais classes de cobertura do Estado: área cultivada, campo, área urbana, banhado, lagoa e floresta. Os resultados demonstraram que, para o SEBAL, asperdas médias anuais (mm ano-1) ocorrem, em ordem decrescente nas classes banhado (827), lagoa (732), floresta (686), área cultivada (458), campo (453) e área urbana (276). Para o S-SEBI, esta ordem é a seguinte: floresta (918), banhado (870), lagoa (669), área cultivada (425), campo (403) e área urbana (363). Ficou evidente que as classes com as menores influências antrópicas apresentaram as maiores taxas de ET. Outra observação feita é que, em média, as estimativas do S-SEBI superestimam a ET em relação ao SEBAL, na porção leste do Estado, e o oposto na porção oeste. Foi verificado, ainda, um eixo de decréscimo da ET na primeira metade do ano da porção noroeste para sudeste, e posterior crescimento na segunda metade do ano, em sentido oposto.As verificações foram feitas de forma indireta por meio de um balanço hídrico anual simplificado em algumas bacias hidrográficas do Estado, por meio de valores de ET real para a cultura do milho em algumas localidades do Estado e medidas de evaporação de tanque do tipo Classe A. Em geral, os resultados foram considerados coerentes, o que confere à metodologia utilizada um grande potencial de uso, uma vez que possibilita acessar a distribuição espacial da ET.

Verificação de ciclos no mercado segurador brasileiro

Este trabalho se propõe a avaliar a existência de ciclos de margem de subscrição no mercado segurador brasileiro para os grupos de ramos de automóvel, patrimonial, responsabilidade civil e transportes a partir de dados da SUSEP. É feita uma introdução em seguros, uma revisão dos artigos que foram realizados no mundo sobre o assunto assim como os estudos discorrendo sobre as possíveis causas para a existência destes ciclos. Em seguida são apresentadas as técnicas econométricas de séries de tempo estruturais e o teste HEGY utilizadas para a verificação dessa hipótese. Foram encontrados ciclos nos grupos de ramos de automóveis, patrimoniais e transportes e não encontramos evidências de ciclos para responsabilidade civil e nem para o agregado de ramos. Os resultados desse estudo sobre a existência, ou não dos ciclos, assim como sua duração considerando as particularidades de cada tipo de ramo, periodicidade das séries e utilização ou não da despesa de comercialização foram analisados para cada grupo de ramos, considerando suas particularidades. Finalmente se fez um comparativo dos resultados obtidos nesse estudo com o que está na literatura para diversos outros mercados de seguros de outros países.

A contribuição de técnicas modernas de reabilitação estrutural para autenticidade e integridade de edificações patrimoniais

This work discusses the study of the application of structural reinforcement and rehabilitation using modern techniques for interventions in repair works of historical buildings as well as the verification of the behavior of works that have already undergone different structural intervention techniques, with the objective of obtaining data to allow a comparative analysis of the advantages/disadvantages of techniques adapted in each case, regarding the interferences related the authenticity and integrity of the buildings belong to the constructed patrimony so as to obtain a basis for the theoretical foundation for choosing the best solution to be adopted in the case study which consists in an intervention of structural rehabilitation of the old historic building in the primary school "Augusto Severo"

Contribuições para verificação automática de applets javacard

The widespread growth in the use of smart cards (by banks, transport services, and cell phones, etc) has brought an important fact that must be addressed: the need of tools that can be used to verify such cards, so to guarantee the correctness of their software. As the vast majority of cards that are being developed nowadays use the JavaCard technology as they software layer, the use of the Java Modeling Language (JML) to specify their programs appear as a natural solution. JML is a formal language tailored to Java. It has been inspired by methodologies from Larch and Eiffel, and has been widely adopted as the de facto language when dealing with specification of any Java related program. Various tools that make use of JML have already been developed, covering a wide range of functionalities, such as run time and static checking. But the tools existent so far for static checking are not fully automated, and, those that are, do not offer an adequate level of soundness and completeness. Our objective is to contribute to a series of techniques, that can be used to accomplish a fully automated and confident verification of JavaCard applets. In this work we present the first steps to this. With the use of a software platform comprised by Krakatoa, Why and haRVey, we developed a set of techniques to reduce the size of the theory necessary to verify the specifications. Such techniques have yielded very good results, with gains of almost 100% in all tested cases, and has proved as a valuable technique to be used, not only in this, but in most real world problems related to automatic verification