Timing analysis of an SDL subset in Uppaal.
Department of Information Technology, Uppsala University
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
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
So, it would be very difficult to do an exhaustive testing on an SDL system
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.
Place: Information technology, Uppsala University
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.
Everyone is welcome !
Updated 27-Apr-2006 17:29 by Roland Grönroos
e-mail: info -at- astec.uu.se