An ASM operational semantics for use case maps

Scenario-driven requirement specifications are widely used to capture and represent functional requirements. Use case maps (UCM) is being standardized as part of the user requirements notation (URN), an addition to ITU-T´s family of languages. UCM models allow the description of functional requirements and high-level designs at early stages of the development process. Recognizing the importance of having a well defined semantic, we propose, in this paper, a concise and rigorous formal semantics for use case maps, defined in terms of multi-agent abstract state machines. The proposed formal semantics addresses UCM´s operational semantics and provides a sound basis for executing UCM specifications using simulation tools and supporting formal verification.