CAN CSA-ISO IEC 10746A-4-2001 Information technology - Open Distributed Processing - Reference Model Architectural semantics AMENDMENT 1 Computational formalization.pdf

1、 Reference number ISO/IEC 10476-4:1998/Amd.1:2001(E)ISO/IEC 2001 Information technology Open Distributed Processing Reference Model: Architectural semantics AMENDMENT 1: Computational formalization Technologies de linformation Traitement rparti ouvert Modle de rfrence: Smantique architecturale AMEND

2、EMENT 1: Formalisation informatique Amendment 1:2003 toNational Standard of CanadaCAN/CSA-ISO/IEC 10746-4-01Amendment 1:2001 to International Standard ISO/IEC 10746-4:1998 has been adopted without modification asAmendment 1:2003 to CAN/CSA-ISO/IEC 10746-4-01. This Amendment was reviewed by the CSA T

3、echnicalCommittee on Information Technology (TCIT) under the jurisdiction of the Strategic Steering Committee onInformation Technology and deemed acceptable for use in Canada.July 2003ISO/IEC 10746-4:1998/Amd.1:2001(E) PDF disclaimer This PDF file may contain embedded typefaces. In accordance with A

4、dobes licensing policy, this file may be printed or viewed but shall not be edited unless the typefaces which are embedded are licensed to and installed on the computer performing the editing. In downloading this file, parties accept therein the responsibility of not infringing Adobes licensing poli

5、cy. The ISO Central Secretariat accepts no liability in this area. Adobe is a trademark of Adobe Systems Incorporated. Details of the software products used to create this PDF file can be found in the General Info relative to the file; the PDF-creation parameters were optimized for printing. Every c

6、are has been taken to ensure that the file is suitable for use by ISO member bodies. In the unlikely event that a problem relating to it is found, please inform the Central Secretariat at the address given below. ISO/IEC 2001 All rights reserved. Unless otherwise specified, no part of this publicati

7、on may be reproduced or utilized in any form or by any means, electronic or mechanical, including photocopying and microfilm, without permission in writing from either ISO at the address below or ISOs member body in the country of the requester. ISO copyright office Case postale 56 CH-1211 Geneva 20

8、 Tel. + 41 22 749 01 11 Fax + 41 22 749 09 47 E-mail copyrightiso.ch Web www.iso.ch Published by ISO in 2002 ii ISO/IEC 2001 All rights reserved ISO/IEC 10746-4:1998/Amd.1:2001(E) ISO/IEC 2001 All rights reserved iiiCONTENTSPage1) Introduction 12) Clause 1 Scope . 13) Clause 2 Normative references .

9、 24) Subclause 3.2 Definitions from ITU-T Recommendation Z.100 25) Subclause 3.3 Definitions from the Z-Base Standard 26) Annex A 3Annex A Computational Formalization. 3A.1 Formalization of the Computational Viewpoint Language in LOTOS 3A.2 Formalization of the Computational Viewpoint Language in SD

10、L. 12A.3 Formalization of the Computational Viewpoint Language in Z . 20A.4 Formalization of the Computational Viewpoint Language in ESTELLE 28ISO/IEC 10746-4:1998/Amd.1:2001(E) iv ISO/IEC 2001 All rights reserved Foreword ISO (the International Organization for Standardization) and IEC (the Interna

11、tional Electrotechnical Commission) form the specialized system for worldwide standardization. National bodies that are members of ISO or IEC participate in the development of International Standards through technical committees established by the respective organization to deal with particular fiel

12、ds of technical activity. ISO and IEC technical committees collaborate in fields of mutual interest. Other international organizations, governmental and non-governmental, in liaison with ISO and IEC, also take part in the work. In the field of information technology, ISO and IEC have established a j

13、oint technical committee, ISO/IEC JTC 1. International Standards are drafted in accordance with the rules given in the ISO/IEC Directives, Part 3. The main task of the joint technical committee is to prepare International Standards. Draft International Standards adopted by the joint technical commit

14、tee are circulated to national bodies for voting. Publication as an International Standard requires approval by at least 75 % of the national bodies casting a vote. Attention is drawn to the possibility that some of the elements of this Amendment may be the subject of patent rights. ISO and IEC shal

15、l not be held responsible for identifying any or all such patent rights. Amendment 1 to International Standard ISO/IEC 10746-4:1998 was prepared by Joint Technical Committee ISO/IEC JTC 1, Information technology, Subcommittee SC 7, Software engineering, in collaboration with ITU-T. The identical tex

16、t is published as ITU-T Rec. X.904/Amd.1. ISO/IEC 10746-4:1998/Amd.1:2001 (E)ITU-T Rec. X.904/Amd.1 (2000 E) 1INTERNATIONAL STANDARDISO/IEC 10746-4:1998/Amd.1:2001 (E)ITU-T Rec. X.904/Amd.1 (2000 E)ITU-T RECOMMENDATIONINFORMATION TECHNOLOGY OPEN DISTRIBUTED PROCESSING REFERENCE MODEL: ARCHITECTURAL

