Estendendo CRefine para o suporte de táticas de refinamento

The use of increasingly complex software applications is demanding greater investment in the development of such systems to ensure applications with better quality. Therefore, new techniques are being used in Software Engineering, thus making the development process more effective. Among these new approaches, we highlight Formal Methods, which use formal languages that are strongly based on mathematics and have a well-defined semantics and syntax. One of these languages is Circus, which can be used to model concurrent systems. It was developed from the union of concepts from two other specification languages: Z, which specifies systems with complex data, and CSP, which is normally used to model concurrent systems. Circus has an associated refinement calculus, which can be used to develop software in a precise and stepwise fashion. Each step is justified by the application of a refinement law (possibly with the discharge of proof obligations). Sometimes, the same laws can be applied in the same manner in different developments or even in different parts of a single development. A strategy to optimize this calculus is to formalise these application as a refinement tactic, which can then be used as a single transformation rule. CRefine was developed to support the Circus refinement calculus. However, before the work presented here, it did not provide support for refinement tactics. The aim of this work is to provide tool support for refinement tactics. For that, we develop a new module in CRefine, which automates the process of defining and applying refinement tactics that are formalised in the tactic language ArcAngelC. Finally, we validate the extension by applying the new module in a case study, which used the refinement tactics in a refinement strategy for verification of SPARK Ada implementations of control systems. In this work, we apply our module in the first two phases of this strategy

Beta: uma ferramenta para geração de testes de unidade a partir de especificações B

Formal methods and software testing are tools to obtain and control software quality. When used together, they provide mechanisms for software specification, verification and error detection. Even though formal methods allow software to be mathematically verified, they are not enough to assure that a system is free of faults, thus, software testing techniques are necessary to complement the process of verification and validation of a system. Model Based Testing techniques allow tests to be generated from other software artifacts such as specifications and abstract models. Using formal specifications as basis for test creation, we can generate better quality tests, because these specifications are usually precise and free of ambiguity. Fernanda Souza (2009) proposed a method to define test cases from B Method specifications. This method used information from the machine s invariant and the operation s precondition to define positive and negative test cases for an operation, using equivalent class partitioning and boundary value analysis based techniques. However, the method proposed in 2009 was not automated and had conceptual deficiencies like, for instance, it did not fit in a well defined coverage criteria classification. We started our work with a case study that applied the method in an example of B specification from the industry. Based in this case study we ve obtained subsidies to improve it. In our work we evolved the proposed method, rewriting it and adding characteristics to make it compatible with a test classification used by the community. We also improved the method to support specifications structured in different components, to use information from the operation s behavior on the test case generation process and to use new coverage criterias. Besides, we have implemented a tool to automate the method and we have submitted it to more complex case studies

Geração automática de hardware apartir de especificações formais: estendendo uma abordagem de tradução

A remoção de inconsistências em um projeto é menos custosa quando realizadas nas etapas iniciais da sua concepção. A utilização de Métodos Formais melhora a compreensão dos sistemas além de possuir diversas técnicas, como a especificação e verificação formal, para identificar essas inconsistências nas etapas iniciais de um projeto. Porém, a transformação de uma especificação formal para uma linguagem de programação é uma tarefa não trivial. Quando feita manualmente, é uma tarefa passível da inserção de erros. O uso de ferramentas que auxiliem esta etapa pode proporcionar grandes benefícios ao produto final a ser desenvolvido. Este trabalho propõe a extensão de uma ferramenta cujo foco é a tradução automática de especificações em CSPm para Handel-C. CSP é uma linguagem de descrição formal adequada para trabalhar com sistemas concorrentes. Handel-C é uma linguagem de programação cujo resultado pode ser compilado diretamente para FPGA's. A extensão consiste no aumento no número de operadores CSPm aceitos pela ferramenta, permitindo ao usuário definir processos locais, renomear canais e utilizar guarda booleana em escolhas externas. Além disto, propomos também a implementação de um protocolo de comunicação que elimina algumas restrições da composição paralela de processos na tradução para Handel-C, permitindo que a comunicação entre múltiplos processos possa ser mapeada de maneira consistente e que a mesma somente ocorra quando for autorizada.

Geração automática de hardware a partir de especificações formais: estendendo uma abordagem de tradução

