Linear temporal logic and z refinement

Since Z, being a state-based language, describes a system in terms of its state and potential state changes, it is natural to want to describe properties of a specified system also in terms of its state. One means of doing this is to use Linear Temporal Logic (LTL) in which properties about the state of a system over time can be captured. This, however, raises the question of whether these properties are preserved under refinement. Refinement is observation preserving and the state of a specified system is regarded as internal and, hence, non-observable. In this paper, we investigate this issue by addressing the following questions. Given that a Z specification A is refined by a Z specification C, and that P is a temporal logic property which holds for A, what temporal logic property Q can we deduce holds for C? Furthermore, under what circumstances does the property Q preserve the intended meaning of the property P? The paper answers these questions for LTL, but the approach could also be applied to other temporal logics over states such as CTL and the mgr-calculus.

Verifying data refinements using a model checker

In this paper, we consider how refinements between state-based specifications (e.g., written in Z) can be checked by use of a model checker. Specifically, we are interested in the verification of downward and upward simulations which are the standard approach to verifying refinements in state-based notations. We show how downward and upward simulations can be checked using existing temporal logic model checkers. In particular, we show how the branching time temporal logic CTL can be used to encode the standard simulation conditions. We do this for both a blocking, or guarded, interpretation of operations (often used when specifying reactive systems) as well as the more common non-blocking interpretation of operations used in many state-based specification languages (for modelling sequential systems). The approach is general enough to use with any state-based specification language, and we illustrate how refinements between Z specifications can be checked using the SAL CTL model checker using a small example.

Compositional class refinement in object-Z

Object-Z allows coupling constraints between classes which, on the one hand, facilitate specification at a high level of abstraction, but, on the other hand, make class refinement non-compositional. The consequence of this is that refinement is not practical for large Systems. This paper overcomes this limitation by introducing a methodology for compositional class refinement in Object-Z. The key step is an equivalence transformation of an arbitrary Object-Z specification to one in which introduced constraints prohibit non-compositional refinements. The methodology also allows the constraints which couple classes to be refined yielding an unrestricted approach to compositional class refinement.

Bayesian refinement of association signals for 14 loci in 3 common diseases

To further investigate susceptibility loci identified by genome-wide association studies, we genotyped 5,500 SNPs across 14 associated regions in 8,000 samples from a control group and 3 diseases: type 2 diabetes (T2D), coronary artery disease (CAD) and Graves' disease. We defined, using Bayes theorem, credible sets of SNPs that were 95% likely, based on posterior probability, to contain the causal disease-associated SNPs. In 3 of the 14 regions, TCF7L2 (T2D), CTLA4 (Graves' disease) and CDKN2A-CDKN2B (T2D), much of the posterior probability rested on a single SNP, and, in 4 other regions (CDKN2A-CDKN2B (CAD) and CDKAL1, FTO and HHEX (T2D)), the 95% sets were small, thereby excluding most SNPs as potentially causal. Very few SNPs in our credible sets had annotated functions, illustrating the limitations in understanding the mechanisms underlying susceptibility to common diseases. Our results also show the value of more detailed mapping to target sequences for functional studies. © 2012 Nature America, Inc. All rights reserved.

Rankamaite from the Urubu pegmatite, Itinga, Minas Gerais, Brazil: Crystal chemistry and Rietveld refinement

A new occurrence of rankamaite is here described at the Urubu pegmatite, Itinga municipality, Minas Gerais, Brazil. The mineral forms cream-white botryoidal aggregates of acicular to fibrous crystals, intimately associated with simpsonite, thoreaulite, cassiterite, quartz, elbaite, albite, and muscovite. The average of six chemical analyses obtained by electron microprobe is (range in parentheses, wt%): Na(2)O 2.08 (1.95-2.13), K(2)O 2.61 (2.52-2.74), Al(2)O(3) 1.96 (1.89-2.00), Fe(2)O(3) 0.01 (0.00-0.03), TiO(2) 0.02 (0.00-0.06), Ta(2)O(5) 81.04 (79.12-85.18), Nb(2)O(5) 9.49 (8.58-9.86), total 97.21 (95.95-101.50). The chemical formula derived from this analysis is (Na(1.55)K(1.28))(Sigma 2.83)(Ta(8.45)Nb(1.64)Al(0.89)Fe(0.01)(3+)Ti(0.01))(Sigma 11.00)[O(25.02)(OH)(5.98)](Sigma 31.00). Rankamaite is an orthorhombic ""tungsten bronze"" (OTB), crystallizing in the space group Cmmm. Its unit-cell parameters refined from X-ray diffraction powder data are: a = 17.224(3), b = 17.687(3), c = 3.9361(7) angstrom, V = 1199.1(3) angstrom(3), Z = 2. Rietveld refinement of the powder data was undertaken using the structure of LaTa(5)O(14) as a starting model for the rankamaite structure. The structural formula obtained with the Rietveld analyses is: (Na(2.21)K(1.26))Sigma(3.37)(Ta(9.12)NB(1.30) Al(0.59))(Sigma 11.00)[O(26.29)(OH)(4.71)](Sigma 31.00). The tantalum atoms are coordinated by six and seven oxygen atoms in the form of distorted TaO(6) octahedra and TaO(2) pentagonal bipyramids, respectively. Every pentagonal bipyramid shares edges with four octahedra, thus forming Ta(5)O(14) units. The potassium atom is in an 11-fold coordination, whereas one sodium atom is in a 10-fold and the other is in a 12-fold coordination. Raman and infrared spectroscopy were used to investigate the room-temperature spectra of rankamaite.

