Duration Calculus in COOZ: A Formal Specification Language for Real-Time
Systems
Xiaodong Yuan(*) and Ying Feng(**)
*Nanjing Automation Research Institute, P.R. China
**Indiana University, USA
Abstract
This paper introduces the idea of continuous time into COOZ, an object-oriented
extension of Z notation, through establishing absolute clock and object clock.
Then we use Duration Calculus to specify the real-time and history constraints
of objects. By these means, COOZ is adapted to formal specifications of
real-time and concurrent systems. A case study of automatic fire alarm system
and the comparison with related work are also given. We make in-depth
discussions in the paper on problems about type conversion, integrability and
isolated points of real-time state,
etc.
Click here for Full Paper (gzipped postscript).