Marius Bozga

Susanne Graf

Alain Kerbrat

Daniel Vincent

Laurent Mounier

Iulian Ober

SDL for Real-Time: What Is Missing? 1

Introduction

The ITU{T Speci cation and Description Language (SDL, 1]) is increasingly used in the development of real-time and embedded systems. This kind of systems impose particular demands on the development language and SDL is a suitable choice in many respects: it is formal, it is supported by powerful development environments integrating advanced facilities (like simulation, model checking, test generation, auto-coding), and it supports many phases of software development ranging from analysis to implementation and on-target deployment.

In this paper we review the needs of a real-time systems developer that are not covered, for various reasons, by SDL. The issues that we examine are heterogeneous, ranging from pure programming issues, like the di culty to specify real timeout emergency procedures in SDL, or the di culty to program atomic transactions, to high-level modeling issues, like the di culty to model time nondeterministic system components, or the impossibility to use the standard formal semantics of SDL in simulation and veri cation. For most issues we strain to give solutions, although sometimes this only means that we favor one alternative among a set of incompatible, equally justi ed choices.

We propose a di erent semantic setting for time in SDL, that allows a exible speci cation of timing requirements and timing knowledge about the system. With our proposal one can capture very general forms of conditions on the duration of actions or the duration between two events. We dispose of analysis methods that work on top of this semantic framework, and by which we can verify general timing properties of a SDL system, such as the minimal/maximal time between two particular events.

We show on a small example how our semantic setting may be used as the basis for other methods [START_REF] Diefenbruch | Performance evaluation of SDL systems adjunct by queueing models[END_REF][START_REF] Roux | SDL performance analysis with ObjectGEODE[END_REF]) of introducing timing properties in a SDL system, methods that are closer to the abstraction level of SDL. The value added by our semantic framework is clearly marked.

2 Types of Problems and General Proposals 2.1 Types of Problems SDL has the double aim of being on one hand a high-level speci cation formalism, which means it must abstract from certain implementation details, and on the other hand a programming formalism from which direct code generation is possible. The problems that we identify in this paper refer to SDL either as a speci cation language, or as a programming language. The problems on each side are di erent because the needs on each side are di erent too.

On the speci cation side, we further have two kinds of problems: expressivity problems and usability problems.

1. An expressivity problem is the impossibility of SDL to capture meaningful information about a system (like, for example, the execution time boundaries of a piece of SDL code). 2. Usability problems relate to the way an SDL model is used in analysis and early design: the modeler must be able to simulate the system or formally verify certain properties. An usability problem is a problem in the de nition of the SDL semantics, which makes it practically or theoretically di cult to construct the global state graph of a SDL system (graph that is used by simulation or veri cation tools).

Semantic Pro les for SDL

The semantics of SDL, as presented in 1], is rather crafted for code generation than for simulation and veri cation. Z.100 maintains that each action takes an indeterminate time to execute, and that a process stays an indeterminate amount of time in a certain state before taking the next reable transition. This notion of a time that is external, unrelated to the SDL system, is practical for code generation in the sense that actual implementations of the system conform to it. However, for simulation and veri cation, this semantics of time is utterly impractical: timer extents do not have any signi cance, any timer that gets in a queue may stay there for an indeterminate amount of time.

Any rigorous attempt to construct the simulation graph of a SDL system (which is the starting point for simulation and veri cation) must account for all possible combinations of execution times, timer expirations and timer consumptions, causing an explosion of the state space. We have here a usability problem, as characterized in section 2.

In practice, simulation and veri cation tools make simplifying assumptions on execution and idle times. The usual convention is that actions take 0 time to execute, and that the system executes immediately whatever it can execute. This option is justi ed by the fact that it generates the highest degree of determinism, thus reducing the state space by an important factor (and in fact, rendering SDL systems analyzable). This is not the only point where the SDL semantics raises usability problems for simulation and veri cation, as we will see in the next sections.

We face here two alternative de nitions of the SDL semantics that are mutually exclusive and equally justi ed (one by the needs of code generators, one by the needs of simulators and veri cation tools). This dichotomy cannot be surpassed by a single SDL semantics. The solution we propose is to adopt multiple semantic pro les of SDL. The idea of de ning multiple semantic pro les of a language is not new: the UML community is on the way to de ning several pro les for UML 2], each one t for a particular application domain (real time, electronic commerce, etc). In the case of SDL, pro les would not correspond to di erent application domains but rather to the di erent usages of a SDL model: code generation, simulation, performance analysis, model checking, test generation etc.

