Scenario-driven requirement specifications are widely used to capture and represent functional requirement. More recently, the Use Case Maps language(UCM), being standardized by ITU-T's as part of the User Requirements Notation (URN) has gained on popularity within the software requirements community. UCM models focus on the description of functional and behavioral requirements as well as high-level designs at the early stages of system development processes. However, timing issues are often overlooked during the initial system design and treated as non-related behavioral issues and described therefore in separate models. We believe that timing aspects must be integrated into the system model during early development stages. In this paper, we present a novel approach to describe timing constraints in UCM specifications.We describe a formal operational semantics of Timed UCM in terms of Timed Automata (TA) that can be analyzed and verified with the UPPAAL model checker tool. Our approach is illustrated using a case study of the IP Multicast Routing Protocol.

Form For Virtual Library edit

Title Formal Verification of Use Case Maps with Real Time Extensions
Authors J. Hassine, J. Rilling and R. Dssouli
Type Conference
Conference/Journal Title SDL-Forum 2007
Volume/Number LNCS 4745
Publisher Springer
Month September
Year 2007
Pages 225-241
DOI 10.1007/978-3-540-74984-4_14
Keywords Timed Use Case Maps, timed automata, verification, model checking, UPPAL
Topic revision: r3 - 19 Aug 2010 - 14:30:40 - Daniel Amyot
This site is powered by FoswikiCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding Foswiki? Send feedback