ITU-T Z 100 ANNEX F3-2016 Specification and Description Language - Overview of SDL-2010《规范描述语言–SDL概述-2010 附件F3：2010年SDL正式定义：动态语义学(研究组17)》.pdf

《ITU-T Z 100 ANNEX F3-2016 Specification and Description Language - Overview of SDL-2010《规范描述语言–SDL概述-2010 附件F3：2010年SDL正式定义：动态语义学(研究组17)》.pdf》由会员分享，可在线阅读，更多相关《ITU-T Z 100 ANNEX F3-2016 Specification and Description Language - Overview of SDL-2010《规范描述语言–SDL概述-2010 附件F3：2010年SDL正式定义：动态语义学(研究组17)》.pdf（106页珍藏版）》请在麦多课文档分享上搜索。

1、 I n t e r n a t i o n a l T e l e c o m m u n i c a t i o n U n i o n ITU-T Z.100 TELECOMMUNICATION STANDARDIZATION SECTOR OF ITU Annex F3 (10/2016) SERIES Z: LANGUAGES AND GENERAL SOFTWARE ASPECTS FOR TELECOMMUNICATION SYSTEMS Formal description techniques (FDT) Specification and Description Langu

2、age (SDL) Specification and Description Language Overview of SDL-2010 Annex F3: SDL-2010 formal definition: Dynamic semantics Recommendation ITU-T Z.100 Annex F3 ITU-T Z-SERIES RECOMMENDATIONS LANGUAGES AND GENERAL SOFTWARE ASPECTS FOR TELECOMMUNICATION SYSTEMS FORMAL DESCRIPTION TECHNIQUES (FDT) Sp

3、ecification and Description Language (SDL) Z.100Z.109 Application of formal description techniques Z.110Z.119 Message Sequence Chart (MSC) Z.120Z.129 User Requirements Notation (URN) Z.150Z.159 Testing and Test Control Notation (TTCN) Z.160Z.179 PROGRAMMING LANGUAGES CHILL: The ITU-T high level lang

4、uage Z.200Z.209 MAN-MACHINE LANGUAGE General principles Z.300Z.309 Basic syntax and dialogue procedures Z.310Z.319 Extended MML for visual display terminals Z.320Z.329 Specification of the man-machine interface Z.330Z.349 Data-oriented human-machine interfaces Z.350Z.359 Human-machine interfaces for

5、 the management of telecommunications networks Z.360Z.379 QUALITY Quality of telecommunication software Z.400Z.409 Quality aspects of protocol-related Recommendations Z.450Z.459 METHODS Methods for validation and testing Z.500Z.519 MIDDLEWARE Processing environment architectures Z.600Z.609 For furth

6、er details, please refer to the list of ITU-T Recommendations. Rec. ITU-T Z.100/Annex F3 (10/2016) i Recommendation ITU-T Z.100 Specification and Description Language Overview of SDL-2010 Annex F3 SDL-2010 formal definition: Dynamic semantics Summary This annex defines the SDL-2010 dynamic semantics

7、. History Edition Recommendation Approval Study Group Unique ID* 1.0 ITU-T Z.100 1984-10-19 11.1002/1000/2222 1.1 ITU-T Z.100 Annex A 1984-10-19 11.1002/1000/6664 1.2 ITU-T Z.100 Annex B 1984-10-19 11.1002/1000/6665 1.3 ITU-T Z.100 Annex C1 1984-10-19 11.1002/1000/6666 1.4 ITU-T Z.100 Annex C2 1984-

8、10-19 11.1002/1000/6667 1.5 ITU-T Z.100 Annex D 1984-10-19 11.1002/1000/6668 2.0 ITU-T Z.100 1987-09-30 X 11.1002/1000/10954 2.1 ITU-T Z.100 Annex A 1988-11-25 11.1002/1000/6669 2.2 ITU-T Z.100 Annex B 1988-11-25 11.1002/1000/6670 2.3 ITU-T Z.100 Annex C1 1988-11-25 11.1002/1000/6671 2.4 ITU-T Z.100

9、 Annex C2 1988-11-25 11.1002/1000/6672 2.5 ITU-T Z.100 Annex D 1988-11-25 X 11.1002/1000/3646 2.6 ITU-T Z.100 Annex E 1988-11-25 11.1002/1000/6673 2.7 ITU-T Z.100 Annex F1 1988-11-25 X 11.1002/1000/3647 2.8 ITU-T Z.100 Annex F2 1988-11-25 X 11.1002/1000/3648 2.9 ITU-T Z.100 Annex F3 1988-11-25 X 11.

