A aplicações dos trataos internacionais de direitos humanos pela jurisdição brasileira

O Brasil, apesar de ter uma participação ativa nos fóruns internacionais de debates sobre a proteção dos direitos humanos, ainda não atua de forma eficiente no adimplemento das obrigações livremente pactuadas, fato este que o levou a ser acionado e condenado pela Corte Interamericana de Direitos Humanos, em virtude da prática de atos violatórios aos ditos direitos, praticados no âmbito dos três Poderes, bem como por todos os Entes Federativos. Diante dessa realidade que se apresenta, o nosso objeto de estudo será investigar a efetivação dos direitos humanos previstos em tratados internacionais pela Jurisdição brasileira. Na esteira desse raciocínio, nossa problemática consiste em demonstrar que os tratados internacionais de direitos humanos, apesar de serem claramente fontes do direito estatal, não vêm sendo devidamente aplicados pelos órgãos que exercem a função jurisdicional em nosso país. Fixada à problemática, nosso objetivo no presente estudo consiste em: 1) descrever a competência constitucional do Poder Judiciário para proteção dos direitos humanos e aplicação dos tratados internacionais; 2) definir o controle jurisdicional de convencionalidade como instrumento de proteção dos direitos humanos a ser utilizados pelos magistrados; e, 3) analisar quase um século de decisões do Supremo Tribunal Federal no que toca a aplicação dos tratados internacionais de direitos humanos. Espera-se efetivamente demonstrar que compete a todos os órgãos estatais o dever de aplicar diretamente os instrumentos internacionais de proteção aos direitos humanos devidamente internalizados. Essa obrigação inegavelmente também recai sobre os que exercem a função jurisdicional. Desta maneira, todos os juízes incumbidos do exercício da jurisdição convertem-se no âmbito estatal em verdadeiros concretizadores dos direitos humanos, sejam eles advindos do sistema global ou do regional de proteção. Dessa forma, devem servir-se do controle de convencionalidade para afastar as manifestações estatais que estejam em dissintonia com o teor dos tratados internacionais de direitos humanos, bem como da interpreção a eles conferida pelas Cortes e Tribunais internacionais

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

Histórias de adoção tardia: considerações a partir da analítica existencial heideggeriana

Adoption establishes a filiation status, resulting from a legal act, which attributes to the child and parents the rights and obligations associated with such condition, being legally irrevocable. Nevertheless, in practice there are adoptions that do not concretize and the child returns to justice during or even after the legal process is closed. Late adoption is the denomination of the adoption of children over two years and it is still permeated by myths and stigmas, leading to a frequent return of the child to justice in these cases. The late adoption involves a process of building a unique relationship with a child whose backstory is commonly marked by the dissolution of the relationship with the family of origin, due to violation of rights and, in some cases, the experience of institutional care. Given such a scenario, this research, based on the Existential Analytic proposed by Martin Heidegger, seeks to understand the experience of mothers and children in the process of late adoption, in order to obtain subsidies to psychological attention in this context. This is a qualitative, phenomenological study with a comprehensive focus. The participants were two mothers and two children who have gone through late adoption for about two years. The procedures of data generation contemplated narrative interviews with mothers and individual meetings with children, in which ludic resources were used as mediators of expression (free drawings, unfinished children's story and "Story-Drawings" on late adoption). The procedures were audiotaped and transcribed. Data analysis was grounded in Heidegger's hermeneutics. The late adoption process, permeated by historical, social and cultural determinants and the web of meanings that create the historical singularity of each person involved have proved to be complex as seen in the narratives. The construction of the meanings of parenthood and filiation has been developing in the families in the study, from the experience of being-with-the-other, caring and dwelling in their peculiar modes of expression. The family of origin and the adoptive family mingle and differentiate by means of the experience of children, especially because of the existence of biological siblings. Data point to the importance of psychological care to family core in late adoption processes

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.