Especificação do micronúcleo FreeRTOS utilizando o método B

This paper presents a contribution to the international Verified Software Repository effort through the formal specification of the microkernel FreeRTOS real-time system. Such specification was made in abstract level making use of the B method . For thus, properties of the microkernel were chosen and selected as specification requisites, which was constructed centered at the functionalities responsible for the utilization of these properties. This properties weres setting as specification requirements. The specification was constructed modeling the function of microkernel that implement this properties. This work intended to encourage the formal verification of FreeRTOS and also contribute to the formal creation of a microkernel real-time systems, based in FreeRTOS. Furthermore, this model brings a formal documentation point view of the microkernel, demonstrating features and how this internal states is changing. Finally, this work could be an example of specification of the actual system by the B method.

Projeto e implementação de uma plataforma MP-SoC usando SystemC

This work presents the concept, design and implementation of a MP-SoC platform, named STORM (MP-SoC DirecTory-Based PlatfORM). Currently the platform is composed of the following modules: SPARC V8 processor, GPOP processor, Cache module, Memory module, Directory module and two different modles of Network-on-Chip, NoCX4 and Obese Tree. All modules were implemented using SystemC, simulated and validated, individually or in group. The modules description is presented in details. For programming the platform in C it was implemented a SPARC assembler, fully compatible with gcc s generated assembly code. For the parallel programming it was implemented a library for mutex managing, using the due assembler s support. A total of 10 simulations of increasing complexity are presented for the validation of the presented concepts. The simulations include real parallel applications, such as matrix multiplication, Mergesort, KMP, Motion Estimation and DCT 2D

KitSmart: Uma biblioteca de componentes para o desenvolvimento rigoroso de aplicações Java Card com o método B

The development of smart card applications requires a high level of reliability. Formal methods provide means for this reliability to be achieved. The BSmart method and tool contribute to the development of smart card applications with the support of the B method, generating Java Card code from B specifications. For the development with BSmart to be effectively rigorous without overloading the user it is important to have a library of reusable components built in B. The goal of KitSmart is to provide this support. A first research about the composition of this library was a graduation work from Universidade Federal do Rio Grande do Norte, made by Thiago Dutra in 2006. This first version of the kit resulted in a specification of Java Card primitive types byte, short and boolean in B and the creation of reusable components for application development. This work provides an improvement of KitSmart with the addition of API Java Card specification made in B and a guide for the creation of new components. The API Java Card in B, besides being available to be used for development of applications, is also useful as a documentation of each API class. The reusable components correspond to modules to manipulate specific structures, such as date and time. These structures are not available for B or Java Card. These components for Java Card are generated from specifications formally verified in B. The guide contains quick reference on how to specify some structures and how some situations were adapted from object-orientation to the B Method. This work was evaluated through a case study made through the BSmart tool, that makes use of the KitSmart library. In this case study, it is possible to see the contribution of the components in a B specification. This kit should be useful for B method users and Java Card application developers

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

Projeto e implementação em FPGA de um processador com conjunto de instrução reconfigurável utilizando VHDL

The Reconfigurable Computing is an intermediate solution at the resolution of complex problems, making possible to combine the speed of the hardware with the flexibility of the software. An reconfigurable architecture possess some goals, among these the increase of performance. The use of reconfigurable architectures to increase the performance of systems is a well known technology, specially because of the possibility of implementing certain slow algorithms in the current processors directly in hardware. Amongst the various segments that use reconfigurable architectures the reconfigurable processors deserve a special mention. These processors combine the functions of a microprocessor with a reconfigurable logic and can be adapted after the development process. Reconfigurable Instruction Set Processors (RISP) are a subgroup of the reconfigurable processors, that have as goal the reconfiguration of the instruction set of the processor, involving issues such formats, operands and operations of the instructions. This work possess as main objective the development of a RISP processor, combining the techniques of configuration of the set of executed instructions of the processor during the development, and reconfiguration of itself in execution time. The project and implementation in VHDL of this RISP processor has as intention to prove the applicability and the efficiency of two concepts: to use more than one set of fixed instructions, with only one set active in a given time, and the possibility to create and combine new instructions, in a way that the processor pass to recognize and use them in real time as if these existed in the fixed set of instruction. The creation and combination of instructions is made through a reconfiguration unit, incorporated to the processor. This unit allows the user to send custom instructions to the processor, so that later he can use them as if they were fixed instructions of the processor. In this work can also be found simulations of applications involving fixed and custom instructions and results of the comparisons between these applications in relation to the consumption of power and the time of execution, which confirm the attainment of the goals for which the processor was developed

