II/1/1/2 DesCaRTeS: Design Calculi for Telecommunications Systems

Introduction

Until recently, the field of telecommunications has focussed on technology relevant to switching and transmission. This technology was used to provide the only telecommunication service offered, namely the Plain Old Telephone Service (POTS). Fast technological developments have made it possible to provide many new services with all kinds of additional features. Higher level services are realized by protocols using lower level services, and telecommunications systems have become rather extensive and complex. One of the symptons of the increasing complexity is the appearance of service feature interactions between the services that are offered in telecommunications systems. Therefore the focus is now changing over to the telecommunication services.

In the telecommunications field, the specification language SDL [2] is frequently used for specification and design of services. The first version of SDL became a recommendation of the International Telecommunications Union (ITU) in 1976. It originated from an informal graphical description technique already commonly used in the telecommunications field at the time of the first computer controlled telephone switches. It has since been extended several times, and the recent revised version of SDL became a recommendation in 1992. In the telecommunications field, SDL has survived description techniques that are more design calculus oriented, such as LOTOS [9], and it will presumably still be used for a long time.

Problem definition

Specification of telecommunications services is usually done with the intention of analysing the behavioural properties of these services and validating their design. During this design process, the services are described at different levels of abstraction, which gives rise to a need to verify that the properties represented by one description are preserved in another, more concrete, description, thus justifying the design step.

The current situation is that there are only means for limited analysis and no means at all for formal verification. The main reason is that the semantics of SDL according to the ITU recommendation [7][8] is at some points inadequate for advanced analysis and formal verification. In particular the semantics of time related features of SDL, such as timers and channels with delay, is insufficiently precise. Moreover, the semantics is at some other points unnecessarily complex. Consequently, proof rules, which are indispensable for formal reasoning about a specification, have not yet been developed and most existing analysis tools, e.g. GEODE [1] and SDT [10], offer at best a limited kind of model checking, which is closely related to simulation of the described behaviour, and generally offer no support for time related features.

The intrinsic highly reactive and distributed nature of prospective telecommunication services demands more advanced analysis than currently possible, in particular analysis giving considerations to timing properties as well. In addition, the increasing complexity of telecommunications systems is in itself becoming a compelling reason to use, at least to a certain extent, formal verification to justify design steps, and the need becomes even more urgent with the increasing emphasis on the dependability of services.

Prerequisites for advanced analysis and formal verification are a dramatically simplified version of SDL together with an adequate semantics, and only when these are available can possibilities for advanced analysis be elaborated and proof rules for formal verification devised.

Aims and Objectives

The DesCaRTeS programme aims to enhance the possibilities for advanced analysis of SDL descriptions, particularly analysis of time related behavioural properties, and to turn SDL into a full-fledged design calculus by adding proof rules to support formal verification. In this way, it can help to improve the quality of prospective telecommunication services by providing a foundation for solving basic technical problems that telecommunications manufacturers and operators encounter in their current attempts to continue developing and providing telecommunication services of outstanding quality.

In addition, the programme, in working closely with research groups in developing countries, aims to help developing countries attain the ability to master their own development of telecommunications systems. This is crucial if they are to remain reasonably self-sufficient in this vital component of their infrastructures.

Existing Related Work

The DesCaRTeS programme can be considered as a continuation of recent work, presented in [3][4][6], which had similar aims.

In [5], a semantics for an interesting subset of SDL, called phiSDL, is given which is novel in that it deals properly with the time related aspects of SDL. The results of the work presented in [3] and [4], together with the semantics of phiSDL, are meant to be used to devise a logic to analyse properties of systems described in SDL, and to adapt an existing model checker to SDL and this logic. The results of the work presented in [6] are meant to be used to elaborate a model for a fully abstract semantics for phiSDL, which is expected to facilitate the quest for proof rules for SDL.

iistinfo@iist.unu.edu, March 1996

DesCaRTeS: Design Calculi for Telecommunications Systems

DeTfoRS: Design Techniques for Real-Time Hybrid Systems

Research Projects

Models for Internet-based Programming

UNU-IIST Home