Formal verification of use case maps with real time extensions

摘要: 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 User Requirements Notation (URN) has gained on popularity within software requirements community. UCM models focus description behavioral well high-level designs at early stages system development processes. However, timing issues often overlooked during initial design treated non-related described therefore in separate models. We believe that aspects must be integrated into model stages. In this paper, we present a novel approach describe constraints specifications. formal operational semantics Timed terms Automata (TA) can analyzed verified with UPPAAL checker tool. Our is illustrated using case study IP Multicast Routing Protocol.