Timed CSP and Object-Z

In this paper we discuss a simple integration of timed CSP and Object-Z. Following existing work, the components in such an integration are written as either Object-Z classes, or timed CSP processes, and are combined together using CSP parallel composition.

Here we discuss the approach in general, and describe how the semantics of timed CSP can be used as the semantics of the integrated notation. We briefly discuss verification and analysis for integrated descriptions, before providing a more in-depth discussion of refinement in this approach. We describe both refinement of individual components, as well as a two-event model which distinguishes between start and end events. The latter allows operation duration to be specified and we show how refinement in this model integrates into traditional state-based simulation rules.