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.

Formalising behaviour trees with CSP

Behaviour Trees is a novel approach for requirements engineering. It advocates a graphical tree notation that is easy to use and to understand. Individual requirements axe modelled as single trees which later on are integrated into a model of the system as a whole. We develop a formal semantics for a subset of Behaviour Trees using CSP. This work, on one hand, provides tool support for Behaviour Trees. On the other hand, it builds a front-end to a subset of the CSP notation and gives CSP users a new modelling strategy which is well suited to the challenges of requirements engineering.

Abstract specification in Object-Z and CSP

A number of integrations of the state-based specification language Object-Z and the process algebra CSP have been proposed in recent years. In developing such integrations, a number of semantic decisions have to be made. In particular, what happens when an operation's precondition is not satisfied? Is the operation blocked, i.e., prevented from occurring, or can it occur with an undefined result? Also, are outputs from operations angelic, satisfying the environment's constraints on them, or are they demonic and not influenced by the environment at all? In this paper we discuss the differences between the models, and show that by adopting a blocking model of preconditions together with an angelic model of outputs one can specify systems at higher levels of abstraction.

A wavelet visible difference predictor

In this paper, we describe a model of the human visual system (HVS) based on the wavelet transform. This model is largely based on a previously proposed model, but has a number of modifications that make it more amenable to potential integration into a wavelet based image compression scheme. These modifications include the use of a separable wavelet transform instead of the cortex transform, the application of a wavelet contrast sensitivity function (CSP), and a simplified definition of subband contrast that allows us to predict noise visibility directly from wavelet coefficients. Initially, we outline the luminance, frequency, and masking sensitivities of the HVS and discuss how these can be incorporated into the wavelet transform. We then outline a number of limitations of the wavelet transform as a model of the HVS, namely the lack of translational invariance and poor orientation sensitivity. In order to investigate the efficacy of this wavelet based model, a wavelet visible difference predictor (WVDP) is described. The WVDP is then used to predict visible differences between an original and compressed (or noisy) image. Results are presented to emphasize the limitations of commonly used measures of image quality and to demonstrate the performance of the WVDP, The paper concludes with suggestions on bow the WVDP can be used to determine a visually optimal quantization strategy for wavelet coefficients and produce a quantitative measure of image quality.

Conformational dynamics of thyroid hormones by variable temperature nuclear magnetic resonance: The role of side chain rotations and cisoid/transoid interconversions

H-1 NMR spectra of the thyroid hormone thyroxine recorded at low temperature and high field show splitting into two peaks of the resonance due to the H2,6 protons of the inner (tyrosyl) ring. A single resonance is observed in 600 MHz spectra at temperatures above 185 K. An analysis of the line shape as a function of temperature shows that the coalescence phenomenon is due to an exchange process with a barrier of 37 kJ mol(-1). This is identical to the barrier for coalescence of the H2',6' protons of the outer (phenolic) ring reported previously for the thyroid hormones and their analogues. It is proposed that the separate peaks at low temperature are due to resonances for H2,6 in cisoid and transoid conformers which are populated in approximately equal populations. These two peaks are averaged resonances for the individual H2 and H6 protons. Conversion of cisoid to transoid forms can occur via rotation of either the alanyl side chain or the outer ring, from one face of the inner ring to the other. It is proposed that the latter process is the one responsible for the observed coalescence phenomenon. The barrier to rotation of the alanyl side chain is greater than or equal to 37 kJ mol(-1), which is significantly larger than has previously been reported for Csp(2)-Csp(3) bonds in other Ph-CH2-X systems. The recent crystal structure of a hormone agonist bound to the ligand-binding domain of the rat thyroid hormone receptor (Wagner et al. Nature 1995, 378, 690-697) shows the transoid form to be the bound conformation. The significant energy barrier to cisoid/transoid interconversion determined in the current study combined with the tight fit of the hormone to its receptor suggests that interconversion between the forms cannot occur at the receptor site but that selection for the preferred bound form occurs from the 50% population of the transoid form in solution.

Characterization of a chemsensory protein (ASP3c) from honeybee (Apis mellifera L.) as a brood pheromone carrier

Chemosensory proteins (CSPs) are ubiquitous soluble small proteins isolated from sensory organs of a wide range of insect species, which are believed to be involved in chemical communication. We report the cloning of a honeybee CSP gene called ASP3c, as well as the structural and functional characterization of the encoded protein. The protein was heterologously secreted by the yeast Pichia pastoris using the native signal peptide. ASP3c disulfide bonds were assigned after trypsinolysis followed by chromatography and mass spectrometry combined with microsequencing. The pairing (Cys(I)-Cys(II), Cys(III)-Cys(IV)) was found to be identical to that of Schistocerca gregaria CSPs, suggesting that this pattern occurs commonly throughout the insect CSPs. CD measurements revealed that ASP3c mainly consists of alpha-helices, like other insect CSPs. Gel filtration analysis showed that ASP3c is monomeric at neutral pH. Using ASA, a fluorescent fatty acid anthroyloxy analogue as a probe, ASP3c was shown to bind specifically to large fatty acids and ester derivatives, which are brood pheromone components, in the micromolar range. It was unable to bind tested general odorants and other tested pheromones (sexual and nonsexual). This is the first report on a natural pheromonal ligand bound by a recombinant CSP with a measured affinity constant.

Latent inhibition and schizophrenia: Pavlovian conditioning of autonomic responses

Latent inhibition (LI) is an important model for understanding cognitive deficits in schizophrenia, Disruption of LI is thought to result from an inability to ignore irrelevant stimuli. The study investigated LI in schizophrenic patients by using Pavlovian conditioning of electrodermal responses in a complete within-subject design. Thirty-two schizophrenic patients, ( 16 acute. unmedicated and 16 medicated patients) and 16 healthy control subjects (matched with respect to age and gender) participated in the study. The experiment consisted of two stages: preexposure and conditioning. During preexposure two visual stimuli were presented, one of which served as the to-be-conditioned stimulus (CSp +) and the other one was the not-to-be-conditioned stimulus (CSp -) during the following conditioning ( = acquisition). During acquisition. two novel visual stimuli (CSn + and CSn -) were introduced. A reaction time task was used as the unconditioned stimulus (US). LI was defined as the difference in response differentiation observed between proexposed and non-preexposed sets of CS + and CS -. During preexposure. the schizophrenic patients did not differ in electrodermal responding from the control subjects, neither concerning the extent of orienting nor the course of habituation. The exposure to novel stimuli at the beginning of the acquisition elicited reduced orienting responses in unmedicated patients compared to medicated patients and control subjects, LI was observed in medicated schizophrenic patients and healthy controls. but not in acute unmedicated patients. Furthermore LI was found to be correlated with the duration of illness: it was attenuated in patients who had suffered their first psychotic episode. (C) 2002 Elsevier Science B.V. All rights reserved.