kirancodes.me
To Proof Maintenance & Beyond!

Blending Object-Z and Timed CSP: An Introduction to TCOZ

Brendan P. Mahony, Jin Song Dong

Abstract

Object-Z is an extension to the Z language designed to facilitate specification in an object-oriented style. It is an excellent tool for modeling data and algorithms, but its object semantics are single threaded and operations are atomic. Therefore, it is difficult to use Object-Z to capture the behaviour of concurrent real-time reactive systems. On the other hand, Timed CSP is good at modeling real-time concurrent behaviour, but has little support for modeling the state of a complex system. This paper introduces a blending of Object-Z and Timed CSP, known as TCOZ. The blended notation is particularly suited for specifying complex systems whose components have their own thread of control.

BibTeX
@inproceedings{Mahony-Dong:ICSE98,
  author    = {Brendan P. Mahony and
               Jin Song Dong},
  title     = {Blending {Object-Z} and Timed {CSP:} An Introduction to {TCOZ}},
  booktitle = {ICSE},
  pages     = {95--104},
  publisher = {{IEEE} Computer Society},
  year      = {1998},
}

Related papers