当前位置:首页 >> >>

2002 Society for Design and Process Science Printed in the United States of America PETRI N


2002 Society for Design and Process Science Printed in the United States of America

PETRI NET MODULES

Julia Padberg* *Technical University Berlin Institute for Software Engineering and Theoretical Computer Science Germany email: padberg@cs.tu-berlin.de

Abstract: Here we present a new module concept for Petri nets that is based on the component concepts of Continuous Software Engineering (CSE). According to that concept two distinguished interfaces are required. These are import and export interfaces. The import describes the assumptions on the environment, e.g. in terms of used components. The export gives an abstraction of the functionality and presents e.g. the offered services. The modules for Petri we introduce here consist of three nets for the import, the body of the module and the export. The import net ??? states the prerequisites the modules assumes. The body net ? represents ? gives an abstraction of the body that can be used by the the internal functionality. The export net environment. We provide module operations to compose larger modules from basic ones. Operations to compose Petri net modules are crucial as the main purpose is composition. In most approaches module concepts come along with just one operation. A great advantage is achieved having different possibilities to compose modules, as it increases the convenience of modeling large systems. We propose three different operations, composition, disjoint union, and union. Our main result in this contribution is that these module operations are compatible with each other.

1. Introduction
The main motivation for Petri net modules is the modeling of component-based systems. Software components are an useful and widely accepted abstraction mechanism. Components are deployed during the entire software life cycle, from analysis to maintenance. The component concept as suggested in (M¨ ller u and Weber, 1998; Weber, 1999) for Continuous Software Engineering (CSE) is the basic concept for our approach. Especially in early software development phases modeling with Petri nets is a common approach. Unfortunately Petri nets do not yet support this component idea. In this paper we present Petri net modules as an abstraction mechanism that corresponds to the component concept of CSE. This concept is realized for Petri Transactions of the SDPS SEPTEMBER 2002, Vol. 6, No. 3, pp. 121-96

nets using the following basic ideas:
? Components consist of three nets: the import net ??? , the export net ? , and the body net ? . The import net presents those parts of the net that need to be provided from the ”outside”. The export net is that what the net module presents to the ”outside. The body is the realization of the export using the import. ? The relation between import ??? and body ? is given by a plain morphism. Export ? and body ? are related by a substitution morphism, that allows mapping one transition to a subnet. ? Different module operations are required for the ?exible composition of modules. At the moment we have union of modules and composition of modules. ? Compatibility between the operations needs to be guaranteed. Provided some conditions are satis?ed the result of ?rst union and then composition or vice versa is the same up to isomorphism. ? The original algebraic module concept is based on a loose semantics. Up to now there is no loose semantics de?ned for Petri nets or other Petri net classes. This is future research and will be investigated in forthcoming papers.

In the area of Petri nets various structuring concepts have been proposed during the last 40 years, some of these are even called modules or modular approach. On the one hand there are hierarchical concepts (e.g. (Jensen, 1992; Buchholz, 1994; He, 1996; Fehling, 1993)). The system is described in an abstract net, while special functionalities are encapsulated into subnets and called like procedures by merging transitions or places and exchange of tokens. On the other hand there is a large variety of connector mechanisms between modules.The communication, coordination or cooperation among components via signals is given by a relation between input and output (e.g. (Christinsen and Hansen, 1994; Sibertin-Blanc, 1994; Desel et al., 2000; Deiters and Gruhn, 1994)). In this way the exchange of tokens or only read-operation of modules is described by special features like read arcs, inhibitor arcs etc. In other approaches places and transitions of modules are merged by well-de?ned operations (e.g. (Kindler, 1995; Battiston et al., 1991b; Battiston et al., 1991a; Broy and Streicher, 1992)). In contrast to these our approach is based on concepts of Continuous Software Engineering (CSE). The advantage is that we must not extend the underlying formalism of Petri nets, but compose modules by means of a connector component. Moreover, there are no approaches that provide different composition operations with explicit compatibility results and composition operations are usually only given implicitly. The approach to Petri net modules as presented in this paper is closely related to algebraic speci?cation modules (Ehrig and Mahr, 1990). Their impact for practical concepts in software engineering has been relevant from the beginning (Weber and Ehrig, 1988). The transfer of these concepts to process description techniques is a recent development. It has been started in (Simeoni, 1999) where modules for graph transformation systems and local action systems have been investigated. A general framework for component concepts based on High-Level Replacement Systems (Ehrig et al., 1991) is presented in (Ehrig and Orejas, 2001). To sum up different process modeling techniques like graph transformation systems, Petri nets and many others besides, the relation between export and body is here formalized in a more general way by transformation rules instead of morphisms and our concept for Petri nets modules ?ts in very well. Moreover, the Petri net modules we introduce can be considered an instantiation of the generic component concept presented in (Ehrig et al., 2002c) (also in this volume). In 3.4. we discuss this relation. This paper is organized as follows: First we introduce Petri net modules in Section 2. The module operations are presented in Section 3. In both sections we use a small example to illustrate the introduced notions. A summary and future work are given in the conclusion in Section 4. Journal of Integrated Design and Process Science SEPTEMBER 2002, Vol. 6, No. 3, 122

