Visual notations like class diagrams, and use case diagrams are very popular with practitioners for capturing requirements of software applications. These notations unfortunately have little or no semantics, and hence cannot be analysed by tools. Formal notations, on the other hand, have associated tools that check speci.cations for stated properties but are difficult to integrate with software development processes in use. Strengths of both approaches can be exploited by giving formal semantics to popular notations. Here we propose a novel usage of UML object diagrams for specifying pre- and post-conditions for use cases and capturing global system properties as class invariants. A translation is defined from object diagrams to the formal notation TLA+. The TLA+ specification is then formally verified using the model checker TLC. The proposed notation is intuitive, expressive and formal. We present a small case study to illustrate its strengths.