Design Calculi for Telecommunications	DesCaRTeS Seminar	UNU-IIST Home
Beyond SDL

II/2/1/3/1 Beyond SDL

Beyond SDL is a series of six one hour lectures on closely related research topics from the DesCaRTeS Programme: the semantics of time related features in SDL; logics for reasoning about systems described in SDL; and abstract semantic models for SDL.

Course attendees should be at least final year undergraduates in computer science.

The titles of the course lectures are as follows:

1. Introduction to SDL.

2. Introduction to Process Algebra.

3. An Adequate Semantics of Time Related Features of SDL.

4. Towards a Logic for Reasoning about SDL Processes, Part I.

5. Towards a Logic for Reasoning about SDL Processes, Part II.

6. Dataflow Networks for an Abstract Model of SDL.

The following describes these lectures in broad outline:

Introduction to SDL

The concepts around which this specification language has been set up, will be explained and illustrated by excerpts from an SDL specification. Besides, an overview will be given of (a) current SDL related issues in telecommunications, (b) research topics originating from these issues (c) the state of affairs with respect to the topics studied.

Introduction to Process Algebra

Process algebra in the form of ACP and some extensions that will be used in later lectures will be reviewed. The extensions discussed include amongst others discrete time process algebra and process algebra with propositional signals. Emphasis will be on the semantic issues involved, in particular the operational semantics of process expressions in terms of transition systems.

An Adequate Semantics of Time Related Features of SDL

A new semantics of an interesting subset of the specification language SDL is given by a translation to discrete time process algebra with propositional signals. The strength of the chosen subset, called phiSDL, is its close connection with full SDL, despite its dramatically reduced size. Novel to the presented semantics is that it relates the time used with timer setting to the time involved in waiting for signals and delay of signals.

Towards a Logic for Reasoning about SDL Processes, Part I

Timed frames are introduced as objects that can form a basis of a model theory for discrete time process algebra. An algebraic setting for timed frames is proposed and results concerning its connection with discrete time process algebra are given. The presented theory of timed frames captures the basic algebraic properties of timed transition systems. Further structure on timed frames is provided by adding signal inserted states to cover discrete time process algebra with propositional signals.

Towards a Logic for Reasoning about SDL Processes, Part II

A logic for signal inserted timed frames is proposed. This logic, called TFL, is a classical first-order logic with quantification over some sets of objects that are relevant to frames, equality and some additional standard predicates. Thus, TFL combines a simple syntax with a high expressivity. Results concerning its distinguishing power are presented. It is sketched how two logics underlying model checkers, can be embedded in TFL.

Dataflow Networks for an Abstract Model of SDL

Dataflow networks are introduced as objects that represent systems as networks of nodes that consume and produce data and channels between them to pass the data through. Process algebra models for dataflow networks are sketched. It is outlined how such dataflow networks and systems described in SDL match together. The importance of a dataflow network model for SDL is explained.

Beyond SDL
	Design Calculi for Telecommunications	DesCaRTeS Seminar	UNU-IIST Home