Resoning About TCOZ
No Thumbnail Available
Date
2002-03-01T00:00:00Z
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
Timed Communicating Object Z (TCOZ) semantically and
syntactically blends Object-Z with TCSP. TCOZ can capture
the data/state and real-time interactions of system components.
TCOZ preserves in large part both the syntax and semantics
of the individual notations and hence can potentially benefit
from existing reasoning systems of the individual notations.
This paper extends and links the Object-Z and TCSP
proof systems for reasoning about TCOZ models.