%PDF-1.3
%
2 0 obj
<<
/Length 4653
>>
stream
1 g
/GS1 gs
0.06 841.89 595.22 -841.83 re
f
BT
/TT2 1 Tf
20 0 0 20 62.5 732.75 Tm
0 g
0 Tc
0 Tw
(Towards a New Formal SDL Semantics)Tj
/TT4 1 Tf
13 0 0 13 62.5 674.41 Tm
(R. Gotzhein, B. Geppert, F. Rler, P. Schaible)Tj
0 -1.0769 TD
(Computer Networks Group,University of Kaiserslautern)Tj
T*
(University of Kaiserslautern, Postfach 3049, D-67653 Kaiserslautern, Germany)Tj
T*
-0.0392 Tw
(Tel: +49 631 205-3426, Fax: +49 631 205-3956, Email: gotzhein@informatik.uni-kl.de)Tj
/TT2 1 Tf
10 0 0 10 270.67 598.41 Tm
0 Tw
(Abstract)Tj
/TT6 1 Tf
-20.817 -1.1 TD
-0.004 Tw
(In 1988, a formal semantics for SDL has been added as Annex F to the Z.100 SDL standard [5,6,7,8]. Along with)Tj
T*
-0.011 Tw
(the efforts to improve SDL, the semantics has been revised several times since then. To understand the semantics,)Tj
T*
-0.04 Tw
(intimate knowledge of the language Meta IV is required. Meta IV is a formal language based on synchronous com-)Tj
T*
0.012 Tw
(munication between a set of concurrent processes. Essentially, Annex F defines a sequence of Meta IV programs)Tj
T*
-0.057 Tw
(that take an SDL specification as input, determine the correctness of its static semantics, perform a number of trans-)Tj
T*
-0.012 Tw
(formations to replace several language constructs, and interpret the specification. It has been argued that this style)Tj
T*
0 Tw
(of defining the formal semantics is particularly suitable for tool builders.)Tj
0.851 -1.1 TD
-0.006 Tw
(With the ongoing work to improve SDL, and a new version called SDL-2000 to pass the standardization bodies)Tj
-0.851 -1.1 TD
-0.02 Tw
(shortly, it has become apparent that a decision concerning the SDL semantics needs to be taken. One alternative is)Tj
T*
0.026 Tw
(to revise the existing SDL semantics, which has the advantage of continuity. Another alternative currently under)Tj
T*
0.021 Tw
(consideration is to redo the SDL semantics, which offers an opportunity for improvement. In this paper, some of)Tj
T*
0.004 Tw
(the choices that go along with a new definition of a formal SDL semantics are presented and discussed. Based on)Tj
T*
0 Tw
(the results of this discussion, a coarse outline for a new formal semantics is proposed.)Tj
/TT2 1 Tf
20.511 -2.2 TD
(Keywords)Tj
-9.124 -1.1 TD
(formal description technique, formal semantics, SDL)Tj
/TT6 1 Tf
11 0 0 11 62.5 329.75 Tm
[(1)-1561.8(SOME DESIGN OBJECTIVES)]TJ
10 0 0 10 62.5 304.41 Tm
0.044 Tw
(Among the primary design objectives of a formal SDL semantics is intelligibility, a prerequisite for acceptance,)Tj
T*
0.074 Tw
(correctness, and maintainability. Generally speaking, intelligibility can be achieved by building on well-known)Tj
T*
-0.002 Tw
(mathematical models and notation, a close correspondance between specification and underlying model, and by a)Tj
T*
0 Tw
(concise and well-structured documentation.)Tj
0.851 -1.1 TD
-0.059 Tw
(As SDL is an evolving language, it can be expected that there will be further versions in the near future, therefore,)Tj
-0.851 -1.1 TD
-0.026 Tw
(maintainability is of similar importance. There are currently several language extensions under discussion, includ-)Tj
T*
0.07 Tw
(ing exception handling, dynamic modification of system structure, real time expressiveness beyond timers, and)Tj
T*
0.017 Tw
(performance specification, as well as removal of some language features. Therefore, the semantical model has to)Tj
T*
0 Tw
(be sufficiently rich and flexible such that these aspects can be formalized with a reasonable effort.)Tj
0.851 -1.1 TD
-0.059 Tw
(Apart from assigning a unique meaning to SDL specifications, a formal semantics should support formal analysis)Tj
-0.851 -1.1 TD
0.04 Tw
(as well as implementation steps. Even if performance aspects are not directly covered by language constructs, it)Tj
T*
0.016 Tw
(should be possible to assign a formal meaning to suitable annotations, based on the same semantical model. This)Tj
T*
0.062 Tw
(would allow to use the same model both for qualitative reasoning as well as for performance and predictability)Tj
T*
-0.055 Tw
(analysis. Implementation support concerns the straightforward generation of correct code that can be executed with)Tj
T*
-0.024 Tw
(varying degrees of parallelism. This can typically be achieved by an operational semantics and a suitable model of)Tj
T*
0 Tw
(concurrency.)Tj
0.851 -1.1 TD
-0.027 Tw
(Finally, SDL is a language that has been successfully used for about 20 years. This observation has an important)Tj
-0.851 -1.1 TD
-0.008 Tw
(implication: there is no room for experiments for defining a formal semantics, but the formal semantics must sup-)Tj
T*
0 Tw
(port SDL as it is currently used [5].)Tj
ET
endstream
endobj
3 0 obj
<<
/ProcSet [/PDF /Text ]
/Font <<
/TT2 4 0 R
/TT4 5 0 R
/TT6 6 0 R
>>
/ExtGState <<
/GS1 7 0 R
>>
>>
endobj
10 0 obj
<<
/Length 6787
>>
stream
1 g
/GS1 gs
0.06 841.89 595.22 -841.83 re
f
BT
/TT6 1 Tf
11 0 0 11 62.5 738.75 Tm
0 g
0 Tc
0 Tw
[(2)-1561.8(DESIGN CHOICES)]TJ
10 0 0 10 62.5 713.41 Tm
-0.013 Tw
(Before and during the design of a formal SDL semantics, a number of decisions have to be made. Some of the op-)Tj
0 -1.1 TD
0 Tw
(tions are addressed subsequently \(for details, see also [4]\).)Tj
/TT2 1 Tf
11 0 0 11 62.5 678.75 Tm
[(2.1)-811.8(Language coverage)]TJ
/TT6 1 Tf
10 0 0 10 62.5 655.41 Tm
-0.019 Tw
(In general, the set of syntactically correct SDL specifications for which a formal semantics is defined, called )Tj
/TT4 1 Tf
43.744 0 TD
0 Tw
(lan-)Tj
-43.744 -1.1 TD
-0.029 Tw
(guage coverage)Tj
/TT6 1 Tf
6.33 0 TD
( in the following, should be as large as possible. There are, however, certain limitations as well as)Tj
-6.33 -1.1 TD
-0.014 Tw
(pragmatic considerations that may reduce language coverage. Without going into technical detail, we will address)Tj
T*
0 Tw
(some of the considerations in this respect.)Tj
0.851 -1.1 TD
-0.03 Tw
(An important criterion for language coverage is that any SDL specification for which a formal semantics is to be)Tj
-0.851 -1.1 TD
0.003 Tw
(defined has to be complete from a formal point of view. A specification containing informal text elements - for)Tj
T*
-0.033 Tw
(instance, informal question and answers attached to a decision-symbol - would be incomplete in this sense. In gen-)Tj
T*
0 Tw
(eral, a complete specification should formally define a set of computations or execution sequences, in one way or)Tj
T*
0.006 Tw
(another. This rules out any informal elements other than comments or annotations, even if they are used in a syn-)Tj
T*
0 Tw
(tactically correct manner.)Tj
0.851 -1.1 TD
-0.047 Tw
(A pragmatic approach to achieve a good language coverage is bottom-up: starting from a set of)Tj
/TT4 1 Tf
38.467 0 TD
(basic language)Tj
-39.318 -1.1 TD
0 Tw
(constructs)Tj
/TT6 1 Tf
4.111 0 TD
-0.028 Tw
[( for which a formal semantics is defined in a rigorous way, further language constructs are included step)]TJ
-4.111 -1.1 TD
-0.029 Tw
(by step. This means that an SDL core language is defined, and that a formal semantics is assigned to specifications)Tj
T*
0.02 Tw
(written in this core language. In subsequent steps, this core language is extended by language constructs that can)Tj
T*
-0.02 Tw
(be defined syntactically, i.e. by translation to the SDL core language, sometimes called normalization. Candi-)Tj
T*
-0.056 Tw
(dates are shorthands such as the *-symbol used in process graphs, structuring elements such as services, and object-)Tj
T*
-0.046 Tw
(oriented language constructs such as redefinition of virtual transitions. Normalization could simply be done by tex-)Tj
T*
-0.009 Tw
(tual replacements, but may also involve transformations, as it would be the case when a set of services is replaced)Tj
T*
0 Tw
(by their product automaton.)Tj
0.851 -1.1 TD
-0.057 Tw
(SDL offers a number of object-oriented language constructs, including block types, process types, specialization,)Tj
-0.851 -1.1 TD
-0.017 Tw
(virtual types, and virtual transitions. Object-oriented constructs provide support for structuring a specification and)Tj
T*
0.022 Tw
(thus to improve its readability and its maintainability. Also, they allow to postpone some design decisions by in-)Tj
T*
0 Tw
(troducing supertypes that may be specialized or partially redefined. As noted before, it is required that SDL spec-)Tj
T*
0.014 Tw
(ifications for which a formal semantics is to be defined be complete. Therefore, it should in principle be possible)Tj
T*
0 Tw
(to eliminate object-oriented language constructs through normalization steps.)Tj
0.851 -1.1 TD
-0.044 Tw
(SDL supports the specification of systems that are open in a topological sense, i.e. systems that may interact with)Tj
-0.851 -1.1 TD
-0.015 Tw
(some environment. Strictly speaking, this type of specification may be considered incomplete from a formal point)Tj
T*
-0.041 Tw
(of view, since the environment is not known. This, however, is a frequent case in distributed systems development,)Tj
T*
-0.06 Tw
(and therefore, it is important that specifications of open systems have a formal semantics. We will address this topic)Tj
T*
0 Tw
(in more detail in a separate section below.)Tj
/TT2 1 Tf
11 0 0 11 62.5 312.75 Tm
[(2.2)-811.8(Mathematical model)]TJ
/TT6 1 Tf
10 0 0 10 62.5 289.41 Tm
-0.054 Tw
(An important design decision concerns the class of mathematical models that underlies the formal semantics. Apart)Tj
T*
0.077 Tw
(from personal preferences that may be influenced by ones background, the pros and cons for possible choices)Tj
T*
0 Tw
(should be considered carefully before a decision is made.)Tj
0.851 -1.1 TD
-0.026 Tw
(The pro of utmost importance for a transition system is the fact that intuitively, the underlying semantical model)Tj
-0.851 -1.1 TD
0.057 Tw
(is a)Tj
/TT4 1 Tf
1.726 0 TD
(set of extended finite state automata)Tj
/TT6 1 Tf
14.701 0 TD
[( communicating)]TJ
/TT4 1 Tf
6.836 0 TD
0 Tw
(asynchronously)Tj
/TT6 1 Tf
6.277 0 TD
0.057 Tw
(. This intuition should somehow be re-)Tj
-29.54 -1.1 TD
-0.007 Tw
(flected in the semantics, which would certainly make it better understandable. Also, the incorporation of time and)Tj
T*
0.016 Tw
(performance aspects is well supported in the context of transition systems. On the other hand, abstract data types)Tj
T*
0 Tw
(are specified algebraically in SDL, which would lead to a slightly heterogeneous formal semantics.)Tj
0.851 -1.1 TD
0.005 Tw
(Important pros for a process algebra are the availability of a bulk of scientific results and the fact that algebraic)Tj
-0.851 -1.1 TD
-0.01 Tw
(specifications of abstract data types can be accommodated in a straightforward manner. On the other hand, the in-)Tj
T*
-0.036 Tw
(teraction paradigm of most process algebras is)Tj
/TT4 1 Tf
18.553 0 TD
0 Tw
(synchronous)Tj
/TT6 1 Tf
5.055 0 TD
-0.036 Tw
[( communication, which creates a gap between intuitive)]TJ
-23.608 -1.1 TD
0.01 Tw
(and mathematical model. Also, scientific results are usually based on)Tj
/TT4 1 Tf
27.991 0 TD
0 Tw
(basic)Tj
/TT6 1 Tf
2.111 0 TD
0.01 Tw
[( process algebras, which are not suffi-)]TJ
-30.102 -1.1 TD
0 Tw
(ciently expressive to serve as an underlying semantical model.)Tj
/TT2 1 Tf
11 0 0 11 62.5 133.75 Tm
[(2.3)-811.8(Interleaving vs. non-interleaving)]TJ
/TT6 1 Tf
10 0 0 10 62.5 110.41 Tm
-0.051 Tw
(Most FDTs in the area of concurrent systems such as SDL, Estelle and Lotos have an interleaving semantics, which)Tj
T*
0.011 Tw
(means that all activities are sequentialized in the underlying model. The intention, though, is to allow for parallel)Tj
T*
0.085 Tw
(implementations. However, sequentializations are much easier to treat both to define the formal semantics and)Tj
ET
endstream
endobj
11 0 obj
<<
/ProcSet [/PDF /Text ]
/Font <<
/TT2 4 0 R
/TT4 5 0 R
/TT6 6 0 R
>>
/ExtGState <<
/GS1 7 0 R
>>
>>
endobj
13 0 obj
<<
/Length 7625
>>
stream
1 g
/GS1 gs
0.06 841.89 595.22 -841.83 re
f
BT
/TT6 1 Tf
10 0 0 10 62.5 739.41 Tm
0 g
0 Tc
-0.017 Tw
(when analyzing a given system. The reason is that at any time, one deals only with single transitions, not with sets)Tj
0 -1.1 TD
-0.052 Tw
(of transitions. Alternatively, it may be possible to define a non-interleaving semantics, sometimes called true-con-)Tj
T*
0.05 Tw
(currency semantics [1]. The advantage here could be that existing causal dependences are explicitly stated and)Tj
T*
0 Tw
(not buried in the set of all possible interleavings.)Tj
/TT2 1 Tf
11 0 0 11 62.5 682.75 Tm
[(2.4)-811.8(Granularity of state transitions)]TJ
/TT6 1 Tf
10 0 0 10 62.5 659.41 Tm
0.052 Tw
(An important design choice concerns the granularity of)Tj
/TT4 1 Tf
22.745 0 TD
(state transitions)Tj
/TT6 1 Tf
6.47 0 TD
(, i.e. state changes in the underlying se-)Tj
-29.215 -1.1 TD
-0.031 Tw
(mantical model)Tj
8 0 0 8 124.13 652.41 Tm
0 Tw
(1)Tj
10 0 0 10 128.13 648.41 Tm
-0.031 Tw
(. The concept of state transition can be identified both in transition systems as well as in process)Tj
-6.563 -1.1 TD
-0.056 Tw
(algebras that have an operational semantics. On the set of state transitions, a transitive, asymmetrical relation called)Tj
/TT4 1 Tf
T*
-0.005 Tw
(causal dependence relation)Tj
/TT6 1 Tf
11.232 0 TD
(can be defined. This relation captures the degree of concurrency: two state transitions)Tj
-11.232 -1.1 TD
-0.021 Tw
(are called)Tj
/TT4 1 Tf
4.068 0 TD
0 Tw
(concurrent)Tj
/TT6 1 Tf
4.388 0 TD
-0.021 Tw
[( if they are not causally dependent. The causal dependence relation can be represented in dif-)]TJ
-8.456 -1.1 TD
0.006 Tw
(ferent ways. Direct representations exist, for instance, in non-interleaving models, while it is indirectly expressed)Tj
T*
0 Tw
(in interleaving models.)Tj
0.851 -1.1 TD
-0.013 Tw
(Given a particular semantical model, the state transitions of that model are atomic execution units by definition.)Tj
-0.851 -1.1 TD
-0.057 Tw
(However, there are several alternatives of associating state transitions with SDL specifications. For instance, a state)Tj
T*
-0.008 Tw
(transition could correspond to an SDL action \(e.g., task, output, set, call\), some sequence of SDL actions, an SDL)Tj
T*
-0.003 Tw
(transition, or be more or less unrelated to the SDL specification. If state transitions are related to the SDL specifi-)Tj
T*
0.014 Tw
(cation, the causal dependence relation can be established not only in the underlying model, but also on the speci-)Tj
T*
-0.016 Tw
(fication level. We consider this as essential for the intelligibility of SDL specifications, because it is a prerequisite)Tj
T*
-0.033 Tw
(for understanding the specified concurrency. Therefore, we require that state transitions and SDL specifications be)Tj
T*
0 Tw
(related.)Tj
0.851 -1.1 TD
-0.022 Tw
(In the existing SDL semantics, a state transition corresponds to an \(explicit or implicit)Tj
8 0 0 8 412.6 498.41 Tm
0 Tw
(2)Tj
10 0 0 10 416.6 494.41 Tm
-0.022 Tw
(\) SDL)Tj
/TT4 1 Tf
2.679 0 TD
0 Tw
(action)Tj
/TT6 1 Tf
2.728 0 TD
(execution)Tj
8 0 0 8 509.55 498.41 Tm
(3)Tj
10 0 0 10 513.55 494.41 Tm
(.)Tj
-45.105 -1.1 TD
0.056 Tw
(This satisfies our basic requirement that state transitions and SDL specifications be related. Moreover, it means)Tj
T*
0.017 Tw
(that causal dependence is defined between SDL actions. Thus, in order to understand a specification, all possible)Tj
T*
-0.028 Tw
(sequences of SDL)Tj
/TT4 1 Tf
7.444 0 TD
0 Tw
(action)Tj
/TT6 1 Tf
2.722 0 TD
-0.028 Tw
(executions that obey the causal dependence relation have to be taken into account. Alter-)Tj
-10.166 -1.1 TD
0.013 Tw
(natively, a state transition may correspond to an SDL)Tj
/TT4 1 Tf
21.67 0 TD
0 Tw
(transition)Tj
/TT6 1 Tf
3.89 0 TD
0.013 Tw
[( execution, which would also satisfy the basic re-)]TJ
-25.56 -1.1 TD
-0.031 Tw
(quirement stated earlier. Consequently, causal dependence can be established between SDL transitions. In order to)Tj
T*
-0.01 Tw
(understand a specification, all possible sequences of SDL transition executions that satisfy this relation have to be)Tj
T*
0 Tw
(considered.)Tj
0.851 -1.1 TD
-0.05 Tw
(In general, it can be observed that a finer granularity of state transitions increases the specified system behaviour.)Tj
-0.851 -1.1 TD
0.004 Tw
(Thus, their granularity has some impact both on the intelligibility and the analysis of SDL specifications. It is ev-)Tj
T*
0.005 Tw
(ident that in general, it is more difficult to foresee all possible system behaviour, if state transitions correspond to)Tj
T*
-0.031 Tw
(SDL action executions. We note here that it has recently been clarified in the standardization body that the atomic-)Tj
T*
(ity of SDL is on the level of actions rather than on the level of transitions. Since the formal semantics must support)Tj
T*
0 Tw
(SDL exactly as it is currently used, the design decision is predetermined in this case.)Tj
/TT2 1 Tf
11 0 0 11 62.5 327.75 Tm
[(2.5)-811.8(Open Systems)]TJ
/TT6 1 Tf
10 0 0 10 62.5 304.41 Tm
0.017 Tw
(SDL supports the specification of \(topologically\))Tj
/TT4 1 Tf
19.986 0 TD
(open systems)Tj
/TT6 1 Tf
5.266 0 TD
(, i.e. systems that have the ability to communicate)Tj
-25.252 -1.1 TD
-0.016 Tw
(with any environment through a well-defined external interface, as well as the specification of closed systems, i.e.)Tj
T*
-0.006 Tw
(systems without this ability. This language feature enhances the applicability of SDL to system development sub-)Tj
T*
-0.036 Tw
(stantially, since in many cases, a system will be embedded into some pre-existing environment that is not specified)Tj
T*
-0.061 Tw
(nor developed with SDL. For instance, a protocol machine can be specified independently of concrete user modules)Tj
T*
0 Tw
(or some underlying service provider.)Tj
0.851 -1.1 TD
-0.056 Tw
(As noted before, specifications of open systems may be considered incomplete from a formal point of view, since)Tj
-0.851 -1.1 TD
-0.018 Tw
(the environment is not known. From the line arguments w.r.t. language coverage, it follows that no formal seman-)Tj
T*
-0.014 Tw
(tics needs to be associated with these specifications. However, this would mean that in many cases of practical in-)Tj
T*
0.031 Tw
(terest, specifications would not have a unique meaning, and therefore, the general benefits of using FDTs would)Tj
T*
0 Tw
(not apply.)Tj
8 0 0 8 62.5 173.6 Tm
(1.)Tj
10 0 0 10 76.68 169.6 Tm
[(W)79.8(e)0( distinguish between speci)]TJ
/TT7 1 Tf
11.8337 0 TD
()Tj
/TT6 1 Tf
0.5562 0 TD
(ed transitions \(called SDL transitions\) and transitions of the underlying)Tj
-12.3899 -1.1 TD
(model \(called state transitions\).)Tj
8 0 0 8 62.5 147.94 Tm
(2.)Tj
10 0 0 10 76.68 143.94 Tm
[(SDL statements are called implicit if the)11.3(y do not appear in the speci)]TJ
/TT7 1 Tf
28.0346 0 TD
()Tj
/TT6 1 Tf
0.5562 0 TD
[(cation, b)18.1(ut are e)14.4(x)15(ecuted according to)]TJ
-28.5907 -1.1 TD
[(the semantical model. F)13.2(or instance, the beha)18.8(viour of delaying channels is captured by implicit statements.)]TJ
8 0 0 8 62.5 122.27 Tm
(3.)Tj
10 0 0 10 76.68 118.27 Tm
[(In f)10(act, an SDL statement e)13.4(x)15(ecution is related to more than one state transition in some cases \(e.g. in a deci-)]TJ
T*
-0.028 Tw
[(sion, the e)24.5(v)25(aluation of the question may need se)21.9(v)15(eral steps\). Ho)24.7(we)25(v)15(e)0(r)39.9(,)0( this concerns only SDL statements with)]TJ
T*
-0.019 Tw
[(ef)24.9(fects that are local to the SDL process, therefore, the simpli)]TJ
/TT7 1 Tf
24.3315 0 TD
0 Tw
()Tj
/TT6 1 Tf
0.5562 0 TD
-0.019 Tw
[(cation made here does not lead to an)15.3(y inconsist-)]TJ
-24.8877 -1.1 TD
0 Tw
(encies.)Tj
ET
endstream
endobj
14 0 obj
<<
/ProcSet [/PDF /Text ]
/Font <<
/TT2 4 0 R
/TT4 5 0 R
/TT6 6 0 R
/TT7 15 0 R
>>
/ExtGState <<
/GS1 7 0 R
>>
>>
endobj
17 0 obj
<<
/Length 7151
>>
stream
1 g
/GS1 gs
0.06 841.89 595.22 -841.83 re
f
BT
/TT6 1 Tf
10 0 0 10 71.01 739.41 Tm
0 g
0 Tc
0.021 Tw
(To broaden the applicability of SDL as a)Tj
/TT4 1 Tf
16.718 0 TD
0 Tw
(formal)Tj
/TT6 1 Tf
2.667 0 TD
0.021 Tw
[( description technique, it is essential that a precise meaning be)]TJ
-20.236 -1.1 TD
0 Tw
(associated also to specifications of systems that are open in the discussed sense. Openness can be understood as a)Tj
T*
-0.008 Tw
(particular type of incompleteness, so the question arises how a formal semantics could be assigned in this case. In)Tj
T*
0.021 Tw
(order to exhibit the intended behaviour, an open system needs stimuli of the environment. Without these stimuli,)Tj
T*
-0.028 Tw
(only a \(possibly empty\) subset of the intended behaviour can occur. Note that the environment is not known at this)Tj
T*
-0.054 Tw
(point, so the actual stimuli are undetermined. A possible solution would be to define a formal semantics that always)Tj
T*
-0.018 Tw
(takes the influence of all possible environments on the behaviour of the specified open system into account. Tech-)Tj
T*
-0.039 Tw
(nically, this can be achieved by taking, at any point of execution, all stimuli that are legal according to the interface)Tj
T*
0.023 Tw
(definition into account, leading to a maximal set of execution sequences. This set is reduced as soon as the envi-)Tj
T*
0.008 Tw
(ronment is \(partially\) determined, i.e. either by specifying a particular environment or by reducing the set of pos-)Tj
T*
0 Tw
(sible environments through behavioural constraints.)Tj
T*
0.003 Tw
(It should be noted that the existing SDL semantics does not address open systems explicitly, and, as a closer look)Tj
T*
0 Tw
(reveals, also not adequately. The reason is that the possible stimuli of the environment are not taken into account.)Tj
T*
0.01 Tw
(Therefore, the existing semantics covers only the behaviour among the system processes plus signals to the envi-)Tj
T*
0.015 Tw
(ronment, but no behaviour triggered through incoming signals. Therefore, any reasoning that involves communi-)Tj
T*
0 Tw
(cation with the environment lacks a formal basis and must be done informally.)Tj
/TT2 1 Tf
11 0 0 11 62.5 550.75 Tm
[(2.6)-811.8(Compositionality)]TJ
/TT6 1 Tf
10 0 0 10 71.01 527.41 Tm
0.029 Tw
(SDL specifications are composed of different kinds of components, including blocks, processes, services, pro-)Tj
-0.851 -1.1 TD
-0.022 Tw
(cedures, channels and signal routes. For certain such compositions that are syntactically correct and satisfy further)Tj
T*
0.038 Tw
(constraints, a formal semantics is defined. The current SDL semantics is defined for the entire specification, not)Tj
T*
0.029 Tw
(for single components. This means that if, say, a certain process is to be analyzed independently, this is not sup-)Tj
T*
0.047 Tw
(ported by the semantics as this process has no meaning independently of its specification context. To avoid this)Tj
T*
-0.008 Tw
(problem, one could think of a specification reduced to this process only. However, this would be the specification)Tj
T*
-0.019 Tw
(of an open system, as this process has some environment with which it exchanges signals. Therefore, analysis of a)Tj
T*
0 Tw
(single process can currently not be done on a semantical basis, but is pure intuition.)Tj
0.851 -1.1 TD
-0.001 Tw
(The problem would be alleviated by a semantics for open system specifications as discussed before. Also, a so-)Tj
-0.851 -1.1 TD
-0.031 Tw
(lution where a formal semantics is assigned to each of the listed components, and rules are defined how these frag-)Tj
T*
0.014 Tw
(ments may be composed to yield the semantics of an entire specification, is perceivable. Yet a third option exists)Tj
T*
-0.041 Tw
(where open system specifications may be composed on a syntactical level. This would, however, require some lan-)Tj
T*
0 Tw
(guage extensions, which are not under discussion at the moment.)Tj
/TT2 1 Tf
11 0 0 11 62.5 371.75 Tm
[(2.7)-811.8(Time)]TJ
/TT6 1 Tf
10 0 0 10 62.5 348.41 Tm
0.028 Tw
(As it is possible in SDL to explicitly refer to real time and to use timer mechanisms, it is necessary to define the)Tj
T*
-0.048 Tw
(meaning of these constructs formally. Also, real time is used for performance and predictability analysis, therefore,)Tj
T*
0 Tw
(the semantic model must include a precise notion of time.)Tj
0.851 -1.1 TD
-0.025 Tw
(There are many research activities on formal methods for real time computing. This demands for some foresight)Tj
-0.851 -1.1 TD
-0.051 Tw
(when designing a real time semantics for SDL \(which is itself an evolving language especially regarding real time\).)Tj
T*
0.042 Tw
(It would be advantageous to have a semantic time model that supports a wide range of possible syntactical time)Tj
T*
-0.042 Tw
(extensions and validation methods. The question arises whether there exists a time model that encompasses at least)Tj
T*
-0.002 Tw
(some of the proposals currently discussed in the literature. Timing extensions of transition systems usually model)Tj
T*
0.04 Tw
(possible system behaviour as timed state \(or transition\) sequences, which associate system states \(or transitions\))Tj
T*
0.008 Tw
(with time instants or time intervals. Possible timed sequences are specified, e.g., by restricting the times at which)Tj
T*
-0.02 Tw
(state transitions may occur with lower-bound and upper-bound requirements, or each state puts constraints on cer-)Tj
T*
-0.043 Tw
(tain clock values, which allow the automaton to reside in a particular state only as long as these constraints are met.)Tj
T*
0 Tw
(Some dual-language approaches even employ real time temporal logic to specify timing requirements.)Tj
0.851 -1.1 TD
-0.014 Tw
(There exist several validation techniques provided with these time models ranging from automata-theoretic rea-)Tj
-0.851 -1.1 TD
-0.025 Tw
(soning or simulation mappings to model checking. The variety of techniques to cope with timeliness can of course)Tj
T*
0.038 Tw
(be supplemented by queueing and scheduling theory or simulative techniques. However, the problem with these)Tj
T*
0.017 Tw
(approaches lies in the construction of a separate mathematical or computer-executable model, which seems to be)Tj
T*
0 Tw
(solvable by a suitable time semantics.)Tj
0.851 -1.1 TD
0.014 Tw
(A semantic time model generally establishes some mapping between system executions and some kind of time)Tj
-0.851 -1.1 TD
-0.01 Tw
(axis. Thereby, time passage can be modeled either by explicit time passage transitions \(similar to the current SDL)Tj
T*
-0.015 Tw
(approach\), or time passage is strictly bound to normal state transitions, e.g., in terms of delays before or execution)Tj
T*
0.002 Tw
(times for transition firing. The semantic model must be rich enough to allow for different degrees of determinism)Tj
T*
0.018 Tw
(regarding the timing behaviour, i.e., in early phases of system development we expect a rather loose \(resp. unde-)Tj
T*
0.06 Tw
(fined\) mapping between system behaviour and reference time while additional knowledge and design decisions)Tj
T*
0 Tw
(will increasingly determine timing behaviour in later phases \(so that mappings are completed\).)Tj
ET
endstream
endobj
18 0 obj
<<
/ProcSet [/PDF /Text ]
/Font <<
/TT2 4 0 R
/TT4 5 0 R
/TT6 6 0 R
>>
/ExtGState <<
/GS1 7 0 R
>>
>>
endobj
20 0 obj
<<
/Length 10678
>>
stream
1 g
/GS1 gs
0.06 841.89 595.22 -841.83 re
f
BT
/TT6 1 Tf
11 0 0 11 62.5 738.75 Tm
0 g
0 Tc
0 Tw
[(3)-1561.8(OUTLINE OF A NEW FORMAL SDL SEMANTICS)]TJ
10 0 0 10 62.5 713.41 Tm
-0.004 Tw
(Taking the discussion in Section 2 into account, we now give a coarse outline for a new formal SDL semantics. It)Tj
0 -1.1 TD
-0.034 Tw
(is based on the definition of a transition system as the underlying mathematical model. Concurrency is modeled by)Tj
T*
-0.028 Tw
(interleaving, with SDL actions as atomic execution units. The semantics covers open systems, and is composition-)Tj
T*
0 Tw
(al. Time passage is coupled to state transitions.)Tj
/TT2 1 Tf
11 0 0 11 62.5 656.75 Tm
[(3.1)-811.8(Outline by example)]TJ
/TT6 1 Tf
10 0 0 10 71.01 633.4099 Tm
-0.02 Tw
(A transition system is defined by a state set)Tj
/TT4 1 Tf
17.401 0 TD
0 Tw
(St)Tj
/TT6 1 Tf
0.778 0 TD
-0.02 Tw
(, a set of start states)Tj
/TT4 1 Tf
7.961 0 TD
0 Tw
(St)Tj
8 0 0 8 340.19 630.91 Tm
(0)Tj
/TT8 1 Tf
10 0 0 10 346.49 633.4099 Tm
<0085>Tj
/TT4 1 Tf
0.943 0 TD
(St)Tj
/TT6 1 Tf
0.778 0 TD
-0.02 Tw
(, and a state transition relation)Tj
/TT8 1 Tf
12.183 0 TD
0 Tw
<0062>Tj
/TT4 1 Tf
0.494 0 TD
-0.02 Tw
(: St)Tj
/TT8 1 Tf
1.571 0 TD
0 Tw
<0041>Tj
/TT4 1 Tf
-44.368 -1.1 TD
0.042 Tw
(Power \(St\))Tj
/TT6 1 Tf
4.347 0 TD
[( that determines, for each state, the next state set. The formal SDL semantics defines, for each com-)]TJ
-4.347 -1.1 TD
0.007 Tw
(plete SDL specification, one such transition system with a structure that closely corresponds to the SDL specifi-)Tj
T*
-0.018 Tw
(cation structure. Intuitively, an SDL specification determines, at any point in execution, a set of)Tj
/TT4 1 Tf
38.198 0 TD
(active objects)Tj
/TT6 1 Tf
5.453 0 TD
(, i.e.)Tj
-43.651 -1.1 TD
-0.033 Tw
(instances of processes, services, procedures, delaying channels, and)Tj
/TT4 1 Tf
27.059 0 TD
(passive objects)Tj
/TT6 1 Tf
5.994 0 TD
(, i.e. instances of variables. We)Tj
-33.053 -1.1 TD
0 Tw
(include, for reasons of intelligibility and maintainability, instances of block sets, blocks, and process sets.)Tj
0.851 -30.045 TD
0.03 Tw
(An active object is characterized by its state set, the set of its start states, and its actions. Actions have a firing)Tj
-0.851 -1.1 TD
-0.035 Tw
(condition and effects that can be local as well as non-local, e.g., if signals are sent on non-delaying communication)Tj
T*
0.047 Tw
(paths. The structure of a state set depends on the object type. Consider the example shown in Figure 1, where a)Tj
T*
0 Tw
(system of two instances of)Tj
/TT4 1 Tf
10.86 0 TD
(Process1)Tj
/TT6 1 Tf
3.666 0 TD
( is specified. The state set of each of these instances is defined by:)Tj
/TT4 1 Tf
-12.825 -2.4 TD
(St)Tj
8 0 0 8 87.29 218.46 Tm
(Process)Tj
10 0 0 10 112.62 220.96 Tm
( = S)Tj
/TT9 1 Tf
1.925 0 TD
()Tj
/TT4 1 Tf
0.549 0 TD
( Var)Tj
/TT9 1 Tf
2 0 TD
()Tj
/TT4 1 Tf
0.549 0 TD
( InQ)Tj
/TT9 1 Tf
2.055 0 TD
()Tj
/TT4 1 Tf
0.549 0 TD
( Timers)Tj
/TT9 1 Tf
3.278 0 TD
()Tj
/TT4 1 Tf
0.549 0 TD
( Expr)Tj
/TT9 1 Tf
2.444 0 TD
()Tj
/TT4 1 Tf
0.549 0 TD
( Clock)Tj
/TT6 1 Tf
2.583 0 TD
(, where)Tj
-19.207 -1.7 TD
()Tj
/TT4 1 Tf
1.417 0 TD
(S)Tj
/TT6 1 Tf
0.5 0 TD
( is the set of control states \()Tj
/TT4 1 Tf
10.971 0 TD
[(Pr)45(ocess1)]TJ
/TT6 1 Tf
3.621 0 TD
(:)Tj
ET
0 G
0 J 0 j 0.6 w 3.86 M []0 d
1 i
261.22 202.96 m
278.44 202.96 l
B*
BT
10 0 0 10 261.22 203.96 Tm
(start, S\),-)Tj
/TT4 1 Tf
3.944 0 TD
-0.1108 Tc
[(Va)-110.8(r)]TJ
/TT6 1 Tf
1.389 0 TD
0 Tc
[( is the set of v)24.5(ariable v)24.2(alues \()]TJ
/TT4 1 Tf
11.642 0 TD
[(Pr)45(ocess1)]TJ
/TT6 1 Tf
3.621 0 TD
[(: Inte)14.5(ger\),)]TJ
-37.633 -1.3 TD
()Tj
/TT4 1 Tf
1.417 0 TD
(InQ)Tj
/TT6 1 Tf
1.555 0 TD
( is the set of input queue contents \()Tj
/TT4 1 Tf
13.943 0 TD
[(Pr)45(ocess1)]TJ
/TT6 1 Tf
3.621 0 TD
(: {A})Tj
8 0 0 8 318.31 194.96 Tm
(*)Tj
10 0 0 10 322.31 190.96 Tm
(\),)Tj
-23.146 -1.3 TD
()Tj
/TT4 1 Tf
1.417 0 TD
[(T)55.2(imer)10(s)]TJ
/TT6 1 Tf
2.713 0 TD
( is the set of timer states \()Tj
/TT4 1 Tf
10.249 0 TD
[(Pr)45(ocess1)]TJ
/TT6 1 Tf
3.621 0 TD
(:)Tj
/TT8 1 Tf
0.528 0 TD
<0092>Tj
/TT6 1 Tf
0.823 0 TD
(\),)Tj
-19.351 -1.3 TD
()Tj
/TT4 1 Tf
1.417 0 TD
(Expr)Tj
/TT6 1 Tf
1.944 0 TD
[( is the set of v)24.5(alues of prede)]TJ
/TT7 1 Tf
11.1664 0 TD
()Tj
/TT6 1 Tf
0.5562 0 TD
[(ned e)14.2(xpressions \(e.g., SELF\),)]TJ
-15.0836 -1.3 TD
()Tj
/TT4 1 Tf
1.417 0 TD
[(Cloc)19.7(k)]TJ
/TT6 1 Tf
2.313 0 TD
[( is the set of process time v)23.9(alues.)]TJ
-5.714 -2.6 TD
-0.057 Tw
(Thus, the state set of)Tj
/TT4 1 Tf
8.213 0 TD
0 Tw
(System1)Tj
/TT6 1 Tf
3.277 0 TD
-0.057 Tw
[( is defined by)]TJ
8 0 0 8 238.35 129.96 Tm
0 Tw
(4)Tj
/TT4 1 Tf
10 0 0 10 244.28 125.96 Tm
-0.057 Tw
(St = St)Tj
8 0 0 8 270.45 123.46 Tm
0 Tw
(Process1)Tj
/TT9 1 Tf
10 0 0 10 301.7 125.96 Tm
()Tj
/TT4 1 Tf
0.55 0 TD
-0.057 Tw
[( St)]TJ
8 0 0 8 316.9 123.46 Tm
0 Tw
(Process1)Tj
/TT6 1 Tf
10 0 0 10 346.23 125.96 Tm
-0.057 Tw
(. The set of start states of a process instance)Tj
-28.373 -1.1 TD
0.039 Tw
(is determined by an action of the creating object instance, which in this example is an object of type process set)Tj
8 0 0 8 62.5 89.27 Tm
0 Tw
(4.)Tj
10 0 0 10 76.68 85.27 Tm
[(W)79.8(e)0( simplify in this e)13.8(xample by ne)14.2(glecting instances of block sets, blocks, process sets, and v)23.1(ariables.)]TJ
/TT11 1 Tf
2.725 45.179 TD
(System)Tj
/TT13 1 Tf
3.889 0 TD
(System1)Tj
ET
1 g
287.98 552.29 m
98.69 552.29 l
B*
287.98 469.13 m
287.98 552.29 l
B*
98.69 469.13 m
287.98 469.13 l
B*
98.69 552.29 m
98.69 469.13 l
B*
270.91 524.25 m
221.65 524.25 l
B*
275.98 517.09 m
270.94 524.25 l
B*
275.98 506.34 m
275.98 517.09 l
B*
221.65 506.34 m
275.98 506.34 l
B*
221.65 524.25 m
221.65 506.34 l
B*
270.94 517.09 m
270.94 524.25 l
B*
275.98 517.09 m
270.94 517.09 l
B*
BT
/TT11 1 Tf
10 0 0 10 224.99 511.35 Tm
0 g
(Signal A;)Tj
ET
1 g
149.12 524.53 60.51 -35.81 re
f
149.12 524.53 60.51 -35.81 re
S
BT
/TT13 1 Tf
10 0 0 10 163.7 503.72 Tm
0 g
(Block1)Tj
ET
98.69 506.63 m
149.12 506.63 l
98.69 506.63 m
101.72 503.94 l
101.72 509.31 m
98.69 506.63 l
149.12 506.63 m
146.09 509.31 l
146.09 503.94 m
149.12 506.63 l
S
BT
/TT11 1 Tf
10 0 0 10 118.86 513.17 Tm
(C1)Tj
-1.512 -1.666 TD
(A)Tj
ET
101.72 503.94 m
103.74 503.94 l
101.72 494.81 m
101.72 503.94 l
103.74 494.81 m
101.72 494.81 l
114.22 503.94 m
112.21 503.94 l
114.22 494.81 m
114.22 503.94 l
112.21 494.81 m
114.22 494.81 l
S
BT
10 0 0 10 133.99 496.51 Tm
(A)Tj
ET
131.97 503.94 m
133.99 503.94 l
131.97 494.81 m
131.97 503.94 l
133.99 494.81 m
131.97 494.81 l
144.48 503.94 m
142.46 503.94 l
144.48 494.81 m
144.48 503.94 l
142.46 494.81 m
144.48 494.81 l
S
1 g
118.17 416.06 48.81 -7.52 re
f
BT
10 0 0 10 105.55 403.94 Tm
0 g
(Block)Tj
/TT13 1 Tf
3.001 0 TD
(Block1)Tj
ET
1 g
99.38 419.21 m
285.95 419.21 l
B*
99.38 336.65 m
99.38 419.21 l
B*
285.95 336.65 m
99.38 336.65 l
B*
285.95 419.21 m
285.95 336.65 l
B*
164.93 392.35 60.51 -35.81 re
f
170.99 392.35 m
219.39 392.35 l
B*
164.93 386.98 m
170.99 392.35 l
B*
164.93 361.91 m
164.93 386.98 l
B*
170.99 356.54 m
164.93 361.91 l
B*
219.39 356.54 m
170.99 356.54 l
B*
225.44 361.91 m
219.39 356.54 l
B*
225.44 386.98 m
225.44 361.91 l
B*
219.39 392.35 m
225.44 386.98 l
B*
BT
10 0 0 10 166.46 370.95 Tm
0 g
(Process1\(2\))Tj
/TT11 1 Tf
12.184 0.108 TD
(C1)Tj
ET
1 g
285.95 374.45 m
225.44 374.45 l
B*
285.95 374.45 m
282.92 371.76 l
B*
282.92 377.13 m
285.95 374.45 l
B*
225.44 374.45 m
228.47 377.13 l
B*
228.47 371.76 m
225.44 374.45 l
B*
BT
10 0 0 10 241.29 380.98 Tm
0 g
(SR1)Tj
3.295 -1.665 TD
(A)Tj
ET
1 g
282.92 371.76 m
280.91 371.76 l
B*
282.92 362.63 m
282.92 371.76 l
B*
280.91 362.63 m
282.92 362.63 l
B*
270.42 371.76 m
272.44 371.76 l
B*
270.42 362.63 m
270.42 371.76 l
B*
272.44 362.63 m
270.42 362.63 l
B*
BT
10 0 0 10 233.9 364.33 Tm
0 g
(A)Tj
ET
1 g
242.59 371.76 m
240.57 371.76 l
B*
242.59 362.63 m
242.59 371.76 l
B*
240.57 362.63 m
242.59 362.63 l
B*
230.08 371.76 m
232.1 371.76 l
B*
230.08 362.63 m
230.08 371.76 l
B*
232.1 362.63 m
230.08 362.63 l
B*
BT
10 0 0 10 338.85 538.44 Tm
0 g
(Process)Tj
/TT13 1 Tf
3.89 0 TD
(Process1)Tj
/TT11 1 Tf
4.168 0 TD
( \(2\))Tj
ET
1 g
499.96 551.57 m
334.57 551.57 l
B*
499.96 336.69 m
499.96 551.57 l
B*
334.57 336.69 m
499.96 336.69 l
B*
334.57 551.57 m
334.57 336.69 l
B*
479.94 526.5 m
419.41 526.5 l
B*
485.04 519.33 m
479.99 526.5 l
B*
485.04 508.59 m
485.04 519.33 l
B*
419.41 508.59 m
485.04 508.59 l
B*
419.41 526.5 m
419.41 508.59 l
B*
479.99 519.33 m
479.99 526.47 l
B*
485.04 519.33 m
479.99 519.33 l
B*
BT
10 0 0 10 421.93 513.28 Tm
0 g
(Dcl x integer;)Tj
ET
1 g
362.81 526.5 40.34 -17.91 re
f
393.06 526.5 m
372.89 526.5 l
B*
393.06 508.59 m
372.89 508.59 l
B*
393.06 508.59 m
398.624 508.59 403.14 512.6 403.14 517.54 c
403.14 522.48 398.624 526.49 393.06 526.49 c
372.89 526.49 m
367.326 526.49 362.81 522.48 362.81 517.54 c
362.81 512.6 367.326 508.59 372.89 508.59 c
S
362.81 499.64 40.34 -17.91 re
f
362.81 499.64 40.34 -17.91 re
S
362.81 472.78 40.34 -17.91 re
f
400.32 472.78 m
365.63 472.78 l
B*
400.32 454.87 m
365.63 454.87 l
B*
365.512 472.785 m
363.742 470.062 362.81 466.974 362.81 463.83 c
362.81 460.686 363.742 457.598 365.512 454.875 c
400.448 454.875 m
402.218 457.598 403.15 460.686 403.15 463.83 c
403.15 466.974 402.218 470.062 400.448 472.785 c
S
362.81 445.92 40.34 -17.91 re
f
403.15 445.92 m
362.81 445.92 l
B*
393.06 436.97 m
403.15 445.92 l
B*
403.15 428.01 m
393.06 436.97 l
B*
362.81 428.01 m
403.15 428.01 l
B*
362.81 445.92 m
362.81 428.01 l
B*
362.81 419.06 40.34 -17.91 re
f
362.81 419.06 40.34 -17.91 re
S
362.81 392.2 40.34 -17.9 re
f
393.06 392.2 m
362.81 392.2 l
B*
403.15 383.25 m
393.06 392.2 l
B*
393.06 374.3 m
403.15 383.25 l
B*
362.81 374.3 m
393.06 374.3 l
B*
362.81 392.2 m
362.81 374.3 l
B*
362.81 365.34 40.34 -17.9 re
f
400.32 365.34 m
365.63 365.34 l
B*
400.32 347.44 m
365.63 347.44 l
B*
365.512 365.345 m
363.742 362.622 362.81 359.534 362.81 356.39 c
362.81 353.246 363.742 350.158 365.512 347.435 c
400.448 347.435 m
402.218 350.158 403.15 353.246 403.15 356.39 c
403.15 359.534 402.218 362.622 400.448 365.345 c
S
BT
10 0 0 10 369.21 486.73 Tm
0 g
(x := 5)Tj
1.066 -2.686 TD
(S)Tj
-0.049 -2.765 TD
(A)Tj
-1.307 -2.488 TD
(x := x+1)Tj
1.346 -2.776 TD
(A)Tj
0.01 -2.754 TD
(S)Tj
ET
382.98 499.64 m
382.98 508.59 l
382.98 472.78 m
382.98 481.73 l
382.98 472.78 m
386 475.47 l
379.95 475.47 m
382.98 472.78 l
382.98 445.92 m
382.98 454.87 l
382.98 419.06 m
382.98 428.01 l
382.98 392.2 m
382.98 401.16 l
382.98 365.34 m
382.98 374.3 l
382.98 365.34 m
386 368.03 l
379.95 368.03 m
382.98 365.34 l
S
BT
/TT2 1 Tf
10 0 0 10 84.47 307.51 Tm
(Figure 1)Tj
/TT6 1 Tf
3.583 0 TD
(: Example of an SDL system speci)Tj
/TT7 1 Tf
13.8306 0 TD
()Tj
/TT6 1 Tf
0.5562 0 TD
(cation)Tj
ET
endstream
endobj
21 0 obj
<<
/ProcSet [/PDF /Text ]
/Font <<
/TT2 4 0 R
/TT4 5 0 R
/TT6 6 0 R
/TT7 15 0 R
/TT8 22 0 R
/TT9 23 0 R
/TT11 24 0 R
/TT13 25 0 R
>>
/ExtGState <<
/GS1 7 0 R
>>
>>
endobj
27 0 obj
<<
/Length 5987
>>
stream
1 g
/GS1 gs
0.06 841.89 595.22 -841.83 re
f
BT
/TT6 1 Tf
10 0 0 10 62.5 739.41 Tm
0 g
0 Tc
-0.048 Tw
(\(not shown here\). Similar actions are associated with with instances of block sets and blocks, yielding the start con-)Tj
0 -1.1 TD
0 Tw
(figuration of)Tj
/TT4 1 Tf
5.277 0 TD
(System1)Tj
/TT6 1 Tf
3.277 0 TD
(.)Tj
-7.703 -61.85 TD
-0.057 Tw
(In order to define the state transition relation)Tj
/TT8 1 Tf
12 0 0 12 247.53 109.91 Tm
0 Tw
<0062>Tj
/TT6 1 Tf
10 0 0 10 253.46 109.91 Tm
-0.057 Tw
(, we apply the formalism of attribute grammars. Note that for SDL,)Tj
-19.096 -1.1 TD
-0.021 Tw
(several grammars are defined in the standard: the concrete graphical grammar \(used in Figure 1\), the concrete tex-)Tj
T*
-0.042 Tw
(tual grammar, and the abstract grammar. The SDL standard defines how to transform an SDL specification into the)Tj
1.069 60.82 TD
0 Tw
(Process-definition)Tj
1.417 -1.1 TD
(Process-name)Tj
/TT4 1 Tf
1.418 -1.1 TD
(Process1)Tj
/TT6 1 Tf
-1.418 -1.1 TD
(Number-of-instances)Tj
/TT15 1 Tf
T*
(initialNumberOfInstances = 2)Tj
0 -1.3 TD
(maxNumberOfInstances)Tj
/TT4 1 Tf
10.167 0 TD
( =)Tj
/TT8 1 Tf
1.175 0 TD
<0027>Tj
/TT6 1 Tf
-9.924 -1.3 TD
(2)Tj
-1.418 -1.1 TD
(Variable-definition-)Tj
/TT2 1 Tf
7.998 0 TD
(set)Tj
/TT15 1 Tf
-7.998 -1.1 TD
(varNames)Tj
/TT4 1 Tf
4.166 0 TD
( = {x})Tj
/TT6 1 Tf
-2.748 -1.1 TD
(Variable-name)Tj
1.417 -1.1 TD
(x)Tj
-2.835 -1.1 TD
(Process-graph)Tj
/TT15 1 Tf
T*
(major states)Tj
/TT4 1 Tf
5.223 0 TD
(= {)Tj
ET
0 G
0 J 0 j 0.6 w 3.86 M []0 d
1 i
152.84 559.11 m
171.18 559.11 l
B*
BT
10 0 0 10 152.84 560.11 Tm
(start, S})Tj
/TT15 1 Tf
-6.548 -1.3 TD
(minor states)Tj
/TT4 1 Tf
5.279 0 TD
(= {s1, s2})Tj
/TT6 1 Tf
-3.861 -1.3 TD
(Process-start-node)Tj
1.417 -1.1 TD
(Transition)Tj
1.417 -1.1 TD
(Graph-node *)Tj
ET
144.06 500.11 m
186.27 500.11 l
B*
BT
10 0 0 10 144.06 501.11 Tm
(Task-node)Tj
/TT15 1 Tf
T*
(Pre)Tj
/TT4 1 Tf
1.444 0 TD
( = \(obj.st.s =)Tj
ET
213.67 489.11 m
232.01 489.11 l
B*
BT
10 0 0 10 213.67 490.11 Tm
(start\))Tj
/TT15 1 Tf
-6.961 -1.2 TD
(Eff)Tj
/TT4 1 Tf
1.583 0 TD
(= \(assign \(obj,x,val\(5\)\); obj.st.s := S\))Tj
/TT6 1 Tf
-0.166 -1.2 TD
(x := 5)Tj
-2.835 -1.1 TD
(Terminator)Tj
1.418 -1.1 TD
(S)Tj
-4.252 -1.1 TD
(State-node-)Tj
/TT2 1 Tf
4.61 0 TD
(set)Tj
/TT6 1 Tf
-3.193 -1.1 TD
(S)Tj
T*
(Input-node-)Tj
/TT2 1 Tf
4.721 0 TD
(set)Tj
ET
129.88 399.11 m
173.76 399.11 l
B*
BT
/TT6 1 Tf
10 0 0 10 129.88 400.11 Tm
(Input-node)Tj
/TT15 1 Tf
0 -1.1 TD
(Pre)Tj
/TT4 1 Tf
1.444 0 TD
( = \(obj.st.s = S)Tj
/TT8 1 Tf
6.267 0 TD
<008e>Tj
/TT4 1 Tf
0.603 0 TD
( first\(obj.st.inQ\).sigType = A\))Tj
/TT15 1 Tf
-8.314 -1.2 TD
(Eff)Tj
/TT4 1 Tf
1.583 0 TD
(= \(obj.st.expr.sender := first\(obj.st.inQ\).sender;)Tj
0.835 -1.2 TD
(remove\(obj.st.inQ\); obj.st.s := s1\))Tj
/TT6 1 Tf
-1 -1.2 TD
(Signal-identifier)Tj
1.417 -1.1 TD
(A)Tj
-1.417 -1.1 TD
(Transition)Tj
1.417 -1.1 TD
(Graph-node *)Tj
ET
172.4 308.11 m
214.61 308.11 l
B*
BT
10 0 0 10 172.4 309.11 Tm
(Task-node)Tj
/TT15 1 Tf
T*
(Pre)Tj
/TT4 1 Tf
1.444 0 TD
( = \(obj.st.s = s1\))Tj
/TT15 1 Tf
-1.444 -1.2 TD
(Eff)Tj
/TT4 1 Tf
1.583 0 TD
(= \(assign \(obj,x,val\(x+1\)\); obj.st.s := s2\))Tj
/TT6 1 Tf
-0.165 -1.2 TD
(x := x+ 1)Tj
ET
172.4 262.11 m
222.95 262.11 l
B*
BT
10 0 0 10 172.4 263.11 Tm
(Output-node)Tj
/TT15 1 Tf
0 -1.1 TD
(sigDest)Tj
0 -1.2 TD
(Pre)Tj
/TT4 1 Tf
1.444 0 TD
( = \(obj.st.s = s2\))Tj
/TT15 1 Tf
-1.444 -1.2 TD
(Eff)Tj
/TT4 1 Tf
1.583 0 TD
(= \()Tj
/TT8 1 Tf
1.258 0 TD
<0099>Tj
/TT4 1 Tf
0.713 0 TD
(obj)Tj
/TT9 1 Tf
1.611 0 TD
( )Tj
/TT8 1 Tf
0.25 0 TD
<0044>Tj
/TT4 1 Tf
0.713 0 TD
( receivers \(A,obj.st.expr.self,)Tj
/TT15 1 Tf
11.47 0 TD
(sigDest)Tj
/TT4 1 Tf
3 0 TD
(\).)Tj
-16.346 -1.2 TD
(obj.st.inQ := add\(obj.st.inQ,)Tj
2.835 -1.2 TD
( \(A,obj.st.expr.self\)\); obj.st.s := S\))Tj
/TT6 1 Tf
-5.669 -1.2 TD
(A)Tj
-2.835 -1.1 TD
(Terminator)Tj
1.417 -1.1 TD
(S)Tj
/TT2 1 Tf
-9.921 -2.9 TD
(Figure 2)Tj
/TT6 1 Tf
3.583 0 TD
[(: Excerpt of the Abstract Syntax T)33.3(ree with Attrib)19.2(utes: Process-de)]TJ
/TT7 1 Tf
26.0237 0 TD
()Tj
/TT6 1 Tf
0.5562 0 TD
(nition)Tj
ET
1 g
423.78 550.69 60.51 -26.86 re
f
469.16 550.69 m
438.91 550.69 l
B*
469.16 523.83 m
438.91 523.83 l
B*
469.16 523.83 m
477.512 523.83 484.29 529.847 484.29 537.26 c
484.29 544.673 477.512 550.69 469.16 550.69 c
438.91 550.69 m
430.558 550.69 423.78 544.673 423.78 537.26 c
423.78 529.847 430.558 523.83 438.91 523.83 c
424.34 513.18 60.5 -26.86 re
S
423.9 460.37 60.51 -26.86 re
f
480.18 460.37 m
428.14 460.37 l
B*
480.18 433.51 m
428.14 433.51 l
B*
427.963 460.37 m
425.308 456.287 423.91 451.655 423.91 446.94 c
423.91 442.225 425.308 437.593 427.963 433.51 c
480.357 433.51 m
483.012 437.593 484.41 442.225 484.41 446.94 c
484.41 451.655 483.012 456.287 480.357 460.37 c
S
423.9 414 60.51 -26.86 re
f
484.41 414 m
423.9 414 l
B*
469.29 400.57 m
484.41 414 l
B*
484.41 387.14 m
469.29 400.57 l
B*
423.9 387.14 m
484.41 387.14 l
B*
423.9 414 m
423.9 387.14 l
B*
423.11 323.54 60.51 -26.86 re
S
423.45 277.42 60.5 -26.86 re
f
468.83 277.42 m
423.45 277.42 l
B*
483.95 263.99 m
468.83 277.42 l
B*
468.83 250.56 m
483.95 263.99 l
B*
423.45 250.56 m
468.83 250.56 l
B*
423.45 277.42 m
423.45 250.56 l
B*
422.78 182.21 60.51 -26.86 re
f
479.05 182.21 m
427.02 182.21 l
B*
479.05 155.35 m
427.02 155.35 l
B*
426.833 182.21 m
424.178 178.127 422.78 173.495 422.78 168.78 c
422.78 164.065 424.178 159.433 426.833 155.35 c
479.227 155.35 m
481.882 159.433 483.28 164.065 483.28 168.78 c
483.28 173.495 481.882 178.127 479.227 182.21 c
S
BT
/TT11 1 Tf
10 0 0 10 440.55 497.27 Tm
0 g
(x := 5)Tj
0.895 -5.499 TD
(S)Tj
-0.073 -4.531 TD
(A)Tj
-1.574 -9.007 TD
(x := x+1)Tj
1.586 -4.713 TD
(A)Tj
-0.019 -9.39 TD
(S)Tj
ET
453.28 513.18 m
453.28 523.83 l
453.41 460.59 m
453.41 486.37 l
453.41 460.37 m
457.95 464.4 l
448.87 464.4 m
453.41 460.37 l
453.39 414.34 m
453.39 433.18 l
453.37 323.93 m
453.37 386.89 l
452.55 277.68 m
452.55 297.18 l
453.01 181.93 m
453.01 250.31 l
453.03 182.21 m
457.57 186.24 l
448.5 186.24 m
453.03 182.21 l
S
endstream
endobj
28 0 obj
<<
/ProcSet [/PDF /Text ]
/Font <<
/TT2 4 0 R
/TT4 5 0 R
/TT6 6 0 R
/TT7 15 0 R
/TT8 22 0 R
/TT9 23 0 R
/TT11 24 0 R
/TT15 29 0 R
>>
/ExtGState <<
/GS1 7 0 R
>>
>>
endobj
31 0 obj
<<
/Length 10096
>>
stream
1 g
/GS1 gs
0.06 841.89 595.22 -841.83 re
f
BT
/TT6 1 Tf
10 0 0 10 62.5 739.41 Tm
0 g
0 Tc
-0.026 Tw
(corresponding abstract syntax representation. Since this representation is more suitable than the concrete form, we)Tj
0 -1.1 TD
0 Tw
(use it as a starting point for assigning a formal semantics to SDL specifications.)Tj
0.851 -1.1 TD
-0.052 Tw
(In Figure 2, an excerpt of the abstract syntax tree \(AST\) of)Tj
/TT4 1 Tf
23.116 0 TD
0 Tw
(System1)Tj
/TT6 1 Tf
3.277 0 TD
-0.052 Tw
[( is listed. With some of its nodes, we associate)]TJ
-27.244 -1.1 TD
-0.036 Tw
(attributes that can be formalized by evaluation rules of a suitable attribute grammar. For instance, the attribute)Tj
/TT15 1 Tf
43.689 0 TD
0 Tw
(var-)Tj
-43.689 -1.1 TD
(Names)Tj
/TT6 1 Tf
2.833 0 TD
0.04 Tw
[( denotes the set of variables that are declared in)]TJ
/TT4 1 Tf
19.618 0 TD
0 Tw
(Process1)Tj
/TT6 1 Tf
3.666 0 TD
0.04 Tw
(. Using these attributes, further attributes called)Tj
/TT15 1 Tf
-26.117 -1.1 TD
0 Tw
(Pre)Tj
/TT6 1 Tf
1.444 0 TD
-0.022 Tw
[( and)]TJ
/TT15 1 Tf
1.901 0 TD
0 Tw
(Eff)Tj
/TT6 1 Tf
1.333 0 TD
-0.022 Tw
[( are derived for designated nodes, such that each pair of such attributes defines an action. For instance,)]TJ
-4.678 -1.1 TD
-0.019 Tw
(the attribute)Tj
/TT15 1 Tf
5.016 0 TD
0 Tw
(Pre)Tj
/TT6 1 Tf
1.444 0 TD
-0.019 Tw
[( associated with)]TJ
ET
0 G
0 J 0 j 0.6 w 3.86 M []0 d
1 i
192.9 672.41 m
236.78 672.41 l
B*
BT
10 0 0 10 192.9 673.41 Tm
(Input-node, when interpreted in the context of an active object)Tj
/TT4 1 Tf
24.994 0 TD
0 Tw
(obj)Tj
/TT6 1 Tf
1.278 0 TD
-0.019 Tw
(, expresses that)Tj
-39.312 -1.1 TD
0.022 Tw
(the control state)Tj
/TT4 1 Tf
6.703 0 TD
0 Tw
(s)Tj
/TT6 1 Tf
0.389 0 TD
0.022 Tw
[( of)]TJ
/TT4 1 Tf
1.376 0 TD
0 Tw
(obj)Tj
/TT6 1 Tf
1.278 0 TD
0.022 Tw
(s state component)Tj
/TT4 1 Tf
7.814 0 TD
0 Tw
(st)Tj
/TT6 1 Tf
0.667 0 TD
0.022 Tw
[( is)]TJ
/TT4 1 Tf
1.21 0 TD
0 Tw
(S)Tj
/TT6 1 Tf
0.5 0 TD
0.022 Tw
(, that the input queue)Tj
/TT4 1 Tf
8.773 0 TD
0 Tw
(inQ)Tj
/TT6 1 Tf
1.5 0 TD
0.022 Tw
[( is not empty, and that the signal type)]TJ
-30.21 -1.1 TD
0.013 Tw
(of the first signal of the)Tj
/TT4 1 Tf
9.686 0 TD
0 Tw
(inQ)Tj
/TT6 1 Tf
1.5 0 TD
0.013 Tw
[( is)]TJ
/TT4 1 Tf
1.193 0 TD
0 Tw
(A)Tj
/TT6 1 Tf
0.611 0 TD
0.013 Tw
(. The attribute)Tj
/TT15 1 Tf
5.925 0 TD
0 Tw
(Eff)Tj
/TT6 1 Tf
1.333 0 TD
0.013 Tw
(, when interpreted in the context of)Tj
/TT4 1 Tf
14.364 0 TD
0 Tw
(obj)Tj
/TT6 1 Tf
1.278 0 TD
0.013 Tw
(, expresses that the pre-)Tj
-35.89 -1.1 TD
0.026 Tw
(defined expression)Tj
/TT4 1 Tf
7.829 0 TD
0 Tw
(sender)Tj
/TT6 1 Tf
2.666 0 TD
0.026 Tw
[( is assigned a certain value, that the first signal is removed from)]TJ
/TT4 1 Tf
26.116 0 TD
0 Tw
(inQ)Tj
/TT6 1 Tf
1.5 0 TD
0.026 Tw
(, and that the next)Tj
-38.111 -1.1 TD
0 Tw
(control state is)Tj
/TT4 1 Tf
6.083 0 TD
(s1)Tj
/TT6 1 Tf
0.889 0 TD
(.)Tj
-6.121 -1.1 TD
(With these preparations, we can now define the next state relation)Tj
/TT8 1 Tf
12 0 0 12 337.06 618.4099 Tm
<0062>Tj
/TT6 1 Tf
10 0 0 10 342.98 618.4099 Tm
( of)Tj
/TT4 1 Tf
1.334 0 TD
(System1)Tj
/TT6 1 Tf
3.276 0 TD
( as follows:)Tj
/TT8 1 Tf
-30.39 -2.3 TD
<0099>Tj
/TT4 1 Tf
0.713 0 TD
(st)Tj
/TT8 1 Tf
1.25 0 TD
<0044>Tj
/TT4 1 Tf
0.713 0 TD
( St.)Tj
/TT8 1 Tf
1.528 0 TD
<0062>Tj
/TT4 1 Tf
0.494 0 TD
(\(st\) = {st)Tj
/TT9 1 Tf
4.464 0 TD
( )Tj
/TT8 1 Tf
0.25 0 TD
<0044>Tj
/TT4 1 Tf
0.713 0 TD
( St |)Tj
/TT8 1 Tf
2.053 0 TD
<009a>Tj
/TT4 1 Tf
0.549 0 TD
(a)Tj
/TT8 1 Tf
0.75 0 TD
<0044>Tj
/TT15 1 Tf
0.963 0 TD
(A)Tj
/TT4 1 Tf
8 0 0 8 236.25 592.9099 Tm
(obj1)Tj
/TT8 1 Tf
10 0 0 10 252.48 595.41 Tm
<0046>Tj
/TT15 1 Tf
1.017 0 TD
(A)Tj
/TT4 1 Tf
8 0 0 8 269.33 592.9099 Tm
(obj2)Tj
10 0 0 10 283.55 595.41 Tm
(. \(st)Tj
/TT8 1 Tf
2.083 0 TD
<0044>Tj
/TT4 1 Tf
0.713 0 TD
( a.)Tj
/TT15 1 Tf
1 0 TD
(Pre)Tj
/TT8 1 Tf
1.694 0 TD
<008e>Tj
/TT4 1 Tf
0.603 0 TD
( \(st,st\))Tj
/TT8 1 Tf
3.639 0 TD
<0044>Tj
/TT4 1 Tf
0.713 0 TD
( a.)Tj
/TT15 1 Tf
1 0 TD
[(Ef)18(f)]TJ
/TT4 1 Tf
1.315 0 TD
(\)},)Tj
/TT6 1 Tf
1.233 0 TD
(where)Tj
-32.696 -1.7 TD
()Tj
/TT15 1 Tf
1.417 0 TD
(A)Tj
/TT4 1 Tf
8 0 0 8 117.36 575.91 Tm
(obj)Tj
/TT6 1 Tf
10 0 0 10 127.59 578.41 Tm
( = {\()Tj
/TT15 1 Tf
1.877 0 TD
(Pre)Tj
/TT6 1 Tf
1.444 0 TD
(,)Tj
/TT15 1 Tf
0.25 0 TD
[(Ef)18(f)]TJ
/TT6 1 Tf
1.315 0 TD
(\) |)Tj
/TT8 1 Tf
1.033 0 TD
<009a>Tj
/TT6 1 Tf
0.549 0 TD
( node)Tj
/TT8 1 Tf
2.444 0 TD
<0044>Tj
/TT6 1 Tf
0.713 0 TD
( nodeSet\()Tj
/TT4 1 Tf
3.805 0 TD
[(Pr)45(ocess1)]TJ
/TT6 1 Tf
3.621 0 TD
(\).)Tj
/TT15 1 Tf
0.833 0 TD
(Pre)Tj
/TT6 1 Tf
1.444 0 TD
( = node.)Tj
/TT15 1 Tf
3.258 0 TD
(Pre)Tj
/TT6 1 Tf
1.444 0 TD
( and)Tj
/TT15 1 Tf
1.944 0 TD
[(Ef)18(f)]TJ
/TT6 1 Tf
1.315 0 TD
( = node.)Tj
/TT15 1 Tf
3.258 0 TD
[(Ef)18(f)]TJ
/TT6 1 Tf
1.315 0 TD
(}\))Tj
-37.52 -2.583 TD
0.008 Tw
(Informally, for each state)Tj
/TT4 1 Tf
10.39 0 TD
0 Tw
(st)Tj
/TT6 1 Tf
1 0 TD
0.008 Tw
[( of)]TJ
/TT4 1 Tf
1.35 0 TD
0 Tw
(St)Tj
/TT6 1 Tf
0.778 0 TD
0.008 Tw
(, the next states are the states)Tj
/TT4 1 Tf
11.888 0 TD
0 Tw
(st)Tj
/TT6 1 Tf
1.481 0 TD
0.008 Tw
(that are reachable from)Tj
/TT4 1 Tf
9.529 0 TD
0 Tw
(st)Tj
/TT6 1 Tf
1 0 TD
0.008 Tw
[( by some action)]TJ
/TT4 1 Tf
6.588 0 TD
0 Tw
(a)Tj
/TT6 1 Tf
-44.855 -1.1 TD
-0.012 Tw
(of an active object. Thereby, the attributes)Tj
/TT15 1 Tf
17.049 0 TD
0 Tw
(Pre)Tj
/TT6 1 Tf
1.444 0 TD
-0.012 Tw
[( and)]TJ
/TT15 1 Tf
1.919 0 TD
0 Tw
(Eff)Tj
/TT6 1 Tf
1.333 0 TD
-0.012 Tw
[( become relations on the state set)]TJ
/TT4 1 Tf
13.383 0 TD
0 Tw
(St)Tj
/TT6 1 Tf
0.778 0 TD
-0.012 Tw
[( when interpreted in the)]TJ
-35.906 -1.1 TD
0.016 Tw
(context of an active object:)Tj
/TT15 1 Tf
11.159 0 TD
0 Tw
(Pre)Tj
/TT6 1 Tf
1.444 0 TD
0.016 Tw
[( determines the firing condition, i.e. the constraint under which the action may be)]TJ
-12.603 -1.1 TD
-0.008 Tw
(selected for execution.)Tj
/TT15 1 Tf
9.251 0 TD
0 Tw
(Eff)Tj
/TT6 1 Tf
1.333 0 TD
-0.008 Tw
[( defines the effects of the action on the system state. By writing)-245.3(nodeSet\()]TJ
/TT4 1 Tf
29.114 0 TD
0 Tw
(Process1)Tj
/TT6 1 Tf
3.666 0 TD
-0.008 Tw
(\), we)Tj
-43.364 -1.1 TD
-0.039 Tw
(refer to certain nodes of the abstract syntax tree where actions that belong to each instance of)Tj
/TT4 1 Tf
36.797 0 TD
0 Tw
(Process1)Tj
/TT6 1 Tf
3.666 0 TD
-0.039 Tw
[( are defined.)]TJ
/TT2 1 Tf
11 0 0 11 62.5 484.91 Tm
0 Tw
[(3.2)-811.8(Open systems)]TJ
/TT6 1 Tf
10 0 0 10 71.01 461.58 Tm
-0.042 Tw
(Next, we outline how the semantics of open systems can be defined. As noted before \(see Section 2.5\), a solution)Tj
-0.851 -1.1 TD
-0.054 Tw
(would be to define a formal semantics that always takes the influence of all possible environments on the behaviour)Tj
T*
0.01 Tw
(of the specified open system into account. Technically, this can be expressed by adding an environment action to)Tj
T*
0.008 Tw
(the transition system, as shown in Figure 3: every time this action is executed, some signal from the environment)Tj
T*
-0.028 Tw
(enters the system and is appended to the input queues of some set of receivers, according to the addressing scheme)Tj
T*
0 Tw
(used in the output-statement.)Tj
/TT2 1 Tf
11 0 0 11 62.5 199 Tm
[(3.3)-811.8(Generalization)]TJ
/TT6 1 Tf
10 0 0 10 71.01 175.67 Tm
0.027 Tw
(The ideas illustrated in the example can be generalized, arriving at the dynamic semantics of an arbitrary SDL)Tj
-0.851 -1.1 TD
0 Tw
(specification which is given by a transition system)Tj
/TT4 1 Tf
20.443 0 TD
(T)Tj
/TT6 1 Tf
0.806 0 TD
0.25 Tc
(=\()Tj
/TT4 1 Tf
1.147 0 TD
0 Tc
(St)Tj
/TT6 1 Tf
0.778 0 TD
(,)Tj
/TT4 1 Tf
0.25 0 TD
(St)Tj
8 0 0 8 304.52 162.17 Tm
(0)Tj
/TT6 1 Tf
10 0 0 10 308.52 164.67 Tm
(,)Tj
/TT8 1 Tf
12 0 0 12 311.02 164.67 Tm
<0062>Tj
/TT6 1 Tf
10 0 0 10 316.95 164.67 Tm
(\), where)Tj
-23.177 -2.3 TD
()Tj
/TT4 1 Tf
1.417 0 TD
(St =)Tj
/TT8 1 Tf
1.953 0 TD
<0046>Tj
/TT4 1 Tf
8 0 0 8 126.56 139.17 Tm
(objectSet)Tj
/TT8 1 Tf
3.9163 0 TD
<0044>Tj
/TT4 1 Tf
0.7138 0 TD
( ObjectSet)Tj
10 0 0 10 196.7 141.67 Tm
( \()Tj
/TT9 1 Tf
0.583 0 TD
()Tj
/TT4 1 Tf
8 0 0 8 208.02 139.17 Tm
( obj)Tj
/TT8 1 Tf
1.7775 0 TD
<0044>Tj
/TT4 1 Tf
0.7137 0 TD
( objectSet)Tj
10 0 0 10 261.27 141.67 Tm
(obj.St\))Tj
/TT6 1 Tf
-16.192 -1.283 TD
(with)Tj
/TT4 1 Tf
2.028 0 TD
(objectSet)Tj
/TT6 1 Tf
3.666 0 TD
( being a )Tj
/TT7 1 Tf
3.4155 0 TD
()Tj
/TT6 1 Tf
0.5562 0 TD
[(nite set of objects that may e)12.6(xist simultaneously under the static constraints of)]TJ
-9.6657 -1.1 TD
(the speci)Tj
/TT7 1 Tf
3.5264 0 TD
()Tj
/TT6 1 Tf
0.5562 0 TD
(cation, and)Tj
/TT4 1 Tf
4.6385 0 TD
(obj.St)Tj
/TT6 1 Tf
2.306 0 TD
( being the state set of the object)Tj
/TT4 1 Tf
12.887 0 TD
(obj)Tj
/TT6 1 Tf
1.278 0 TD
(. Note that only some of the states of)Tj
/TT4 1 Tf
14.943 0 TD
(St)Tj
/TT6 1 Tf
-40.135 -1.1 TD
(may actually be reachable according to the dynamic semantics of the speci)Tj
/TT7 1 Tf
29.8486 0 TD
()Tj
/TT6 1 Tf
0.5562 0 TD
[(cation, in particular)33(, only)]TJ
-30.4048 -1.1 TD
[(some of the object sets may e)13.4(xist under the static constraints.)]TJ
ET
69.17 379.47 m
140.84 379.47 l
B*
BT
10 0 0 10 69.17 380.47 Tm
(System-definition)Tj
/TT15 1 Tf
0 -1.5 TD
(inSignalSet)Tj
T*
(signalDest)Tj
T*
(Pre)Tj
/TT4 1 Tf
1.444 0 TD
( = \(\))Tj
/TT6 1 Tf
15.564 0 TD
(/* environment action */)Tj
/TT15 1 Tf
-17.008 -1.5 TD
(Eff)Tj
/TT4 1 Tf
1.583 0 TD
(= \()Tj
/TT8 1 Tf
1.508 0 TD
<009a>Tj
/TT4 1 Tf
0.549 0 TD
(inSig)Tj
/TT8 1 Tf
2.306 0 TD
<0044>Tj
/TT15 1 Tf
0.963 0 TD
(inSignalSet)Tj
/TT4 1 Tf
4.78 0 TD
(.)Tj
/TT8 1 Tf
0.5 0 TD
<009a>Tj
/TT4 1 Tf
0.549 0 TD
(sigDest)Tj
/TT8 1 Tf
3.25 0 TD
<0044>Tj
/TT15 1 Tf
0.963 0 TD
(signalDest)Tj
/TT4 1 Tf
4.334 0 TD
(.)Tj
/TT8 1 Tf
-17.033 -1.5 TD
<0099>Tj
/TT4 1 Tf
0.713 0 TD
(obj)Tj
/TT9 1 Tf
1.611 0 TD
( )Tj
/TT8 1 Tf
0.25 0 TD
<0044>Tj
/TT4 1 Tf
0.713 0 TD
( receivers\(inSig,obj.st.env,sigDest\). obj.st.inQ := append\(obj.st.inQ, \(sig,obj.st.env\)\)\))Tj
/TT6 1 Tf
-5.413 -1.5 TD
(System-name)Tj
/TT4 1 Tf
2.126 -1.5 TD
(System1)Tj
/TT2 1 Tf
-4.252 -3.3 TD
(Figure 3)Tj
/TT6 1 Tf
3.583 0 TD
[(: Excerpt of the Abstract Syntax T)33.3(ree with Attrib)19.2(utes: System-de)]TJ
/TT7 1 Tf
25.9133 0 TD
()Tj
/TT6 1 Tf
0.5562 0 TD
(nition)Tj
ET
endstream
endobj
32 0 obj
<<
/ProcSet [/PDF /Text ]
/Font <<
/TT2 4 0 R
/TT4 5 0 R
/TT6 6 0 R
/TT7 15 0 R
/TT8 22 0 R
/TT9 23 0 R
/TT15 29 0 R
>>
/ExtGState <<
/GS1 7 0 R
>>
>>
endobj
34 0 obj
<<
/Length 7500
>>
stream
1 g
/GS1 gs
0.06 841.89 595.22 -841.83 re
f
BT
/TT6 1 Tf
10 0 0 10 85.18 739.41 Tm
0 g
0 Tc
0 Tw
()Tj
/TT4 1 Tf
1.417 0 TD
(St)Tj
8 0 0 8 107.13 736.9099 Tm
(0)Tj
10 0 0 10 111.13 739.41 Tm
( =)Tj
/TT6 1 Tf
1.175 0 TD
(set of initial states of the start object \(e.g., system, or processSet\))Tj
-3.77 -1.583 TD
()Tj
/TT8 1 Tf
1.417 0 TD
<0062>Tj
/TT4 1 Tf
0.494 0 TD
(: St)Tj
/TT8 1 Tf
1.611 0 TD
<0041>Tj
/TT4 1 Tf
0.987 0 TD
[( P)79.8(ower \(St\))]TJ
/TT8 1 Tf
-3.092 -1.1 TD
<0099>Tj
/TT4 1 Tf
0.713 0 TD
(st)Tj
/TT8 1 Tf
1.25 0 TD
<0044>Tj
/TT4 1 Tf
0.713 0 TD
( St.)Tj
/TT8 1 Tf
1.528 0 TD
<0062>Tj
/TT4 1 Tf
0.494 0 TD
(\(st\) := {st)Tj
/TT9 1 Tf
4.797 0 TD
( )Tj
/TT8 1 Tf
0.25 0 TD
<0044>Tj
/TT4 1 Tf
0.713 0 TD
( St |)Tj
/TT8 1 Tf
1.803 0 TD
<009a>Tj
/TT4 1 Tf
0.549 0 TD
(obj)Tj
/TT8 1 Tf
1.528 0 TD
<0044>Tj
/TT4 1 Tf
0.713 0 TD
( objectSet\(st\).)Tj
/TT8 1 Tf
6.082 0 TD
<009a>Tj
/TT4 1 Tf
0.549 0 TD
(a)Tj
/TT8 1 Tf
0.75 0 TD
<0044>Tj
/TT15 1 Tf
0.963 0 TD
(A)Tj
/TT4 1 Tf
8 0 0 8 339.97 710.08 Tm
(obj)Tj
10 0 0 10 350.2 712.58 Tm
(. \(st)Tj
/TT8 1 Tf
2.083 0 TD
<0044>Tj
/TT4 1 Tf
0.713 0 TD
( a.)Tj
/TT15 1 Tf
1 0 TD
(Pre)Tj
/TT8 1 Tf
1.694 0 TD
<008e>Tj
/TT4 1 Tf
0.603 0 TD
( \(st,st\))Tj
/TT8 1 Tf
3.639 0 TD
<0044>Tj
/TT4 1 Tf
0.713 0 TD
(a.)Tj
/TT15 1 Tf
0.75 0 TD
[(Ef)18(f)]TJ
/TT4 1 Tf
1.315 0 TD
(\)})Tj
/TT6 1 Tf
-39.012 -1.583 TD
()Tj
/TT15 1 Tf
1.417 0 TD
(A)Tj
/TT4 1 Tf
8 0 0 8 106.02 694.25 Tm
(obj)Tj
/TT6 1 Tf
10 0 0 10 116.25 696.75 Tm
( = {\()Tj
/TT15 1 Tf
1.877 0 TD
(Pre)Tj
/TT6 1 Tf
1.444 0 TD
(,)Tj
/TT15 1 Tf
0.25 0 TD
[(Ef)18(f)]TJ
/TT6 1 Tf
1.315 0 TD
(\) |)Tj
/TT8 1 Tf
1.033 0 TD
<009a>Tj
/TT6 1 Tf
0.549 0 TD
( node)Tj
/TT8 1 Tf
2.444 0 TD
<0044>Tj
/TT6 1 Tf
0.713 0 TD
( nodeSet\(node\()Tj
/TT4 1 Tf
6.082 0 TD
(obj.identi)Tj
/TT16 1 Tf
3.8052 0 TD
()Tj
/TT4 1 Tf
0.5 0 TD
(er)Tj
/TT6 1 Tf
0.8338 0 TD
(\),includeNodes\()Tj
/TT4 1 Tf
6.415 0 TD
(obj.type)Tj
/TT6 1 Tf
3.194 0 TD
(\),)Tj
-20.521 -1.284 TD
( delimitingNodes\()Tj
/TT4 1 Tf
9.749 0 TD
(obj.type)Tj
/TT6 1 Tf
3.194 0 TD
(\)\).)Tj
/TT15 1 Tf
1.166 0 TD
(Pre)Tj
/TT6 1 Tf
1.444 0 TD
( = node.)Tj
/TT15 1 Tf
3.258 0 TD
(Pre)Tj
/TT6 1 Tf
1.444 0 TD
( and)Tj
/TT15 1 Tf
1.944 0 TD
[(Ef)18(f)]TJ
/TT6 1 Tf
1.315 0 TD
( = node.)Tj
/TT15 1 Tf
3.259 0 TD
[(Ef)18(f)]TJ
/TT6 1 Tf
1.314 0 TD
(}\))Tj
-42.545 -2.3 TD
0.034 Tw
(Generally speaking, the transition system associated with an SDL specification is obtained from the definition)Tj
-0.851 -1.1 TD
0.003 Tw
(of objects in a compositional way: global state set, start states, and state transition relation are defined in terms of)Tj
T*
0.013 Tw
(the states and actions of objects. Since all objects are defined in a uniform way, the formal semantics is modular,)Tj
T*
-0.009 Tw
(which improves its maintainability. Also, the way actions are defined supports the generation of code. Finally, in-)Tj
T*
0.014 Tw
(coming signals from the environment can be incorporated in the same uniform way, by introducing an additional)Tj
T*
0 Tw
(action.)Tj
/TT2 1 Tf
11 0 0 11 62.5 582.25 Tm
[(3.4)-811.8(Time)]TJ
/TT6 1 Tf
10 0 0 10 71.01 558.91 Tm
0.011 Tw
(To model time, we introduce a conceptual clock for all active objects. Note that these clocks are used to model)Tj
-0.851 -1.1 TD
0.05 Tw
(the laws of nature, they should not be confused with physical clocks. Each clock keeps track of the local object)Tj
T*
0.022 Tw
(time, it is advanced when the object executes actions, or when the object is waiting and other actions occur. Due)Tj
T*
0.062 Tw
(to the interleaving semantics, clock values may differ, and the maximum clock value is perceived as the global)Tj
T*
0 Tw
(time.)Tj
1.057 -3.474 TD
(Process-graph)Tj
2.126 -1.1 TD
(Transition)Tj
ET
0 G
0 J 0 j 0.6 w 3.86 M []0 d
1 i
115.59 457.17 m
157.8 457.17 l
B*
BT
10 0 0 10 115.59 458.17 Tm
(Task-node)Tj
/TT15 1 Tf
T*
(minMaxET)Tj
/TT6 1 Tf
5.029 0 TD
(= \(2,5\))Tj
/TT15 1 Tf
-5.029 -1.3 TD
(Pre)Tj
/TT4 1 Tf
1.444 0 TD
(,)Tj
/TT15 1 Tf
0.5 0 TD
(Eff)Tj
/TT6 1 Tf
0.182 -1.3 TD
(x := 5)Tj
-4.252 -1.3 TD
(State-node-)Tj
/TT2 1 Tf
4.61 0 TD
(set)Tj
/TT6 1 Tf
-2.484 -1.1 TD
(S)Tj
ET
115.59 374.17 m
159.47 374.17 l
B*
BT
10 0 0 10 115.59 375.17 Tm
(Input-node)Tj
/TT15 1 Tf
T*
(minMaxET)Tj
/TT6 1 Tf
5.029 0 TD
(= \(2,9\))Tj
/TT15 1 Tf
-5.029 -1.3 TD
(Pre)Tj
/TT4 1 Tf
1.444 0 TD
( = \(action selected for execution)Tj
/TT8 1 Tf
13.228 0 TD
<008e>Tj
/TT4 1 Tf
-10.42 -1.3 TD
( global time is advanced a minimum distance)Tj
/TT8 1 Tf
18.332 0 TD
<008e>Tj
/TT4 1 Tf
0.603 0 TD
( ...\))Tj
/TT15 1 Tf
-23.187 -1.3 TD
(Eff)Tj
/TT4 1 Tf
1.583 0 TD
(= \(...; obj.st.clock := obj.st.clock + executionTime;)Tj
2.669 -1.3 TD
( clocks of waiting processes := obj.st.clock;)Tj
T*
( for all waiting processes: select action for execution\))Tj
/TT6 1 Tf
-2.126 -1.3 TD
(Signal-identifier)Tj
2.126 -1.1 TD
(A)Tj
-2.126 -1.1 TD
(Transition)Tj
ET
158.11 252.17 m
200.32 252.17 l
B*
BT
10 0 0 10 158.11 253.17 Tm
(Task-node)Tj
/TT15 1 Tf
T*
(minMaxET)Tj
/TT6 1 Tf
5.029 0 TD
(= \(2,5\))Tj
/TT15 1 Tf
-5.029 -1.3 TD
(Pre)Tj
/TT4 1 Tf
1.444 0 TD
(,)Tj
/TT15 1 Tf
0.5 0 TD
(Eff)Tj
/TT6 1 Tf
0.182 -1.3 TD
(x := x+ 1)Tj
ET
158.11 204.17 m
208.66 204.17 l
B*
BT
10 0 0 10 158.11 205.17 Tm
(Output-node)Tj
/TT15 1 Tf
0 -1.1 TD
(minMaxET)Tj
/TT6 1 Tf
5.029 0 TD
(= \(4,5\))Tj
/TT15 1 Tf
-5.029 -1.3 TD
(Pre, Eff)Tj
/TT6 1 Tf
2.126 -1.3 TD
(A)Tj
-4.252 -1.1 TD
(Terminator)Tj
2.126 -1.1 TD
(S)Tj
ET
1 g
417.44 509.56 60.51 -26.86 re
f
462.82 509.56 m
432.57 509.56 l
B*
462.82 482.7 m
432.57 482.7 l
B*
462.82 482.7 m
471.172 482.7 477.95 488.717 477.95 496.13 c
477.95 503.543 471.172 509.56 462.82 509.56 c
432.57 509.56 m
424.218 509.56 417.44 503.543 417.44 496.13 c
417.44 488.717 424.218 482.7 432.57 482.7 c
418 472.05 60.51 -26.86 re
S
417.37 422.87 60.51 -26.86 re
f
473.64 422.87 m
421.61 422.87 l
B*
473.64 396.01 m
421.61 396.01 l
B*
421.433 422.87 m
418.778 418.787 417.38 414.155 417.38 409.44 c
417.38 404.725 418.778 400.093 421.433 396.01 c
473.827 396.01 m
476.482 400.093 477.88 404.725 477.88 409.44 c
477.88 414.155 476.482 418.787 473.827 422.87 c
S
417.32 386.36 60.5 -26.86 re
f
477.83 386.36 m
417.32 386.36 l
B*
462.7 372.93 m
477.83 386.36 l
B*
477.83 359.5 m
462.7 372.93 l
B*
417.32 359.5 m
477.83 359.5 l
B*
417.32 386.36 m
417.32 359.5 l
B*
416.15 267.4 60.51 -26.85 re
S
417.11 218.78 60.51 -26.86 re
f
462.49 218.78 m
417.11 218.78 l
B*
477.62 205.35 m
462.49 218.78 l
B*
462.49 191.92 m
477.62 205.35 l
B*
417.11 191.92 m
462.49 191.92 l
B*
417.11 218.78 m
417.11 191.92 l
B*
415.94 162.58 60.51 -26.86 re
f
472.21 162.58 m
420.18 162.58 l
B*
472.21 135.72 m
420.18 135.72 l
B*
420.003 162.58 m
417.348 158.497 415.95 153.865 415.95 149.15 c
415.95 144.435 417.348 139.803 420.003 135.72 c
472.397 135.72 m
475.052 139.803 476.45 144.435 476.45 149.15 c
476.45 153.865 475.052 158.497 472.397 162.58 c
S
BT
/TT11 1 Tf
10 0 0 10 434.21 456.14 Tm
0 g
(x := 5)Tj
0.875 -5.136 TD
(S)Tj
-0.078 -3.544 TD
(A)Tj
-1.611 -11.858 TD
(x := x+1)Tj
1.648 -4.963 TD
(A)Tj
-0.068 -5.49 TD
(S)Tj
ET
446.95 472.04 m
446.95 482.7 l
447.07 422.58 m
447.07 445.23 l
446.88 422.87 m
451.42 426.9 l
442.34 426.9 m
446.88 422.87 l
446.64 386.33 m
446.8 396.04 l
447.03 267.58 m
447.03 359.83 l
446.22 218.79 m
446.22 240.58 l
446.39 162.83 m
446.64 191.83 l
446.2 162.58 m
450.73 166.61 l
441.66 166.61 m
446.2 162.58 l
S
BT
/TT2 1 Tf
10 0 0 10 73.07 108.67 Tm
(Figure 4)Tj
/TT6 1 Tf
3.583 0 TD
[(: Excerpt of the Abstract Syntax T)33.3(ree with Attrib)19.2(utes: Real-time)]TJ
ET
endstream
endobj
35 0 obj
<<
/ProcSet [/PDF /Text ]
/Font <<
/TT2 4 0 R
/TT4 5 0 R
/TT6 6 0 R
/TT8 22 0 R
/TT9 23 0 R
/TT11 24 0 R
/TT15 29 0 R
/TT16 36 0 R
>>
/ExtGState <<
/GS1 7 0 R
>>
>>
endobj
38 0 obj
<<
/Length 6359
>>
stream
1 g
/GS1 gs
0.06 841.89 595.22 -841.83 re
f
BT
/TT6 1 Tf
10 0 0 10 71.01 739.41 Tm
0 g
0 Tc
-0.001 Tw
(In SDL, it is currently possible to refer to the current time, and to use timer mechanisms. In the example shown)Tj
-0.851 -1.1 TD
-0.01 Tw
(in Figure 4, we go one step further in assuming that an execution time interval can be associated with each action.)Tj
T*
0.005 Tw
(The intended meaning is that if an action is selected for execution, it will consume an arbitrary amount of time in)Tj
T*
-0.04 Tw
(this interval. To model the timing behaviour, we include the selected action of an active object into the object state.)Tj
T*
0.012 Tw
(Furthermore, we extend the firing condition of an action by requiring that the action has been selected for execu-)Tj
T*
-0.04 Tw
(tion, and that by executing this action, the global time is advanced a minimum distance. The latter condition is nec-)Tj
T*
-0.01 Tw
(essary to avoid effects such as signals arriving in the past. The additional effects of an action are the advancement)Tj
T*
-0.017 Tw
(of the local clock by the execution time of the action, the advancement of local clocks of all waiting active objects)Tj
T*
0.05 Tw
(to the global time, and the selection of executable actions including an execution time within the specified time)Tj
T*
0 Tw
(interval for all waiting objects \(in that order\).)Tj
0.851 -54.161 TD
0.052 Tw
(Figure 5 shows an excerpt of a labeled reachability graph of)Tj
/TT4 1 Tf
24.812 0 TD
0 Tw
(System1)Tj
/TT6 1 Tf
3.277 0 TD
0.052 Tw
(. Each node represents a reachable state,)Tj
-28.94 -1.1 TD
-0.041 Tw
(which is characterized by the control states, the variable values, the input queues, the clock values, and the selected)Tj
/TT4 1 Tf
12.879 47.963 TD
0 Tw
[(s)-4118.8(x)-4130.2(inQ)-3874(cloc)19.5(k)-5031.2(selAction)]TJ
-8.523 -1.2 TD
[(Pr)45(ocess1:1)]TJ
/TT6 1 Tf
8.439 0 TD
[(S)-4007.8(9)-3927()-4243.9(93)-5090(\(input A, 3\))]TJ
/TT4 1 Tf
-8.439 -1.2 TD
[(Pr)45(ocess1:2)]TJ
/TT6 1 Tf
8.273 0 TD
[(s2)-3840.8(7)-4288(<)0(>)-4605.1(9)0(4)-4840(\(output A, 4\))]TJ
ET
0 0 0.5 rg
0 0 0.5 RG
0 J 0 j 0.6 w 3.86 M []0 d
1 i
102.06 540.35 m
102.06 563.85 l
B*
170.06 539.85 m
170.06 577.85 l
B*
476.19 540.35 m
476.19 577.85 l
B*
476.44 578.1 m
169.81 578.1 l
B*
476.44 564.1 m
101.81 564.1 l
B*
476.44 540.1 m
101.81 540.1 l
B*
BT
/TT4 1 Tf
10 0 0 10 191.87 483.47 Tm
0 g
[(s)-4117.8(x)-4131.2(inQ)-3874(cloc)19.5(k)-5031.2(selAction)]TJ
-8.523 -1.2 TD
[(Pr)46(ocess1:1)]TJ
/TT6 1 Tf
8.273 0 TD
[(s1)-3839.8(9)-4289(<)0(>)-4605.1(9)0(6)-5151(\(x:=x+1, 3\))]TJ
/TT4 1 Tf
-8.273 -1.2 TD
[(Pr)46(ocess1:2)]TJ
/TT6 1 Tf
8.273 0 TD
[(s2)-3839.8(7)-4289(<)0(>)-4605.1(9)0(4)-4840(\(output A, 4\))]TJ
ET
0 0 0.5 rg
102.64 456.39 m
102.64 479.89 l
B*
170.63 455.89 m
170.63 493.89 l
B*
476.77 456.39 m
476.77 493.89 l
B*
477.02 494.14 m
170.38 494.14 l
B*
477.02 480.14 m
102.39 480.14 l
B*
477.02 456.14 m
102.39 456.14 l
B*
BT
/TT4 1 Tf
10 0 0 10 191.61 398.71 Tm
0 g
[(s)-4118.8(x)-4130.2(inQ)-3875(cloc)19.5(k)-5030.2(selAction)]TJ
-8.523 -1.2 TD
[(Pr)45(ocess1:1)]TJ
/TT6 1 Tf
8.273 0 TD
[(s1)-3840.8(9)-3927()-4244.9(96)-5150(\(x:=x+1, 3\))]TJ
/TT4 1 Tf
-8.273 -1.2 TD
[(Pr)45(ocess1:2)]TJ
/TT6 1 Tf
8.44 0 TD
[(S)-4006.8(7)-4288(<>)-4606.1(98)-5192(\(w)10.2(aiting, -\))]TJ
ET
0 0 0.5 rg
102.38 371.62 m
102.38 395.12 l
B*
170.38 371.12 m
170.38 409.12 l
B*
476.52 371.62 m
476.52 409.12 l
B*
476.77 409.37 m
170.13 409.37 l
B*
476.77 395.37 m
102.13 395.37 l
B*
476.77 371.37 m
102.13 371.37 l
B*
BT
/TT4 1 Tf
10 0 0 10 191.36 314.56 Tm
0 g
[(s)-4118.8(x)-4131.2(inQ)-3874(cloc)19.5(k)-5031.2(selAction)]TJ
-8.523 -1.2 TD
[(Pr)45(ocess1:1)]TJ
/TT6 1 Tf
8.273 0 TD
[(s2)-3590.8(10)-3678()-4243.9(99)-4840(\(output A, 5\))]TJ
/TT4 1 Tf
-8.273 -1.2 TD
[(Pr)45(ocess1:2)]TJ
/TT6 1 Tf
8.44 0 TD
[(S)-4006.8(7)-4289(<>)-4605.1(99)-5192(\(w)10.2(aiting, -\))]TJ
ET
0 0 0.5 rg
102.13 287.48 m
102.13 310.98 l
B*
170.13 286.98 m
170.13 324.98 l
B*
476.27 287.48 m
476.27 324.98 l
B*
476.52 325.23 m
169.88 325.23 l
B*
476.52 311.23 m
101.88 311.23 l
B*
476.52 287.23 m
101.88 287.23 l
B*
BT
/TT4 1 Tf
10 0 0 10 191.74 229.79 Tm
0 g
[(s)-4118.8(x)-4130.2(inQ)-3874(cloc)19.5(k)-5031.2(selAction)]TJ
-8.524 -1.2 TD
[(Pr)44(ocess1:1)]TJ
/TT6 1 Tf
8.44 0 TD
[(S)-3757.8(1)0(0)-3677()-3993.9(104)-4840(\(input A, 4\))]TJ
/TT4 1 Tf
-8.44 -1.2 TD
[(Pr)44(ocess1:2)]TJ
/TT6 1 Tf
8.44 0 TD
[(S)-4007.8(7)-3927()-3993.9(104)-4840(\(input A, 2\))]TJ
ET
0 0 0.5 rg
102.5 202.71 m
102.5 226.21 l
B*
170.5 202.21 m
170.5 240.21 l
B*
476.64 202.71 m
476.64 240.21 l
B*
476.89 240.46 m
170.25 240.46 l
B*
476.89 226.46 m
102.25 226.46 l
B*
476.89 202.46 m
102.25 202.46 l
B*
0 G
1.08 w
289.84 589.17 m
289.84 590.63 l
287.2 590.13 m
289.84 580.91 l
292.49 590.13 l
289.84 589.17 l
s
0 g
287.2 590.13 m
289.84 580.91 l
292.49 590.13 l
289.84 589.17 l
f*
2 J
289.84 612.12 m
289.84 615.62 l
S
[5.995 5.995 ]5.995 d
289.84 594.13 m
289.84 612.12 l
S
[]0 d
289.84 590.63 m
289.84 594.13 l
S
0 J
289.6 505.4 m
289.6 506.86 l
286.95 506.36 m
289.6 497.14 l
292.24 506.36 l
289.6 505.4 l
s
286.95 506.36 m
289.6 497.14 l
292.24 506.36 l
289.6 505.4 l
f*
2 J
289.6 506.86 m
289.6 537.15 l
S
0 J
289.84 420.88 m
289.84 422.34 l
287.2 421.84 m
289.84 412.62 l
292.49 421.84 l
289.84 420.88 l
s
287.2 421.84 m
289.84 412.62 l
292.49 421.84 l
289.84 420.88 l
f*
2 J
289.84 422.34 m
289.84 452.63 l
S
0 J
289.47 335.86 m
289.47 337.33 l
286.83 336.83 m
289.47 327.61 l
292.12 336.83 l
289.47 335.86 l
s
286.83 336.83 m
289.47 327.61 l
292.12 336.83 l
289.47 335.86 l
f*
2 J
289.47 337.33 m
289.47 367.62 l
S
0 J
289.47 251.72 m
289.47 253.18 l
286.83 252.68 m
289.47 243.46 l
292.12 252.68 l
289.47 251.72 l
s
286.83 252.68 m
289.47 243.46 l
292.12 252.68 l
289.47 251.72 l
f*
2 J
289.47 253.18 m
289.47 283.47 l
S
BT
10 0 0 10 303.98 517.6 Tm
(1. input A)Tj
0.106 -8.829 TD
(2. output A)Tj
0.212 -8.192 TD
(3. x:=x+1)Tj
0.054 -8.882 TD
(4. output A)Tj
ET
0 J
290.38 185.32 m
290.38 186.78 l
287.73 186.28 m
290.38 177.06 l
293.02 186.28 l
290.38 185.32 l
s
287.73 186.28 m
290.38 177.06 l
293.02 186.28 l
290.38 185.32 l
f*
2 J
290.38 198 m
290.38 201.5 l
S
[7.722 7.722 ]7.722 d
290.38 190.28 m
290.38 198 l
S
[]0 d
290.38 186.78 m
290.38 190.28 l
S
BT
/TT2 1 Tf
10 0 0 10 104.46 137.63 Tm
(Figure 5)Tj
/TT6 1 Tf
3.583 0 TD
(: Excerpt of a reachability graph: Real-time)Tj
ET
endstream
endobj
39 0 obj
<<
/ProcSet [/PDF /Text ]
/Font <<
/TT2 4 0 R
/TT4 5 0 R
/TT6 6 0 R
>>
/ExtGState <<
/GS1 7 0 R
>>
>>
endobj
41 0 obj
<<
/Length 4863
>>
stream
1 g
/GS1 gs
0.06 841.89 595.22 -841.83 re
f
BT
/TT6 1 Tf
10 0 0 10 62.5 739.41 Tm
0 g
0 Tc
0.031 Tw
(action of the process instances. In the first state, the action input A will be selected, because its execution will)Tj
0 -1.1 TD
-0.023 Tw
(advance the global time by a minimum distance, i.e. to 96. When input A has been executed \(with the effect that)Tj
T*
-0.028 Tw
(the signal A is removed from the input queue, and that the new control state is s1\), the local clock is advanced, and)Tj
T*
-0.037 Tw
(a new action together with an execution time within the specified interal is selected. The next action to be executed)Tj
T*
-0.003 Tw
(is output A, which brings)Tj
/TT4 1 Tf
11.263 0 TD
0 Tw
(Process1:2)Tj
/TT6 1 Tf
4.499 0 TD
-0.003 Tw
( into a waiting state, since there are no fireable actions. For this reason, its)Tj
-15.762 -1.1 TD
0.032 Tw
(local clock has to be advanced after the next action of)Tj
/TT4 1 Tf
22.099 0 TD
0 Tw
(Process1:1)Tj
/TT6 1 Tf
4.499 0 TD
0.032 Tw
(, and also after the action output A, before a)Tj
-26.598 -1.1 TD
-0.014 Tw
(further action can be selected. It is important that this selection takes place after the advancement of the clock, be-)Tj
T*
0 Tw
(cause at local time 99, no signal A has been in the queue of)Tj
/TT4 1 Tf
23.968 0 TD
(Process1:2)Tj
/TT6 1 Tf
4.499 0 TD
(.)Tj
11 0 0 11 62.5 637.75 Tm
[(4)-1561.8(CURRENT STATUS)]TJ
10 0 0 10 62.5 612.4099 Tm
0.046 Tw
(Currently, the proposed new formal SDL semantics is being worked out in detail. Formalization is based on the)Tj
0 -1.1 TD
0.069 Tw
(abstract SDL grammar, which is defined in the Z.100 Recommendations. The abstract grammar is extended by)Tj
T*
0 Tw
(evaluation rules, yielding an attribute grammar. Attributes include actions, determined by firing condition and ef-)Tj
T*
-0.029 Tw
(fects, which are defined for about 20 different node types. This defines, for each complete SDL specification, an)Tj
T*
0.002 Tw
(attributed abstract syntax tree, from which the transition system is then directly obtained. We expect the resulting)Tj
T*
0 Tw
(semantics to be extremely concise.)Tj
0.851 -1.1 TD
0.025 Tw
(The outline presented in this paper leaves enough room for improvements concerning, e.g., the notation that is)Tj
-0.851 -1.1 TD
-0.014 Tw
(used. In [2,3], a formal dynamic semantics for what is termed Basic SDL is provided in terms of an Abstract State)Tj
T*
0.056 Tw
(Machine \(ASM\). It should be investigated how this approach is related to the semantics proposed in this paper,)Tj
T*
-0.021 Tw
(whether it is applicable to full SDL, and what aspects of real-time can be modeled. A major advantage of ASMs is)Tj
T*
0 Tw
(the existence of a tool environment supporting the execution of ASM models.)Tj
11 0 0 11 62.5 477.75 Tm
[(5)-1561.8(REFERENCES)]TJ
10 0 0 10 62.5 452.41 Tm
-0.044 Tw
[([1])-1102(E. Brinksma, J.-P. Katoen, R. Langerak, D. Latella:)]TJ
/TT4 1 Tf
22.802 0 TD
(Partial Order Models for Quantitative Extensions of LO-)Tj
-20.534 -1.1 TD
0 Tw
(TOS)Tj
/TT6 1 Tf
1.778 0 TD
-0.023 Tw
(, Computer Networks and ISDN Systems, Special Issue on Trends in Formal Description Techniques,)Tj
-1.778 -1.1 TD
0 Tw
(1998 \(forthcoming\))Tj
-2.268 -1.4 TD
[([2])-1102(U. Glsser:)]TJ
/TT4 1 Tf
7.017 0 TD
(ASM Semantics of SDL: Concepts, Methods, Tools)Tj
/TT6 1 Tf
20.277 0 TD
( \(this volume\))Tj
-27.294 -1.4 TD
0.04 Tw
[([3])-1102(U. Glsser, R. Karges:)]TJ
/TT4 1 Tf
11.677 0 TD
(Abstract State Machine Semantics of SDL)Tj
/TT6 1 Tf
16.951 0 TD
(, Journal of Universal Computer Science,)Tj
-26.36 -1.1 TD
0 Tw
(3\(12\):1382-1414, 1997)Tj
-2.268 -1.4 TD
-0.007 Tw
[([4])-1102(R. Gotzhein, F. Rler, P. Schaible:)]TJ
/TT4 1 Tf
16.865 0 TD
(Towards a Formal SDL-Semantics - Design Choices and Outline)Tj
/TT6 1 Tf
25.998 0 TD
(, ITU-)Tj
-40.595 -1.1 TD
0 Tw
(T SG10 TD 79-E, Geneva, March 24 - April 1, 1998)Tj
-2.268 -1.4 TD
0.022 Tw
[([5])-1102(ITU-T Recommendation Z.100,)]TJ
/TT4 1 Tf
15.362 0 TD
(Specification and Description Language \(SDL\))Tj
/TT6 1 Tf
18.978 0 TD
(, International Telecommu-)Tj
-32.072 -1.1 TD
0 Tw
(nications Union, Geneva, 03/93)Tj
-2.268 -1.4 TD
0.001 Tw
[([6])-1102(ITU-T Recommendation Z.100, Annex F.1,)]TJ
/TT4 1 Tf
20.019 0 TD
(SDL formal definition: Introduction)Tj
/TT6 1 Tf
14.364 0 TD
(, International Telecommu-)Tj
-32.115 -1.1 TD
0 Tw
(nications Union, Geneva, 03/93)Tj
-2.268 -1.4 TD
-0.017 Tw
[([7])-1102(ITU-T Recommendation Z.100, Annex F.2,)]TJ
/TT4 1 Tf
19.931 0 TD
(SDL formal definition: Static semantics)Tj
/TT6 1 Tf
15.766 0 TD
(, International Telecom-)Tj
-33.429 -1.1 TD
0 Tw
(munications Union, Geneva, 03/93)Tj
-2.268 -1.4 TD
0.008 Tw
[([8])-1102(ITU-T Recommendation Z.100, Annex F.3,)]TJ
/TT4 1 Tf
20.058 0 TD
(SDL formal definition: Dynamic Semantics)Tj
/TT6 1 Tf
17.31 0 TD
(, International Tele-)Tj
-35.1 -1.1 TD
0 Tw
(communications Union, Geneva, 03/93)Tj
ET
endstream
endobj
42 0 obj
<<
/ProcSet [/PDF /Text ]
/Font <<
/TT4 5 0 R
/TT6 6 0 R
>>
/ExtGState <<
/GS1 7 0 R
>>
>>
endobj
7 0 obj
<<
/Type /ExtGState
/SA false
/SM 0.02
/OP false
/op false
/OPM 1
/BG2 /Default
/UCR2 /Default
/HT /Default
/TR2 /Default
>>
endobj
43 0 obj
<<
/Type /FontDescriptor
/Ascent 701
/CapHeight 0
/Descent -298
/Flags 4
/FontBBox [-167 -299 1094 827]
/FontName /IEKKPG+Symbol
/ItalicAngle 0
/StemV 0
/FontFile2 44 0 R
>>
endobj
44 0 obj
<<
/Filter /FlateDecode
/Length 21998
/Length1 41588
>>
stream
HW}t33;;Y9UH8jE`BŒу4NˡfwfGfgYUR;i4R
RK/E|T@b}z<ͽ7 oN?=G.܋CՀgyߓ !#Xt0!ŋGzg+[P͛ K C'nA}`}\.B~L0W s۱_UcAv"Цr2.yQbCNnhH49J& q/jX@c
g-8p82'耬&~\LW`QaC4YCn_\,EhM0
.0`%31 0C :0lk*Ga(e`