A semantic pro le would de ne a semantics that is particularly suitable for a certain type of manipulation of a SDL model. A semantic pro le for code generation, for example, would support real parallelism between the agents composing a system, while a semantic pro le for simulation and veri cation would propose quasi-parallel execution of agents, that is, interleaving of transitions or transition actions.

If we accept the need for di erent semantic pro les, it follows that the de nition of pro les should be parameterized. Parametric semantic pro les allow to reuse the common part of two di erent semantics, and outline only the di erences. For example, a semantic pro le for simulation and veri cation could have a parameter which determines whether whole transitions are atomic, or whether only the SDL statements (output, task, set, reset, etc) should be atomic (the fact that TAU SDL Validator 15] supports such a parameter suggests it is useful). There is no need to have two whole di erent pro les for these two cases, since most of the semantics is the same in the two cases. A parameter would be a simple and clean solution.

Semantic pro les allow the SDL standard to follow the path that was already undertaken by SDL tools, which are highly parameterized. The parameters used by tools such as ObjectGEODE 16] and TAU 15] represent in fact small variations in the semantics used by the tools.

Introducing pro les in the SDL standard has the advantage that all existing pro les would be concentrated together, and that compliance relationships between pro les could be de ned formally.

A theoretical basis for de ning pro les and inter-pro le compliance relationships does not exist and is hard to develop, but the current practice of SDL tools, which employ the notion of pro le implicitly and without discipline, demands it.

3 What is Missing on the Programming Side?

SDL has several characteristics that are attractive for real-time systems designers: asynchronous communication is a rst class language feature, a speci cation is organized in a logical hierarchy that can be mapped in many ways to di erent physical con gurations of software modules (and SDL code generators usually provide this feature), external code may be called from SDL making it possible to use system libraries directly from SDL.

There are however several mechanisms, often employed in real-time systems, which should be natively implemented in the language. We review some of them here.

Interruptive Timers

SDL o ers native mechanisms for writing time dependent code: one can consult the system clock from SDL (through the implicit variable now), can set timers, wait for a timer to expire or receive an asynchronous message when it expires. SDL timer timeouts are always received as asynchronous messages. For general-purpose time dependent code this is usually ne, but it may be di cult to write real timeout emergency procedures using timers. To ensure that a piece of code is executed immediately as a consequence of a timeout, the SDL programmer must rst make sure that the agent handling the timer is idle when the timer is received. If this is not the case, then the process may consume the asynchronous timer message from the message queue only when it nishes its current job, which may be too late.

SDL needs a notion of emergency timer, whose expiration is taken immediately into account by the receiving agent. Emergency actions which interrupt the normal execution of an agent were already introduced in SDL'2000, with the advent of exceptions. All we need is a link between the exception mechanism and the system time.

Our proposal goes towards the introduction of the notion of interruptive timer in the language. An interruptive timer is a timer that raises an exception instead of sending an asynchronous message when it expires. With interruptive timers, one can easily set up real timeout emergency procedures.

Atomic Code Sequences and Synchronization

Atomicity and mutual exclusion may be achieved in SDL by directly inserting system calls in the SDL code. However, these are patterns that are very commonin real-time systems, and SDL could bene t from native constructs for expressing atomicity and mutual exclusion. Additionally, inserting system calls in SDL for achieving atomicity and mutual exclusion has a severe drawback: as we mentioned in the beginning of Section 3, one advantage of SDL is that it can be mapped to di erent physical software con gurations. The system calls for obtaining mutual exclusion are di erent when agents are mapped to threads and when they are mapped to processes. This means that the SDL code must di er from con guration to con guration, which is a regression.

With native SDL constructs for atomicity and mutual exclusion, a code generator could generate the right synchronization, rollback or deadlock protection code in every possible mapping. Moreover, atomicity and mutual exclusion would be taken into account in simulation (which is not the case when using system calls), and deadlocks or other kind of errors that they may introduce could be detected earlier.

The same discussion stays valid for general purpose synchronization code. Some forms of synchronization between SDL agents may be achieved only through external system calls. There too, native SDL constructs would be bene c. [START_REF] Alur | A theory of timed automata[END_REF] What Is Missing on the Speci cation Side?

