Prova automática de satisfatibilidade módulo teoria aplicada ao método B

Este trabalho apresenta uma extensão do provador haRVey destinada à verificação de obrigações de prova originadas de acordo com o método B. O método B de desenvolvimento de software abrange as fases de especificação, projeto e implementação do ciclo de vida do software. No contexto da verificação, destacam-se as ferramentas de prova Prioni, Z/EVES e Atelier-B/Click n Prove. Elas descrevem formalismos com suporte à checagem satisfatibilidade de fórmulas da teoria axiomática dos conjuntos, ou seja, podem ser aplicadas ao método B. A checagem de SMT consiste na checagem de satisfatibilidade de fórmulas da lógica de primeira-ordem livre de quantificadores dada uma teoria decidível. A abordagem de checagem de SMT implementada pelo provador automático de teoremas haRVey é apresentada, adotando-se a teoria dos vetores que não permite expressar todas as construções necessárias às especificações baseadas em conjuntos. Assim, para estender a checagem de SMT para teorias dos conjuntos destacam-se as teorias dos conjuntos de Zermelo-Frankel (ZFC) e de von Neumann-Bernays-Gödel (NBG). Tendo em vista que a abordagem de checagem de SMT implementada no haRVey requer uma teoria finita e pode ser estendida para as teorias nãodecidíveis, a teoria NBG apresenta-se como uma opção adequada para a expansão da capacidade dedutiva do haRVey à teoria dos conjuntos. Assim, através do mapeamento dos operadores de conjunto fornecidos pela linguagem B a classes da teoria NBG, obtem-se uma abordagem alternativa para a checagem de SMT aplicada ao método B

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

Formal verification of PLC programs using the B Method

PLCs (acronym for Programmable Logic Controllers) perform control operations, receiving information from the environment, processing it and modifying this same environment according to the results produced. They are commonly used in industry in several applications, from mass transport to petroleum industry. As the complexity of these applications increase, and as various are safety critical, a necessity for ensuring that they are reliable arouses. Testing and simulation are the de-facto methods used in the industry to do so, but they can leave flaws undiscovered. Formal methods can provide more confidence in an application s safety, once they permit their mathematical verification. We make use of the B Method, which has been successfully applied in the formal verification of industrial systems, is supported by several tools and can handle decomposition, refinement, and verification of correctness according to the specification. The method we developed and present in this work automatically generates B models from PLC programs and verify them in terms of safety constraints, manually derived from the system requirements. The scope of our method is the PLC programming languages presented in the IEC 61131-3 standard, although we are also able to verify programs not fully compliant with the standard. Our approach aims to ease the integration of formal methods in the industry through the abbreviation of the effort to perform formal verification in PLCs

Contribuições para o processo de verificação de satisfatibilidade módulo teoria em Event-B

Event-B is a formal method for modeling and verification of discrete transition systems. Event-B development yields proof obligations that must be verified (i.e. proved valid) in order to keep the produced models consistent. Satisfiability Modulo Theory solvers are automated theorem provers used to verify the satisfiability of logic formulas considering a background theory (or combination of theories). SMT solvers not only handle large firstorder formulas, but can also generate models and proofs, as well as identify unsatisfiable subsets of hypotheses (unsat-cores). Tool support for Event-B is provided by the Rodin platform: an extensible Eclipse based IDE that combines modeling and proving features. A SMT plug-in for Rodin has been developed intending to integrate alternative, efficient verification techniques to the platform. We implemented a series of complements to the SMT solver plug-in for Rodin, namely improvements to the user interface for when proof obligations are reported as invalid by the plug-in. Additionally, we modified some of the plug-in features, such as support for proof generation and unsat-core extraction, to comply with the SMT-LIB standard for SMT solvers. We undertook tests using applicable proof obligations to demonstrate the new features. The contributions described can potentially affect productivity in a positive manner.

Nossa notação m' na prova de Rorschach: ampliação e restrição do fator m de Klopfer

