QoS Specification Based on SDL/MSC and Temporal Logic
Stefan Leue · KOPS (University of Konstanz) · 1994
Many telecommunications systems engineers find it convenient to specify functional properties of their systems using state-transition based formal description techniques like SDL or Message Sequence Charts (MSCs). However, the expressiveness of these techniques does not capture Quality of Service (QoS)or Network Performance (Np) requirements because many of these rely on real-time bunds and probability constraints which these FDTs do not allow to express. However, suitably extended teporal logics allow specifications given in SDL or MSC with temporal logic based specifications of QoS or Np requirements. We show how SDL and MSC specifications fit together with Temporal logic specifications. Then we give examples of delay bound, delay jitter, isochronicity, stochastic reliability and stochastic dely bound constraint specifications. We discuss how our method helps in the specification of Np/QoS mapping problems, of QoS negotiation mechanisms, and of QoS monitoring. Finally we hint at methods for the formal verification of QoS and Np specifications.