Extending Object-Z for specifying real-time systems

摘要

Object-Z is one of the object-oriented extensions to the formal notation Z. Though Object-Z notation includes some temporal operators to deal with history invariants, it still cannot be used as is for the specification of real-time system. The paper proposes an extension to Object-Z to specify real-time constraints. The novelty of the approach lies in the minimal set of syntactic extensions and the visible separation of real-time constraints from the specification of classes in the application. The proposed new language is called Real-Time Object-Z (RTOZ). The semantics of RTOZ provides a consistent mapping between the class definitions and the real-time constraints. The paper describes the syntactic extensions to Object-Z and illustrates the expressive power of RTOZ through the specification of a robotic assembly cell. A type checker for RTOZ is currently under development.