2. Petri Net Modules
In this section we de?ne Petri net modules. More precisely the notions and results we present in this paper are given for place/transition nets. Since we use a categorical approach these notions and results easily can be transferred to other Petri net classes provided they are given categorically. Petri net modules consist of three nets, namely the import net ??? , the body net ? , and the export net ? . These are related with two different kinds of morphisms. So we ?rst need to de?ne the different notions of morphisms and to invest their speci?c properties. The use of those constructions and conditions can be seen in the subsequent section (Section 3.) where module operations are introduced. Due to space limitations we have skipped the proofs here. All proofs can be found in (Padberg, 2001). Here we give only the basic constructions that are required for understanding.

2.1. Preliminaries
First we give a short intuition of the underlying basics. The precise de?nitions can be found in (Padberg, 2001). Here we use the algebraic notion of Petri nets as introduced in (Meseguer and Montanari, 1990). Hence a Petri net is given by the set of transitions and the set of places and the pre- and post domain function.
¨ ¨ ¨

operations and relations as ¨, ?, , and so on. Nevertheless we need the pre- and post-sets as well. Hence we have as usually ? ? the set of all places in the pre- domain of a transition ?. Analogously ?? , ? ? and ?? . Moreover we need to state how often is a basic element with in an element of the free commutative monoid ? ? ? ¨. given. We de?ne this for an element ? ? ? and a word ? ? ? ¨ with ? ? Subnets ? ? ? ? ?? ? of a given net ? with ? ? ? can be easily de?ned by subsets of places and transitions, where the pre- and postdomain of transitions may be extended. ? ?? ? denotes the set of all subnets. Note that this subnet relation is not an inclusion in terms of plain morphisms.

?? ? ? ? ? , where ? is the free commutative monoid over ? , or the set of ?nite multisets over ??×? ? . So an element ? ? ? can be presented as a linear sum ? ?? ? ? ? and we can extend the usual
?

2.2. Morphisms of Petri Nets
Morphisms are the basic entity in category theory; they can present the internal structure of objects and relate the objects. So they are the basis for the structural properties a category may have and can be used successfully to de?ne various structuring techniques. Based on the algebraic notion of Petri nets (Meseguer and Montanari, 1990) we use simple homomorphisms that are generated over the set of places. These morphisms map places to places and transitions to transitions. They preserve ?ring and they yield nice categorical properties as cocompleteness. Plain morphisms are presented as usual by an arrow De?nition 1 (Plain Morphisms) / ?? is given by ?? A plain morphism / ?? so that ?? ?? ? ? ? and post analogously. These morphisms give rise to the category
/ .

? ? ??
? ? ??
¨

with ?

??
/

?? and ?

?

??.

?

A more elaborate notion of morphisms are substitution morphisms. These map places to places as well. But they can map a single transition to a whole subnet. Hence they substitute a transition by a net. These Transactions of the SDPS SEPTEMBER 2002, Vol. 6, No. 3, 123

morphisms are more complicated and do net yield nice categorical properties. But they capture a very broad idea of re?nement and hence are adequate for the relation between the export net and the body net. Subsequently substitution morphisms are presented by an undulate arrow /o /o /o / . De?nition 2 (Substitution Morphisms) ?? /o /o /o / ?? is given by A substitution morphism ? ? / ? ??? ? with ??? ?? ?? ?? such that ?? ?
?

? ? ? ? with ? ???? ??? ?? ?? ??×??? ?

??
/

?? and ?

? ? ? ?? ? ?? and ? ? ? ?? ? ? ??
? ?

Composition of substitution morphisms ?? /o /o /o / ?? and ?? /o /o /o / ?? is given by: ? / ? ??? ? is de?ned by ? ? ??? ? ? ? ? ? ? ? ? ? where ? ? ? ?? ? ????? ?? . Since ? ?? this construction is well de?ned. all ??

?

?