Removing inconsistencies in a project is a less expensive activity when done in the early steps of design. The use of formal methods improves the understanding of systems. They have various techniques such as formal specification and verification to identify these problems in the initial stages of a project. However, the transformation from a formal specification into a programming language is a non-trivial task and error prone, specially when done manually. The aid of tools at this stage can bring great benefits to the final product to be developed. This paper proposes the extension of a tool whose focus is the automatic translation of specifications written in CSPM into Handel-C. CSP is a formal description language suitable for concurrent systems, and CSPM is the notation used in tools support. Handel-C is a programming language whose result can be compiled directly into FPGA s. Our extension increases the number of CSPM operators accepted by the tool, allowing the user to define local processes, to rename channels in a process and to use Boolean guards on external choices. In addition, we also propose the implementation of a communication protocol that eliminates some restrictions on parallel composition of processes in the translation into Handel-C, allowing communication in a same channel between multiple processes to be mapped in a consistent manner and that improper communication in a channel does not ocurr in the generated code, ie, communications that are not allowed in the system specification

Controle de mofo-cinzento (amphobotrys ricini) da mamoneira (ricinus communis l.) por métodos químico, biológico e com óleos essenciais

Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq)

Um estudo das componentes simétricas generalizadas em sistemas trifásicos não senoidais

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES)

Métodos para a tomada de decisão em portfólio de produtos: um levantamento em empresas dos setores eletrônico, óptico e de informática

Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)

Análise de aspectos socioeconômicos e tecnológicos da agropecuária na Bacia Hidrográfica do Rio Mogi Guaçu

Currently, owing to the occurrence of environmental problems, along with the need of environmental preservation, both the territory management of Hydrographic Basin and the conservation of natural resources have proven to have remarkable importance. Thus, the mean goal of the research is to raise and scrutinize social-economic and technologic data from the Mogi Guaçu River Hydrographic Basin (São Paulo, Brazil). The aim is to group municipalities with similar characteristics regarding the collected data, which may direct joint actions in the Hydrographic Basin Management. There were used both the methods of factorial analysis and automatic hierarchical classifications. Additionally, there is going to be applied a Geographical Information System to represent the outcomes of the methods aforementioned, through the evolvement of a geo-referenced database, which will allow the obtainment of information categorically distributed including theme maps of interest. The main characteristics adopted to group the municipalities were: agricultural area, sugar cane production, small farms, animal production, number of agriculture machinery and equipments and agricultural income. The methodology adopted in the Mogi Guaçu River Hydrographic Basin will be analyzed vis-à-vis its appropriateness on basin management, as well as the possibility of assisting the studies on behalf of the São Paulo Hydrographic Basin groups, to regional development.

Regulador de crescimento em plantas de trigo: reflexos sobre o desenvolvimento vegetativo, rendimento e qualidade de grãos

RESUMO Reguladores de crescimento podem ser utilizados com o intuito de evitar o acamamento do trigo, porém, podem apresentar outros benefícios, em função da melhoria da interceptação de luz e da realocação de carbono. O objetivo deste trabalho foi avaliar a influência do regulador de crescimento (trinexapac-etil) sobre o desenvolvimento vegetativo, os componentes da produção e a qualidade de grãos de dois cultivares de trigo distintos em relação à susceptibilidade ao acamamento. Um experimento foi realizado em casa de vegetação e outro a campo. No experimento em casa de vegetação, foram avaliadas as variáveis de desenvolvimento vegetativo (estatura de planta, relação entre raiz e parte aérea, áreas foliares unitária e total, comprimento e matéria seca de raízes) em plantas de trigo, com e sem a aplicação de trinexapac-etil, em estádio de primeiro nó visível e segundo nó perceptível. A campo foram avaliadas variáveis de desenvolvimento vegetativo (clorofila, estatura e área foliar), rendimento (número de espigas, massa de mil grãos e produtividade) e qualidade (massa do hectolitro e conteúdo de proteína), em plantas de trigo com variações de aplicação de trinexapac-etil (testemunha sem aplicação, perfilhamento e primeiro nó visível e segundo perceptível). O regulador de crescimento trinexapac-etil aumenta a relação entre raiz e parte aérea do cultivar Mirante e a produtividade dos cultivares Quartzo e Mirante. Porém, não interfere na qualidade de grãos desses cultivares.

Plataforma de desenvolvimento de aplicações web orientadas a mensagens