17、SEMANTICSAMENDMENT 1Computational formalization1) IntroductionReplace the lst paragraph of the introductionThis Recommendation | International Standard is an integral part of the ODP Reference Model. It contains aformalisation of the ODP modelling concepts defined in ITU-T Rec. X.902 | ISO/IEC 10746

18、-2, clauses 8 and 9. Theformalisation is achieved by interpreting each concept in terms of the constructs of the different standardised formaldescription techniques.withThis Recommendation | International Standard is an integral part of the ODP Reference Model. It contains aformalization of the ODP

19、modelling concepts defined in ITU-T Rec. X.902 | ISO/IEC 10746-2, clauses 8 and 9 and inITU-T Rec. X.903 | ISO/IEC 10746-3, clause 7 (Computational Language). The formalization is achieved by interpretingeach concept in terms of the constructs of the different standardized formal description techniq

20、ues.2) Clause 1 ScopeReplace the fourth bullet under The RM-ODP consists ofITU-T Rec. X.904 | ISO/IEC 10746-4: Architectural Semantics: contains a formalisation of the ODP modellingconcepts defined in ITU-T Rec. X.902 | ISO/IEC 10746-2, clauses 8 and 9, and a formalisation of the viewpointlanguages

21、of ITU-T Rec. X.903 | ISO/IEC 10746-3. The formalisation is achieved by interpreting each concept in termsof the constructs of the different standardised formal description techniques. This text is normative.withITU-T Rec. X.904 | ISO/IEC 10746-4: Architectural Semantics: contains a formalization of

22、 the ODP modellingconcepts defined in ITU-T Rec. X.902 | ISO/IEC 10746-2, clauses 8 and 9, and a formalization of the computationalviewpoint language of ITU-T Rec. X.903 | ISO/IEC 10746-3. The formalization is achieved by interpreting each conceptin terms of the constructs of the different standardi

23、zed formal description techniques. This text is normative.Replace the fourth paragraphThe purpose of this Recommendation | International Standard is to provide an architectural semantics for ODP. Thisessentially takes the form of an interpretation of the basic modelling and specification concepts of

24、 ITU-T Rec. X.902 |ISO/IEC 10746-2 and the viewpoint languages of ITU-T Rec. X.903 | ISO/IEC 10746-3, using the various features ofdifferent formal specification languages. An architectural semantics is developed in four different formal specificationlanguages: LOTOS, ESTELLE, SDL and Z. The result

25、is a formalisation of ODPs architecture. Through a process ofiterative development and feedback, this has improved the consistency of ITU-T Rec. X.902 | ISO/IEC 10746-2 andITU-T Rec. X.903 | ISO/IEC 10746-3.withThe purpose of this Recommendation | International Standard is to provide an architectura

26、l semantics for ODP. Thisessentially takes the form of an interpretation of the basic modelling and specification concepts of ITU-T Rec. X.902 |ISO/IEC 10746-2 and the computational viewpoint language of ITU-T Rec. X.903 | ISO/IEC 10746-3, using the variousfeatures of different formal specification

27、languages. An architectural semantics is developed in four different formal2 ITU-T Rec. X.904/Amd.1 (2000 E)specification languages: LOTOS, ESTELLE, SDL and Z. The result is a formalization of ODPs architecture. Through aprocess of iterative development and feedback, this has improved the consistenc

28、y of ITU-T Rec. X.902 |ISO/IEC 10746-2 and ITU-T Rec. X.903 | ISO/IEC 10746-3.Add the following paragraph at the end of Scope:Annex A shows one way in which the computational viewpoint language of ITU-T Rec. X.903 | ISO/IEC 10746-3 can berepresented in the formal languages LOTOS, SDL, Z and Estelle.

29、 This Recommendation | International Standard alsomakes use of the concepts defined in ITU-T Rec. X.902 | ISO/IEC 10746-2.3) Clause 2 Normative referencesChange publication date for ITU-T Recommendation Z.100 from (1993) to (1999).ISO/IEC 13568:Add the following reference:Z Notation, ISO/IEC JTC 1 S

30、C 22 WG 19 Advanced Working Draft 2.C, July 13th 1999.4) Subclause 3.2 Definitions from ITU-T Recommendation Z.100Replace the list with the following terms:active, adding, all, alternative, and, any, as, atleast, axioms, block, call, channel, comment, connect, connection,constant, constants, create,

31、 dcl, decision, default, else, endalternative, endblock, endchannel, endconnection,enddecision, endgenerator, endnewtype, endoperator, endpackage, endprocedure, endprocess, endrefinement, endselect,endservice, endstate, endsubstructure, endsyntype, endsystem, env, error, export, exported, external,

32、fi, finalized, for,fpar, from, gate, generator, if, import, imported, in, inherits, input, interface, join, literal, literals, map, mod, nameclass,newtype, nextstate, nodelay, noequality, none, not, now, offspring, operator, operators, or, ordering, out, output,package, parent, priority, procedure,