Note that these morphisms do not preserve properties. They can be restricted in order to preserve liveness (see for example (Urb? sek and Padberg, 2002)). aˇ Example 3 (Substitution Morphisms)

1111 0000 1111 0000 1111 0000 1111 0000 1111 0000 111111 000000 111111 000000 111111 000000 111111 000000

1111 111111111 0000 000000000 11 00 1111 111111111 0000 000000000 1111111 0000000 111 000 1111 0000 111 000 11111 00000 1111 0000 11111 00000 11 00 1111 0000 111 000 11 00 1111 111 0000 000 11111 00000 11 00 111 000 11 11 00 00 111111 1111 111 000000 0000 000 11 11 00 00 111 000 11 11 00 00 11111111 00000000 111111 1111 000000 0000 111111 000000
11 00 11 00 11 00 11 00 11 00

Figure 1. A substitution morphism.

The green 1 transition is mapped to the subnet consisting of green places and transitions. The striped transition is mapped to the subnet consisting of striped places and transitions. The places in the pre- and post-domain have to be preserved in following sense: Places in the pre-domain of the transition are mapped to places in the subnet to which the transition has been mapped. Conversely we can determine the net that surrounds a transition, i.e. all the adjacent places and the transition itself present a subnet of the target net. De?nition 4 (Net of a Transition) Given a transition ? ? ? for some net ? , then ? ???? the net surrounding ? is given by :

?

? ????
with
? ??
1
?

?? ? ? ? ?? ? ??×?? ?

? ?,
?

It may be grey if you have a black & white presentation. Then we assume the readers substitute susequently green by grey.

Journal of Integrated Design and Process Science

SEPTEMBER 2002, Vol. 6, No. 3, 124

? ??

? , and / ? ? with ?? ? ??? ? ?? ? ? ? analogously ??×??
¨

??

?

???,

?
The net surrounding a transition is the basis to relate the two notions of morphisms. Plain morphisms are a special case of substitution morphisms, where each transition is mapped the surrounding net of its target transition. The other way round: if a substitution morphisms maps all transitions to subnets containing only one transition, then it is plain as well. Lemma 5 (Plain Morphisms and Substitution Morphisms) / ?? given by ?? ? ? ? ? can be expressed as a substitution morphism Each plain morphism ? /o /o /o / ?? given by ? ?? ? ? ? ? where ? ??? ?? ?????. Moreover, if a substitution morphism ?? /o /o /o / ?? by ? ? ? ? has for all ? ? ?? ? ??? ? ???? ? ¨ ¨ ? ? ?? ? ?? ? and ? ???×?? ???? ??×????? ? then it is plain with for some ? ? ?? so that ? ??? ? ???? ? ??? ?? . Proof is trivial. The above fact can be expressed in categorical terms as well. Then we have a functor relating the two categories of Petri nets with the different morphisms.

?

???

Lemma 6 (Category of Petri Nets with Substitution Morphisms) consisting of Petri nets and substitution morphisms is a category. Moreover, / egory of and we have the inclusion functor ? , with ? ? ?

???

???

??

???

?? is a (full) subcat?

as in Lemma 5.

?

Proof is trivial. The inclusion functor de?ned above is cocontinuous, that means colimits are preserved. Given a colimit then the inclusion into yields again a colimit diagram. diagram in This is an essential result as it allows de?ning the module operations in terms of operation on Petri nets in Section 3. Lemma 7 (Inclusion ?

??

???

??
/

??? is Cocontinuous)

?

In the subsequent proof we show the preservation of pushouts explicitly as they are one of the main constructions we use. The proof can be found in (Padberg, 2001) here we just sketch the preservation of pushouts.

Transactions of the SDPS

SEPTEMBER 2002, Vol. 6, No. 3, 125

Proof Sketch: Given the following pushout (1) in

??, then we have the commutative square (2) in ??? as ? is a functor.
/ ??

??
???

??
?

/ ?? U U
???

U U

?

U U

U U

??

??



?

/ ??



??



U / ?? U *j *j *j *j *j *j !a !a U U *j *j *j *j *j *j !a !a U U ?? *j *j * ! 

?



?

?? Let ?? ?? /o /o /o / ? and ?? ?? /o /o /o / ? with ?? ? ? . ?? /o /o /o / ? where ? is the uniquely induced morphism by pushout ?? in We construct unique / ? ?? ? is given by ? ??

? ?.

? ? ?. So, colimits in ?? are colimits in ??? as well. But these consistmerely ofplain morphisms. For diagrams
?

