Timing Analysis of an SDL subset in Uppaal


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.

Full report here.