A multitude of data models has been proposed for specifying static aspects (data) and operational aspects (operations on data) of the real world. However, it is often desirable to describe additional aspects of the real world. For example dynamic models have been developed for the description of temporal aspects. The motivation for this thesis was to design a dynamic model reflecting the philosophy of the object-oriented approach. In particular the temporal aspects emphasized by the proposed model are the description of the temporal evolution of object behaviour and of the temporal properties and rules concerning the cooperation of a collection of objects. We have chosen the language of propositional temporal logic as the underlying formalism of our model. The satisfiability algorithm of temporal logic has been the basis for providing a rigorous and automatic procedure for the verification of user provided specifications.