CAN CSA-ISO IEC 15909-1A-2012 Software and system engineering - High-level Petri nets - Part 1 Concepts definitions and graphical notation - AMENDMENT 1 Symmetric Nets.pdf

1、Software and system engineering High-level Petri nets Part1:Concepts,definitionsandgraphicalnotation AMENDMENT1:SymmetricNetsAmendment 1:2012 (IDT) toNational Standard of CanadaCAN/CSA-ISO/IEC 15909-1-05(ISO/IEC 15909-1:2004, IDT)NOT FOR RESALE.PUBLICATION NON DESTINE LA REVENTE.CSA Standards Update

2、 ServiceAmendment 1:2012 toCAN/CSA-ISO/IEC 15909-1-05March 2012Title:Software and system engineering High-level Petri nets Part1:Concepts,definitionsandgraphicalnotation AMENDMENT1:SymmetricNetsPagination:13 pages (iii preliminary and 10 text)To register for e-mail notification about any updates to

3、this publication go on-line to shop.csa.caclick on E-mail Services under MY ACCOUNTclick on CSA Standards Update ServiceThe List ID that you will need to register for updates to this publication is 2417460.If you require assistance, please e-mail techsupportcsa.ca or call 416-747-2233.Visit CSAs pol

4、icy on privacy at csagroup.org/legal to find out how we protect your personal information.Reference numberISO/IEC 15909-1:2004/Amd.1:2010(E)ISO/IEC 2010INTERNATIONAL STANDARDISO/IEC15909-1First edition2004-12-01AMENDMENT 12010-05-15Software and system engineering High-level Petri nets Part 1: Concep

5、ts, definitions and graphical notation AMENDMENT 1: Symmetric Nets Ingnierie du logiciel et du systme Rseaux de Petri de haut niveau Partie 1: Concepts, dfinitions et notation graphique AMENDEMENT 1: Rseaux symtriques ISO/IEC 15909-1:2004/Amd.1:2010(E) PDF disclaimer This PDF file may contain embedd

6、ed typefaces. In accordance with Adobes 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 no

7、t infringing Adobes licensing policy. 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 we

8、re optimized for printing. Every care 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. COPYRIGHT PROTECTED DOCUMENT ISO/IEC 2010 All rights

9、reserved. Unless otherwise specified, no part of this publication 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 re

10、quester. ISO copyright office Case postale 56 CH-1211 Geneva 20 Tel. + 41 22 749 01 11 Fax + 41 22 749 09 47 E-mail copyrightiso.org Web www.iso.org ii ISO/IEC 2010 All rights reservedAmendment 1:2012 to CAN/CSA-ISO/IEC 15909-1-05ISO/IEC 15909-1:2004/Amd.1:2010(E)ForewordISO (the International Organ

11、ization for Standardization) and IEC (the International Electrotechnical Commission) formthe specialized system for worldwide standardization. National bodies that are members of ISO or IEC participate in thedevelopment of International Standards through technical committees established by the respe

12、ctive organization to dealwith particular fields of technical activity. ISO and IEC technical committees collaborate in fields of mutual interest. Otherinternational organizations, governmental and non-governmental, in liaison with ISO and IEC, also take part in the work. Inthe field of information

13、technology, ISO and IEC have established a joint technical committee, ISO/IEC JTC 1.International Standards are drafted in accordance with the rules given in the ISO/IEC Directives, Part 2.The main task of the joint technical committee is to prepare International Standards. Draft International Stand

14、ards adoptedby the joint technical committee are circulated to national bodies for voting. Publication as an International Standard requiresapproval by at least 75 % of the national bodies casting a vote.Attention is drawn to the possibility that some of the elements of this document may be the subj

15、ect of patent rights. ISOshall not be held responsible for identifying any or all such patent rights.Amendment 1 to ISO/IEC 15909-1:2004 was prepared by Joint Technical Committee ISO/IEC JTC 1, Information technol-ogy, Subcommittee SC 7, Software and systems engineering.This amendment to ISO/IEC 159

16、09-1 concerns the addition of a class of high-level nets, known as Symmetric Nets, toAnnex B and the corresponding changes required to the Conformance Clause. Additional references related to SymmetricNets are to be included in the Bibliography. Revised Annex B is included in full, due to some minor

17、 notational correctionsin clause B.1.cISO/IEC 2010 - All rights reserved iiiAmendment 1:2012 to CAN/CSA-ISO/IEC 15909-1-05FINAL DRAFT AMENDMENT ISO/IEC 15909-1:2004/Amd.1:2010(E)Software and system engineering High-level Petri nets Part 1:Concepts, definitions and graphical notationAMENDMENT 1: Symm

18、etric NetsPage 19, ConformanceInsert the following subclause after subclause 9.1 (PN Conformance):9.2 Conformance to Symmetric NetsThis subclause expresses the requirements for a tool implementing high-level Petri nets to conform to the Symmetric Netclass.9.2.1 Level 1To claim Level 1 conformance to

