Formal semantics and verification of use case maps