Time and asynchrony in interactions among distributed real-time objects

Abstract

This paper presents a framework for specifying and verifying distributed real-time object-oriented systems. An earlier paper [18] introduced a process calculus for describing distributed objects using local clocks. It was based on synchronous communication and thus could not sufficiently model asynchronous communication in distributed systems. In this paper we propose a new process calculus with the ability to express asynchronous message passing, communication delay, and delayed processing. It can describe temporal and behavioral properties of distributed real-time objects. Based on the new calculus, we develop a verification method by means of algebraic order relations. The relations are speed-sensitive and can decide whether two distributed real-time objects are behaviorally equivalent and whether one of them can perform its behaviors faster than the other. They offer a suitable method for proving the correctness and reusability of real-time objects in asynchronous communication settings. Some examples are shown to demonstrate the calculus and the relations.