A Formalism for Real-Time Concurrent Object-Oriented Computing

Abstract

We investigate a formal model for reasoning about real-time object-oriented computations. The model is an extension of CCS with the notion of time, called RtCCS(Real-time Calculus of Communication Systems). It can naturally model real-time concurrent objects as communicating processes and represent the timed properties of objects. We define two timed equivalences based on CCS's bisimulation and derive algebraic laws for reasoning about real-time processes. The equivalences provide a formal framework for analyzing the behavior and timing of real-time computations. Also, we define a sound and complete equational proof system for finite processes. Some examples in RtCCS are shown in order to demonstrate its usefulness. © 1992, ACM. All rights reserved.