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

Neuronal Assembly Detection and Cell Membership Specification by Principal Component Analysis

LOPES-DOS-SANTOS, V. , CONDE-OCAZIONEZ, S. ; NICOLELIS, M. A. L. , RIBEIRO, S. T. , TORT, A. B. L. . Neuronal assembly detection and cell membership specification by principal component analysis. Plos One, v. 6, p. e20996, 2011.

An investigation of Hebbian phase sequences as assembly graphs

Hebb proposed that synapses between neurons that fire synchronously are strengthened, forming cell assemblies and phase sequences. The former, on a shorter scale, are ensembles of synchronized cells that function transiently as a closed processing system; the latter, on a larger scale, correspond to the sequential activation of cell assemblies able to represent percepts and behaviors. Nowadays, the recording of large neuronal populations allows for the detection of multiple cell assemblies. Within Hebb's theory, the next logical step is the analysis of phase sequences. Here we detected phase sequences as consecutive assembly activation patterns, and then analyzed their graph attributes in relation to behavior. We investigated action potentials recorded from the adult rat hippocampus and neocortex before, during and after novel object exploration (experimental periods). Within assembly graphs, each assembly corresponded to a node, and each edge corresponded to the temporal sequence of consecutive node activations. The sum of all assembly activations was proportional to firing rates, but the activity of individual assemblies was not. Assembly repertoire was stable across experimental periods, suggesting that novel experience does not create new assemblies in the adult rat. Assembly graph attributes, on the other hand, varied significantly across behavioral states and experimental periods, and were separable enough to correctly classify experimental periods (Naïve Bayes classifier; maximum AUROCs ranging from 0.55 to 0.99) and behavioral states (waking, slow wave sleep, and rapid eye movement sleep; maximum AUROCs ranging from 0.64 to 0.98). Our findings agree with Hebb's view that assemblies correspond to primitive building blocks of representation, nearly unchanged in the adult, while phase sequences are labile across behavioral states and change after novel experience. The results are compatible with a role for phase sequences in behavior and cognition.

Natureza morta...edifício com vida: uma arquitetura sustentável para o Serviço de Verificação de Óbitos

Sustainability in buildings, while reducing the impact on the environment, contributes to the promotion of social welfare, to increase the health and productivity of occupants. The search for a way of build that meets the aspirations and development of humanity without, however, represent degradation of the environment, has become the great challenge of contemporary architecture. It is considered that the incorporation of principles that provide a sustainable building with careful choices of design solutions contribute to a better economic and thermal performance of the building, as well as functional and psychological comfort to its users. Based on this general understanding, this paper presents an architecture project aimed to health care whose the solutions adopted follow carefully the relevant legislation and sets his sights on the theme of sustainability. The methodology began with studies on the themes of verification service of deaths, sustainability and those application in construction developed through research in academic studies and analysis of architectural projects, using them like reference for the solutions adopted. Within the project analysis was performed a visit to the verification service of deaths in the city of Palmas in Tocantins, subsidizing information that, plus the relevant legislation, led to functional programming and pre-dimensional of the building to be designed. The result of this programming environments were individual records with information from environmental restrictions, space required for the development of activities, desirable flow and sustainability strategies, that can be considered as the first product of relevance of the professional master's degree. Finally we have outlined the basic design architecture of a Verification Service of Death SVO/RN (in portuguese), whose process of projecting defined as a guiding line of work four points: the use of bioclimatic architecture as the main feature projectual, the use of resources would provide minimal harm to the environment, the use of modulation and structure to the building as a form of rationalization and finally the search for solutions that ensure environmental and psychological comfort to users. Importantly to highlight that, besides owning a rare theme in literature that refers to architectural projects, the whole project was drawn up with foundations in projective criteria that contribute to environmental sustainability, with emphasis on thermal performance, energy efficiency and reuse of rainwater

O poder legislativo na verificação da legitimidade constitucional do processo de construção das leis

It is known that, in the Democratic State of Law paradigm, one of the most instigating themes is the legitimity of the Law. It justifies the interest in reflecting about the Legislative Process instituted by the Brasilian 1988 Constitution, more specifically field of the constitutionality control as away to guaranty of the legitimity of the Law. The research that is developed here, intents to bring to reflection the basis and the ways the Legislative Power has to proceed to Constitutionality Control of the laws and of the Legislative Process. As the focus taken here is about the Legislative Power, it starts from the presupposed that only by the adoption of legislative process which has to be connected to a rational speech, that will evidence the Democratic and Procedimental Law dimensions, guarantee the possibility of the public and private spheres of life act in complementarity that is such needed to the stabilization of the social expectatives and the concretization of the Brazilian Constitution

