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.

Writing the body of the mother: Narrative moments in Tsushima Yuko, Ariyoshi Sawako and Enchi Fumiko

This discussion argues the transformative potential inherent in the corporeal experience of motherhood as represented in selected textual moments of Japanese narrative. Narratives that address the experiences of the body of the mother are informed and given substance by an intense physicality, and thus have the potential to contest processes of social inscription in addition to suggesting alternative possibilities for all readers, not just those occupying an embodied maternal space. The discussion features brief events from the work of three writers who have written as mothers: Tsushima Y(u)macrko, Ariyoshi Sawako and Enchi Fumiko. In Yama o hashiru onna (1980; translated as Woman Running in the Mountains, 1991), Tsushima Y(u)macrko invites the reader to consider the embodied response to light of Takiko, a young pregnant woman. Emiko, the protagonist of Hishoku (Without Colour, 1967) by Ariyoshi Sawako, is the Japanese wife of an African American and has just given birth to a child. The daughter protagonist in Enchi Fumiko's 'Kami' ('Hair', 1957) operates a hairdressing business that is viable only with her mother's unpaid labour. The narratives are read through a matrix of post-structuralist theories of embodiment, drawing on the work of writers such as Julia Kristeva, Luce Irigaray and Elizabeth Grosz.