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.