Klopfer's differentiation of movement scores, among which inanimate movement integrating the minor movements group, was no doubt opportune and needed. Their peculiar meaning has been clearly stressed and enriched by Piotrowski in his reformulation of Rorschach variables. It is our belief that Rorschach himself would take such step. Our criteria for scoring this determinant are somewhat different of both Klopfer's and Piotrowski's. On the one hand, masks, facial traits, emotional expressions, body parts in motion are not entered there. On the other, we score as such human or animal movement, provided this does not originate in the blot shape directly, but in the subjective reaction against the sensed muscular tension. Basic requirement for this scoring is the kinesthetic component, as for Mever since Rorschach's elaboration; and common trait distinctive for any response to be so scored ? be it an abstraction, an inanimate object, an animal or human being ? must be the subjective way of feeling the movement: (a) intention, blocking, struggle for achieving, for instance, or (b) activity of nature elements. Due to this subjective meaning we use the symbol m'intead of mfor this category. We already find these two kinds (a) and (b) of movement responses in Rorschach's text, respectively in the Examplesand in his posthumous Contribution.Either may point to a flight from emotional stress or to outstanding mental ability.

Técnica de bombeio e prova para medidas de absorção de estado excitado e de emissão estimulada, em materiais sólidos dopados com íons terras raras

Rare earth ion doped solid state materials are the most important active media of near-infrared and visible lasers and other photonic devices. In these ions, the occurrence of Excited State Absorptions (ESA), from long lived electronic levels, is commonplace. Since ESA can deeply affect the efficiencies of the rare earth emissions, evaluation of these transitions cross sections is of greatest importance in predicting the potential applications of a given material. In this paper a detailed description of the pump-probe technique for ESA measurements is presented, with a review of several examples of applications in Nd3+, Tm3+ and Er3+ doped materials.

Educação em direito na formação para cidadania : um estudo exploratório de concepções de estudantes do terceiro ano do ensino médio sobre direitos e obrigações essenciais ao exercício da vida civil

O presente trabalho teve como objetivo principal investigar concepções que estudantes do terceiro ano do ensino médio possuem sobre direitos e obrigações essenciais ao exercício da cidadania. Para tanto, foi elaborado um questionário composto de 20 questões fechadas e 9 questões abertas na forma de estudo de caso abordando alguns direitos e obrigações essenciais ao exercício pleno da vida civil. O instrumento foi submetido a 136 estudantes, entre 16 e 18 anos, de ambos os sexos, regularmente matriculados no terceiro ano de três escolas públicas de Ensino Médio. Os resultados apontam que, de modo geral, as concepções dos estudantes sobre legislação estão mais próximas das disposições legislativas naqueles direitos que permeiam sua realidade prática e, vai se distanciando à medida que os direitos propostos estavam distantes de sua realidade, de modo que, aparentemente, o conhecimento que os mesmos possuem acerca dos direitos repousam mais no senso comum que no aprendizado escolar. As conclusões apontam a necessidade de estratégias pedagógicas para inserção de noções de Direito para os estudantes do Ensino Médio, principalmente transversalmente aos conteúdos concernentes às disciplinas da área das Ciências Humanas. Com base nessas conclusões, foi elaborada uma proposta com sugestões de diretrizes para implementação da Educação em Direito no contexto das disciplinas de História, Geografia, Sociologia e Filosofia, à partir de um entrelaçamento entre os conteúdos presentes no Currículo Básico da Escola Estadual do Espírito Santo e dispositivos legislativos que pudessem dialogar com as temáticas, em busca de estabelecer uma proposta mínima que pudesse, sem prejuízo do desenvolvimento dos conteúdos, servir como instrumento para promoção da Educação em Direito, contribuindo, assim, na formação para a Cidadania.

Interpretação e utilidade da prova calórica

