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

II/2/1/3/2 DesCaRTeS Seminar

The DesCaRTeS Seminar comprises:

1. a one-week course, at post-graduate/post-doctoral level, on SDL, its use in software development, and selected research topics of the DesCaRTeS Programme. This consists of a series of 12 morning lectures of 45 minutes each complemented by 4 afternoon exercise sessions of 3 hours each.

2. a two-week workshop, for four to six selected participants, with exploratory research experiments on topics of the DesCaRTeS Programme. This consists of 10 morning and 10 afternoon sessions, each of 3.5 hours.

The titles of the course lectures are as follows:

1. Design Calculi in Software Development: Theory and Practice.

2. Survey of Flat SDL.

3. Software Development Using SDL, Part 1.

4. Software Development Using SDL, Part 2.

5. Survey of Discrete Time Process Algebra.

6. Process Algebraic Underpinning of Communication and Timing in SDL, Part 1.

7. Process Algebraic Underpinning of Communication and Timing in SDL, Part 2.

8. Timed Frames: Transition Systems for an Operational Semantics of SDL.

9. Timed Frame Logic: A Basis for Model Checking.

10. Towards Advanced Analysis of SDL Descriptions.

11. Timed Asynchronous Dataflow Networks for an Abstract Semantics of SDL.

12. Towards Proof Rules for SDL.

The following describes the lectures in broad outline:

Design Calculi in Software Development: Theory and Practice

Design calculi allow to formulate formal descriptions of software systems and to calculate properties of single descriptions and relations between pairs of them. The nature of formal descriptions and the importance of the ability to calculate properties of them are explained. The still widespread resistance to use design calculi is discussed, and the policy to take it away that underlies the DesCaRTeS Programme is sketched.

Survey of Flat SDL

We give an overview of phiSDL - standing for flat SDL - which is a small subset of SDL. The strength of this subset is its close connection with full SDL, despite its dramatically reduced size. For example, apart from the data type definitions, SDL descriptions can be transformed to phiSDL descriptions.

Software Development Using SDL

An overview is given of how SDL is currently used and what complementing tools and techniques are available. A typical sequence of stages in current software development using SDL is sketched. The basic problems that are encountered in this practice and their connections with the DesCaRTeS Programme are touched upon. In addition to the simple telephone answering machine, the OSI concept of layer service is used for illustration.

Survey of Discrete Time Process Algebra

Process algebra in the form of ACP (Algebra of Communicating Processes) and its extension to a discrete time process algebra with relative timing is reviewed. Additionally the extension with propositional signals in the discrete time setting is presented in brief. Thus the process algebra underlying the process algebra semantics given for phiSDL is largely covered. Emphasis will be on the semantic issues, in particular the operational semantics of process expressions in terms of transition systems.

Process Algebraic Underpinning of Communication and Timing in SDL

A new semantics of a subset of phiSDL is presented. In this subset process creation and delaying channels are left out from phiSDL to concentrate on the process algebraic underpinning of SDL's most distinctive features, viz. its communication and timing mechanisms. The semantics is given by a translation to discrete time process algebra with propositional signals. Novel to the presented semantics is that it deals properly with the time related aspects of SDL.

Timed Frames: Transition Systems for an Operational Semantics of SDL

Simple timed frame algebra and its extension with signal insertion are presented. Results concerning the connection between timed frame algebra and discrete time process algebra, showing that timed frames can form a basis of a model theory for discrete time process algebra, are also presented. These results justify the choice to use timed frames for an operational semantics of phiSDL. The further structure on timed frames, provided by signal insertion, is needed to cover discrete time process algebra with propositional signals.

Timed Frame Logic: A Basis for Model Checking

We give a survey of TFL (Timed Frame Logic), a first-order logic for signal inserted timed frames. This logic is meant to be taken as the starting point for devising a logic that is suitable to analyse properties of systems described in phiSDL. It is a classical logic with quantification over some standard sorts and with some standard predicates. Thus, TFL combines a simple syntax with a high expressivity. Results concerning its distinguishing power are presented, and it is sketched how some logics underlying model checkers can be embedded in TFL.

Towards Advanced Analysis of SDL Descriptions

This lecture is intended for the presentation of the latest results of the ongoing work on an operational semantics of phiSDL and a logic to analyse properties of systems described in phiSDL. It will include a timed frame model for discrete time process algebra with relative timing that is isomorphic to its standard model. This allows us to check whether a discrete time process satisfies a property expressed in TFL.

Timed Asynchronous Dataflow Networks for an Abstract Semantics 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. A process algebra model for asynchronous dataflow networks is sketched. We adapt this model and add some standard atomic components to obtain a model that is close to the concepts around which SDL has been set up and well suited as the underlying model for an abstract semantics of phiSDL.

Towards Proof Rules for SDL

This lecture is intended for the presentation of the latest results of the ongoing work on a fully abstract semantics of phiSDL. Such a semantics is meant to be taken as the starting point for devising proof rules for phiSDL.

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