Utilizando programação orientada a aspectos no projeto de sistemas hardware desenvolvidos com SystemC

New programming language paradigms have commonly been tested and eventually incorporated into hardware description languages. Recently, aspect-oriented programming (AOP) has shown successful in improving the modularity of object-oriented and structured languages such Java, C++ and C. Thus, one can expect that, using AOP, one can improve the understanding of the hardware systems under design, as well as make its components more reusable and easier to maintain. We apply AOP in applications developed using the SystemC library. Several examples will be presented illustrating how to combine AOP and SystemC. During the presentation of these examples, the benefits of this new approach will also be discussed

Tvoice :um sistema de manipulação de linguagens para auxiliar portadores de necessidades especiais através da web

This work presents the tVoice, software that manipulates tags languages, extracting information and, being integral part of the VoiceProxy system, it aids bearers of special needs in the access to the Web. This system is responsible for the search and treatment of the documents in the Web, extracting the textual information contained in those documents and preceding the capability of generating eventually through translation techniques, an audio script, used by the of interface subsystem of VoiceProxy, the iVoice, in the process of voice synthesis. In this stage the tVoice, besides the treatment of the tag language HTML, processes other two formats of documents, PDF and XHTML. Additionally to allow that, besides the iVoice, other interface subsystems can make use of the tVoice through remote access, we propose distribution systems techniques based in the model Client-Server providers operations of the fashion of a proxy server treatment of documents

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

Da compreensão novas viagens de Gulliver

Ayant comme opérateur cognitif le livre Les Voyages de Gulliver, de Jonathan Swift, la thése, écrite au format d'un journal de bord, suit dévoilant des indices pour une archéologie de la compréhension, au-delà de problématiser les interconexions entre communication et compréhension à l'actuel procés de planétarism. En suite, réalise quelques essais qui problématisent l'éthique, la science, et la condition humaine, sous l'inspiration du Parlément des Choses, suggéreé par Bruno Latour, où sont présents, symétriquement, les sciences, les scientists, les politiques, les natures, les cultures, et les sociétés. Pour une telle aventure, sont agencées des ideas de penseurs de diverses domaines de la connaissance, comme Edgar Morin, Henri Atlan, Hans-Georg Gadamer, Isabelle Stengers, David Bohm, Maria da Conceição de Almeida, Cremilda Medina, María Zambrano, Michel Serres, Boris Cyrulnik, dentre autres. Lettres de musique, registres littéraires et cinématographiques servent de points d'appuy pour la contextualization du récit de ce voyage qui ne comporte pas seulement la compréhension de la compléxité de l'être-humain, mais aussi, la compréhension des conditions dans lequelles sont forgées les mentalités et pratiques les actions. Ainsi, toule compréhension est un voyage sans fin: arrive à quelques ports, se ré-approvisionne et part à nouveau. Toute compréhension est ponctuelle, parcielle, provisoire, lacunaire et inachevée.

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

Novel insights into the genomic basis of citrus canker based on the genome sequences of two strains of Xanthomonas fuscans subsp aurantifolii

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

Is The amphibian tree of life really fatally flawed?

