Abstract
SDL is intended for the specification of complex, event-driven, real-time, and interactive applications involving many concurrent activities that communicate using discrete signals.

Although the behaviour of an SDL system is clearly defined by the semantics of SDL, analysis of the real-time behavoiur is still hard to do for such a system. Timing and the arrival order of signals is of paramount significance for correct behaviour. So, it would be very difficult to do an exhaustive testing on an SDL system during run-time. This is partially because we cannot control the order of arrival of signals to a process, at least not for signals internal to the SDL system. No matter how many times we run a test suite, it is possible that signals always come in the same order at a specific state of the system.

Happily, there are verification tools for analysis of models of real-time systems e.g., Uppaal . The basis of the Uppaal model is the notion of timed automata developed by Alur and Dill as an extension of classical finite--state automata with clock variables. If we could transform an SDL system into a network of timed automata while conserving its behaviour we would be able to let Uppaal do the verification.

In this report we describe and implement a translation from an SDL (Specification and Description Language) syntax to a language (xta) used in the Uppaal tool. We show how it is possible to simulate implicit and explicit channels, queues, timers, dynamic process creation and process execution. Apart from timers we can also simulate worst and best execution time per action statement in the process.

E-mail: hessel@docs.uu.se
Web: http://user.it.uu.se/~hessel/

ASTEC seminar
May 14, 2002

Place: Information technology, Uppsala University
Room: 1113
Time: 15.15-16.00 (+ discussions)

Room 1113 is in building 1, floor 1, room 13 (in the southern part of the building).

Help on how to find ASTEC Seminars.

There will be an extended period for discussions after the seminar.

Speakers are encouraged to give an short (5 min) introduction to the subject at the begining of the talk.
Listeners are excused if they have to leave after 16.00.