10、1002/1000/3649 3.0 ITU-T Z.100 1988-11-25 11.1002/1000/3153 3.1 ITU-T Z.100 Annex C 1993-03-12 X 11.1002/1000/3155 3.2 ITU-T Z.100 Annex D 1993-03-12 X 11.1002/1000/3156 3.3 ITU-T Z.100 Annex F1 1993-03-12 X 11.1002/1000/3157 _ * To access the Recommendation, type the URL http:/handle.itu.int/ in th

11、e address field of your web browser, followed by the Recommendations unique ID. For example, http:/handle.itu.int/11.1002/1000/ 11830-en. ii Rec. ITU-T Z.100/Annex F3 (10/2016) 3.4 ITU-T Z.100 Annex F2 1993-03-12 X 11.1002/1000/3158 3.5 ITU-T Z.100 Annex F3 1993-03-12 X 11.1002/1000/3159 3.6 ITU-T Z

12、.100 App. I 1993-03-12 X 11.1002/1000/3160 3.7 ITU-T Z.100 App. II 1993-03-12 X 11.1002/1000/3161 4.0 ITU-T Z.100 1993-03-12 X 11.1002/1000/3154 4.1 ITU-T Z.100 (1993) Add. 1 1996-10-18 10 11.1002/1000/3917 5.0 ITU-T Z.100 1999-11-19 10 11.1002/1000/4764 5.1 ITU-T Z.100 (1999) Cor. 1 2001-10-29 17 1

13、1.1002/1000/5567 6.0 ITU-T Z.100 2002-08-06 17 11.1002/1000/6029 6.1 ITU-T Z.100 (2002) Amd. 1 2003-10-29 17 11.1002/1000/7091 6.2 ITU-T Z.100 (2002) Cor. 1 2004-08-29 17 11.1002/1000/356 7.0 ITU-T Z.100 2007-11-13 17 11.1002/1000/9262 8.0 ITU-T Z.100 2011-12-22 17 11.1002/1000/11387 8.1 ITU-T Z.100

14、 Annex F1 2000-11-24 10 11.1002/1000/5239 8.2 ITU-T Z.100 Annex F2 2000-11-24 10 11.1002/1000/5576 8.3 ITU-T Z.100 Annex F3 2000-11-24 10 11.1002/1000/5577 8.4 ITU-T Z.100 Annex F1 2015-01-13 17 11.1002/1000/12354 8.5 ITU-T Z.100 Annex F2 2015-01-13 17 11.1002/1000/12355 8.6 ITU-T Z.100 Annex F3 201

15、5-01-13 17 11.1002/1000/12356 9.0 ITU-T Z.100 2016-04-29 17 11.1002/1000/12846 9.1 ITU-T Z.100 Annex F1 2016-10-29 17 11.1002/1000/13040 9.2 ITU-T Z.100 Annex F2 2016-10-29 17 11.1002/1000/13041 9.3 ITU-T Z.100 Annex F3 2016-10-29 17 11.1002/1000/13042 Keywords Specification and Description Language

16、, SDL-2010, formal definition, Dynamic semantics, Behaviour semantics, SDL-2010 abstract machine, SAM, Compilation function, SAM programs, Data semantics. Rec. ITU-T Z.100/Annex F3 (10/2016) iii FOREWORD The International Telecommunication Union (ITU) is the United Nations specialized agency in the

17、field of telecommunications, information and communication technologies (ICTs). The ITU Telecommunication Standardization Sector (ITU-T) is a permanent organ of ITU. ITU-T is responsible for studying technical, operating and tariff questions and issuing Recommendations on them with a view to standar

18、dizing telecommunications on a worldwide basis. The World Telecommunication Standardization Assembly (WTSA), which meets every four years, establishes the topics for study by the ITU-T study groups which, in turn, produce Recommendations on these topics. The approval of ITU-T Recommendations is cove

19、red by the procedure laid down in WTSA Resolution 1. In some areas of information technology which fall within ITU-Ts purview, the necessary standards are prepared on a collaborative basis with ISO and IEC. NOTE In this Recommendation, the expression “Administration“ is used for conciseness to indic