? is well de?ned as ?? is pushout is

? ? ??? ?? ? ? ??? ??
?

? ??? ? ? ??? ?
?? ??

with ? ? ?

where one morphism is plain and the other is a substitution morphism we need the subsequent condition that ensures the existence of pushouts.

De?nition 8 (Compatibility Condition for Pushouts) / ?? and a substitution morphism ?? Given a plain morphism compatibility condition is satis?ed if: ? For all ?? ?? ? ?? we have ? ??? ? ? ???? ? implies ? ??? ? ? ? ??? ?. We the call and jointly injective. Lemma 9 (Pushouts in ) In the category we have pushouts for a plain morphism ?? ?? /o /o /o / ?? if the PO-compatibility condition is satis?ed.
/

??

/o /o /o /

?? the PO-

???

???

? ?

?? and a substitution morphism

Due to space limitation we refer again to (Padberg, 2001) and give here only the construction of the pushout. Proof Sketch: / ?? and a substitution morphism ?? ?? /o /o /o / ?? so that the Given a plain morphism PO-compatibility condition is satis?ed, then we have ?? ??? ?? ?? ? ??×?? ? where
? ?? ? ??

?? ·?? ?? is pushout in

? ?,

? ?? ? ? ? ? ? ? ? ? ? ? ? ? ? , hence we have: ?? ? ?? implies ?? ? ??

?

?? ? ??

(?)

and, Journal of Integrated Design and Process Science SEPTEMBER 2002, Vol. 6, No. 3, 126

?
? ??
?

? ??? ? ???
? ?

?

??? ?? ?? ? ?? ? ? ? ?? ? ??? ??

??×?? is de?ned analogously. ?? is well de?ned due to (?).
2.3. The Category of Modules of Petri Nets
We now introduce modules of Petri nets. The import is mapped to the body net by a plain morphism. The export net is mapped to the body net by a substitution morphism. This substitution morphism expresses the re?nement of the export by the body net.
?

De?nition 10 (Petri Net Modules) A Petri net module ??

???
A

?

/ /

?? ? ??? ? ?? ???? and ?? ?? ? ??
1. ?? 2. ??

(Petri)

module morphism ?? ?? ? is given by ?? with ?? ? ?? ? / ???? , ?? / ?? ?? , / ? ? , where ? ? ?? are plain and the following net
? ?? ? ??

?

o o/ ?o/ o/

consists of two morphisms ? where ? is a plain morphism and ? is a substitution morphism.

????

?

?

?

conditions hold:

?? ? ?? ? ?? ? ??

This gives rise to the category

????

?? O 888 ?? OO 888 88  ? ???? ? / ? 8 ? 88?? 88 88 88 88 88 88 88 88 88 8 88 88 88 88 ?? ?? ? 888 ?? 88 88 88 OO ? 88 88 O ?    ? ???? ? / ? ?

of Petri net modules.

?

Example 11 (Simple Module) We have an example with three modules that describe the process of writing urging and offering letters. The module ?? ? given in Figure 2 provides the writing of a letter via the export to the environment. It imports two precise processes for the urging and offering letters. In Figure 3 we show the corresponding modules. In Example 16 we then illustrate the composition of these modules. The module ?? ? in Figure 2 has the import net ???? with the two transitions Urge and Offer and their adjacent places. These are mapped to the net ? ? by a non-injective morphism. The import describes that this module assumes these two transitions to be abstractions. The export net ?? consists of a transition and two adjacent places.

Transactions of the SDPS

SEPTEMBER 2002, Vol. 6, No. 3, 127

Letter

Write

Finished Letter

EXP W

Letter Urge

Letter Offer

Letter Urge Offer

Finished Letter

Urging Letter

Offering Letter Offering Letter Urging Letter

IMPW

BOD W
Figure 2.

??

?.

The places are mapped to the corresponding places in the body net ? ? . The transition is mapped to the whole net ? ? . Hence the morphism ?? /o /o /o / ? ? is a substitution morphism. The export abstracts from the possibilities to write either an urging or offering letter.

?

Next we state that we can construct arbitrary colimits in the category . In (Padberg, 2001) we construct the initial object, arbitrary coproducts and pushouts for the proof. Here we merely state the construction of pushouts as these are the formal foundation of the union operation for modules given in the next section. Lemma 12 (

????

????

is cocomplete)

?
??
for ??

????

Proof Sketch: has pushouts that are denoted by ?? ? ?? ? ·?? / ?? ? and ?? ? ?? ? / ?? ? . ?? ? We have a component-wise construction, so we obtain the subsequent diagram

