Timed communicating object Z

This paper describes a timed, multithreaded object modeling notation for sp ecifying real-time, concurrent, and reactive systems. The notation Timed Co mmunicating Object Z (TCOZ) builds on Object Z's strengths in modeling comp lex data and algorithms, and on Timed CSP's strengths in modeling process c ontrol and real-time interactions. TCOZ is novel in that it includes timing primitives, properly separates process control and data/algorithm issues a nd supports the modeling of true multithreaded concurrency. TCOZ is particu larly well-suited for specifying complex systems whose components have thei r own thread of control. The expressiveness of the notation is demonstrated by a case study in specifying a multilift system that operates in real-tim e.