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 distrib-uted information systems. We do not assume global time for concurrent object sys-tems. 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 calling 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