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.

Stressor categorization: acute physical and psychological stressors elicit distinctive recruitment patterns in the amygdala and in medullary noradrenergic cell groups

It has been hypothesized that the brain categorizes stressors and utilizes neural response pathways that vary in accordance with the assigned category. If this is true, stressors should elicit patterns of neuronal activation within the brain that are category-specific. Data from previous Immediate-early gene expression mapping studies have hinted that this is the case, but interstudy differences in methodology render conclusions tenuous. In the present study, immunolabelling for the expression of c-fos was used as a marker of neuronal activity elicited in the rat brain by haemorrhage, immune challenge, noise, restraint and forced swim. All stressors elicited c-fos expression in 25-30% of hypothalamic paraventricular nucleus corticotrophin-releasing-factor cells, suggesting that these stimuli were of comparable strength, at least with regard to their ability to activate the hypothalamic-pituitary-ad renal axis. In the amygdala, haemorrhage and immune challenge both elicited c-fos expression in a large number of neurons in the central nucleus of the amygdala, whereas noise, restraint and forced swim primarily elicited recruitment of cells within the medial nucleus of the amygdala. In the medulla, all stressors recruited similar numbers of noradrenergic (A1 and A2) and adrenergic (C1 and C2) cells. However, haemorrhage and immune challenge elicited c-fos expression In subpopulations of A1 and A2 noradrenergic cells that were significantly more rostral than those recruited by noise, restraint or forced swim. The present data support the suggestion that the brain recognizes at least two major categories of stressor, which we have referred to as 'physical' and 'psychological'. Moreover, the present data suggest that the neural activation footprint that is left in the brain by stressors can be used to determine the category to which they have been assigned by the brain.

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.

Categorization and characterization of transcript-confirmed constitutively and alternatively spliced introns and exons from human

By spliced alignment of human DNA and transcript sequence data we constructed a data set of transcript-confirmed exons and introns from 2793 genes, 796 of which (28%) were seen to have multiple isoforms. We find that over one-third of human exons can translate in more than one frame, and that this is highly correlated with G+C content. Introns containing adenosine at donor site position +3 (A3), rather than guanosine (G3), are more common in low G+C regions, while the converse is true in high G+C regions. These two classes of introns are shown to have distinct lengths, consensus sequences and correlations among splice signals, leading to the hypothesis that A3 donor sites are associated with exon definition, and G3 donor sites with intron definition. Minor classes of introns, including GC-AG, U12-type GT-AG, weak, and putative AG-dependant introns are identified and characterized. Cassette exons are more prevalent in low G+C regions, while exon isoforms are more prevalent in high G+C regions. Cassette exon events outnumber other alternative events, while exon isoform events involve truncation twice as often as extension, and occur at acceptor sites twice as often as at donor sites. Alternative splicing is usually associated with weak splice signals, and in a majority of cases, preserves the coding frame. The reported characteristics of constitutive and alternative splice signals, and the hypotheses offered regarding alternative splicing and genome organization, have important implications for experimental research into RNA processing. The 'AltExtron' data sets are available at http://www.bit.uq.edu.au/altExtron/ and http://www.ebi.ac.uk/similar tothanaraj/altExtron/.

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.