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 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.

MDA-based re-engineering with Object-Z

This paper describes a practical application of MDA and reverse engineering based on a domain-specific modelling language. A well defined metamodel of a domain-specific language is useful for verification and validation of associated tools. We apply this approach to SIFA, a security analysis tool. SIFA has evolved as requirements have changed, and it has no metamodel. Hence, testing SIFA’s correctness is difficult. We introduce a formal metamodelling approach to develop a well-defined metamodel of the domain. Initially, we develop a domain model in EMF by reverse engineering the SIFA implementation. Then we transform EMF to Object-Z using model transformation. Finally, we complete the Object-Z model by specifying system behavior. The outcome is a well-defined metamodel that precisely describes the domain and the security properties that it analyses. It also provides a reliable basis for testing the current SIFA implementation and forward engineering its successor.

Proving Temporal Properties of Z Specifications Using Abstraction

This paper presents a systematic approach to proving temporal properties of arbitrary Z specifications. The approach involves (i) transforming the Z specification to an abstract temporal structure (or state transition system), (ii) applying a model checker to the temporal structure, (iii) determining whether the temporal structure is too abstract based on the model checking result and (iv) refining the temporal structure where necessary. The approach is based on existing work from the model checking literature, adapting it to Z.

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.