Algoritmos inteligentes para auto-correção, auto-verificação e auto-validação de medidas em sensores

This work presents a set of intelligent algorithms with the purpose of correcting calibration errors in sensors and reducting the periodicity of their calibrations. Such algorithms were designed using Artificial Neural Networks due to its great capacity of learning, adaptation and function approximation. Two approaches willbe shown, the firstone uses Multilayer Perceptron Networks to approximate the many shapes of the calibration curve of a sensor which discalibrates in different time points. This approach requires the knowledge of the sensor s functioning time, but this information is not always available. To overcome this need, another approach using Recurrent Neural Networks was proposed. The Recurrent Neural Networks have a great capacity of learning the dynamics of a system to which it was trained, so they can learn the dynamics of a sensor s discalibration. Knowingthe sensor s functioning time or its discalibration dynamics, it is possible to determine how much a sensor is discalibrated and correct its measured value, providing then, a more exact measurement. The algorithms proposed in this work can be implemented in a Foundation Fieldbus industrial network environment, which has a good capacity of device programming through its function blocks, making it possible to have them applied to the measurement process

Metodologia de Verificação Funcional para Circuitos Analógicos

This work proposes a new methodology to verify those analog circuits, providing an automated tools to help the verifiers to have a more truthful result. This work presents the development of new methodology for analog circuits verification. The main goal is to provide a more automated verification process to certify analog circuits functional behavior. The proposed methodology is based on the golden model technique. A verification environment based on this methodology was built and results of a study case based on the validation of an operational amplifier design are offered as a confirmation of its effectiveness. The results had shown that the verification process was more truthful because of the automation provided by the tool developed

Desenvolvimento de uma cadeira de rodas robótica para transporte de portador de necessidades especiais

The objective of the dissertation was the realization of kinematic modeling of a robotic wheelchair using virtual chains, allowing the wheelchair modeling as a set of robotic manipulator arms forming a cooperative parallel kinematic chain. This document presents the development of a robotic wheelchair to transport people with special needs who overcomes obstacles like a street curb and barriers to accessibility in streets and avenues, including the study of assistive technology, parallel architecture, kinematics modeling, construction and assembly of the prototype robot with the completion of a checklist of problems and barriers to accessibility in several pathways, based on rules, ordinances and existing laws. As a result, simulations were performed on the chair in various states of operation to accomplish the task of going up and down stair with different measures, making the proportional control based on kinematics. To verify the simulated results we developed a prototype robotic wheelchair. This project was developed to provide a better quality of life for people with disabilities

The influence of visual inter-hemispheric connections on spiking, assembly and LFP activities, and their phase relationship during figure-ground stimulation

