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

Efeito da temperatura ambiente e do empenamento sobre o desempenho de frangas leves e semipesadas

Este trabalho foi conduzido para determinar os efeitos da temperatura ambiente e do empenamento das aves sobre o desempenho de duas linhagens de postura na fase de crescimento (10ª a 13ª semana de idade). Foram alojadas 480 aves de reposição da marca Hy-line, sendo 240 aves de cada linhagem W-36 (leve) e Brown (semipesada), em 5 câmaras climáticas com temperaturas de 12, 18, 24, 30 e 36ºC. em cada temperatura foram avaliadas 3 coberturas de pena; 100% (não depenada), 50% (depenada em 50% do corpo) e 0% (totalmente depenada). A análise estatística dos dados foi realizada segundo um esquema fatorial (5 x 3 x 2) sendo: 5 temperaturas, 3 porcentagens de cobertura de pena e 2 linhagens. Os dados foram submetidos a uma análise de regressão para a obtenção das curvas respostas com os melhores ajustes. A linhagem semipesada apresentou maior consumo de ração em relação à linhagem leve em todas as temperaturas. Houve diminuição do ganho de peso em função da redução no consumo de ração e aumento da temperatura. A linhagem leve apresentou uma maior amplitude nas faixas de conforto térmico (18,33ºC a 32,00ºC) do que a linhagem semipesada (23,75ºC a 29,50ºC).

Efeito da suplementação de cromo em dois níveis energéticos para poedeiras leves

Pós-graduação em Zootecnia - FMVZ

Estudo termoanalítico de complexos do fármaco Ibuprofeno com lantanídeos (III) leves no estado sólido com exceção do promécio

This Final Paper had as it main goal to make a thermoanalytical study of lighter trivalent lanthanides (Lanthanum, Cerium, Praseodymium, Neodymium, Samarium and Europium) with the Ibuprofen ligand (nonsteroidal anti-inflammatory) that have a general formula LnL3.nH2O, on solid state, where Ln are the Lanthanides, L is the Ibuprofen ligand and n = number of water molecules of hydration that went from 1,0 to all the compounds. In order to characterize this compounds, it has been used the thermoanalytical techniques TG-DTA (thermogravimetry - Diferential Thermal Analysis) and DSC (Diferential Scanning Calorimetry), Fourier transformed infrared spectroscopy (FTIR) and complexometric titration with EDTA. Through the TG-DTA technique, it has been possible to set the thermal stability of the compounds, the number of thermal decomposition steps and temperatures that ocurred that also provided stoichiometry to the synthesized compounds. The DSC technique has shown the enthalpy of dehydration of the samarium and europium compounds, it was not possible to see it in the other compounds due to a endothermic peak on the DSC curve not being formed. In the case of neodymium, a thermal event ocurred, in which it could be a oxidative decarboxylation right after the dehydration. The infrared was utilised to study the carboxilate groups streches, and so, suggest a ligand metals compound coordination, that to this present paper has been a bidentade bridged coordenation. At last, the complexometric tritation was used to very the ammount of metal present in each compound, and so, verify if the proposed stoichiometry was according to the theory

Comparação de compósitos obtidos via RTM de resina epóxi e fibra de carbono com e sem descontinuidade nos tecidos

Technology is growing interest in the use of composites, due to the requirement of lighter materials and more resistant, factors essential to meet the project specifications and reduce the operational cost. In the production of high performance structural composites, considering the aerospace criteria, the domestic industry has shown interest in the process of resin transfer molding (RTM) for reproducibility and low cost. This process is suitable for producing components of polymeric composites with relatively simple geometries, consistent thicknesses, high quality finish with no size limitations. The objective of this work was machined carbon steel to make a matched-die tooling for RTM and produce two composite plates of epoxy resin and carbon fiber fabric with and without induced discontinuities, which were compared towards their impregnation with ultrasound, their properties via tensile tests and thermal analysis. In ultrasonic inspection, it was found good impregnation of the preform of both composites. In the thermal analysis it was possible to check the degradation temperature of the composites, the glass transition temperature and it was found that the composites showed no effective cure cycles, but presented good performance in the tensile test when compared with aluminum alloy 7050 T7451 . The results showed that the injection strategy was appropriate since the laminate exhibited a good quality for the proposed application

Associação de carboidrases e fitase em dietas valorizadas e seus efeitos sobre desempenho e qualidade dos ovos de poedeiras leves

A total of 350 commercial Bovans White laying hens were used to evaluate the association of carbohydrases and phytase in enriched diets and its effects on performance and egg quality of laying hens. The experiment used a randomized design with five treatments and seven replicates. The treatments were: 1. Positive control without added enzymes and without nutrient enrichment, 2. Negative control (NC) 1 with 1.5% and 6% AME (kcal/kg) enrichment for corn and soybean meal respectively, 2% crude protein (CP) enrichment, and digestible limiting digestible amino acids plus the full matrix for the phytase enzyme; 3. NC 2 with 1.5% and 6% AME (kcal/kg) enrichment, respectively, for corn and soybean meal and 2% crude protein (CP) enrichment, and digestible limiting amino acids plus the sparse matrix for the phytase enzyme, 4. NC 1 supplemented with 100 g ton(-1) carbohydrase and 30g ton(-1) phytase, 5. NC 2 supplemented with 100 g ton(-1) carbohydrase and 30g ton(-1) phytase. According to the results, the positive control treatments, NC1 and NC2, with or without enzyme supplementation, showed guaranteed performance for feed intake, egg yield, weight, egg loss and shell quality.

Glutamina na dieta de poedeiras leves submetidas ao estresse pelo calor e à termoneutralidade

The aim of this study was to evaluate the effect of glutamine supplementation of the diet on intestinal mucosa morphology, performance, and egg quality of commercial laying hens, submitted to heat stress and thermoneutral conditions. In this study, 96 (Isa Babcock) laying hens at 35 weeks of age were used and distributed in a completely randomized design according to a 2x2 factorial arrangement, with two levels of ambient temperature (thermoneutral and hot) and two levels of glutamine in the diet (0.0 and 1.0% of inclusion), in 6 replicates of 4 hens per box. Feed intake, daily egg production, feed conversion per kilogram of eggs, and egg quality were obtained in two periods of 28 days each. Heat stress decreased egg production and quality, and glutamine supplementation improved egg quality and feed conversion. The heat and glutamine supplementation provided an increase in calliciform cells quantity in duodenum and ileum, respectively. Significant morphological modifications in the intestinal mucosa of laying hens were not found.

Métodos de debicagem: desenvolvimento e desempenho produtivo de poedeiras leves e semipesadas

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

Métodos de debicagem: desenvolvimento e desempenho produtivo de poedeiras leves e semipesadas

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