A prova calórica é o teste da avaliação otoneurológica que verifica a integridade do reflexo vestíbulo-ocular e possibilita avaliar cada labirinto separadamente. Os principais aspectos relacionados à realização, interpretação e utilidade da prova calórica foram revistos. MÉTODOS: Realizou-se revisão sistemática sobre as publicações ocorridas nos últimos cem anos sobre o assunto. Incluíram-se artigos originais transversais e longitudinais, de revisão e meta-análise. Excluíram-se revisões de papeleta, relatos de caso e editoriais. Os descritores utilizados foram: prova calórica, nistagmo, sistema vestibular, preponderância direcional, predomínio labiríntico, teste calórico monotermal, teste calórico com água gelada, fenômeno de Bell. Pesquisou-se as bases de dados COCHRAINE, MEDLINE, LILACS, CAPES. RESULTADOS: De 818 resumos de artigos, selecionou-se inicialmente 93 que preenchiam os critérios de inclusão. A leitura dos artigos resultou na seleção final de 55. Na análise dos artigos, enfatizou-se na discussão fundamentos da prova calórica, tipos de estimulação utilizados, prova calórica monotermal e com água gelada, questões relacionadas à interpretação dos resultados, variáveis e artefatos. COMENTÁRIOS FINAIS: os valores de referência utilizados na prova calórica podem variar de serviço para serviço, com ponto de corte definido a partir de estudos locais. Semiotécnica cuidadosa é fundamental para elevar a sensibilidade do exame.

Anotação, numa perspectiva de Direito Penal e de Criminologia, de alguns dos aspectos do Acórdão do Supremo Tribunal de Justiça (português), de 28 de Setembro de 2011 - os problemas do direito ao silêncio e do dever em o arguido se sujeitar a aplicações de prova no processo penal

Resumo: 1 – Sumário do Acórdão do Supremo Tribunal de Justiça, de 28 de Setembro de 2011; 2 – Texto completo do Acórdão do Supremo Tribunal de Justiça, de 28 de Setembro de 2011, Juiz Conselheiro Raul BORGES (Relator), Juiz Conselheiro Armindo MONTEIRO cfr. http://www.dgsi.pt , 20 de Janeiro de 2012; 3 – Anotação; 3.1 – Introdução à anotação; 3.2 – Algumas das referências, por parte do Acórdão do Supremo Tribunal de Justiça, de 28 de Setembro de 2011, aos problemas do direito ao silêncio e do dever em o arguido se sujeitar a aplicações de prova no processo penal; 3.3 – «Teoria geral» dos problemas do direito ao silêncio em contraste com o dever de sujeição do arguido a diligências de prova no contexto do direito processual penal lusitano; 4 - Conclusão. § Abstract: 1 - Summary of the Judgement of the Supreme Court of Justice of 28 September 2011 2 - Full text of the Judgement of the Supreme Court of Justice of 28 September 2011, Councillor Judge Raul Borges (Reporter), Councillor Judge Armindo Monteiro cf. . http://www.dgsi.pt, January 20, 2012, 3 - Note: 3.1 - Introduction to the annotation; 3.2 - Some of the references, by the Judgement of the Supreme Court of Justice of 28 September 2011, the problems the right to silence and the duty in the defendant be subject to applications of proof in criminal proceedings; 3.3 - "general Theory" of the problems the right to silence in contrast to the duty of subjection of the accused to proof steps in the right context criminal procedure Lusitanian 4 - Conclusion. P.S.: este é o "abstract" tal qual como surge no artigo.

Prova de hemaglutinação passiva para a evidenciação da toxina do C. diphtherias na lesão diftérica