O projecto apresentado neste relatório consiste na implementação de uma plataforma de desenvolvimento de aplicações Web orientada a mensagens, capaz de facilitar a construção de páginas Web e de automatizar o acesso a dados com base nos requisitos do problema. O foco da solução é baseado nos requisitos que forem definidos, de modo a desenvolver uma aplicação Web que responda a esses requisitos. A estratégia adoptada visa reduzir o acoplamento e aumentar a coesão dos módulos funcionais. Para reduzir o acoplamento e aumentar a coesão dos módulos funcionais separou-se a apresentação dos dados, permitindo assim que o desenvolvimento e os testes sejam realizados independentemente um do outro. O desenvolvimento é baseado em normas padronizadas (standards) de modo a facilitar a integração com outras tecnologias. Para o desenvolvimento do trabalho foi adoptada uma metodologia ágil. A gestão de projecto foi realizada com recurso a uma plataforma de gestão de projecto, que permitiu registar e organizar todas as informações e tarefas realizadas ao longo do projecto. Após a conclusão da plataforma e como caso de estudo, foi realizada uma aplicação baseada num cenário real de gestão académica (Portal Académico) para aferir os conceitos envolvidos.

Invisibilidade do uso de drogas e a assistência de profissionais dos serviços de Aids

OBJETIVO: Descrever a influência das concepções dos profissionais de saúde sobre o cuidado prestado a pacientes usuários de drogas vivendo com HIV/Aids. MÉTODOS: Estudo qualitativo baseado em entrevistas semi-estruturadas com 22 profissionais de diferentes categorias, pertencentes a dois serviços especializados em DST/Aids da rede municipal de São Paulo, em 2002. As entrevistas foram gravadas e submetidas à análise temática. RESULTADOS: Os profissionais relataram dificuldades em identificar usuários de drogas entre seus pacientes, indicando a invisibilidade da questão. Acham os usuários de drogas pacientes mais difíceis de tratar, por tumultuarem o serviço e/ou não aderirem ao tratamento. Embora reconheçam necessidades especiais dos pacientes usuários e que lidar com o uso de drogas seja importante, os profissionais de saúde acreditam que essas questões fogem de suas atribuições. Os profissionais mostraram limites pessoais e técnicos para o manejo desses casos, indicando sua falta de capacitação específica como importante. Assim, recomendam a criação de serviços especializados para esse atendimento, reconhecendo os serviços em que atuam como inadequados e, embora conhecessem o projeto de redução de danos, pouco participavam dele. CONCLUSÕES: Elementos técnicos, ideológicos e pessoais, tais como crenças, valores e dimensões afetivo-emocionais, mostraram-se relevantes para ampliar ou recusar vínculos mais específicos com o paciente usuário de drogas. As concepções sobre o uso de drogas podem interferir no desenvolvimento de uma assistência melhor e da eqüidade no cuidado em saúde.

Separação de dados hiperespectrais por análise de componentes dependentes

A separação de dados hiperespectrais pretende determinar quais as substâncias presentes numa imagem e quais as suas concentrações em cada pixel. Esta comunicação apresenta um método não-supervisionado, denominado de Análise de Componentes Dependentes (DECA), que efectua a separação destes dados automaticamente. Este método assume que cada pixel é uma mistura linear das assinaturas (reflectâncias ou radiâncias) das substâncias presentes pesadas pelas respectivas concentrações (abundâncias). Estas abundâncias são modeladas por misturas de distribuições de Dirichlet, que por si garantem as restrições de não-negatividade e soma unitária impostas pelo processo de aquisição. A matriz de assinaturas é estimada por um algoritmo Esperança-Maximização generalizado (GEM). O método DECA tem um desempenho melhor que os métodos baseados em análise de componentes independentes e que os métodos baseados na geometria dos dados. Nesta comunicação apresentam-se resultados desta metodologia, com dados simulados (baseados em reflectâncias espectrais da base de dados do laboratório USGS) e com dados hiperespectrais reais adquiridos pelo sensor AVIRIS, ilustrando a potencialidade da técnica.

Tolerância a falhas em sistemas de tempo-real distribuídos e embebidos