Wiens (2007, Q. Rev. Biol. 82, 55-56) recently published a severe critique of Frost et al.'s (2006, Bull. Am. Mus. Nat. Hist. 297, 1-370) monographic study of amphibian systematics, concluding that it is a disaster and recommending that readers simply ignore this study. Beyond the hyperbole, Wiens raised four general objections that he regarded as fatal flaws: (1) the sampling design was insufficient for the generic changes made and taxonomic changes were made without including all type species; (2) the nuclear gene most commonly used in amphibian phylogenetics, RAG-1, was not included, nor were the morphological characters that had justified the older taxonomy; (3) the analytical method employed is questionable because equally weighted parsimony assumes that all characters are evolving at equal rates; and (4) the results were at times clearly erroneous, as evidenced by the inferred non-monophyly of marsupial frogs. In this paper we respond to these criticisms. In brief: (1) the study of Frost et al. did not exist in a vacuum and we discussed our evidence and evidence previously obtained by others that documented the non-monophyletic taxa that we corrected. Beyond that, we agree that all type species should ideally be included, but inclusion of all potentially relevant type species is not feasible in a study of the magnitude of Frost et al. and we contend that this should not prevent progress in the formulation of phylogenetic hypotheses or their application outside of systematics. (2) Rhodopsin, a gene included by Frost et al. is the nuclear gene that is most commonly used in amphibian systematics, not RAG-1. Regardless, ignoring a study because of the absence of a single locus strikes us as unsound practice. With respect to previously hypothesized morphological synapomorphies, Frost et al. provided a lengthy review of the published evidence for all groups, and this was used to inform taxonomic decisions. We noted that confirming and reconciling all morphological transformation series published among previous studies needed to be done, and we included evidence from the only published data set at that time to explicitly code morphological characters (including a number of traditionally applied synapomorphies from adult morphology) across the bulk of the diversity of amphibians (Haas, 2003, Cladistics 19, 23-90). Moreover, the phylogenetic results of the Frost et al. study were largely consistent with previous morphological and molecular studies and where they differed, this was discussed with reference to the weight of evidence. (3) The claim that equally weighted parsimony assumes that all characters are evolving at equal rates has been shown to be false in both analytical and simulation studies. (4) The claimed strong support for marsupial frog monophyly is questionable. Several studies have also found marsupial frogs to be non-monophyletic. Wiens et al. (2005, Syst. Biol. 54, 719-748) recovered marsupial frogs as monophyletic, but that result was strongly supported only by Bayesian clade confidence values (which are known to overestimate support) and bootstrap support in his parsimony analysis was < 50%. Further, in a more recent parsimony analysis of an expanded data set that included RAG-1 and the three traditional morphological synapomorphies of marsupial frogs, Wiens et al. (2006, Am. Nat. 168, 579-596) also found them to be non-monophyletic.Although we attempted to apply the rule of monophyly to the naming of taxonomic groups, our phylogenetic results are largely consistent with conventional views even if not wth the taxonomy current at the time of our writing. Most of our taxonomic changes addressed examples of non-monophyly that had previously been known or suspected (e.g., the non-monophyly of traditional Hyperoliidae, Microhylidae, Hemiphractinae, Leptodactylidae, Phrynobatrachus, Ranidae, Rana, Bufo; and the placement of Brachycephalus within Eleutherodactylus, and Lineatriton within Pseudoeurycea), and it is troubling that Wiens and others, as evidenced by recent publications, continue to perpetuate recognition of non-monophyletic taxonomic groups that so profoundly misrepresent what is known about amphibian phylogeny. (C) The Willi Hennig Society 2007.

Reduced allergic lung inflammation in rats following formaldehyde exposure: Long-term effects on multiple effector systems

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

Classification and characterization of places for mapping of environment using hierarchical neural network and omnivision

Mobile robots need autonomy to fulfill their tasks. Such autonomy is related whith their capacity to explorer and to recognize their navigation environments. In this context, the present work considers techniques for the classification and extraction of features from images, using artificial neural networks. This images are used in the mapping and localization system of LACE (Automation and Evolutive Computing Laboratory) mobile robot. In this direction, the robot uses a sensorial system composed by ultrasound sensors and a catadioptric vision system equipped with a camera and a conical mirror. The mapping system is composed of three modules; two of them will be presented in this paper: the classifier and the characterizer modules. Results of these modules simulations are presented in this paper.

Miscibility in a degenerate fermionic mixture induced by linear coupling

We consider a one-dimensional mean-field-hydrodynamic model of a two-component degenerate Fermi gas in an external trap, each component representing a spin state of the same atom. We demonstrate that the interconversion between them (linear coupling), imposed by a resonant electromagnetic wave, transforms the immiscible binary gas into a miscible state, if the coupling constant, kappa, exceeds a critical value, kappa(cr). The effect is predicted in a variational approximation, and confirmed by numerical solutions. Unlike the recently studied model of a binary Bose-Einsten condensate with the linear coupling, the components in the immiscible phase of the binary fermion mixture never fill two separated domains with a wall between them, but rather form antilocked (pi-phase-shifted) density waves. Another difference from the bosonic mixture is spontaneous breaking of symmetry between the two components in terms of the numbers of atoms in them, N(1) and N(2). The latter effect is characterized by the parameter nu equivalent to(N(1)-N(2))/(N(1)+N(2)) (only N(1)+N(2) is a conserved quantity), the onset of miscibility at kappa >=kappa(cr) meaning a transition to nu equivalent to 0. At kappa