Note:
Postcript
version (242 p.)
Abstract:
The proper capture of desired system properties is a pivotal step in providing high quality systems. The formal specification of these properties is necessary to provide unambiguous documentation as well as automated transformation of system requirements during all stages of the life cycle. The standardized Formal Description Techniques (FDTs) Estelle and SDL have proved useful for the specification of traditional protocols and distributed systems. With the availability of high-speed networks new applications with additional requirements and characteristics are becoming reality. These requirements are often referred to as {\em Quality of Service} (QoS) requirements. We show that the above mentioned FDTs do not possess the expressiveness to capture important classes of QoS requirements, namely quantitative deterministic real-time-related properties. It is the purpose of this paper to exemplify steps that need to be taken in order to overcome this deficit.
We first discuss choices that need to be made when designing a suitable real-time execution model for SDL and Estelle and proceed to present two remedies to the inexpressiveness problem: First, we introduce the concept of complementary real-time specification by reconciling the semantic models of Metric Temporal Logic and SDL and showing how both languages can be used in a complementary fashion. Second, we suggest a language extension and the corresponding semantic interpretation for Estelle. While we present examples from the domain of multimedia and broadband systems, the applicability of our specification methods extends to hard real-time systems. Finally, we discuss extensions of our techniques to capture QoS stochastic properties, and we allude to formal requirements verification and automatic implementation based on our techniques.
Technical Report 97-08, Department of Electrical and Computer Engineering,
University of Waterloo. PostScript-File
(54 p.)
Abstract:
Many telecommunications systems engineers find it convenient to specify functional properties of their systems using state-transition based formal description techniques like SDL, Estelle or Message Sequence Charts (MSCs). However, the expressiveness of these techniques does not capture real-time requirements, an important class of Quality of Service (QoS) requirements in telecommunications systems design. In this paper we introduce a method for the integration of functional system properties given as SDL specifications with real-time temporal logic specifications. We call the resulting specifications {\em complementary specifications}. First we proof the inexpressiveness of SDL with respect to hard real-time bound requirements. Next we define a common model theoretic foundation which allows SDL specifications to be used jointly with temporal logic specifications. Then we give examples of real-time related delay bound, delay jitter, and isochronicity constraint QoS specifications. We also discuss how our method helps in the specification of various QoS mechanisms, like QoS negotiation, QoS monitoring and jitter compensation. We finally also point at the use of these specifications in a formal verification context.
Abstract:
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 on real-time bounds and probability constraints which these FDTs do not allow to express. However, suitably extended temporal logics allow for a description of these requirements. We introduce a method for the integration of functional system 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 delay 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.