Este documento descreve um modelo de tolerância a falhas para sistemas de tempo-real distribuídos. A sugestão deste modelo tem como propósito a apresentação de uma solu-ção fiável, flexível e adaptável às necessidades dos sistemas de tempo-real distribuídos. A tolerância a falhas é um aspeto extremamente importante na construção de sistemas de tempo-real e a sua aplicação traz inúmeros benefícios. Um design orientado para a to-lerância a falhas contribui para um melhor desempenho do sistema através do melhora-mento de aspetos chave como a segurança, a confiabilidade e a disponibilidade dos sis-temas. O trabalho desenvolvido centra-se na prevenção, deteção e tolerância a falhas de tipo ló-gicas (software) e físicas (hardware) e assenta numa arquitetura maioritariamente basea-da no tempo, conjugada com técnicas de redundância. O modelo preocupa-se com a efi-ciência e os custos de execução. Para isso utilizam-se também técnicas tradicionais de to-lerância a falhas, como a redundância e a migração, no sentido de não prejudicar o tempo de execução do serviço, ou seja, diminuindo o tempo de recuperação das réplicas, em ca-so de ocorrência de falhas. Neste trabalho são propostas heurísticas de baixa complexida-de para tempo-de-execução, a fim de se determinar para onde replicar os componentes que constituem o software de tempo-real e de negociá-los num mecanismo de coordena-ção por licitações. Este trabalho adapta e estende alguns algoritmos que fornecem solu-ções ainda que interrompidos. Estes algoritmos são referidos em trabalhos de investiga-ção relacionados, e são utilizados para formação de coligações entre nós coadjuvantes. O modelo proposto colmata as falhas através de técnicas de replicação ativa, tanto virtual como física, com blocos de execução concorrentes. Tenta-se melhorar ou manter a sua qualidade produzida, praticamente sem introduzir overhead de informação significativo no sistema. O modelo certifica-se que as máquinas escolhidas, para as quais os agentes migrarão, melhoram iterativamente os níveis de qualidade de serviço fornecida aos com-ponentes, em função das disponibilidades das respetivas máquinas. Caso a nova configu-ração de qualidade seja rentável para a qualidade geral do serviço, é feito um esforço no sentido de receber novos componentes em detrimento da qualidade dos já hospedados localmente. Os nós que cooperam na coligação maximizam o número de execuções para-lelas entre componentes paralelos que compõem o serviço, com o intuito de reduzir atra-sos de execução. O desenvolvimento desta tese conduziu ao modelo proposto e aos resultados apresenta-dos e foi genuinamente suportado por levantamentos bibliográficos de trabalhos de in-vestigação e desenvolvimento, literaturas e preliminares matemáticos. O trabalho tem também como base uma lista de referências bibliográficas.

Desenvolvimento de um Projecto Agenda 21 Local para o Município de São Brás de Alportel

Relatório de Estágio de Mestrado em Globalização e Ambiente

Comparação dos métodos ENF e 4-ENF para determinação da tenacidade ao corte de juntas adesivas

Ao longo destes últimos anos as ligações adesivas têm vindo a verificar um aumento progressivo em aplicações estruturais em detrimento das ligações mecânicas convencionais. Esta alteração de paradigma deve-se às vantagens que as juntas adesivas possuem relativamente aos outros métodos de ligação. A mecânica da fratura e os Modelos de Dano Coesivo (MDC) são critérios comuns para prever a resistência em juntas adesivas e usam como parâmetros fundamentais as taxas de libertação de energia. Pelo facto do ensaio 4-Point End Notched Flexure (4-ENF), aplicado em juntas adesivas, ainda estar pouco estudado é de grande relevância um estudo acerca da sua viabilidade para a determinação da taxa crítica de libertação de energia de deformação ao corte (GIIc). Esta dissertação tem como objetivo principal efetuar uma comparação entre os métodos End- Notched Flexure (ENF) e 4-ENF na determinação de GIIc em juntas adesivas. Para tal foram utilizados 3 adesivos: Araldite® AV138, Araldite® 2015 e SikaForce® 7752. O trabalho experimental passou pela conceção e fabrico de uma ferramenta para realização do ensaio 4-ENF, seguindo-se o fabrico e a preparação dos provetes para os ensaios. Pelo facto do ensaio 4-ENF ainda se encontrar pouco divulgado em juntas adesivas, e não se encontrar normalizado, uma parte importante do trabalho passou pela pesquisa e análise em trabalhos de investigação e artigos científicos. A análise dos resultados foi realizada por comparação direta dos valores de GIIc com os resultados obtidos no ensaio ENF, sendo realizada por série de adesivo, através da comparação das curvas P-δ e curvas-R. Como resultado verificou-se que o ensaio 4-ENF em ligações adesivas não é o mais versátil para a determinação do valor de GIIc, e que apenas um método de obtenção de GIIc é viável. Este método é baseado na medição do comprimento de fenda (a). Ficou evidenciado que o ensaio ENF, devido a ser um ensaio normalizado, por apresentar um setup mais simples e por apresentar uma maior disponibilidade de métodos para a determinação do valor de GIIc, é o mais recomendado. Conclui-se assim que o ensaio 4-ENF, embora sendo uma alternativa ao ensaio ENF, tem aplicação mais limitada.