BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B

Java Card technology allows the development and execution of small applications embedded in smart cards. A Java Card application is composed of an external card client and of an application in the card that implements the services available to the client by means of an Application Programming Interface (API). Usually, these applications manipulate and store important information, such as cash and confidential data of their owners. Thus, it is necessary to adopt rigor on developing a smart card application to improve its quality and trustworthiness. The use of formal methods on the development of these applications is a way to reach these quality requirements. The B method is one of the many formal methods for system specification. The development in B starts with the functional specification of the system, continues with the application of some optional refinements to the specification and, from the last level of refinement, it is possible to generate code for some programming language. The B formalism has a good tool support and its application to Java Card is adequate since the specification and development of APIs is one of the major applications of B. The BSmart method proposed here aims to promote the rigorous development of Java Card applications up to the generation of its code, based on the refinement of its formal specification described in the B notation. This development is supported by the BSmart tool, that is composed of some programs that automate each stage of the method; and by a library of B modules and Java Card classes that model primitive types, essential Java Card API classes and reusable data structures

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

Verificação formal automatizada para sistemas de raciocínio procedural (PRS) utilizando redes de petri coloridas (RPC)

Este trabalho apresenta uma técnica de verificação formal de Sistemas de Raciocínio Procedural, PRS (Procedural Reasoning System), uma linguagem de programação que utiliza a abordagem do raciocínio procedural. Esta técnica baseia-se na utilização de regras de conversão entre programas PRS e Redes de Petri Coloridas (RPC). Para isso, são apresentadas regras de conversão de um sub-conjunto bem expressivo da maioria da sintaxe utilizada na linguagem PRS para RPC. A fim de proceder fia verificação formal do programa PRS especificado, uma vez que se disponha da rede de Petri equivalente ao programa PRS, utilizamos o formalismo das RPCs (verificação das propriedades estruturais e comportamentais) para analisarmos formalmente o programa PRS equivalente. Utilizamos uma ferramenta computacional disponível para desenhar, simular e analisar as redes de Petri coloridas geradas. Uma vez que disponhamos das regras de conversão PRS-RPC, podemos ser levados a querer fazer esta conversão de maneira estritamente manual. No entanto, a probabilidade de introdução de erros na conversão é grande, fazendo com que o esforço necessário para garantirmos a corretude da conversão manual seja da mesma ordem de grandeza que a eliminação de eventuais erros diretamente no programa PRS original. Assim, a conversão automatizada é de suma importância para evitar que a conversão manual nos leve a erros indesejáveis, podendo invalidar todo o processo de conversão. A principal contribuição deste trabalho de pesquisa diz respeito ao desenvolvimento de uma técnica de verificação formal automatizada que consiste basicamente em duas etapas distintas, embora inter-relacionadas. A primeira fase diz respeito fias regras de conversão de PRS para RPC. A segunda fase é concernente ao desenvolvimento de um conversor para fazer a transformação de maneira automatizada dos programas PRS para as RPCs. A conversão automática é possível, porque todas as regras de conversão apresentadas seguem leis de formação genéricas, passíveis de serem incluídas em algoritmos

Aplicação do método B ao projeto formal de software embarcado

This work shows a project method proposed to design and build software components from the software functional m del up to assembly code level in a rigorous fashion. This method is based on the B method, which was developed with support and interest of British Petroleum (BP). One goal of this methodology is to contribute to solve an important problem, known as The Verifying Compiler. Besides, this work describes a formal model of Z80 microcontroller and a real system of petroleum area. To achieve this goal, the formal model of Z80 was developed and documented, as it is one key component for the verification upto the assembly level. In order to improve the mentioned methodology, it was applied on a petroleum production test system, which is presented in this work. Part of this technique is performed manually. However, almost of these activities can be automated by a specific compiler. To build such compiler, the formal modelling of microcontroller and modelling of production test system should provide relevant knowledge and experiences to the design of a new compiler. In ummary, this work should improve the viability of one of the most stringent criteria for formal verification: speeding up the verification process, reducing design time and increasing the quality and reliability of the product of the final software. All these qualities are very important for systems that involve serious risks or in need of a high confidence, which is very common in the petroleum industry