?

?

?

???? J

tt tt tt t ztt JJ JJ JJ JJ $

???? J
???

JJ JJ JJ JJ $

???? ??

?

ss ss ss s yss
? K

?
???

? K

KK KK KK KK %

????

t tt tt tt ztt

KK KK KK KK % / /

?

s ss ss ss yss
?

?

?

where (1) and (2) are pushouts in the category / ? ? and ???? morphism. As ????

?? and/ ?

? ? is the induced pushout ? ? are plain so is ?? .
?

????

Journal of Integrated Design and Process Science

SEPTEMBER 2002, Vol. 6, No. 3, 128

Analogously, we obtain – as ? is cocontinuous – from pushout (3) in ?? /o /o /o / ? ? :
t tt tt tt ytt JJ JJ JJ JJ %

??? the induced morphism ?
?
??? ? K

?

?? J
???

?? J

?? ? ? KK tt KK t KK tt KK tt K% t yt /o /o /o /o /o /o /o /o /o /o /o ??/o /o /o /o /o /o /o /o /o /o /o /o / /o ??
/

JJ JJ JJ JJ %

s ss ss ss yss

KK KK KK KK %

?

s ss ss ss ss y
?

?

?

Hence we obtain ??

?

????? ??

?

?

o o/ ?? o/ o/

?? ? as the pushout.

?

3. Composition of Petri Net Modules
In order to construct models of large systems we propose to use a variety of operations to put modules together. We call these module operations. The use of various module operations directly rises the question whether the nodules obtained by different operations ina still consistent. In order to guarantee this we prove compatibility between the module operations. In this section we de?ne three module operations, namely union, disjoint union, and composition. Susequently we state their compatibility (for the proof see (Padberg, 2001)). These are important results since it ensures the consistency of modules that are composed in various ways.

3.1. Module Operations
The ?rst operation we introduce is the Disjoint Union. Disjoint union is a special case of the Union of modules. Union allows a de?ned overlapping of the modules that is glued together.

???? Given Petri net modules ?? ? ?? ?? given by the coproduct in category

De?nition 13 (Disjoint Union of Petri Net Modules)

?

????
/

?

o o/ ?o/ o/

? ? for ? ? then there is ??

.

?

In Example 16 we use the disjoint union for combining the modules ?? ? and ?? ? . De?nition 14 (Union of Petri Net Modules) Given the Petri net modules ?? ???? ? / ? o o/ ?o/ o/ ? ? for ? / ?? ? and ?? ? / ?? ?? ? net module morphisms ?? ? ?? ? is ?? ? ?? ? ·?? ? ?? ? given by the corresponding pushout in category

????
?

??

with the then there .

?

The next module operation Composition describes the hierarchical composition of two modules, where the ?rst module uses the export of the second one for its import. This results in a new module with the import of the second one, the export of the ?rst one and a new composed body. De?nition 15 (Composition of Petri Net Modules)
/ ? o o/ o/ o/ Given two Petri net modules ?? ???? ? ? for ? ? and let /o /o /o / ???? ?? be a morphism so that the PO-compatibility conditions is satis?ed for

?

?

Transactions of the SDPS

SEPTEMBER 2002, Vol. 6, No. 3, 129

?? and ?? ? , then the composition ?? ? ? ? ? ????? ? ?/ ? ? ? ? / ?? ? with:
?

?

??

?

? ??

?

is de?ned by ??

?

?

?

?

?? ????
O O O 

??
/

?? OO
O  O O O O O

? ??
?

?

????

??
/

?? ?? O O ?? O  ? ? ? ?
?

O O 

O
?

/

?

?
Example 16 (Module Operations) In Example 11 we have the import ???? of two transitions with disjoint sets of places. To match this import we ?rst do a disjoint union of the following modules ?? ? and ?? ? (see Figure 3).
Letter Urge Letter Offer

Urging Letter

Offering Letter

EXP U

EXP O

Letter

Get Urge

Letter

Get Offer

Billing

Billing Type Adress

Sales Dep

Sales Dep Type Adress

IMP U BOD U

Urging Letter

IMP O

Offering Letter

Figure 3.

??

? and ?? ?

BOD O

The resulting module ?? ?? is the composed with module ?? ? In Figure 4 we show the construction with the intermediate nets. ? ??? is the pushout of ? ?? ·????? ? ? . In Figure 5 we ?nally ???? ?? . see the result of the composition. Note that ?????? ????? and

Journal of Integrated Design and Process Science

