Formal verification of use case maps with real time extensions

Jameleddine Hassine*, Juergen Rilling, Rachida Dssouli

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

10 Scopus citations


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.

Original languageEnglish
Title of host publicationSDL 2007
Subtitle of host publicationDesign for Dependable Systems - 13th International SDL Forum, Proceedings
PublisherSpringer Verlag
Number of pages17
ISBN (Print)3540749837, 9783540749837
StatePublished - 2007
Externally publishedYes

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4745 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Formal verification of use case maps with real time extensions'. Together they form a unique fingerprint.

Cite this