On the speci cation side things are more critical. As mentioned in introduction, the role of SDL in the system development process is twofold: on one hand it is a speci cation language that must be capable to abstract away certain implementation details while still capturing an accurate image of the system under development, on the other hand it is a description language that must be able to express an implementation down to the last details. These two roles of the language are sometimes con icting, and in many cases the description side has been given priority, to the detriment of high-level speci cation.

Control over Time Progress

The problem used as an example in the beginning of Section 2.2 is an important usability problem in itself. A simulator that would use the semantics of time as described in Z.100 1], would have no control over the way time progresses. As a result, the simulator would not guarantee elementary properties like:

1. when a timer expires, it is treated in a reasonable amount of time.

2. when two timers are set at the same time, the timer set with the lower delay will be consumed rst.

This will lead to the exploration of a number of undesirable execution paths that can never actually happen in the system implementation, and eventually to state space explosion. A semantic pro le for simulation must give the simulator some control over the progress of time. Existing simulation tools do this, by assuming that actions take 0 time to execute, and that time never progresses while the system has something to execute. These means of controlling the time progress in simulation are limited. There are cases when the user needs to control the simulation time in more exible ways: { to specify that in a certain state, an unlimited amount of time may pass, even though the system has something to execute (make place for lazy, is it really necessary ???).

{ to specify that in a state, a bounded amount of time may pass regardless of whether there is something to execute or not. In this case, there is a number of consequent problems as to the speci cation of the amount of time ( xed or with lower and upper bounds; speci ed statically or dynamically).

We propose a concrete solution to this problem in Section 5.

Assumptions on Execution Times

There is also an expressivity problem related to the usability problem of section 4.1: since the standard semantics of SDL assumes an indeterminate amount of time may pass while the system is in a state or while it executes an action, there are no means to specify the execution times of (a sequence of) actions.

Such information may be meaningful in simulation or in veri cation. The well functioning of the system may depend on the assumptions on execution times.

Currently, in order to introduce assumptions on minimal execution times, the user is forced to use timers and to introduce explicit waiting. For maximal execution times, the user must also introduce timers and additional invalid states that will have to be considered as unreachable when the state graph is built. So in order to express high-level speci cations, one needs to use programming features.

There exists already several approaches to introducing execution time assumptions in SDL specications. The ObjectGEODE Simulator 14] uses a syntactic extension by which one can associate an execution time (interval) to an action. 9] uses a more elaborate approach in which execution times are dynamically calculated with the help of queuing machines, so that they are depending on the amount of work and on the charge of the system.

We will not introduce here new SDL extesions for expressing execution times. Instead, we introduce a semantic framework that allows a simulator to control the progress of time (Section 5) and we show how existing approaches for expressing execution times [START_REF] Roux | SDL performance analysis with ObjectGEODE[END_REF][START_REF] Diefenbruch | Performance evaluation of SDL systems adjunct by queueing models[END_REF]) can be adapted to our semantic framework, with bene ts in terms of analysis power.

Atomicity of Transition Elements

The lack of programming constructs for expressing atomicity, mutual exclusion, and synchronization was outlined in Section 3.2. The same problem may be characterized as an expressivity problem of SDL as a high-level speci cation language.

Besides that, the lack of a notion of atomicity poses usability problems. Z.100 1] asserts that the agents composing a system are executed in a real parallel environment. In order to work, a simulator has to assume a certain degree of atomicity. Existing SDL simulation and veri cation tools make simplifying assumptions: that statements are atomic, or that entire transitions are atomic, or that sequences of statements that take 0 time to execute are atomic.

The place for such assumptions would ideally be an SDL semantic pro le for simulation and veri cation.

Flexible Channel Speci cations

SDL de nes channels as reliable means for transporting messages: a channel never looses messages.

Additionally, a channel may either be non-delayable (i.e. messages arrive instantaneously at the other end) or with non-speci ed delays (but keeping the order of the conveyed messages).

These attributes are insu cient for characterizing real communication channels. For example, SDL is used to describe ow control protocols such as the alternating bit protocol from the OSI stack. Such protocols are built upon the assumption that channels are unreliable, and it is their mission to make them reliable through software. If the assumptions on channels cannot be marked in SDL, the resulted description of the protocol cannot be used in simulation: the simulator will never cover the parts that handle signal loss.