SEPTEMBER 2002, Vol. 6, No. 3, 130

Transactions of the SDPS
Figure 4. Composition of
Letter Urge

Letter

Write

Finished Letter

EXP W

Letter Urge

Letter Offer

Letter Urge Offer

Finished Letter

Urging Letter

Offering Letter Offering Letter Urging Letter

IMPW

BOD W

Letter Offer

??
?? and ?? ?
Letter Get Urge Billing Sales Dep Billing Type Adress

Urging Letter

Offering Letter Billing Letter Sales Dep Finished Letter

SEPTEMBER 2002, Vol. 6, No. 3, 131

EXP UO

Get Offer Letter Get Offer Get Urge

Sales Dep Type Adress Type Adress

Type Adress

Offering Letter

IMP UO BOD UO

Urgring Letter

Offering Letter

BOD WUO

Urgring Letter

Letter

Write

Finished Letter

EXP WUO

Billing

Letter

Sales Dep

Finished Letter

Get Offer Get Urge

Type Adress Billing Type Adress Sales Dep Offering Letter

IMP

WUO

BOD WUO

Urgring Letter
Figure 5.

??

???

?
3.2. Compatibility Results
We now come to the main result of this paper: The compatibility of the module operations with each other. This yields a kind of distributivity law for composition and (disjoint) union. Other kinds of such laws are stated informally in Subsection 3.3. The compatibility of union and composition requires a technical condition ensuring that pushouts that preserve jointly injective morphisms, i.e. that preserve they the conditions given in De?nition 8. here we skip this condition and again refer to (Padberg, 2001). Theorem 17 (Compatibility of Union and Composition) / ?? ? and ? ?? ? ?? ? Given ? ? ?? ? ? / ?? / ?? ? We have and ?? ? ?? ? ? ?
/

??
?

?

, as well as

??

??? ???
?

?

·?? ? ?? ? ? ? ???
?

?

?

·?? ? ?? ? ?
?

?

??

?

?

? ·???

?? ?

??

?

?

???

?

?

?

??

?

?

?

provided that the compositions via ? ? , and ? are well-de?ned, the compatibility condition (De?nition 5 in (Padberg, 2001) ) is satis?ed, and the following compatibility condition holds: Journal of Integrated Design and Process Science SEPTEMBER 2002, Vol. 6, No. 3, 132

?

and
?

? ? ? ? ? ?

??

? ?

?

?

?

?

?

For the proof see (Padberg, 2001). As a direct consequence of the above Theorem we have that union is also compatible with disjoint union. This follows directly since disjoint union is a special case of union.

Corollary 18 (Compatibility of Disjoint Union and Composition) Given ??? ? ?? and ??? ? ? ?? then we have

?
?

?

???

?

??

?

?

?
?

?

??

?

?
?

?

??

?

provided that the compositions via , and ?

? ? are well-de?ned.
?

?

3.3. Laws for Module Operations
Here we state informally the basic laws we have for module operations These laws make use of the nice properties colimits have. Clearly, they result from the underlying theory and do not present a surprise for readers familiar with category theory. Hence we do not treat then in detail. Here we also have skipped the assumptions. Nevertheless such laws are of eminent importance for the practical use. So we have stated them here explicitly.

Associativity

? ??? ?? ? ? ??? ? ? ?? ? ? ???
??
? ?

? ???

? ??

?

? ? ?? ? ? ?? ? ? ? ??
?

? ??

?

? ?

due to properties of colimits

Commutativity

?? ??
?

?

? ??

? ?

?? ??

? ?

? ??

? ?

·?? ? ??

·?? ? ??

due to properties of colimits

Transactions of the SDPS

SEPTEMBER 2002, Vol. 6, No. 3, 133

Distributivity

??? ???
?

?

·?? ? ?? ? ? ? ???
?
?

?

?

·?? ? ?? ? ?
?

?

? ??

? ·???
?

?? ?

??

?

?

???
?

?

?

?

??

?

?

?

?
?

?

???

? ??

?

?
?

?

??

?
?

?

??

?

see Theorem 17 and Corollary 18

3.4. Relation to the Transformation-Based Component Framework
In (Ehrig et al., 2002a) a very promising approach has been presented as an instantiation of a generic component approach. Main results concerning compositionality are given in (Ehrig et al., 2002b) and show that semantics and correctness for a system can be inferred from that of its components. Our approach presented in this paper can be considered as an instance of this general framework as presented in (Ehrig et al., 2002c) in this volume. This abstract approach gives a general frame for the modularization of process description techniques. There ? ?? a generic transformation ?? ? ?? ? ? is introduced. For the general framework the  ? / ?? extension properties is required. That is for each inclusion ? ?? ? and each trans ? /  ? ? ?? ?? ? ?? ? and a transformation formation ?? ? ?? ? ? there are ? ? ? ?? ?? ?? ? ? ?? ? so that the following diagram commutes:

