Model checking visual specification of requirements

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 analyzed by tools. Formal notations, on the other hand, have associated tools that check specifications 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/sup +/. The TLA/sup +/ 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.