TY - GEN
T1 - Formal verification of use case maps with real time extensions
AU - Hassine, Jameleddine
AU - Rilling, Juergen
AU - Dssouli, Rachida
PY - 2007
Y1 - 2007
N2 - 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 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.
AB - 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 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.
UR - http://www.scopus.com/inward/record.url?scp=38149077429&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-74984-4_14
DO - 10.1007/978-3-540-74984-4_14
M3 - Conference contribution
AN - SCOPUS:38149077429
SN - 3540749837
SN - 9783540749837
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 225
EP - 241
BT - SDL 2007
PB - Springer Verlag
ER -