?? ?? ? ??


?



?

/

??
/

?

?

?


?

??



?? ?
?
?

?

If we use the substitution morphisms in De?nition 2as transformations and injective plain morphisms as inclusions then the extension property is satis?ed because of Lemma 9. Due to the satisfaction of this property we can obtain the transformation semantics as well. The composition is obviously based on the same concepts. In section 4 in (Ehrig et al., 2002b) an example based on algebraic high level nets and so-called double pushout transformations is given. Apart from the data type substitution morphisms introduced in De?nition 2 are slightly more general than the double pushout transformations in (Ehrig et al., 2002c).

4. Conclusion
In this paper we have presented Petri net modules as a formal modeling technique for component-based systems. We have investigated Petri net modules that have the same internal structure as components in the CSE approach. Moreover we have several module operations that allow putting modules together in a well-de?ned and consistent way. Hence Petri net modules present an adequate and powerful modeling technique for the process view of components. We have shown that they conform the basic principles of component-based software engineering and the component concept in the CSE approach. Journal of Integrated Design and Process Science SEPTEMBER 2002, Vol. 6, No. 3, 134

In (Padberg and Buder, 2001) we have presented a case study using Petri net modules for the modeling of a telephone service center. We have developed a Petri net model of an automated telephone service center with a variety of telephone services. The overall system consists of three major services: the telephone enquiry service, the message delivery service, and the payment service. All services start with an announcement concerning the selection of the corresponding service. The telephone enquiry service gives the customer information about telephone numbers. The customer is asked for the data; either the name, the postal code, the city or the street. The corresponding entry in the database is announced subsequently. The message delivery service forwards a message recorded by the customer to another recipient. Here the customer leaves a message, a telephone number and set a time for delivering the message. Then the order is entered into the database and carried out at the speci?ed point of time. Finally the payment service allows changing the payment mode or checking the account balance. Our case study contains twelve basic modules that can be composed to an abstract description of the overall system. Subsequently we present four basic modules concerning the message delivery service. The work we have presented here is a ?rst step towards a full theory as well as towards a practical approach for modeling components. Future work in this area comprises:
? Transfer of this module concept to other formal techniques used for the modeling of other views. ? Extension to further important module operations as renaming, re?nement, or even recursion as in (Ehrig and Mahr, 1990). ? Explicit descriptions of dependencies and propagation of dependencies within and between modules (e.g. the relevance for an evolution of components has already be stated in (Gro?e-Rhode et al., 2000)). ? In order to transfer the module semantics of (Ehrig and Mahr, 1990) we ?rst need to develop an loose semantics for Petri nets. This is an open issue for behavioral speci?cations in general.

References
Battiston, E., F. De Cindio and G. Mauri (1991a). OBJSA Nets: A Class of High-Level Nets Having Objects as Domains. In: Advances in Petri Nets (Rozenberg/Jensen, Ed.). Springer. Battiston, E., F. De Cindio, G. Mauri and L. Rapanotti (1991b). Morphisms and Minimal Models for OBJSA Nets. In: 12? International Conference on Application and Theory of Petri Nets. Gjern, Denmark. pp. 455–476. extended version: Technical Report i. 4.26, Progretto Finalizzato Sistemi Informatici e Calcolo Parallelo. Consiglio Nazionale delle Ricerche (CNR), Italy, Jan, 1991. Broy, M. and T. Streicher (1992). Modular functional modelling of petri nets with individual tokens. Advances in Petri Nets. Buchholz, P. (1994). Hierachical high level Petri nets for complex system analysis. In: Application and Theory of Petri Nets. Vol. LNCS 815. Springer. pp. 119–138. Christinsen, S. and N.D. Hansen (1994). Coloured petri nets extended with channels for synchronous communication. In: Application and Theory of Petri Nets. Vol. LNCS 815. Springer. pp. 159–178. Deiters, W. and V. Gruhn (1994). The F UN S OFT Net Approach to Software Process Management. International Journal on Software Engineering and Knowledge Engineering 4(2), 229–256. Transactions of the SDPS SEPTEMBER 2002, Vol. 6, No. 3, 135