In practice, when one needs to model a channel which losses messages, or which delays messages by a rule, he has to explicitly describe the behavior of the channel in SDL(with an SDL process, for instance). This approach has several drawbacks: { once the behavior of the channel is speci ed, all messages will arrive at destination with a wrong sender PID. { the channel description must be replicated over and over again for every lossy channel in the system (note that a generic Process Type cannot be used, because the channel description depends on the types of the conveyed signals, which di er from channel to channel).

{ dynamic creation of timers is needed in order to transport an inde nite number of messages at once on a delayable channel.

A simple solution to this problem is to allow the user to specify in SDL:

1. whether a channel looses messages or not, and the loss probability 2. upper and lower time bounds for the delays applied to the message conveyed by a channel, as well as the probability law followed by delays More complicated solutions which take into account the type and size of a message can be imagined.

Again, the ideal place for such extensions would be an SDL pro le for simulation, veri cation and performance analysis.

Timed SDL Semantics Based on Transition Urgencies

In this section we introduce a semantic framework that can be used in connection with SDL to solve the problems of controlling time progress in simulation, problems described in Section 4.1. Basically, we introduce a set of constructs for controlling simulation time progress, for which we dispose of powerful analysis methods that allow to derive interesting timing information (such as the minimal/maximal time span between two events) and to verify timing properties of SDL systems.

The framework presented here is not a direct solution to the problems described in Sections 3 and 4. Instead, it may constitute the underlying semantics for other temporized extensions of SDL (such as 9, 14]), which solve the abouve mentioned problems, and which are closer to the abstraction level of SDL. Therefore, the constructs we introduce below are not meant to be used directly by SDL modelers.

The constructs identi ed here are inspired from Timed Automata with urgencies, a high-level formalism for modeling temporal properties of reactive systems. For a thorough understanding of the semantics behind these constructs, the reader is referred to 3, 4] (timed automata), and 5] (timed automata with urgencies).

As stated in Section 4.1, in order for a semantics to be usable in simulation and veri cation, the simulator has to have control over the system time. In SDL, the system time is represented by the value of the implicit variable now. Our idea is the following: we consider that time may only progress while the system stays in a simulation state, and time does not progress while the simulator executes a system transition (that is, now is not modi ed during a transition). Note that we talk about simulation states and simulation transitions, which may di er from SDL states and transitions: for example, if transitions are not atomic but SDL statements are, there will be a simulator state between each of the SDL statements on a SDL transition, and there will be a simulator transition for each individual SDL statement.

Moreover, the progress of time in a simulator state is controlled (bounded) by the transitions that may be triggered next. We identify three categories of transition urgencies:

1. eager transitions, which have priority over time progress. If in a simulator state there is an eager transition enabled, time cannot progress until the transition (or another enabled transition) is taken.

2. lazy transitions, which do not have priority over time. An enabled lazy transition does not inhibit the progress of time in the simulation state. Therefore, time may progress with an inde nite amount, if the other enabled transitions allow it too.

3. delayable transitions, which have priority over time progress only when time progress would disable them. Time progress may disable a transition if the transition has an enabling condition depending on time (i.e. on the value of now). Therefore, a delayable transition will usually have an enabling condition depending on now, such as now x or now ? x y (where x and y may be integer variables or constants). Then, time may progress in the simulation state until now = x (or now ? x = y).

With this semantics, the simulator can control the progress of the system time by identifying the urgency of the simulator transitions enabled in a certain state.

The source of this information on urgencies di er from case to case, depending on the concrete SDL timed extensions introduced at user level. We can imagine an extension of SDL in which the user puts the urgency information directly in the SDL model, like in the example in Section 6. Urgency information may also be derived from other kinds of timed annotations, as we will see in Section 7.

Transition urgencies were implemented in IF 6, 7], a speci cation language developed at VER-IMAG for prototyping semantic variations of the constructs of a SDL-like language. We have also implemented the extensions in the ObjectGEODE Simulator 13], with good results in terms of both what we can express with them and what analyses we can perform on annotated models.

However, such extensions are not very close to the level of abstraction of SDL, and modelers may nd it di cult to produce the urgency annotations and the related information. As we mentioned already, our extensions are rather thought to be the semantic basis for more user-level constructs, such as those introduced in 9, 14]. Section 7 is dedicated to showing how such user-level extensions are projected on our semantic framework, and what advantages we acquire by using this framework.

Example: the Bounded Retransmission Protocol

We illustrate here on a simple example some of the speci cation problems of SDL that have been identi ed in this paper, and we show how they can be solved using our semantic framework.

Speci cation of the protocol