Buraco negros, correspondência AdS/BCFT e fluido/gravidade

Einstein’s equations with negative cosmological constant possess the so-called anti de Sitter space, AdSd+1, as one of its solutions. We will later refer to this space as to the "bulk". The holographic principle states that quantum gravity in the AdSd+1 space can be encoded by a d−dimensional quantum field theory on the boundary of AdSd+1 space, invariant under conformal transformations, a CFTd. In the most famous example, the precise statement is the duality of the type IIB string theory in the space AdS5 × S 5 and the 4−dimensional N = 4 supersymmetric Yang-Mills theory. Another example is provided by a relation between Einstein’s equations in the bulk and hydrodynamic equations describing the effective theory on the boundary, the so-called fluid/gravity correspondence. An extension of the "AdS/CFT duality"for the CFT’s with boundary was proposed by Takayanagi, which was dubbed the AdS/BCFT correspondence. The boundary of a CFT extends to the bulk and restricts a region of the AdSd+1. Neumann conditions imposed on the extension of the boundary yield a dynamic equation that determines the shape of the extension. From the perspective of fluid/gravity correspondence, the shape of the Neumann boundary, and the geometry of the bulk is sourced by the energy-momentum tensor Tµν of a fluid residing on this boundary. Clarifying the relation of the Takayanagi’s proposal to the fluid/gravity correspondence, we will study the consistence of the AdS/BCFT with finite temperature CFT’s, or equivalently black hole geometries in the bulk.

Análise do comportamento de técnicas de correspondência binocular para imagens em alta definição

This work presents an analysis of the behavior of some algorithms usually available in stereo correspondence literature, with full HD images (1920x1080 pixels) to establish, within the precision dilemma versus runtime applications which these methods can be better used. The images are obtained by a system composed of a stereo camera coupled to a computer via a capture board. The OpenCV library is used for computer vision operations and processing images involved. The algorithms discussed are an overall method of search for matching blocks with the Sum of the Absolute Value of the difference (Sum of Absolute Differences - SAD), a global technique based on cutting energy graph cuts, and a so-called matching technique semi -global. The criteria for analysis are processing time, the consumption of heap memory and the mean absolute error of disparity maps generated.

Outorga onerosa do direito de construir e dinâmica do mercado imobiliário formal: planejamento e descaminhos na expansão urbana de Parnamirim RN (2008-2010)

The `Outorga Onerosa do Direito de Construir - OODC` (Public Concession of Building Rights), instrument instituted by The City Statute in 2001, has as main objective the recovery of urban property, seeking for a fair distribution the urbanization benefits. The possibility of usage of the OODC instrument is linked to the maximum utilization coefficient, determined to specific areas in accordance to existing infrastructure conditions, further taking into account the formal real estate market, expansion axis and crowding. Being an instrument which establishes values to be paid for a better use of land, it maintains a narrow relation to the real estate, incentivizing or discouraging the crowding in specific areas. The present study investigates the relationship between the criteria for the making of the Public Concession of Building Rights instrument and the dynamics of the formal real estate market. It takes as empiric universe Parnamirim (RN), part of the Natal Metropolitan Area (RN), focusing on the application of the OODC in the period of 2008-2010. It seeks to better understand the necessary basis for the formulation of the instrument, about how it works and its relation to the formal real estate market. It aims to depict the formal real estate market by presenting the production of urban space in Parnamirim in terms of intensity and nature of the real estate, furthermore identifying the licensed properties through the application of the municipality instrument. For the conclusion, it is discussed the criteria for the formation of OODC, its relationship to the dynamics of the formal real estate market and its influencing possibilities in the processes of usage and occupation of land in the context of urban planning