20、ate both a telecommunication administration and a recognized operating agency. Compliance with this Recommendation is voluntary. However, the Recommendation may contain certain mandatory provisions (to ensure, e.g., interoperability or applicability) and compliance with the Recommendation is achieve

21、d when all of these mandatory provisions are met. The words “shall“ or some other obligatory language such as “must“ and the negative equivalents are used to express requirements. The use of such words does not suggest that compliance with the Recommendation is required of any party. INTELLECTUAL PR

22、OPERTY RIGHTSITU draws attention to the possibility that the practice or implementation of this Recommendation may involve the use of a claimed Intellectual Property Right. ITU takes no position concerning the evidence, validity or applicability of claimed Intellectual Property Rights, whether asser

23、ted by ITU members or others outside of the Recommendation development process. As of the date of approval of this Recommendation, ITU had not received notice of intellectual property, protected by patents, which may be required to implement this Recommendation. However, implementers are cautioned t

24、hat this may not represent the latest information and are therefore strongly urged to consult the TSB patent database at http:/www.itu.int/ITU-T/ipr/. ITU 2017 All rights reserved. No part of this publication may be reproduced, by any means whatsoever, without the prior written permission of ITU. iv

25、 Rec. ITU-T Z.100/Annex F3 (10/2016) Table of Contents Page Annex F3 SDL-2010 formal definition: Dynamic semantics . 1 F3.1 General information 1 F3.2 Behaviour semantics . 2 F3.3 Data semantics 76 Appendix I to Annex F3 List of abstract syntax grammar rules used. 95 Rec. ITU-T Z.100/Annex F3 (10/20

26、16) 1 Recommendation ITU-T Z.100 Specification and Description Language Overview of SDL-2010 Annex F3 SDL-2010 formal definition: Dynamic semantics F3.1 General information An overview of the formal semantics is described in clause F1.2 (Annex F1). F3.1.1 Definitions from Annex F1 The following defi

27、nitions for the syntax and semantics of ASMs are used within Annex F3. The domains and functions are defined in Annex F1 and listed here for cross-referencing reasons. The keywords case, choose, constraint, controlled, derived, do, domain, else, elseif, endcase, endchoose, enddo, endextend, endif, e

28、ndlet, endwhere, extend, forall, if, initially, let, monitored, of, shared, static, then, where, with. The domains TIME, AGENT, X, BOOLEAN, NAT, REAL, TOKEN, DEFINITIONAS1. The functions take, program, Self, undefined, true, false, empty, head, tail, last, length, toSet, parentAS1, parentAS1ofKind,

29、rootNodeAS1. The operation symbols *, +, -set, -seq, =, , , , , , , , , , , See also Figure F3-1 below for an overview of the functions on schedules. Figure F3-1 Signal instances at a gate Operations on schedules To ensure that the order on signals is preserved when new signals are added to the sche

30、dule of a gate, there is a special insertion function insert on schedules. insert(si:SIGNALINST, t:TIME, siSeq:SIGNALINST*): SIGNALINST* =def if siSeq = empty then siSeq elseif t siSeq else insert(si, t, siSeq.tail) 6 Rec. ITU-T Z.100/Annex F3 (10/2016) endif The function insert defines the result o

31、f inserting some signal instance si with the intended arrival time t into a finite signal instance list siSeq, representing (for example) the schedule of a gate. Analogously, a function delete is used to remove a signal from a finite signal instance list siSeq. delete(si:SIGNALINST, siSeq:SIGNALINST

32、*): SIGNALINST* =def if siSeq = empty then empty elseif siSeq.head = si then siSeq.tail else delete(si, siSeq.tail) endif The macros INSERT and DELETE update the schedule of a gate g by assigning some new signal list to g.schedule. INSERT(si:SIGNALINST, t:TIME, g:GATE) g.schedule := insert(si,t,g.sc

33、hedule) si.arrival := t+si.delay DELETE(si:SIGNALINST, g:GATE) g.schedule := delete(si,g.schedule) The function nextSignal yields, for a sequence of signal instances and a signal instance, the next signal instance of the sequence, or the value undefined, if the next signal instance is not determined

34、. nextSignal(si: SIGNALINST, siSeq:SIGNALINST*): SIGNALINST =def if siSeq = empty then undefined elseif siSeq.head = si then if siSeq.tail = empty then undefined else siSeq.tail.head endif else nextSignal(si, siSeq.tail) endif The function selectContinuousSignal yields, for a set of continuous signa