19、 the Symmetric Net class of this International Standard, an implementation shall demon-strate that it has the semantics defined in clause 4, with the types (domains) and pre and post functions that can be derivedfrom the Symmetric Net Graph defined in Annex B.2, by providing a mapping from the imple

20、mentations syntax to thesemantic model in a similar way to that defined in clause 8.9.2.2 Level 2To claim Level 2 conformance to the Symmetric Net class of this International Standard, an implementation must satisfy therequirements for Level 1 conformance to the Symmetric Net class and additionally

21、shall include the syntax of the SymmetricNet Graph defined in Annex B.2 and the notational conventions of clause 7.Change the numbering of HLPN Conformance to subclause 9.3.Page 25, Annex BReplace normative Annex B with the text starting on the next page, which adds new clause B.2 to define the Symm

22、etric Netclass of High-level Petri Net Graphs (HLPNGs).cISO/IEC 2010 - All rights reserved 1Cover page and page 1In the document title, replace “Software and system engineering” with “Systems and software engineering”.Amendment 1:2012 to CAN/CSA-ISO/IEC 15909-1-05ISO/IEC 15909-1:2004/Amd.1:2010(E)An

23、nex B(normative)Net ClassesThe purpose of this Annex is to define various classes of nets as subclasses of the HLPNG. It currently comprises twoclauses: B.1 for Place/Transition nets (without capacities), which is a common form of Petri nets where tokens are simplyblack dots; and B.2 for Symmetric N

24、ets, which describes a basic form of coloured Petri nets with simple types that areamenable to efficient analysis. Other subclasses may include Elementary Net systems and other high-level nets.B.1 Place/Transition NetsA Place/Transition net graph (without capacity), PTNG, is a special HLPNGPTNG =(NG

25、,Sig,V ,H,Type,AN,M0)where NG =(P,T,F) is a net graph Sig =(S, O) with S = Dot,Bool,Mdot, O = Dot,trueBool,1Mdot,2Mdot,. V = H =(dot,Boolean,dot,true,1primereverse,2primereverse,.) a many-sorted algebra for the signature Sig, with dot = ,dot = (,n)|n N and HDot= dot, HBool= Boolean, HMdot= dot, (Dot

26、)H= , (trueBool)H= true,(1Mdot)H= 1primereverse, (2Mdot)H= 2primereverse etc. Type : P dot,Boolean,dot is a function that assigns the type dot to all places (p P,Type(p)=dot). AN =(A,TC) is a pair of net annotations. A : F 1Mdot,2Mdot,. is a function that annotates each arc with a syntactic positive

27、 integer constant,that when evaluated becomes the corresponding multiset over dot. TC : T trueBool is a function that annotates every transition with the syntactic constant true (which byconvention is omitted) that on evaluation is the Boolean value true. M0: P dot.Although this is a rather baroque

28、definition of Place/Transition nets, it can be seen to be in one to one correspondence witha more usual definition given below.PTNG =(NG,W ,M0)where NG =(P,T;F) is a net graph. W : F N+is the weight function, assigning a positive integer to each arc. M0: P N is the initial marking assigning a natura

29、l number of tokens to each place. These are represented by dots().This is because: the transition condition is true for each transition, and hence doesnt need to be considered,2 cISO/IEC 2010 - All rights reservedAmendment 1:2012 to CAN/CSA-ISO/IEC 15909-1-05ISO/IEC 15909-1:2004/Amd.1:2010(E) the ty

30、pe of each place is the same, comprising a single value , and hence there is no need for typing places, the number of dots () associated with each arc (Weight function) are in one to one correspondence with the positiveintegers, and the number of dots () associated with each place (marking) are in o

31、ne to one correspondence with the Naturals.B.2 Symmetric NetsB.2.1 IntroductionSymmetric Net Graphs place restrictions on the many-sorted algebra of HLPNGs. Firstly, the carriers of the algebra (Types)are finite. Secondly, basic types are defined and then further types (products and multisets) are b

32、uilt from them. Basic typesare classified as unordered, linearly ordered or circular. This classification depends on the functions that are associated withthe type as defined below (see subclause B.2.5).A symmetric net graph, SNG, is a special HLPNGSNG =(NG,Sig,V ,H,Type,AN,M0)with the following res

33、trictions on the signature Sig =(S, O), algebra, H =(SH,OH), typing function, Type, and arcannotations, AN. The set of sorts, S, is partitioned to reflect the structure of the types of Symmetric Net Graphs. Theallowed operators are defined for the sorts (including explicit operators for multiset con

34、stants). The restrictions on SHaredetermined by defining all the allowable types. Then the allowable set of functions are defined, which enables the set offunctions comprising OHto be determined.B.2.2 SortsSymmetric Net Graphs allow the use of three kinds of basic sorts: Usorts, LOsorts and Csorts w

35、hich are disjoint andwhere Bool Usorts LOsorts. Basic sorts are defined as the union:BasicSorts = UsortsLOsorts Csorts.A product sort may be created for each combination of basic sorts:Psorts PROD| BasicSortsand Length() 2where Length is a function that takes a string and returns its length.A multis