The example we propose is the so-called \Bounded Retransmission Protocol" (BRP), which provides a le transfer service through an unreliable medium between two entities, a Transmitter and a Receiver. More precisely, each le is splitted into several packets and each packet is transmitted in sequence using the well-known alternating bit protocol. However, in case of packet loss, only a bounded number of retransmission are performed, and thus the le delivery is not guaranteed. In this situation, both entities should abort the current transfer, and proceed to the next le. This protocol has been used as a running example for several veri cation tools 12, 8, 11], and we consider here a simple version mainly focussed on its timing behaviour.

The SDL speci cation of this protocol ( gure 1) is composed of a Transmitter and a Receiver process, brie y described below:

The Transmitter rst waits for a transfer request issued by the environment (Put(p), where p is the number of packets). When a transfer request is issued, it starts sending each packet (m,b) one by one, where m indicates whether the packet is a first, middle or last element of the le, and b is the alternating bit. After each sent of a packet, the Transmitter starts a timer s repeat and waits either from an acknowledgement issued by the receiver, or for the expiration of s repeat. If a correct acknowledgement is received, it resets s repeat and proceeds to the next packet, unless it was the last one, in which case the entire le is delivered to the upper layer (Get(p)). However, if s repeat expires, the same packet is resent up to max retry attempts (s repeat being restarted after each resent). If none of these resent succeeds, then the Transmitter aborts the current le transfer and reports the failure to its upper layer. This is done either using an Abort message when the current packet was a middle one, or using a Dont know message when the current packet is a first or a last one (since in this case the Receiver may have either correctly received the entire le, or no received any packet at all). Finally, after a transfer abortion the Transmitter starts a timer s abort and waits for its expiration before processing the next le.

The Receiver continuously waits for packet receptions. When a first packet is received, it initialises its alternating bit, starts a timer r abort and sends back an acknowledgement to the Transmitter. Each subsequent packet is acknowledged (according to the \alternating bit" policy), and the timer r abort is restarted upon each reception of a new packet. When a last packet is received, the Receiver considers that the entire le has been correctly transmitted: it delivers it to its upper layer (Get(p)), stops its timer, and waits for a new le. However, if an expected packet lates to arrive, then the timer r abort expires and the Receiver can assume that the transfer has been aborted. It informs its upper layer (Abort), and waits for a new le. One of the main correctness criterion of this protocol is that both the Transmitter and the Receiver should decide to abort the same le transfers. However, this is achieved only when precise constraints are ful lled between timers values and action durations. In particular: { if the timer r abort expires too early, then the Receiver will consider that the current transfer is aborted whereas other packets of the same le may still arrive; { if the timer t abort expires too early, then the Transmitter will proceed to the next le after an abortion before this abortion was detected by the Receiver (which will never detect it later); { nally, if the timer t abort is set to a value smaller than max retry times the transmission delay, then the Transmitter will always abort the current transfer . . . As stated in section 4, if this speci cation is simulated following the Z.100 time semantics, no guaranties are ensured about the relative expiration times of the di erent timers. Therefore, even if the timers are set to correct values, many incorrect (and irealistic !) execution scenarios will be observed, preventing any validation result.

On the other hand, simulating this speci cation using the default time semantics of ObjectGEODE (i.e., each transition takes 0 time and is considered eager) is also not satisfying since it excludes realistic scenarios. For instance, using this semantics, the timer r abort can never expire before the reception of an expected packet (expiration will take place only after the packet loss). Thus, this too deterministic time behaviour will only lead to partial validation results. These two limitations can be avoided using the notion of transition urgency introduced in section 5.

More precisely, lazy and delayable transitions are used to specify some parts of the system supposed to take a certain amount of time to execute, or those occurrence is only controlled by the environment (they may occur at a speci ed or unspeci ed frequency). All other transitions (and in particular timeout expirations) are supposed to be eager. In the BRP speci cations the non eager transitions are the following:

{ The transfer requests (Put(p)) issued by the environment, which may occur at an unspeci ed rate, and which should therefore be declared as lazy; { The packet transmission (Sdt(m,b)), which is supposed to take a non deterministic amount of time within a given interval to model the transmission delay, and which should be declared as delayable. (Note that the delay required to transmit the acknowledgements are omitted here, but they could have been introduced similarly). The goal is to show how the semantic framework introduced in Section 5 may be used as a basis for de ning a precise semantics for SDL extensions such as the ObjectGEODE Simulator extensions 14] or QSDL, the extended SDL implemented in the tool QUEST 9].

The ObjectGEODE Performance Evaluation Extensions

The ObjectGEODE Simulator implements a series of SDL extensions, for modeling timing properties of systems. The modeler has the possibility to split the system among multiple processors, to give priorities to processes, and to declare execution durations on actions. We can use these extesions to specify the process Transmitter from our example in Section 6. Namely, we use the ObjectGEODE extensions to model the non-deterministic waiting time before the transmission of signal SDT, as shown in Fig. 3. The transition shown in Fig. 3 may replace the transition outgoing from the state Send, in the initial speci cation of the BRP protocol (Fig. 1.

In ObjectGEODE, execution durations on actions are speci ed statically, by a time interval and a probability distribution (not used here). The actions that have no duration speci ed, are considered to take 0 time. The semantics of time consuming actions is the following: when an agent reaches a time consuming action, it enters an implicit state in which it stays for a time period complying to the speci ed interval. While the agent is in that state, only agents executed by other physical processors may execute. The other agents executed by the same physical processor as the blocked agent are blocked too. When time elapses, the agent exits the implicit state and executes the action in 0 time. In our example, the simulator executes all the actions described in the process Transmitter before the informal task 'non-deterministic wait'. Then, the simulator puts the Transmitter in an implicit state, where it stays for a period of d_trans_min to d_trans_max time units. At the end of this period, the Transmitter exits the implicit state, and the simulator executes the output of SDT in 0 time. This semantics can be captured using urgencies. Associating a delay to an action is equivalent to splitting the initial transition with an implicit intermediate state and an implicit delayable transition, as shown in Fig. 2.

The advantage of using our semantic framework for expressing execution times is that our analysis methods allow to consider both lower and upper limits simultaneously during simulation. The analysis methods we have developed on our model work with time intervals, and we can compute the minimal/maximal time span between two arbitrary occurrences in the system.

QSDL

Queuing SDL (QSDL, 9]) is an extension of SDL with constructs for modeling timing properties of systems, developed at the University of Essen, Germany. QSDL was developed for doing performance modeling and analysis on SDL systems.

The tool supporting QSDL, QUEST 10], implements a discrete-time semantics that resembles the semantics implemented in ObjectGEODE and TAU. Time passes in simulation states, normal transition actions take 0 time to execute. Additionally, QSDL introduces a new SDL statement, which takes time and which may be put on transitions: request. Like in ObjectGEODE, described in the previous section, this time consuming action introduces in fact an implicit simulation state, in which the calling agent stays for as long as the request takes.

