Techniques for specifying temporal properties of an application are presented, based on the assumption that static and behavioral properties have been described within some object-oriented model. These techniques enable the specification of the dynamic evolution of object behavior and the interactions of collections of cooperating objects. The underlying formalism used for our specifications is the language of first-order temporal logic. A method for checking consistency of specifications is also presented.