36、et sort may be created for each basic sort and product sort:Msorts sms|s BasicSorts Psorts.Finally, there is the special dedicated sort, nat, (that is always interpreted as the Natural numbers, N, in the algebra) whichis required for various operations involving Msorts.Hence the set of sorts, S, is

37、given byS = Usorts LOsorts Csorts Psorts Msortsnat.B.2.3 OperatorsOperators for LOsortsComparison operators are defined for each sort in LOsorts:CompOps = (s.s,Bool),(s.s,Bool)|s LOsortsNOTE 1: Infix notation is used for these comparison operators.Operators for Csorts:A set of unary operators is def

38、ined for each sort in Csorts:CircularOps = Succ(s,s),Pred(s,s)|s Csorts.cISO/IEC 2010 - All rights reserved 3Amendment 1:2012 to CAN/CSA-ISO/IEC 15909-1-05ISO/IEC 15909-1:2004/Amd.1:2010(E)Specific Operators on Basic Sorts:The following specific operators are defined for basic sorts: Operators for B

39、ool:BoolOps = not(Bool,Bool),and(Bool.Bool,Bool),or(Bool.Bool,Bool),implies(Bool.Bool,Bool);NOTE 2: Infix notation is used for binary operators. A set of unary operators with output sorts in LOsorts:PartitioningOps = PartitionOp(b,lo)|b BasicSorts, lo LOsorts;NOTE 3: Symmetric nets are based on “wel

40、l formed nets” (see Bibliography items 25 and 26). The intent of thisoperator is to allow the notion of “static subclasses” introduced for “well formed nets” to be used in Symmetric nets. A set of tupling operators with output sorts in Psorts:TuplingOps = ()(,P ROD)| BasicSorts,PROD Psorts.NOTE 4: T

41、upling operators are required to allow us to write a tuple on an arc. The convention is adopted to use outfixnotation, where the additional set of parenthesis is dropped, e.g. (x, y, z) is written (x, y, z).Projection Operators on Product Sorts:A set of projection operators that select the ith compo

42、nent of a tuple:ProjectionOps = Proji(PROD(b1.bn),bi)|i 1,.,n,n1,b1.bn BasicSorts, andPROD(b1.bn) PsortsOperators for both Basic Sorts and Product Sorts: Equality Predicate:EqualityOps = =(s.s,Bool)|s BasicSorts Psorts; A set of conversion operators with output sorts in Msorts:Convert2MOps = primere

43、verse(nat.s,sms)|s BasicSorts Psorts,sms Msorts.NOTE 5: As usual, the convention is adopted to use infix notation for these operators.Operators on Multiset Sorts:The following operators are defined for multiset sorts: Addition and subtraction operations:MbinaryOps = +(s.s,s),(s.s,s)|s Msorts; Scalin

44、g Operation:MscalingOps= (nat.s,s)|s Msorts; Predicates for equality and comparison:Mpredicates = =(s.s,Bool),(s.s,Bool)|s Msorts; Cardinality operation:Mcardinality = |(s,nat)|s Msorts.NOTE 6: Infix Notation is used for multiset operations, except for cardinality which uses Outfix notation.Constant

45、s for all sortsA set called Constants is defined which contains constants of any sort. In particular, it includes dedicated constants: BoolConstants Constants where BoolConstants = trueBool,falseBool;4 cISO/IEC 2010 - All rights reservedAmendment 1:2012 to CAN/CSA-ISO/IEC 15909-1-05ISO/IEC 15909-1:2

46、004/Amd.1:2010(E) NatConstants Constants where NatConstants = 0nat, 1nat, 2nat,.;NOTE 7: Natural constants are required for multiset scaling and conversion. for s Msorts,alls,emptys Constants.NOTE 8: allsdenotes (in the algebra) a multiset with exactly one occurrence of each element of its basis set

47、.Set of allowed Operators:All the operators (and constants) defined above are gathered into the set OpsSN. Then O OpsSN, where the input and output sorts of each operator must be in S; and only one unary operator with output sort in LOsorts is allowed for each basic sort: for b1,b2 BasicSorts andlo1

48、,lo2 LOsorts, o(b1,lo1),o(b2,lo2) O and o(b1,lo1)negationslash= o(b2,lo2)implies b1 negationslash= b2.NOTE 9: The rationale for this restriction is to enable the use of symbolic reachability graph techniques.B.2.4 TypesIn the algebra, H =(SH,OH), a type is associated with each sort, i.e. SH= Hs|s S.

49、 The corresponding sets of typesin the algebra are: UnorderedTypes = Hs|s Usorts; LinearOTypes = Hs|s LOsorts; CircularTypes = Hs|s Csorts; ProductTypes = Hs|s Psorts; MultisetTypes = Hs|s Msorts; Hnat= N; HBool= Boolean.Basic types:BasicTypes = UnorderedTypes LinearOTypes CircularTypes.BasicTypes is the