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.

Novel genes regulated by Sonic Hedgehog in pluripotent mesenchymal cells

Sonic Hedgehog is a secreted morphogen involved in patterning a wide range of structures in the developing embryo. Disruption of the Hedgehog signalling cascade leads to a number of developmental disorders and plays a key role in the formation of a range of human cancers. The identification of genes regulated by Hedgehog is crucial to understanding how disruption of this pathway leads to neoplastic transformation. We have used a Sonic Hedgehog (Shh) responsive mouse cell line, C3H/10T1/2, to provide a model system for hedgehog target gene discovery. Following activation of cell cultures with Shh, RNA was used to interrogate microarrays to investigate downstream transcriptional consequences of hedgehog stimulation. As a result 11 target genes have been identified, seven of which are induced (Thrombomodulin, GILZ, BF-2, Nr4a1, IGF2, PMP22, LASP1) and four of which are repressed (SFRP-1, SFRP-2, Mip1-gamma, Amh) by Shh. These targets have a diverse range of putative functions and include transcriptional regulators and molecules known to be involved in regulating cell growth or apoptosis. The corroboration of genes previously implicated in hedgehog signalling, along with the finding of novel targets, demonstrates both the validity and power of the C3H/10T1/2 system for Shh target gene discovery.

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.