ISO/IEC 15909-1:2004/Amd 1:2010
(Amendment)Systems and software engineering — High-level Petri nets — Part 1: Concepts, definitions and graphical notation — Amendment 1: Symmetric Nets
Systems and software engineering — High-level Petri nets — Part 1: Concepts, definitions and graphical notation — Amendment 1: Symmetric Nets
Ingénierie des systèmes et du logiciel — Réseaux de Petri de haut niveau — Partie 1: Concepts, définitions et notation graphique — Amendement 1: Réseaux symétriques
General Information
Relations
Standards Content (Sample)
INTERNATIONAL ISO/IEC
STANDARD 15909-1
First edition
2004-12-01
AMENDMENT 1
2010-05-15
Software and system engineering —
High-level Petri nets —
Part 1:
Concepts, definitions and graphical
notation
AMENDMENT 1: Symmetric Nets
Ingénierie du logiciel et du système — Réseaux de Petri de haut
niveau —
Partie 1: Concepts, définitions et notation graphique
AMENDEMENT 1: Réseaux symétriques
Reference number
ISO/IEC 15909-1:2004/Amd.1:2010(E)
©
ISO/IEC 2010
---------------------- Page: 1 ----------------------
ISO/IEC 15909-1:2004/Amd.1:2010(E)
PDF disclaimer
This PDF file may contain embedded typefaces. In accordance with Adobe's 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 Adobe's 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 were 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 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
ISO's member body in the country of the requester.
ISO copyright office
Case postale 56 • CH-1211 Geneva 20
Tel. + 41 22 749 01 11
Fax + 41 22 749 09 47
E-mail copyright@iso.org
Web www.iso.org
Published in Switzerland
ii © ISO/IEC 2010 – All rights reserved
---------------------- Page: 2 ----------------------
ISO/IEC 15909-1:2004/Amd.1:2010(E)
Foreword
ISO (the International Organization for Standardization) and IEC (the International 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 fields 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 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 Standards adopted
by the joint technical committee 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 document may be the subject of patent rights. ISO
shall 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 15909-1 concerns the addition of a class of high-level nets, known as Symmetric Nets, to
Annex B and the corresponding changes required to the Conformance Clause. Additional references related to Symmetric
Nets are to be included in the Bibliography. Revised Annex B is included in full, due to some minor notational corrections
in clause B.1.
�c ISO/IEC 2010 - All rights reserved iii
---------------------- Page: 3 ----------------------
FINAL 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 notation
AMENDMENT 1: Symmetric Nets
Cover page and page 1
In the document title, replace “Software and system engineering” with “Systems and software engineering”.
Page 19, Conformance
Insert the following subclause after subclause 9.1 (PN Conformance):
9.2 Conformance to Symmetric Nets
This subclause expresses the requirements for a tool implementing high-level Petri nets to conform to the Symmetric Net
class.
9.2.1 Level 1
To claim Level 1 conformance to 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 derived
from the Symmetric Net Graph defined in Annex B.2, by providing a mapping from the implementation’s syntax to the
semantic model in a similar way to that defined in clause 8.
9.2.2 Level 2
To claim Level 2 conformance to the Symmetric Net class of this International Standard, an implementation must satisfy the
requirements for Level 1 conformance to the Symmetric Net class and additionally shall include the syntax of the Symmetric
Net 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 B
Replace normative Annex B with the text starting on the next page, which adds new clause B.2 to define the Symmetric Net
class of High-level Petri Net Graphs (HLPNGs).
�c ISO/IEC 2010 - All rights reserved 1
---------------------- Page: 4 ----------------------
ISO/IEC 15909-1:2004/Amd.1:2010(E)
Annex B
(normative)
Net Classes
The purpose of this Annex is to define various classes of nets as subclasses of the HLPNG. It currently comprises two
clauses: B.1 for Place/Transition nets (without capacities), which is a common form of Petri nets where tokens are simply
‘black dots’; and B.2 for Symmetric Nets, which describes a basic form of coloured Petri nets with simple types that are
amenable to efficient analysis. Other subclasses may include Elementary Net systems and other high-level nets.
B.1 Place/Transition Nets
A Place/Transition net graph (without capacity), PTNG, is a special HLPNG
PTNG=(NG,Sig,V ,H ,Type,AN ,M )
0
where
• NG =(P,T,F) is a net graph
• Sig =(S, O) with S ={Dot,Bool,Mdot}, O ={• ,true ,1 ,2 ,.}
Dot Bool Mdot Mdot
• V =∅
� �
• H =({dot,Boolean,µdot},{•,true,1 •,2 •,.}) a many-sorted algebra for the signature Sig, with dot ={•},
µdot ={{(•,n)}|n ∈ N} andH = dot,H = Boolean,H = µdot, (• ) =•, (true ) = true,
Dot Bool Mdot Dot H Bool H
� �
(1 ) = 1 •, (2 ) = 2 • etc.
Mdot H Mdot H
• 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→{1 ,2 ,.} is a function that annotates each arc with a syntactic ‘positive integer’ constant,
Mdot Mdot
that when evaluated becomes the corresponding multiset overdot.
– TC : T→{true } is a function that annotates every transition with the syntactic constant true (which by
Bool
convention is omitted) that on evaluation is the Boolean valuetrue.
• M : P → µdot.
0
Although this is a rather baroque definition of Place/Transition nets, it can be seen to be in one to one correspondence with
a more usual definition given below.
PTNG=(NG,W ,M )
0
where
• NG =(P,T;F) is a net graph.
+
• W : F → N is the weight function, assigning a positive integer to each arc.
• M : P → N is the initial marking assigning a natural number of tokens to each place. These are represented by dots
0
(•).
This is because:
• the transition condition is true for each transition, and hence doesn’t need to be considered,
2 �c ISO/IEC 2010 - All rights reserved
---------------------- Page: 5 ----------------------
ISO/IEC 15909-1:2004/Amd.1:2010(E)
• the type 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 positive
integers, and
• the number of dots (•) associated with each place (marking) are in one to one correspondence with the Naturals.
B.2 Symmetric Nets
B.2.1 Introduction
Symmetric 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 built from them. Basic types
are classified as unordered, linearly ordered or circular. This classification depends on the functions that are associated with
the type as defined below (see subclause B.2.5).
A symmetric net graph, SNG, is a special HLPNG
SNG=(NG,Sig,V ,H ,Type,AN ,M )
0
with the following restrictions on the signature Sig =(S, O), algebra, H =(S ,O ), typing function, Type, and arc
H H
annotations, AN. The set of sorts, S, is partitioned to reflect the structure of the types of Symmetric Net Graphs. The
allowed operators are defined for the sorts (including explicit operators for multiset constants). The restrictions on S are
H
determined by defining all the allowable types. Then the allowable set of functions are defined, which enables the set of
functions comprising O to be determined.
H
B.2.2 Sorts
Symmetric Net Graphs allow the use of three kinds of basic sorts: Usorts, LOsorts and Csorts which are disjoint and
where Bool ∈ Usorts∪LOsorts. Basic sorts are defined as the union:
BasicSorts = Usorts∪ LOsorts∪ Csorts.
A product sort may be created for each combination of basic sorts:
∗
Psorts⊆{PROD | σ∈ BasicSorts andLength(σ)≥ 2}
σ
where Length is a function that takes a string and returns its length.
A multiset sort may be created for each basic sort and product sort:
Msorts⊆{s | s∈ BasicSorts∪Psorts}.
ms
Finally, there is the special dedicated sort, nat, (that is always interpreted as the Natural numbers, N, in the algebra) which
is required for various operations involvingMsorts.
Hence the set of sorts, S, is given by
S = Usorts∪ LOsorts∪ Csorts∪Psorts∪ Msorts∪{nat}.
B.2.3 Operators
Operators for LOsorts
Comparison operators are defined for each sort in LOsorts:
CompOps ={< ,≤ ,> ,≥ | s∈ LOsorts}
(s.s,Bool) (s.s,Bool) (s.s,Bool) (s.s,Bool)
NOTE 1: Infix notation is used for these comparison operators.
Operators for Csorts:
A set of unary operators is defined for each sort in Csorts:
CircularOps ={Succ ,Pred | s∈ Csorts}.
(s,s) (s,s)
�c ISO/IEC 2010 - All rights reserved 3
---------------------- Page: 6 ----------------------
ISO/IEC 15909-1:2004/Amd.1:2010(E)
Specific Operators on Basic Sorts:
The following specific operators are defined for basic sorts:
• Operators for Bool:
BoolOps ={not ,and ,or ,implies };
(Bool,Bool) (Bool.Bool,Bool) (Bool.Bool,Bool) (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∈ BasicSorts, lo∈ LOsorts};
(b,lo)
NOTE 3: Symmetric nets are based on “well formed nets” (see Bibliography items 25 and 26). The intent of this
operator 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 ={() | σ∈ BasicSorts ,PROD ∈ Psorts}.
(σ,PROD ) σ
σ
NOTE 4: Tupling operators are required to allow us to write a tuple on an arc. The convention is adopted to use outfix
notation, 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 component of a tuple:
i
ProjectionOps ={Proj | i∈{1,.,n},n > 1,b .b ∈ BasicSorts,and
1 n
(PROD ,b )
(b .b ) i
n
1
PROD ∈ Psorts}
(b .b )
1 n
Operators for both Basic Sorts and Product Sorts:
• Equality Predicate:
EqualityOps ={= | s∈ BasicSorts∪Psorts};
(s.s,Bool)
• A set of conversion operators with output sorts in Msorts:
Convert2MOps ={� | s∈ BasicSorts∪Psorts,s ∈ Msorts}.
(nat.s,s ) ms
ms
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∈ Msorts};
(s.s,s) (s.s,s)
• Scaling Operation:
MscalingOps ={∗ | s∈ Msorts};
(nat.s,s)
• Predicates for equality and comparison:
Mpredicates ={= ,≤ | s∈ Msorts};
(s.s,Bool) (s.s,Bool)
• Cardinality operation:
Mcardinality ={|| | s∈ Msorts}.
(s,nat)
NOTE 6: Infix Notation is used for multiset operations, except for cardinality which uses Outfix notation.
Constants for all sorts
A set called Constants is defined which contains constants of any sort. In particular, it includes dedicated constants:
• BoolConstants⊂ Constants where BoolConstants ={true ,false };
Bool Bool
4 �c ISO/IEC 2010 - All ri
...
Questions, Comments and Discussion
Ask us and Technical Secretary will try to provide an answer. You can facilitate discussion about the standard in here.