On a refinement of Craig's lattices

Let p be an odd prime. A family of (p - 1)-dimensional over-lattices yielding new record packings for several values of p in the interval [149... 3001] is presented. The result is obtained by modifying Craig's construction and considering conveniently chosen Z-submodules of Q(zeta), where zeta is a primitive pth root of unity. For p >= 59, it is shown that the center density of the (p - 1)-dimensional lattice in the new family is at least twice the center density of the (p - 1)-dimensional Craig lattice. (C) 2010 Elsevier B.V. All rights reserved.

Improvement of photon transport model by including coupled photon-electron transport and kernel refinement

The first part of this work deals with the inverse problem solution in the X-ray spectroscopy field. An original strategy to solve the inverse problem by using the maximum entropy principle is illustrated. It is built the code UMESTRAT, to apply the described strategy in a semiautomatic way. The application of UMESTRAT is shown with a computational example. The second part of this work deals with the improvement of the X-ray Boltzmann model, by studying two radiative interactions neglected in the current photon models. Firstly it is studied the characteristic line emission due to Compton ionization. It is developed a strategy that allows the evaluation of this contribution for the shells K, L and M of all elements with Z from 11 to 92. It is evaluated the single shell Compton/photoelectric ratio as a function of the primary photon energy. It is derived the energy values at which the Compton interaction becomes the prevailing process to produce ionization for the considered shells. Finally it is introduced a new kernel for the XRF from Compton ionization. In a second place it is characterized the bremsstrahlung radiative contribution due the secondary electrons. The bremsstrahlung radiation is characterized in terms of space, angle and energy, for all elements whit Z=1-92 in the energy range 1–150 keV by using the Monte Carlo code PENELOPE. It is demonstrated that bremsstrahlung radiative contribution can be well approximated with an isotropic point photon source. It is created a data library comprising the energetic distributions of bremsstrahlung. It is developed a new bremsstrahlung kernel which allows the introduction of this contribution in the modified Boltzmann equation. An example of application to the simulation of a synchrotron experiment is shown.

Refinement methods for software architecture design using the software architecture model

Modern software systems are often large and complicated. To better understand, develop, and manage large software systems, researchers have studied software architectures that provide the top level overall structural design of software systems for the last decade. One major research focus on software architectures is formal architecture description languages, but most existing research focuses primarily on the descriptive capability and puts less emphasis on software architecture design methods and formal analysis techniques, which are necessary to develop correct software architecture design. ^ Refinement is a general approach of adding details to a software design. A formal refinement method can further ensure certain design properties. This dissertation proposes refinement methods, including a set of formal refinement patterns and complementary verification techniques, for software architecture design using Software Architecture Model (SAM), which was developed at Florida International University. First, a general guideline for software architecture design in SAM is proposed. Second, specification construction through property-preserving refinement patterns is discussed. The refinement patterns are categorized into connector refinement, component refinement and high-level Petri nets refinement. These three levels of refinement patterns are applicable to overall system interaction, architectural components, and underlying formal language, respectively. Third, verification after modeling as a complementary technique to specification refinement is discussed. Two formal verification tools, the Stanford Temporal Prover (STeP) and the Simple Promela Interpreter (SPIN), are adopted into SAM to develop the initial models. Fourth, formalization and refinement of security issues are studied. A method for security enforcement in SAM is proposed. The Role-Based Access Control model is formalized using predicate transition nets and Z notation. The patterns of enforcing access control and auditing are proposed. Finally, modeling and refining a life insurance system is used to demonstrate how to apply the refinement patterns for software architecture design using SAM and how to integrate the access control model. ^ The results of this dissertation demonstrate that a refinement method is an effective way to develop a high assurance system. The method developed in this dissertation extends existing work on modeling software architectures using SAM and makes SAM a more usable and valuable formal tool for software architecture design. ^