Desel, J., G. Juh? s and R. Lorenz (2000). Process semantics of Petri nets over partial algebra. In: Proceeda ings of the XXI International Conference on Applications and Theory of Petri Nets (M. Nielsen and D. Simpson, Eds.). Vol. LNCS 1825. Springer. pp. 146–165. Ehrig, H., A. Habel, H.-J. Kreowski and F. Parisi-Presicce (1991). From graph grammars to high level replacement systems. In: Lecture Notes in Computer Science 532. Springer Verlag. pp. 269–291. Ehrig, H. and B. Mahr (1990). Fundamentals of Algebraic Speci?cation 2: Module Speci?cations and Constraints. Vol. 21 of EATCS Monographs on Theoretical Computer Science. Springer Verlag. Berlin. Ehrig, H. and F. Orejas (2001). A Generic Component Concept for Integrated Data Type and Process Speci?cation Techniques. Technical Report 2001/12. Technische Universit¨ t Berlin, FB Informatik. a Ehrig, H., F. Orejas, B. Braatz, M. Klein and M. Piirainen (2002a). A Generic Component Concept for System Modelling. In: Proc. FASE 2002: Formal Aspects of Software Engineering. Ehrig, H., F. Orejas, B. Braatz, M. Klein and M. Piirainen (2002b). A Transformation-Based Component Framework for a Generic Integrated Modeling Technique. In: Proc. of the Sixth World Conference on Integrated Design& Process Technology (IDPT’02). CD-ROM, 15 pages. Ehrig, H., F. Orejas, B. Braatz, M. Klein and M. Piirainen (2002c). A transformation-based component framework for a generic integrated modeling technique. Journal of Integrated Design and Process Science 6(3), 36–63. Fehling, R. (1993). A concept of hierarchical Petri nets with building blocks. In: Advances in Petri Nets’93. Springer. pp. 148–168. Lecture Notes in Computer Science 674. Gro?e-Rhode, M., R.-D. Kutsche and F. B¨ bl (2000). Concepts for the evolution of component-based softu ware systems. Technical Report 2000/11. TU Berlin. He, X. (1996). A Formal De?nition of Hierarchical Predicate Transition Nets. In: Application and Theory of Petri Nets. Vol. LNCS 1091. Springer. pp. 212–229. Jensen, K. (1992). Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Vol. 1: Basic Concepts.. EATCS Monographs in Theoretical Computer Science ed.. Springer Verlag. Kindler, E. (1995). Modularer Entwurf verteilter Systeme mit Petrinetzen. PhD thesis. Technische Universit¨ t M¨ nchen, Institut f¨ r Informatik. a u u Meseguer, J. and U. Montanari (1990). Petri Nets are Monoids. Information and Computation 88(2), 105– 155. M¨ ller, H. and Weber, H., Eds.) (1998). Continuous Engineering of Industrial Scale Software Systems. IBFI, u Schlo? Dagstuhl. Dagstuhl Seminar Report #98092. Padberg, J. (2001). Place/Transition Net Modules: Transfer from Algebraic Speci?cation Modules. Technical Report TR 01-3. Technical University Berlin. Padberg, J. and M. Buder (2001). Structuring with Petri Net Modules: A Case Study. Technical Report TR 01-4. Technical University Berlin. Journal of Integrated Design and Process Science SEPTEMBER 2002, Vol. 6, No. 3, 136

Sibertin-Blanc, C. (1994). Cooperative Nets. In: Application and Theory of Petri Nets’94. pp. 471–490. Springer LNCS 815. Simeoni, M. (1999). A Categorical Approach to Modularization of Graph Transformation Systems using Re?nements. PhD thesis. Universit` Roma ”La Sapienza”. a Urb? sek, M. and J. Padberg (2002). Preserving liveness with rule-based re?nement of place/transition sysaˇ tems. In: Proc. IDPT 2002: Sixth World Conference on Integrated Design and Process Technology, CD-ROM (Society for Design and Process Science (SDPS), Eds.). p. 10. Weber, H. (1999). Continuous Engineering of Communication and Software Infrastructures. Vol. 1577 of Lecture Notes in Computer Science 1577. pp. 22–29. Springer Verlag. Berlin, Heidelberg, New York. Weber, H. and H. Ehrig (1988). Speci?cation of concurrently executable modules and distributed modular systems. In: Proc. IEEE Workshop on Future Trends of Distr. Comp. Systems in the 1990s, Hongkong. IEEE. pp. 202–215.

Transactions of the SDPS

SEPTEMBER 2002, Vol. 6, No. 3, 137


相关文章:
更多相关标签: