Specifying Distributed Information Systems: Fundamentals of an Object-Oriented Approach Using Distributed Temporal Logic

摘要

We present fundamentals of an approach to object-oriented specification of distributed information systems. We do not assume global time for concurrent object systems. For specifying those systems we propose Dtl, a distributed temporal logic. The main contribution is that Dtl is capable of specifying complex constraints about the behavior of distributed systems and communication between concurrent objects. For instance, we distinguish different kinds of synchronous communication such as immediate caling vs. deferred calling. The ideas are illustrated by examples given in Troll, a formal object-oriented specification language. We introduce notations for formally specifying object-based distributed systems. finally, we briefly explain how Dtl is semantically explained in terms of a true concurrent model, i.e., labelled event structures, and which concepts for in-the large specification are covered by our approach.