Foi demonstrada a presença da toxina do C. diphtheriae, através de prova de hemaglutinação passiva, usando-se hemácias sensibilizadas com antitoxina diftérica, na lesão da garganta de 47,7% dos casos suspeitos de difteria examinados no presente trabalho. De 53,0% dos mesmos pacientes pôde ser isolado bacilo diftérico toxígeno. A prova de hemaglutinação passiva foi a única positiva em 13,0% dos casos e a cultura, a única positiva em 18,9%. Em 42 crianças normais ou portadoras de faringite ou amigdalite sem nenhuma característica clínica de difteria, a prova de hemaglutinação passiva foi negativa. O processo descrito, de execução muito simples, pode acusar o resultado em menos de 2 horas e oferece grande possibilidade de aplicação vantajosa no diagnóstico da difteria.

Impregnação tuberculosa em menores de quatorze anos, detectada pela prova tuberculínica, em duas áreas do município de São Paulo

Os autores estudaram as reações ao teste tuberculínico com PPD Rt-23, nos menores de 14 anos de dois bairros do município de São Paulo. No Dispensário da Faculdade de Saúde Pública foram examinadas 18.129 pessoas, no período de 1960 a 1969 e, no Dispensário da Associação dos Sanatórios Populares "Campos do Jordão" 38.436 pessoas, no período de 1966 a 1969, usando-se a mesma técnica e orientação. A porcentagem de reações positivas manteve-se inferior a 10,6%, nas pessoas examinadas.

Distribuição das medidas de induração e eritema na prova tuberculínica: aplicação de um método gráfico de decomposição de uma distribuição de freqüências em componentes normais

O teste tuberculínico, segundo a técnica de Mantoux, pretende classificar as pessoas de acordo com o tamanho da reação provocada por uma única e especificada dose de tuberculina. Dados empíricos mostram que as medidas de tais reações, obtidas em populações genéricas, representam a mistura de distintos grupos componentes. Com a finalidade de separar tais grupos, objetivando a solução posterior do problema de classificação, foi utilizado um método gráfico de decomposição de uma distribuição de freqüências em componentes normais para decompor distribuições de freqüências de medidas de induração e eritema. A decomposição obtida permite verificar que o número de componentes que descreve a distribuição da variável induração não é o mesmo que para a variável eritema, para os dados considerados.

Classificação de pessoas na prova tuberculínica: aplicação de um modelo estatístico quando a distribuição de freqüências da induração é uma mistura de componentes normais

O problema de classificar pessoas de acordo com o tamanho da induração, na prova tuberculínica segundo a técnica de Mantoux, é resolvido, para um conjunto de dados obtidos em uma população genérica, utilizando-se o critério estatístico de "melhores regiões possíveis de classificação". São obtidas estimativas das probabilidades de classificação errada.

Prova tuberculínica, BCG oral e infecção tuberculosa em crianças menores de 5 anos

São relatados os resultados das provas tuberculínicas com PPD Rt23, 2 UT, em crianças menores de um ano e de um a 4 anos, matriculadas na Clínica Pediátrica do Hospital das Clínicas da Faculdade de Medicina da USP, São Paulo, Brasil, no período de 1971 a 1975. Em 665 crianças menores de um ano encontrou-se 3,15% de reatores fracos e 6,62% de reatores fortes e em 1.298 crianças de um a 4 anos, 0,69% de reatores fracos e 5,5% de reatores fortes. Nas mesmas crianças, foram estudadas as relações entre vacinação BCG oral prévia e positividade à prova tuberculínica nos 2 grupos etários considerados e nos quais se obteve a informação de vacinação anterior com BCG oral. Em 575 crianças menores de um ano e 1.113 de um a 4 anos encontrou-se associação positiva entre vacinação BCG oral prévia e positividade à prova tuberculínica. Analisando a relação entre o número de doses de BCG oral prévio e o resultado das provas tuberculínicas pelo método de Goodman, verificou-se que a proporção de crianças que tinham tomado 3 doses e mais de BCG oral e que apresentaram reação forte à prova tuberculínica é significantemente maior que a observada para os não reatores, fato esse não verificado para o grupo de um a 4 anos. Nas crianças que tomaram uma ou duas doses não foram encontradas diferenças estatisticamente significantes.