Timed CSP and Object-Z

Derrick, John (2003) Timed CSP and Object-Z. In: 3rd International Conference on B and Z Users, JUN 04-06, 2003, TURKU, FINLAND. (The full text of this publication is not available from this repository)

The full text of this publication is not available from this repository. (Contact us about this Publication)
Official URL
http://dx.doi.org/10.1007/3-540-44880-2_19

Abstract

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.

Item Type: Conference or workshop item (Paper)
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 18:01
Last Modified: 12 May 2014 11:13
Resource URI: http://kar.kent.ac.uk/id/eprint/13963 (The current URI for this page, for reference purposes)
  • Depositors only (login required):