35、l transitions and a set of natural numbers, an element of the transition set with a priority not contained in the set of natural numbers, such that this priority is the maximum priority of all transitions not having priorities in this set of natural numbers. selectContinuousSignal(tSet: SEMTRANSITIO

36、N-set, nSet: NAT-set): SEMTRANSITION =def if t1 tSet: t1.s-NAT nSet then undefined else take(t tSet: t.s-NAT nSet t1 tSet: (t1.s-NAT nSet t.s-NAT t1.s-NAT) endif F3.2.1.1.3 Channels Channels, as declared in a given SDL-2010 specification, consist of either one or two unidirectional channel paths. In

37、 the SAM model, each channel path is identified with an object of a derived domain LINK. The elements of LINK are SAM agents, such that their behaviour is defined through LINK-PROGRAM. LINK =def AGENT LINKSEQ =def LINK* Intuitively, elements of LINK are considered as point-to-point connection primit

38、ives for the transport of signals. More specifically, each l of LINK is able to convey certain signal types, as specified by l.with, from an originating gate l.from to a destination gate l.to, and l.nodelay indicating if l is non-delaying. controlled with: LINK SIGNAL-set Rec. ITU-T Z.100/Annex F3 (

39、10/2016) 7 controlled from: LINK GATE / need to have optional result here, because function is also called within allConnections with general AGENT controlled to: LINK GATE controlled noDelay: LINK NODELAY Signal delays SDL-2010 considers channels as reliable and order-preserving communication links

40、. A channel is able to delay the transport of a signal for an indeterminate and non-constant time interval. Although the exact delaying behaviour is not further specified, the fact that channels are reliable implies that all delays are finite. Signal delays are modelled through a monitored function

41、delay stating the dependency on external conditions and events. In a given SAM state, delay associates finite time intervals from a domain DURATION to the elements of LINK, where the duration of a particular signal delay appears to be chosen non-deterministically. DURATION =def REAL monitored delay:

42、 LINK DURATION Integrity constraints There are two important integrity constraints on the function delay: 1. Taking into account that there are also non-delaying channels, the only admissible value for non-delaying channel paths is 0. 2. For every link agent l, the value of (now + l.delay) increases

43、 monotonically (with respect to now). The second integrity constraint is needed in order to ensure that channel paths are order-preserving: that is, signals transported via the same channel path (and therefore are inserted into the same destination schedule) cannot overtake each other. Channel behav

44、iour A link agent l performs a single operation: signals received at gate l.from are forwarded to gate l.to. That means, l permanently watches l.from waiting for the next deliverable signal in l.from.queue. Whenever l is applicable to a waiting signal si (as identified by the l.from.queue.head), it

45、attempts to remove si from l.from.queue in order to insert it into l.to.schedule. This attempt need not necessarily be successful as, in general, there may be several link agents competing for the same signal si. But, how does a link agent l know whether it is applicable to a signal si? Now, this de

46、cision does of course depend on the values of si.toArg, si.viaArg, si.signalType and l.with. In other words, l is a legal choice for the transportation of si only, if the following two conditions hold: (1) si.signalType l.with and (2) there exists an applicable path connecting l.to to some final des

47、tination that matches with the address information and the path constraints of si. Abstractly, this decision can be expressed using a predicate applicable, defined in clause F3.2.1.1.4. The domain TOARG is defined in clause F3.2.1.1.1. F3.2.1.1.4 Reachability When signals are sent, it has to be dete

48、rmined whether there currently is an applicable communication path: a path consisting of a sequence of links that can transfer the signal, and that satisfies further constraints as specified by the optional to- and via-arguments. The predicate applicable formally states all conditions that must be s

49、atisfied. applicable(s: SIGNAL, toArg: TOARG , viaArg: VIAARG, g: GATE, l: LINK): BOOLEAN =def commPath allConnections (g): ( ll commPath: s ll.with ll.owner undefined) if commPath = empty then l = undefined (g.direction = outDir) 8 Rec. ITU-T Z.100/Annex F3 (10/2016) (toArg = undefined s g.gateAS1.s-Out-signal-identifier-set) (g.direction = inDir) (validDestinationGate(g, toArg) / to self s g.gateAS1.s-In-signal-identifier-set)