33、process, provided, redefined, referenced, refinement, rem, remote, reset, return,returns, revealed, reverse, save, select, self, sender, service, set, signal, signallist, signalroute, signalset, spelling, start,state, stop, struct, substructure, synonym, syntype, system, task, then, this, timer, to,

34、 type, use, via, view, viewed, virtual,with, xor.5) Subclause 3.3 Definitions from the Z-Base StandardChange subclause title to:3.3 Definitions from the Z Notation.Replace the list with following terms:axiomatic description, data refinement, hiding, operation refinement, overriding, schema (operatio

35、n, state, framing),schema calculus, schema composition, sequence, type.ISO/IEC 10746-4:1998/Amd.1:2001 (E)ISO/IEC 10746-4:1998/Amd.1:2001 (E)ITU-T Rec. X.904/Amd.1 (2000 E) 36) Annex AAdd a new Annex A as follows:Annex AComputational FormalizationA.1 Formalization of the Computational Viewpoint Lang

36、uage in LOTOSA.1.1 ConceptsThe formalization of the computational language in LOTOS uses the concepts defined in the formalization of the basicmodelling and structuring rules given in ITU-T Rec. X.902 | ISO/IEC 10746-2 clauses 8 and 9.Elementary Structures Associated with Operational and Signal Inte

37、rfacesTo formalize the computational language in LOTOS it is necessary to introduce certain elementary structures. Theseinclude parameters that might be associated with certain computational interfaces and a basic model of information thatmight be used in a stream flow.To formalize parameters it is

38、necessary to introduce two concepts: names for things and types for things. Names aresimply labels. As we shall see, the computational viewpoint requires that checks, e.g. for equality, are done on theselabels when interfaces are constructed. We may represent names generally by:type Name is Booleans

39、orts Nameopns newName: - NameanotherName: Name - Name_eq_,_ne_: Name, Name - Boolendtype(*Name*)For brevity sake we omit the equations, which are expected to be obvious. It is possible to be more prescriptive here, e.g.using character strings from the LOTOS library. The only thing we are interested

40、in regarding names is that we candetermine their equality or inequality.As discussed in this Recommendation | International Standard, a type in the ODP sense may not be interpreted directly inthe process algebra part of LOTOS. It is however possible to model types through the Act One part of LOTOS.U

41、nfortunately, whilst Act One was designed specifically for representing types, it is limited in the ways in which typesand types relationships are checked. For example, it is not possible to check subtyping or equivalence up to isomorphismbetween types due to type equality in Act One being based on

42、name equivalence of sorts. As a basis for reasoning herewe introduce an elementary notion of types that allows us to test for equality, inequality and subtyping.type AnyType is Booleansorts AnyTypeopns newType: - AnyTypeanotherType: AnyType - AnyType_eq_,_isSubtype_: AnyType, AnyType - Boolendtype (

43、* AnyType *)A parameter is a relation between a name and its underlying type representation. Thus a parameter may be representedby:type Param is Name, AnyTypesorts Paramopns newParam: Name, AnyType - Param_eq_,_ne_,_isSubtype_: Param, Param - Boolendtype (* Param *)As previously, we require checks o

44、n the equality or inequality of parameters as well as when one parameter is a subtypeof another. Two parameters are in a subtype relationship when their types are in a subtype relationship. It is also usefulfor us to introduce sequences of these parameters.type PList is String actualizedby Paramusin

45、g sortnames PList for String Param for Element Bool for FBoolopns _isSubtype_: PList, PList - Boolendtype (* PList *)4 ITU-T Rec. X.904/Amd.1 (2000 E)Here we use the type String from the LOTOS library actualised with the type Param defined previously. We also includean operation here isSubtype that

46、can check whether one sequence of parameters is a subtype of another. One parameterlist is a subtype of a second when all of the parameters it contains are subtypes of those found in the first. In addition theparameters should be in the same position in their respective lists. It should be noted tha

47、t these parameters might containreferences to interfaces used to restrict the interactions that can take place. Whilst it is quite possible to model aninterface in the process algebra, it is not possible to model a reference to that interface in the process algebra that, looselyspeaking, captures th

48、e functionality of that interface. To overcome this, we model interface references in Act One. Giventhat an interface reference captures, amongst other things, the signature of the interface, we provide an Act One model ofsignatures for operations. Operations consist of a name, a sequence of inputs

49、and possibly a sequence of outputs. Forsimplicitys sake, we do not consider here whether the operation is of infix, prefix or suffix notation. This may berepresented by:type Op is Name, PListsorts Opopns makeOp: Name, PList - OpmakeOp: Name, PList, PList - OpgetName: Op - NamegetInps: Op - PListgetOuts: Op - PList_eq_: Op, Op - Booleqns forall op1,op2: Op, n: Name; pl1, pl2: PListofsort Name getName(makeOp(n,pl1,pl2) = n;ofsort PList getInps(makeOp(n,pl1) = pl1;getInps(makeOp(n,pl1,pl2) = pl1;getOuts(makeOp(n,pl1) = IRefNULL : -