Virtual LibraryFormal methods Virtual LibraryZ notation Virtual LibraryObject-Z notation

The TCOZ Home Page

Timed Communicating Object Z (TCOZ) is an integration of Object-Z and Timed CSP.

Introduction

The design of complex systems requires powerful mechanisms for modeling state, concurrent events, and real-time behaviour; as well as for structuring and decomposing systems in order to control complexity. Methods integration has become a recent research trend in software specification and design. In the graphical area, many object-oriented methods have merged into one, the Unified Modeling Language (UML). Although traditional formal methods have not scale-up well, integrated formal methods show great promise. Timed Communicating Object Z (TCOZ) is one of the recent integrations.

Summary

Timed CSP and Object-Z complement each other in their expressiveness. Object-Z has strong data and state modeling capabilities. The Z mathematical toolkit is extended with object oriented structuring techniques. Timed CSP has strong process control modeling capabilities. The multi-threading and synchronisation primitives of CSP are extended with timing primitives. The approach taken in TCOZ is to identify operation schemas (both syntactically and semantically) with (terminating) CSP processes that perform only state update events; to identify active classes with non-terminating CSP processes; and to allow arbitrary (channel-based) communications interfaces between objects. The syntactic implications of this approach is that the basic structure of a TCOZ document is the same as for Object-Z. A document consists of a sequence of definitions, including type and constant definitions in the usual Z style. TCOZ varies from Object-Z in the structure of class definitions, which may include CSP channel and processes definitions. In fact, all operation definitions in TCOZ are considered to define CSP processes. The CSP view of an operation schema is that it describes all the sequences of update events which change the system state as required by the schema predicate. The exact nature and granularity of these update events is left undetermined in TCOZ (at least at the syntactic level), but by allowing an operation to consist of a number of events, it becomes feasible to specify its temporal properties when describing the operation. Since operation schemas take on the syntactic role of CSP processes, they may be combined with other schemas and even CSP processes using the standard CSP process operators. Thus it becomes possible to represent true multi-threaded computation even at the operation level, something that would not be possible with other approaches. In addition to the inherited CSP's channel-based communication mechanism, in which messages represent discrete synchronisations between processes, TCOZ is extended with continuous-function interface mechanisms inspired by process control theory, the sensors and the actuators. Those communication interfaces (channels, sensors and actuators) are given an independent, first class role in TCOZ. This allows the communications and control topology of a network of objects to be designed orthogonally to their class structure and reduces the need to reference other classes in class definitions, thereby enhancing the modularity of system specifications.

TCOZ on web with its UML photos

The XML/XSL approach is used to the development of a web environment for TCOZ and the projection techniques and tools from TCOZ (in XML) to some UML (in XMI) diagrams are developed using XSL Transformations (XSLT). For more details, see ZML.

Supported by

Recent Report

Publications

Other integrated approaches (partial collection):

Some Books on Object-Z/Z and Timed-CSP/CSP:

Latex for Z/Object-Z/TCOZ

Download this zip file for latex examples and sty files for Z/Object-Z/TCOZ. Note that Object-Z guide file is very useful.