Desde os descobrimentos pioneiros de Hubel e Wiesel acumulou-se uma vasta literatura descrevendo as respostas neuronais do córtex visual primário (V1) a diferentes estímulos visuais. Estes estímulos consistem principalmente em barras em movimento, pontos ou grades, que são úteis para explorar as respostas dentro do campo receptivo clássico (CRF do inglês classical receptive field) a características básicas dos estímulos visuais como a orientação, direção de movimento, contraste, entre outras. Entretanto, nas últimas duas décadas, tornou-se cada vez mais evidente que a atividade de neurônios em V1 pode ser modulada por estímulos fora do CRF. Desta forma, áreas visuais primárias poderiam estar envolvidas em funções visuais mais complexas como, por exemplo, a separação de um objeto ou figura do seu fundo (segregação figura-fundo) e assume-se que as conexões intrínsecas de longo alcance em V1, assim como as conexões de áreas visuais superiores, estão ativamente envolvidas neste processo. Sua possível função foi inferida a partir da análise das variações das respostas induzidas por um estímulo localizado fora do CRF de neurônios individuais. Mesmo sendo muito provável que estas conexões tenham também um impacto tanto na atividade conjunta de neurônios envolvidos no processamento da figura quanto no potencial de campo, estas questões permanecem pouco estudadas. Visando examinar a modulação do contexto visual nessas atividades, coletamos potenciais de ação e potenciais de campo em paralelo de até 48 eletrodos implantados na área visual primária de gatos anestesiados. Estimulamos com grades compostas e cenas naturais, focando-nos na atividade de neurônios cujo CRF estava situado na figura. Da mesma forma, visando examinar a influência das conexões laterais, o sinal proveniente da área visual isotópica e contralateral foi removido através da desativação reversível por resfriamento. Fizemos isso devido a: i) as conexões laterais intrínsecas não podem ser facilmente manipuladas sem afetar diretamente os sinais que estão sendo medidos, ii) as conexões inter-hemisféricas compartilham as principais características anatômicas com a rede lateral intrínseca e podem ser vistas como uma continuação funcional das mesmas entre os dois hemisférios e iii) o resfriamento desativa as conexões de forma causal e reversível, silenciando temporariamente seu sinal, permitindo conclusões diretas a respeito da sua contribuição. Nossos resultados demonstram que o mecanismo de segmentação figurafundo se reflete nas taxas de disparo de neurônios individuais, assim como na potência do potencial de campo e na relação entre sua fase e os padrões de disparo produzidos pela população. Além disso, as conexões laterais inter-hemisféricas modulam estas variáveis dependendo da estimulação feita fora do CRF. Observamos também uma influência deste circuito lateral na coerência entre potenciais de campo entre eletrodos distantes. Em conclusão, nossos resultados dão suporte à ideia de um mecanismo complexo de segmentação figura-fundo atuando desde as áreas visuais primárias em diferentes escalas de frequência. Esse mecanismo parece envolver grupos de neurônios ativos sincronicamente e dependentes da fase do potencial de campo. Nossos resultados também são compatíveis com a hipótese que conexões laterais de longo alcance também fazem parte deste mecanismo

Uma abordagem para a verificação do comportamento excepcional a partir de regras de designe e testes

Checking the conformity between implementation and design rules in a system is an important activity to try to ensure that no degradation occurs between architectural patterns defined for the system and what is actually implemented in the source code. Especially in the case of systems which require a high level of reliability is important to define specific design rules for exceptional behavior. Such rules describe how exceptions should flow through the system by defining what elements are responsible for catching exceptions thrown by other system elements. However, current approaches to automatically check design rules do not provide suitable mechanisms to define and verify design rules related to the exception handling policy of applications. This paper proposes a practical approach to preserve the exceptional behavior of an application or family of applications, based on the definition and runtime automatic checking of design rules for exception handling of systems developed in Java or AspectJ. To support this approach was developed, in the context of this work, a tool called VITTAE (Verification and Information Tool to Analyze Exceptions) that extends the JUnit framework and allows automating test activities to exceptional design rules. We conducted a case study with the primary objective of evaluating the effectiveness of the proposed approach on a software product line. Besides this, an experiment was conducted that aimed to realize a comparative analysis between the proposed approach and an approach based on a tool called JUnitE, which also proposes to test the exception handling code using JUnit tests. The results showed how the exception handling design rules evolve along different versions of a system and that VITTAE can aid in the detection of defects in exception handling code

Contribuições para verificação automática de applets javacard

The widespread growth in the use of smart cards (by banks, transport services, and cell phones, etc) has brought an important fact that must be addressed: the need of tools that can be used to verify such cards, so to guarantee the correctness of their software. As the vast majority of cards that are being developed nowadays use the JavaCard technology as they software layer, the use of the Java Modeling Language (JML) to specify their programs appear as a natural solution. JML is a formal language tailored to Java. It has been inspired by methodologies from Larch and Eiffel, and has been widely adopted as the de facto language when dealing with specification of any Java related program. Various tools that make use of JML have already been developed, covering a wide range of functionalities, such as run time and static checking. But the tools existent so far for static checking are not fully automated, and, those that are, do not offer an adequate level of soundness and completeness. Our objective is to contribute to a series of techniques, that can be used to accomplish a fully automated and confident verification of JavaCard applets. In this work we present the first steps to this. With the use of a software platform comprised by Krakatoa, Why and haRVey, we developed a set of techniques to reduce the size of the theory necessary to verify the specifications. Such techniques have yielded very good results, with gains of almost 100% in all tested cases, and has proved as a valuable technique to be used, not only in this, but in most real world problems related to automatic verification

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