892 resultados para B formal method
Resumo:
A novel technique is presented to facilitate the implementation of hierarchical b-splines and their interfacing with conventional finite element implementations. The discrete interpretation of the two-scale relation, as common in subdivision schemes, is used to establish algebraic relations between the basis functions and their coefficients on different levels of the hierarchical b-spline basis. The subdivision projection technique introduced allows us first to compute all element matrices and vectors using a fixed number of same-level basis functions. Their subsequent multiplication with subdivision matrices projects them, during the assembly stage, to the correct levels of the hierarchical b-spline basis. The proposed technique is applied to convergence studies of linear and geometrically nonlinear problems in one, two and three space dimensions. © 2012 Elsevier B.V.
Resumo:
The main chlorophyll a/b light-harvesting complex (LHC 11) has been isolated directly from thylakoid membranes of marine green alga (Bryopsis corticulans Setch.) by two consecutive runs of anion exchange and gel-filtration chromatography. LHC 11 proteins in the membrane extracts treated with 3% n-Octyl-b-D-glucopyranoside (OG) obtained specific binding ability on Q Sepharose column, and thus were isolated from the thylakoid membranes in a highly selective fraction. The monomeric, trimeric and oligomeric subcomplexes of LHC 11 have been obtained by fractionation of the LHC 11 mixes with sucrose density gradient ultracentrifugation. The SDS-PAGE analysis of peptide composition and absorption spectrum showed that LHC 11 monomers, trimers and oligomers prepared through this work were intact and in high purity. Our report is the first to show that it is possible to purify LHC If directly from thylakoid membranes without extensively biochemical purification.
Resumo:
Current and past research has brought up new views related to the optimization of neural networks. For a fixed structure, second order methods are seen as the most promising. From previous works we have shown how second order methods are of easy applicability to a neural network. Namely, we have proved how the Levenberg-Marquard possesses not only better convergence but how it can assure the convergence to a local minima. However, as any gradient-based method, the results obtained depend on the startup point. In this work, a reformulated Evolutionary algorithm - the Bacterial Programming for Levenberg-Marquardt is proposed, as an heuristic which can be used to determine the most suitable starting points, therefore achieving, in most cases, the global optimum.
Resumo:
We apply to the Senegalese input-output matrix of 1990, disagregated into formal and informal activities, a recently designed structural analytical method (Minimal-Flow-Analysis) which permits to depict the direct and indirect production likanges existing between activities.
Resumo:
The work reported in this paper is motivated by biomimetic inspiration - the transformation of patterns. The major issue addressed is the development of feasible methods for transformation based on a macroscopic tool. The general requirement for the feasibility of the transformation method is determined by classifying pattern formation approaches an their characteristics. A formal definition for pattern transformation is provided and four special cases namely, elementary and geometric transformation based on repositioning all and some robotic agents are introduced. A feasible method for transforming patterns geometrically, based on the macroscopic parameter operation of a swarm is considered. The transformation method is applied to a swarm model which lends itself to the transformation technique. Simulation studies are developed to validate the feasibility of the approach, and do indeed confirm the approach.
Resumo:
The background error covariance matrix, B, is often used in variational data assimilation for numerical weather prediction as a static and hence poor approximation to the fully dynamic forecast error covariance matrix, Pf. In this paper the concept of an Ensemble Reduced Rank Kalman Filter (EnRRKF) is outlined. In the EnRRKF the forecast error statistics in a subspace defined by an ensemble of states forecast by the dynamic model are found. These statistics are merged in a formal way with the static statistics, which apply in the remainder of the space. The combined statistics may then be used in a variational data assimilation setting. It is hoped that the nonlinear error growth of small-scale weather systems will be accurately captured by the EnRRKF, to produce accurate analyses and ultimately improved forecasts of extreme events.
Resumo:
We use the continuum discretized coupled channel method to study the effects of breakup on different reaction mechanisms for the (8)B + (58)Ni system. We devote special attention to the role of continuum-continuum couplings.
Resumo:
Nuclear (p,alpha) reactions destroying the so-called ""light-elements"" lithium, beryllium and boron have been largely studied in the past mainly because their role in understanding some astrophysical phenomena, i.e. mixing-phenomena occurring in young F-G stars [1]. Such mechanisms transport the surface material down to the region close to the nuclear destruction zone, where typical temperatures of the order of similar to 10(6) K are reached. The corresponding Gamow energy E(0)=1.22 (Z(x)(2)Z(X)(2)T(6)(2))(1/3) [2] is about similar to 10 keV if one considers the ""boron-case"" and replaces in the previous formula Z(x) = 1, Z(X) = 5 and T(6) = 5. Direct measurements of the two (11)B(p,alpha(0))(8)Be and (10)B(p,alpha)(7)Be reactions in correspondence of this energy region are difficult to perform mainly because the combined effects of Coulomb barrier penetrability and electron screening [3]. The indirect method of the Trojan Horse (THM) [4-6] allows one to extract the two-body reaction cross section of interest for astrophysics without the extrapolation-procedures. Due to the THM formalism, the extracted indirect data have to be normalized to the available direct ones at higher energies thus implying that the method is a complementary tool in solving some still open questions for both nuclear and astrophysical issues [7-12].
Resumo:
To date there are no analytical techniques designed to exclusively measure bioavailable iron in marine environments. The goal of this research is to develop such a technique by isolating the bioavailable iron using the terrestrial siderophore desferrioxamine B (DFB). This project contained many challenging aspects, but the specific goal of this study was to develop a robust analytical technique for quantification of Fe(III)-DFB complexes at nanomolar concentrations. Past work showed that oxalate (Ox) promotes photodissociation of Fe(III)-DFB to Fe(Il), and we are specifically interested in the mechanism of this process. A model was developed using known thermodynamic constants for Fe(III)-DFB and Fe(III) oxalato complexes and adjusting for ionic strength. The model was confirmed by monitoring the UV-VIS absorbance of the system at a variety of oxalate concentrations and pH. The model did not include ternary complexes. Next., the rate of Fe(1I) production during UV irradiation was examined. The results showed that the rate of Fe(II) production was based entirely on the [Fe(Ox)?]3- speciation, and that reoxidation of Fe(II) occurred via reactive oxygen intermediates. This reoxidation could be avoided by either decreasing the oxygen concentration or by adding a Fe(II) stabilizing reagent, such as ferrozine. Further studies need to be done to confirm that these results apply at sub nanomolar concentrations, and the issue of Fe(II) reoxidation at lower Fe concentrations needs to be addressed.
Resumo:
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.
Resumo:
Formal methods and software testing are tools to obtain and control software quality. When used together, they provide mechanisms for software specification, verification and error detection. Even though formal methods allow software to be mathematically verified, they are not enough to assure that a system is free of faults, thus, software testing techniques are necessary to complement the process of verification and validation of a system. Model Based Testing techniques allow tests to be generated from other software artifacts such as specifications and abstract models. Using formal specifications as basis for test creation, we can generate better quality tests, because these specifications are usually precise and free of ambiguity. Fernanda Souza (2009) proposed a method to define test cases from B Method specifications. This method used information from the machine s invariant and the operation s precondition to define positive and negative test cases for an operation, using equivalent class partitioning and boundary value analysis based techniques. However, the method proposed in 2009 was not automated and had conceptual deficiencies like, for instance, it did not fit in a well defined coverage criteria classification. We started our work with a case study that applied the method in an example of B specification from the industry. Based in this case study we ve obtained subsidies to improve it. In our work we evolved the proposed method, rewriting it and adding characteristics to make it compatible with a test classification used by the community. We also improved the method to support specifications structured in different components, to use information from the operation s behavior on the test case generation process and to use new coverage criterias. Besides, we have implemented a tool to automate the method and we have submitted it to more complex case studies
Resumo:
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