The di erence between QSDL and the ObjectGEODE performance evaluation extensions comes from the fact that the execution time of a request is not speci ed statically. QSDL uses the concept of queuing machine to compute the dynamic execution time of a request. Queuing machines represent computing resources shared between several agents of an SDL system, for which the agents compete.

For projecting the QSDL extensions on our semantic framework which uses transition urgencies to control time progress, we need is to model QSDL queuing machines by SDL automata annotated with urgencies. The task is not trivial, because the behavior of a queuing machine depends on a series of parameters:

1. the speed. The absolute amount of work, which is a parameter of the request, is rst divided by the speed of the machine, to obtain an amount of work relative to the machine 2. the number of processors. A machine may have from one to an in nity of processors. Perfect parallelism is assumed (i.e. if a machine has n requests to process simultaneously, m processors, and a speed s, the rate at which each request is processed is r = m n s if n m and r = s if n < m).

3. the scheduling policy. In case of multiple, competing requests, the scheduling policy determines which requests are serviced and which are put on hold. QSDL de nes the following scheduling policies: FIFO with three variants (non-preemptive, priority non-preemptive, and priority preemptive), Processor Time Sharing, In nite Processors, Random non-preemptive, and LIFO priority preemptive. For details, see 10]

We can model QSDL queuing machines in terms of SDL automata with urgencies, with few modi cations to our semantic model. These modi cations preserve the decidability results established in the basic framework, so that our analysis tools can work on the modi ed semantic model. Our idea is not to replace the QSDL extensions with our own, but to base the QSDL semantics on our notion of urgency. Doing this would boost the power of veri cation methods applicable to QSDL.

Conclusions

Fig. 1 .

 1 Fig. 1. The Bounded Retransmission Protocol in SDL

Figure 2 Fig. 2 .

 22 Figure2gives a correct speci cation of the Transmitter process including the urgencies annotations.

Fig. 3 .

 3 Fig. 3. The BRP Transmitter delay modeled using the ObjectGEODE performance evaluation extensions