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.

Specification, refinement and verification of concurrent systems - An integration of Object-Z and CSP

This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of modelling complex data structures needed to define the component processes of such systems, and CSP enables the concise specification of process interactions. The basis of the integration is a semantics of Object-Z classes identical to that of CSP processes. This allows classes specified in Object-Z to he used directly within the CSP part of the specification. In addition to specification, we also discuss refinement and verification in this model. The common semantic basis enables a unified method of refinement to be used, based upon CSP refinement. To enable state-based techniques to be used fur the Object-Z components of a specification we develop state-based refinement relations which are sound and complete with respect to CSP refinement. In addition, a verification method for static and dynamic properties is presented. The method allows us to verify properties of the CSP system specification in terms of its component Object-Z classes by using the laws of the the CSP operators together with the logic for Object-Z.

Structural refinement of systems specified in object-z and CSP

This paper is concerned with methods for refinement of specifications written using a combination of Object-Z and CSP. Such a combination has proved to be a suitable vehicle for specifying complex systems which involve state and behaviour, and several proposals exist for integrating these two languages. The basis of the integration in this paper is a semantics of Object-Z classes identical to CSP processes. This allows classes specified in Object-Z to be combined using CSP operators. It has been shown that this semantic model allows state-based refinement relations to be used on the Object-Z components in an integrated Object-Z/CSP specification. However, the current refinement methodology does not allow the structure of a specification to be changed in a refinement, whereas a full methodology would, for example, allow concurrency to be introduced during the development life-cycle. In this paper, we tackle these concerns and discuss refinements of specifications written using Object-Z and CSP where we change the structure of the specification when performing the refinement. In particular, we develop a set of structural simulation rules which allow single components to be refined to more complex specifications involving CSP operators. The soundness of these rules is verified against the common semantic model and they are illustrated via a number of examples.

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.

Structuring real-time Object-Z specifications

This paper presents a means of structuring specifications in real-time Object-Z: an integration of Object-Z with the timed refinement calculus. Incremental modification of classes using inheritance and composition of classes to form multi-component systems are examined. Two approaches to the latter are considered: using Object-Z's notion of object instantiation and introducing a parallel composition operator similar to those found in process algebras. The parallel composition operator approach is both more concise and allows more general modelling of concurrency. Its incorporation into the existing semantics of real-time Object-Z is presented.

The effect of grain refinement and silicon content on grain formation in hypoeutectic Al-Si alloys

The effect of increasing the amount of added grain refiner on grain size and morphology has been investigated for a range of hypoeutectic Al-Si alloys. The results show a transition in grain size at a silicon concentration of about 3 wt% in unrefined alloys; the grain size decreasing with silicon content before the transition, and increasing beyond the transition point. A change in morphology also occurs with increased silicon content. The addition of grain refiner leads to greater refinement for silicon contents below the transition point than for those contents above the transition point, while the transition point seems to remain unchanged. The slope of the grain size versus silicon content curve after the transition seems to be unaffected by the degree of grain refinement. The results are related to the competitive processes of nucleation and constitutional effects during growth and their impact on nucleation kinetics. (C) 1999 Elsevier Science S.A. All rights reserved.

Efficient discovery of immune response targets by cyclical refinement of QSAR models of peptide binding

Peptides that induce and recall T-cell responses are called T-cell epitopes. T-cell epitopes may be useful in a subunit vaccine against malaria. Computer models that simulate peptide binding to MHC are useful for selecting candidate T-cell epitopes since they minimize the number of experiments required for their identification. We applied a combination of computational and immunological strategies to select candidate T-cell epitopes. A total of 86 experimental binding assays were performed in three rounds of identification of HLA-All binding peptides from the six preerythrocytic malaria antigens. Thirty-six peptides were experimentally confirmed as binders. We show that the cyclical refinement of the ANN models results in a significant improvement of the efficiency of identifying potential T-cell epitopes. (C) 2001 by Elsevier Science Inc.

The Las Campanas/AAT Rich Cluster Survey - II. The environmental dependence of galaxy colours in clusters at z similar to 0.1

We present a photometric investigation of the variation in galaxy colour with environment in 11 X-ray-luminous clusters at 0.07 less than or equal to z less than or equal to 0.16 taken from the Las Campanas/AAT Rich Cluster Survey. We study the properties of the galaxy populations in individual clusters, and take advantage of the homogeneity of the sample to combine the clusters together to investigate weaker trends in the composite sample. We find that modal colours of galaxies lying on the colour-magnitude relation in the clusters become bluer by d(B - R)/dr(p) = -0.022 +/- 0.004 from the cluster core out to a projected radius of r(p) = 6 Mpc, further out in radius than any previous study. We also examine the variation in modal galaxy colour with local galaxy density, 2, for galaxies lying close to the colour-magnitude relation, and find that the median colour shifts bluewards by d(B - R)/d log(10)(Sigma) = -0.076 +/- 0.009 with decreasing local density across three orders of magnitude. We show that the position of the red envelope of galaxies in the colour-magnitude relation does not vary as a function of projected radius or density within the clusters, suggesting that the change in the modal colour results from an increasing fraction of bluer galaxies within the colour-magnitude relation, rather than a change in the colours of the whole population. We show that this shift in the colour-magnitude relations with projected radius and local density is greater than that expected from the changing morphological mix based on the local morphology-density relation. We therefore conclude that we are seeing a real change in the properties of galaxies on the colour-magnitude relation in the outskirts of clusters. The simplest interpretation of this result (and similar constraints in local clusters) is that an increasing fraction of galaxies in the lower density regions at large radii within clusters exhibit signatures of star formation in the recent past, signatures which are not seen in the evolved galaxies in the highest density regions.

A framework for specification-based testing

Test templates and a test template framework are introduced as useful concepts in specification-based testing. The framework can be defined using any model-based specification notation and used to derive tests from model-based specifications-in this paper, it is demonstrated using the Z notation. The framework formally defines test data sets and their relation to the operations in a specification and to other test data sets, providing structure to the testing process. Flexibility is preserved, so that many testing strategies can be used. Important application areas of the framework are discussed, including refinement of test data, regression testing, and test oracles.

Supporting contexts in program refinement

A program can be refined either by transforming the whole program or by refining one of its components. The refinement of a component is, for the main part, independent of the remainder of the program. However, refinement of a component can depend on the context of the component for information about the variables that are in scope and what their types are. The refinement can also take advantage of additional information, such as any precondition the component can assume. The aim of this paper is to introduce a technique, which we call program window inference, to handle such contextual information during derivations in the refinement calculus. The idea is borrowed from a technique, called window inference, for handling context in theorem proving. Window inference is the primary proof paradigm of the Ergo proof editor. This tool has been extended to mechanize refinement using program window inference. (C) 1997 Elsevier Science B.V.