A Generic Approach to Connector Architectures Part I: The General Framework

See discussions, stats, and author profiles for this publication at: https://www.researchgate.net/publication/220443976

A Generic Approach to Connector Architectures Part II: Instantiation to Petri Nets and CSP ARTICLE in FUNDAMENTA INFORMATICAE · JANUARY 2010 Impact Factor: 0.72 · DOI: 10.3233/FI-2010-240 · Source: DBLP

READS

18

6 AUTHORS, INCLUDING: Fernando Orejas

Julia Padberg

Polytechnic University of Catalonia

Hochschule für Angewandte Wissenschafte…

188 PUBLICATIONS 1,203 CITATIONS

166 PUBLICATIONS 1,167 CITATIONS

SEE PROFILE

SEE PROFILE

Elvira Pino Polytechnic University of Catalonia 23 PUBLICATIONS 95 CITATIONS SEE PROFILE

All in-text references underlined in blue are linked to publications on ResearchGate, letting you access and read them immediately.

Available from: Elvira Pino Retrieved on: 09 February 2016

Fundamenta Informaticae XXI (2001) 1–29

1

IOS Press

A Generic Approach to Connector Architectures Part II: Instantiation to Petri Nets and CSP Fernando Orejas Universitat Polit`ecnica de Catalunya, Dept. LSI Campus Nord, M`odul C5, 08034 Barcelona [email protected]

Hartmut Ehrig Technische Universitat Berlin, SeKr. FR6-1, Franklinstr. 28/29, 10587 Berlin [email protected]

Markus Klein Technische Universitat Berlin, SeKr. FR6-1, Franklinstr. 28/29, 10587 Berlin [email protected]

Julia Padberg Technische Universitat Berlin, SeKr. FR6-1, Franklinstr. 28/29, 10587 Berlin [email protected]

Elvira Pino Departament LSI Universitat Polit`ecnica de Catalunya, Dept. LSI Campus Nord, M`odul C5, 08034 Barcelona [email protected]

Sonia P´erez CEIS, Inst. Sup. Polit´ecnico Jos´e Antonio Echevarr´ıa, Havana, Cuba [email protected]

Abstract. The aim of this paper is to show how the generic approach to connector architectures, presented in the first part of this work, can be applied to a given modeling formalism to define architectural component and connector notions associated to that formalism. Starting with a review of the generic approach, in this second part of the paper we consider two modeling formalisms: elementary Petri nets and CSP. As main results we show that both cases satisfy the axioms of our component framework, so that the results concerning the semantics of architectures can be applied. Moreover, a small case study in terms of Petri Nets is presented in order to show how the results can be applied to a connector architecture based on Petri nets..

Keywords: Architectural connectors, formal software modelling, software architecture, Petri nets, CSP.

1. Introduction In the first part of this work we presented a generic framework for the definition of architectural components and connectors, following the approach introduced in [1], that in our opinion can be instantiated to any (reasonable) modeling formalism. The idea was to provide a formal and conceptual tool for defining basic architectural notions associated to widely used modeling formalisms.

2

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

In particular, to show how our framework works, we consider in this paper the instantiation to two specification techniques: Petri nets and CSP. In addition, we present in a small case study a connector architecture based on Petri nets and show how the semantics can be computed using the results of the generic framework. The choice of these two formalisms is based on different reasons. On the one hand we chose Petri Nets because it is a well-known technique used industrially in the modeling of software (and also hardware and embedded) systems. In our opinion, however, it lacks a satisfactory notion of component up to now. Actually, one of the main contributions of this paper is to provide a component concept for Petri Nets using architectural connectors by instantiation of our generic framework. In particular, in the Section 5 we relate our Petri net components with other approaches to Petri net modules and components in the literature. The case of CSP is quite different. In this case, the architectural connector’s approach, whose main ideas we follow, was introduced using Wright, an architecture description language based on CSP [1]. Actually, the main aim of presenting the CSP instantiation is to show in which sense our approach is related to the approach presented in [1]. In particular, we can see that in most notions, which both papers study, the definitions correspond to each other, although we make explicit some aspects that in [1] are implicit. This is normal since language constructions may make unnecessary to be explicit in some cases. In addition, if we consider the results presented in the first part of this work, we study important aspects which are not studied in [1]. This refers especially to the semantics of interconnection and architectures and their related properties. Nevertheless, there is one main difference between our instantiation and the constructions used in [1]. In particular, we cannot use the compatibility relation between ports and roles used in [1] to connect a component with an architectural connector, because it is not transitive. Instead, we use a refinement relation which is less general than compatibility. In Sect. 4 we discuss this issue in more detail. The paper is organized as follows. In the following section we give a small account of the concepts presented in the first part of this work. Then, in section 3, we present the Petri Net instantiation of our approach, presenting also our small case study. In section 4, the CSP instantiation. Finally, in section 5 we draw some conclusions.

2. A generic framework for architectural components and connectors In this section, we briefly describe the basic ingredients of our generic framework. However, we advice the interested reader to look at this paper together with its first part, for more details concerning the generic framework. Following [1], in our framework we consider two kinds of constructions: components and connectors. Components are units that provide some kind of services and that can be connected with other components through connectors, and connectors are units that describe the interaction of the connected components. A component is a unit consisting of a body and some interfaces, called ports, which provide abstract views of the body. A connector is a unit consisting of two or more interfaces, called roles, and a body. The roles describe the expected behavior and services provided by the component to which they will be connected, while the body describes the interaction of the components that will be connected through the roles. In this sense, the body of a connector extends the specifications included in the roles by defining over them an interaction policy. Therefore, the first ingredient of our framework is the class of models or specifications that is used to describe the bodies and interfaces (i.e. the ports and the roles) of components and connectors. In addition, we have to consider the relations between the bodies and their interfaces in a given component or connector. As said above, the body of a connector can be seen as extending the models

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

3

describing the ports. In this sense, we say that a port must be embedded in the body of a connector. These embeddings, in many cases, will just be inclusions. However, this is not always the case. For instance, in Section 4 CSP embeddings are inclusions that satisfy some additional conditions. On the other hand, a port can be seen as an abstract view of a component or, equivalently, we may see the body of a component as some form of refinement of its ports. We denote these refinement relations by transformations. Moreover, we consider that embeddings are a special kind of transformations since, in principle, a port could be just a description of part of a component. Therefore, the second ingredient of our framework are a class of transformations, and a class of embeddings (included in the class of transformations, that are used to relate the interfaces with the body of a connector or a component. For technical reasons, we assume that for every model there is a special identity embedding. Components are connected to connectors by binding a port of the component with a role of the connector. However this binding is only possible if the role and the port are compatible in some sense. Typically, this compatibility is expressed by asking the port to be some form of refinement of the role. Therefore, in our context we consider that a role can be bound to a port if there is a transformation from the role to the port. Then, to define the semantics and to prove some properties of composition we need to compose embeddings (respectively transformations) to yield new embeddings (respectively transformations). Therefore, we need that the classes of embeddings and transformations are closed under composition. Moreover we also need this composition to be transitive. In order to be able to define an adequate semantics of the composition of components via connectors, and in general of architectures we must ask the given modeling framework to satisfy some requirements. In particular, one of these requirements is to have a parallel extension construction, which is the basis for defining the semantics of component composition. In particular, parallel extension is equivalent to ask embeddings and transformations to be compatible in the following sense. If a given model M embeds a family of models M1 , . . . , Mn and we know that each of these submodels can be transformed into the models M1′ , . . . , Mn′ , respectively, then we should be able to transform in parallel all these submodels in the context of M yielding a model M ′ , which embeds M1′ . . . , Mn′ and is a transformation of M. Moreover, the result of this transformation must be uniquely determined by the given transformations and embeddings. Figure 1 depicts a diagram, in terms of parallel extension, for the composition of n components with bodies B1 , . . . , Bn through a connector with body B and roles R1 , . . . , Rn . Note that each role Ri is connected to a port of Pi j of one component. More precisely, the semantics of this composition is a component whose body B′ is obtained by parallel extension and whose ports are all the ports of the connected components who have not been bound to a role. However, depending on the embedding and transformations involved, this construction may not always exist. This means that our given modeling framework should include a notion of parallel consistency that states when parallel extensions are possible. This kind of composition is associative and compatible with component transformation. Moreover we also show that the result of two overlapping connections via two connectors is independent of the order to compute the single compositions. In particular, this means that composition is associative. These results are used for giving semantics to architectures. More precisely, if we see an architecture as a graph that displays all the connections between connectors and components, in the first part of this work we show that the semantics of an architecture can be obtained by computing all the connections between components and connectors. We do this by means of graph transformation. In particular, we use a rule that transforms any occurrence of a composition diagram by the corresponding result. The results mentioned above ensure that the final result of this transformation process is independent of the order in which we compute these connections. In particular, we prove that this transformation system is Church-Rosser and terminating and, moreover, compatible with component transformation.

4

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

R1 B P11 B BBB

...

BB B r1 con1 BBB BB 

P1k1

Rn || || | ||  |~ | rn

B

conn

Pnkn

Pn1

|| BBBB ||| p1k pnk ||||| BBBB 1 p11 BBBB |n|| pn $   z ||| 1 .. .. Bn \d :B B1 ?? . . BBB B  | | ?? p1m1 ||| BBBBBpnmn  | ?  | BBB ??  |||| BBBB ??  r′ r1′ |||||    n

P1m1

B′

Pnmn

Figure 1. Composition of components

Summarizing, the notion of component framework describes the properties that a given modeling formalism must satisfy in order to support our notions of component and connector and the associated results. Definition 2.1. (Component Framework) A component framework F consists of: • A class of models M , including bodies and ports of components and bodies and roles of connectors. • A class of transformations T and a class of embeddings E , with E ⊆ T , such that they are closed under composition, in the sense that if t1 : M1 ⇒ M2 and t2 : M2 ⇒ M3 are in T (respectively e1 : M1 → M2 and e2 : M2 → M3 are in E ) then their composition t2 ◦ t1 is also in T (respectively, e2 ◦ e1 is in E ). Moreover, this composition is associative, and for every model M there is a special identity which is neutral with respect to embedding and transformation composition. • A parallel consistency relation for J-indexed families of transformations with respect to Jindexed families of embeddings that satisfies the parallel extension property, which means that this relation ensures the existence of parallel extension satisfying some additional properties.

3. Architectural Connectors based on Petri nets The aim of this section is twofold. On one hand, the generic framework is instantiated to use Petri nets as a modelling language. On the other hand, using some Petri net connectors and components, we describe a small system modelling the functionality of a secured door. In particular, in the first subsection we briefly introduce our small case study. Then, in the following subsection, we study the instantiation of our generic framework to the case of Petri nets. Finally, in the last subsection we describe the architecture of the system in some detail and construct its semantics according to the general framework provided in the first part of this work.

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

5

3.1. Introduction to the example The following sample component/connector architecture describes the functionality of a secured door. The architecture contains three components: The door itself, a key lock, and a biometric scanning unit. The general idea is that the door only opens if the key is inserted and turned and the biometric scan has recognized a pattern of a person authorized to operate the door. The three units are connected via two connectors: CON1 and CON2. This situation is depicted by means of the architecture graph of the example in Fig. 3 and by its architecture diagram in Fig. 2. Though being very small, the example contains a typical problem of today’s applied engineering, namely the consistent connection of different technical devices and software components via defined interfaces. CON1

KEY

CON2

DOOR

SCAN

Figure 2. Architecture Graph of the example

BOD CON1 O iSSS SSS SSS SSS SS ROL2 CON1 ROL1 CON1

 POR1 KEY

BOD CON2 O iii4 i i i i i i iii iiii ROL1 CON2 ROL2 CON2

 POR3 DOOR hh hhhh h h h h hhhh  px hhh BOD DOOR ks POR2 DOOR

 POR2 DOOR

 POR1 SCAN

  BOD KEYSS BOD SCAN t SSS tt SSS tt SSS t SSS t )  tt tt t BOD KEY&DOOR t VVVV tt VVVV tt VVVV t t VVVV tt VV* ytt BOD KEY&DOOR&SCAN Figure 3. Architecture Diagram of the example

3.2. Instantiation of the Framework to Petri nets In this section we show how the specification technique of Petri Nets fits into our generic framework. This includes the definition of embeddings and transformations and, based on that, the construction of extensions and parallel extensions. For simplicity, we use a special notion of Petri nets, allowing only

6

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

arcs and place weights of arity one, but the main constructions should generalize without problems. In addition, we handle the corresponding initial markings. The following notion of nets is a slight modification of the well known process nets in the sense of [25]. Definition 3.1. (Marked Process Net) A marked process net MPN = (P, T, pre, post, mark) over a given label set L consists of a set of places P and a set of transitions T . The functions pre, post : T → P (P) represent the connecting arcs, and the set mark ⊆ P contains all the initially marked places. In order to define suitable notions of transformations and embeddings, we first introduce a notion of general morphism between marked process nets. In this notion, in addition to the compatibility with the pre and post functions, we ask for the preservation and reflection of the marked places. Definition 3.2. (MPN Morphism) Given two marked process nets MPNi = (Pi , Ti , prei , posti , marki ) (i = 1, 2). An MPN morphism f : MPN1 → MPN2 consists of mappings fP : P1 → P2 , fT : T1 → T2 , such that 1. The diagram in Fig. 4 commutes componentwise for the pre and post functions, 2. fP∗−1 (mark2 ) = mark1 , where fP∗ denotes the obvious extension of fP to sets of places. T1

pre1

//

post1

P (P1 ) fP∗

fT



T2 Figure 4.

pre2

//

post2



P (P2 )

MPN Morphism

Embeddings can now be defined as special MPN morphisms. We require that they are injective, in the sense that they do not merge places or transitions. In addition, the initial marking is not only preserved, but should also reflected by the embeddings. Definition 3.3. (MPN Embedding) A morphism of marked process nets e : MPN1 → MPN2 , where MPNi = (Pi , Ti , prei , posti , marki ) for (i = 1, 2), is an embedding, if eP and eT are injective mappings. It should be obvious that the identity morphism is an embedding and that the composition of two embeddings is an embedding. The following notion of transformation of marked process nets is an adaption of the substitution morphisms for general (not marked) petri nets, presented in [23]. These morphisms allow to replace transitions of the original net by whole subnets in the target net. Moreover, we allow renamings of existing places and transitions. Again, the markings are preserved and reflected.

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

7

Definition 3.4. (MPN Transformation) A transformation s : MPN1 =⇒ MPN2 of a net MPN1 to a net MPN2 , with MPNi = (Pi , Ti , prei , posti , marki ) for (i = 1, 2), is given by an injective mapping of places sP : P1 → P2 and a mapping sT : T1 → P (MPN2 ), where P (MPN2) denotes the set of all subnets of MPN2, sT (t) := MPNt2 ⊆ MPN2 , and MPN2t = (Pt2 , T2t , pret2 , post2t , mark2t ), such that the following properties hold: 1. sP (pre1 (t)) ⊆ Pt2 , 2. sP (post1 (t)) ⊆ Pt2 , 3. s∗−1 P (mark2 ) = mark1 , This notion of transformation does not ensure the preservation of properties of the transformed nets. But, according to the morphisms in [23] and [28], our notion can be enhanced to model actual refinements of Petri-Nets that do preserve some given properties, e.g. liveness. Now, although embeddings are not exactly transformations, we can show that we can consider them as a special case of these transformations: Corollary 3.1. (MPN Embeddings define MPN Transformations) Each embedding e : MPN1 → MPN2 has an associated transformation trafo(e) = s : MPN1 =⇒ MPN2 . Proof: First, we define sP = eP and sT (t) = (pre(t) ∪ post(t), {t}, pret2 , post2t , mark2t ), where pret2 , post2t are, respectively, e∗P (pre1 (t)) and e∗P (post1 (t)). The set mark2t is given by all places eP (p) with p ∈ mark1 and p ∈ pre(t) ∪ post(t). That is, sT (t) is the subnet of MPN2 consisting only of the transition eT (t) and the places which are in its pre and post sets. Thus, by construction all conditions of transformations are satisfied. ⊓ ⊔ It should be obvious that the identity embedding defines an identity transformation. Now, in order to prove that transformations are closed under composition, we first see how we can apply a transformation s : MPN1 =⇒ MPN2 to a subnet MPN of MPN2: Definition 3.5. (Application of an MPN Transformation) Given a transformation s : MPN1 =⇒ MPN2 , with MPNi = (Pi , Ti , prei , posti , marki ) for (i = 1, 2), and a net, MPN = (P, T, pre, post, mark), with MPN ∈ P (MPN1 ), we define the application of s to MPN, denoted s[MPN] as the net MPN ′ = (P′ , T ′ , pre′ , post ′ , mark′ ) where: P′ T′ pre′ (t) post′ (t) mark′

:= := := := :=

{p ∈ P2 |∃t ∈ T p is a place in sT (t)} {t ′ ∈ T2 |∃t ∈ T t ′ is a transition in sT (t)} pre2 (t) post2 (t) {p ∈ mark2 |p ∈ P′ }.

Now we can define the composition of transformations. The idea is quite simple. If we have the transformations s : MPN1 =⇒ MPN2 and s′ : MPN2 =⇒ MPN3 then to define the composition s′′ = s′ ◦ s : MPN1 =⇒ MPN3 the key idea is to define s′′ (t) = s′ [sT (t)], for every t in T1 .

8

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

Definition 3.6. (Composition of MPN Transformations) Given s : MPN1 =⇒ MPN2 and s′ : MPN2 =⇒ MPN3 , with MPNi = (Pi , Ti , prei , posti , marki ) for (i = 1, 2, 3), the composition of s and s′ , denoted s′ ◦s, is the transformation s′′ : MPN1 =⇒ MPN3 , defined: s′′P (p) := s′′T (t) :=

s′P (sP (p)), ∀p ∈ P1 s′ [sT (t)], ∀t ∈ T1

It is routine to prove that s′ ◦ s is indeed a transformation (i.e., it satisfies the four properties associated to transformations) and that composition is associative. Now we have to prove that we can build parallel extensions associated to these notions of embedding and transformation, provided that the adequate notion of parallel consistency is satisfied. So, let us define the parallel consistency property that ensures the existence of parallel extensions. Definition 3.7. ( Parallel Consistency) Given families of transformations and embeddings (si : MPNi =⇒ MPNi′ )i∈I , (ei : MPNi → MPN)i∈I with MPN = (P, T, pre, post, mark), MPNi = (Pi , Ti , prei , posti , marki ) (i ∈ I), MPNi′ = (P′i , Ti′ , pre′i , posti′ , marki′ ) (i ∈ I), these transformations are parallel consistent with respect to these embeddings if ∀i, i′ ∈ I ∀t ∈ Ti , t′ ∈ Ti′ if ei,T (t) = ei′ ,T (t ′ ) then there exists an isomorphism φ : si,T (t) → si′ ,T (t ′ ) such that for every p ∈ Pi , p′ ∈ Pi′ if ei,P (p) = ei′ ,P (p′ ) then φ(si,P ((p)) = si′ ,P (p′ ). This means, following the intuition described in Part 1 of this paper, that the given family of transformations is parallel consistent if every transition shared by two nets, MPN i and MPN i′ , is refined in the same way by the transformations si and si′ . Based on this notion of parallel consistency we are now able to construct the parallel extension of a family of transformations. Theorem 3.1. (Parallel Extension for MPNs) Parallel consistency satisfies the parallel extension property. Proof: Given families of transformations and embeddings (si : MPNi =⇒ MPNi′ )i∈I , (ei : MPNi → MPN)i∈I as depicted in Fig. 5 (|I| = n) with MPN = (P, T, pre, post, mark), MPNi = (Pi , Ti , prei , posti , marki ) (i ∈ I), MPNi′ = (P′i , Ti′ , pre′i , posti′ , marki′ ) (i ∈ I), such that the family of transformations is parallel consistent with respect to the family of embeddings, we define their parallel extension as follows.

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

MPN1J

...

JJ e JJ 1 JJ JJ $

MPNn t tt tt t t tz t en

MPN

s1

s



sn



MPN1′

II ′ II e1 II II I$ 

9

MPNn′ e′n

u uu uu u u uz u

MPN ′

Figure 5. Parallel Extension for MPNs

First we define the net MPN ′ = (P′ , T ′ , pre′ , post′ , mark′ ): P′ := T ′ := pre′ (t) :=

post′ (t) :=

mark′ :=

( i∈I P′i ⊎ P)/ ≡1 U ( i∈I Ti′ ⊎ {t|t ∈ T ∧ t ∈ / ∪i∈I e∗i (Ti )})/ ≡2 if ∃i ∈ I such that t ∈ Ti′ then {[p]1 |p ∈ pre′i (t)} else {[p]1 |p ∈ pre(t)} if ∃i ∈ I such that t ∈ Ti′ then {[p]1 |p ∈ posti′ (t)} else {[p]1 |p ∈ post(t)} {[p]1 |p ∈ mark ∨ p ∈ marki′ f or some i ∈ I} U

where ⊎ denotes disjoint union, [p]1 denotes the equivalence class of p with respect to ≡1 , and ≡1 and ≡2 are the least equivalence relations satisfying: • ∀i ∈ I∀p ∈ Pi : si,P (p) ≡1 ei,P (p) • ∀i, i′ ∈ I∀p ∈ Pi , p′ ∈ Pi′ if ei,P (p) = ei′ ,P (p′ ) then si,P (p) ≡1 si′ ,P (p′ )) • ∀i, i′ ∈ I∀t ∈ Ti ,t ′ ∈ Ti′ if ei,T (t) = ei′ ,T (t ′ ), by parallel consistency, there exists an isomorphism φ : si,T (t) → si′ ,T (t ′ ) such that for every p ∈ Pi , p′ ∈ Pi′ if ei,P (p) = ei′ ,P (p′ ) then φ(si,P ((p)) = si′ ,P (p′ ). Then for every p ∈ si,P (t) and every t ′′ ∈ si,T (t) we have pi ≡1 φ(pi ) and ti′′ ≡2 φ(ti′′ ). It is routine to see that the parallel consistency of (si )i∈I with respect to (ei )i∈I ensures the correctness of the definition. In particular, it is routine to prove that the definition is independent of the isomorphism φ chosen, in the sense that if MPN ′ and MPN ′′ are two nets obtained by parallel extension with a different choice of isomorphisms then they are isomorphic. In addition, it should be obvious that, for every i ∈ I, if e′i,P and e′i,T are, respectively, the canonical injections from Pi′ and Ti′ to the corresponding disjoint unions then, e′i is an embedding. Now, we define the transformation s′ as follows: sP (p) := [p]1 sT (t) := if ∃i ∈ I such that t ∈ Ti then [si,T (t)] else (s∗P (pre(t)) ∪ s∗P (post(t)), {[t]2 }, {[p]1 |p ∈ pre(t)}, {[p]1 |p ∈ post(t)}, {[p]1 |p ∈ markt }),

10

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

where markt is given by the intersection of mark and pre(t) ∪ post(t) and, assuming that si,T (t) = (Pt , Tt , pret , postt , markt ), then [si,T (t)] is the net: ([Pt ]1 , [Tt ]2 , {[p]1 |p ∈ pret }, {[p]1 |p ∈ postt }, {[p]1 |p ∈ markt }) Again, it is routine to check that the fact that embeddings and transformations preserve and reflect markings implies that s is well-defined. Now, we have to prove that our notion of parallel extension of marked Petri nets satisfies the additional properties that parallel consistency must satisfy with respect to parallel extension. The first one is that parallel extension diagrams are closed under vertical composition. More precisely, if MPN ′ is the parallel extension of {si }i∈I with respect to {ei }i∈I and MPN ′′ is the parallel extension of {s′i }i∈I with respect to {e′i }i∈I , as in Fig. 6, then we have to prove that MPN ′′ is the parallel extension of {s′i ◦ si }i∈I with respect to {ei }i∈i MPN1I

II ′ II e1 II II I$ 

u e′n uu u u uu uz u

s1

MPN1′ s′1

MPNn u en uuu u u uu uz u





...

II IIe1 II II I$

MPN1′′

MPN s

′

sn



MPNn′ s′n



MPNn′′

MPN II II uu II uu ′ u s I u II u ′′ e′′1 $  zuu en MPN ′′

Figure 6. Vertical composition of parallel extensions

If we call MPN ′′ the result of the parallel extension of {s′i ◦ si }i∈I with respect to {ei }i∈i , and MPN + the result of the parallel extension of {s′i }i∈I with respect to {e′i }i∈i , we will prove MPN ′′ = MPN +. Then, proving that the corresponding embeddings (from MPNi′ to MPN ′′ and from MPNi′ to MPN +, respectively) coincide and the transformations from MPN to MPN ′′ and from MPN to MPN + also coincide is routine. U U According to the above definitions, we have P′′ = ( i∈I P′′i ⊎ P)/ ≡1′′ , P+ = ( i∈I P′′i ∪ P′ )/ ≡1+ U and P′ = ( i∈I Pi′ ⊎ P)/ ≡1′ , where ≡1′′ , ≡1+ and ≡1′ are the equivalence relations on the sets of places corresponding to the three parallel extensions involved, as defined above. This means that U U P+ = ( i∈I P′′i ∪ ( i∈I P′i ⊎ P)/ ≡1′ )/ ≡1+ . Therefore, to show that P′′ = P+ we have to prove: 1. ∀i ∈ I∀p ∈ Pi′ ∃p′ ∈ ( e′i,P (p) ≡1+ s′i,T (p).

′′ i∈I Pi

U

⊎ P)[p]1′ ≡1+ p′ . However this is obviously true, since [p]1′ =

2. ∀p, p′ ∈ ( i∈I Pi′′ ⊎ P)(p ≡1′′ p′ ) i f f (p ≡1 p′ ), where ≡1 is the least equivalence including ≡1′ and ≡1+ . Let us first prove the left-to-right implication: U

• Suppose p′ ≡1′′ p′′ because there is a p ∈ Pi such that p′ = s′i,P (si,P (p)) and p′′ = ei,P (p). Then, we have that si,P (p) ≡1′ ei,P (p), and this implies that s′i,P (si,P (p)) ≡1 ei,P (p).

• Suppose p ≡1′′ p′ because pi ∈ Pi , pi′ ∈ Pi′ such that p = ei,P (pi ) and p′ = ei′ ,P (pi′ ). Then, we have that si,P (p) ≡1′ si′ ,P (p′ ) and hence s′i,P (si,P (p)) ≡1 s′i′ ,P (si′ ,P (p′ ))

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

11

• Suppose p ≡1′′ p′ because t ∈ Ti ,t ′ ∈ Ti′ , ei,T (t) = ei′ ,T (t ′ ), p ∈ s′i,T (si,T (t)), p′ ∈ s′i′ ,T (si′ ,T (t)), φ′′ : s′i,T (si,T (t)) → s′i′ ,T (si′ ,T (t)) is the isomorphism defined by parallel consistency, and φ′′ (p) = p′ . Since parallel extension is independent of the specific isomorphisms φ′′ chosen, let us assume that φ′′ is defined as follows. For every p′′i ∈ s′i,T (si,T (t)), if there is a p′i ∈ si,T (t) such that s′i,T (p′i ) = p′′i , then we define φ′′ (p′′i ) = s′i′ ,T (φ(p′i )), where φ : si,T (t) → si′ ,T (t ′ ) is the isomorphism associated to t and t ′ used to define MPN ′. But if p′′i ∈ s′i,T (t ′′ )) for some t ′′ ∈ si,T (t), then we define φ′′ (p′′i ) = φ′ (p′′i ), where φ′ : s′i,T (t ′′ ) → s′i′ ,T (φ(t ′′ )) is the isomorphism associated to t ′′ and φ(t ′′ ) used to define MPN +. Similarly, for every ti′′ ∈ s′i,T (si,T (t)) where ti′′ ∈ s′i,T (ti′ )) for some ti′ ∈ si,T (t), then we define φ′′ (ti′′ ) = φ′ (ti′′ ), where φ′ : s′i,T (ti′ ) → s′i′ ,T (φ(ti′ )) is the isomorphism associated to t ′′ and φ(t ′′ ) used to define MPN +. Now, it is routine to prove that φ′′ is indeed an isomorphism and, moreover, that for every p ∈ Pi , p′ ∈ Pi′ if ei,P (p) = ei′ ,P (p′ ) then φ′′ (s′i,T (si,P ((p))) = s′i′ ,T (si′ ,P (p′ )). But now, by construction, if φ′′ (p) = p′ and there is a pi ∈ si,T (t) such that s′i,T (pi ) = p then this means that p′ = s′i′ ,T (φ(pi )), pi ≡1′ φ(pi ) and p ≡1 p′ . On the other hand, if if φ′′ (p) = p′ and p ∈ s′i,T (t ′′ )) for some t ′′ ∈ si,T (t), then this means that p′ = φ′ (p′′i ), where φ′ : s′i,T (t ′′ ) → s′i′ ,T (φ(t ′′ )) is the isomorphism associated to t ′′ and φ(t ′′ ) used to define MPN +. But this implies that t ′′ ≡2′ φ(t ′′ ) and p ≡1 p′ . Conversely, proving the right-to-left implication is very similar, taking into account that we have already proved that every place p ∈ Pi′ is equivalent, with respect to ≡1+ , to a place p′ ∈ U ( i∈I Pi′′ ⊎ P). The proof that T ′′ = T + is similar (but simpler) to the proof for the sets of places. On the other hand, the proof that pre′′ = pre+ , post ′′ = post + , and mark′′ = mark+ is trivial taking into account their definitions. The second property that we should prove is that, if t0 : MPN0 =⇒ MPN0′ is an embedding, then t0 is parallel consistent with respect to any other embedding e0 : MPN0 → MPN, which means that the corresponding (parallel) extension diagram, depicted in Fig. 7, always exists. But, according to the definition of parallel consistency for MPNs, this property trivially holds. Finally, the last property that we have to prove is that, given the extension diagram in Fig. 7, where t0 and t ′ are embeddings, we have that for all embeddings ek : MPNk → MPN, 1 ≤ k ≤ n the diagram in Fig. 8 is a parallel extension diagram, where e′k is the composition of ek and t ′ .

...

MPN0I

MPN0

e0

/ MPN t′

t0



MPN0′

e′0



/ MPN ′

Figure 7. Extension of embeddings

MPNn MPN1 ggggg g uu g g u g e n gg u t0 id uu id gggg uu gggggg gg u   zu sggg ... MPN0′ MPNn MPN1 MPN II ′ u ggggg g ′ g g II e0 e′1 uu e g n gg u II t′ ggggg uu II I$  zuuuggggggggg sg II IIe0 II II I$

e1

MPN ′

Figure 8. Extension of embeddings as parallel extension

12

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

To prove this property it is enough to notice that, according to the above definitions, if t0 is an embedding, the result of the extension in diagram 7 and of the parallel extension in diagram 8, MPN ′, in both cases is essentially just the (componentwise) union of MPN and MPN0′ (where MPN0 is the shared part of MPN and MPN0′ ). ⊓ ⊔ As a consequence, we have proven that Petri nets are a component framework: Theorem 3.2. The class of Marked Petri nets together with the notions introduced above of embedding, transformation, parallel consistency, and parallel extension form a component framework.

3.3. The Architecture in Detail The connector CON1 in Fig. 9 consists of a body net BOD and two role descriptions ROL1 and ROL2, which are included into the body part along the corresponding Petri net inclusions. The dashed lines mark the images of the two roles in the body net. The role ROL1 is meant to specify the required behavior of the used lock mechanism. The second role describes the required behavior of the door. This connector simply reports the release of the key lock from ROL1 to ROL2 via the transition ack key unlock. The key lock can be closed again, after the door is opened via the transition open door, and the connector has reported this event along the transition fin key check. The connector assumes, that the key lock is initially closed. Thus, the role ROL1 bears a token on place locked. Both, place and token are included into the body of the connector. The connectors and the components in our abstract framework are assembled to architectures by transformations between the roles and the ports of the connectors and components, respectively. As mentioned, ROL2 of CON1 is meant to be realized by the door component. The corresponding transformation, i.e. an MPN transformation in our concrete instantiation, is shown in Fig. 10. It maps the places key? to sec1? and key checked to sec1 checked. The transition open door is mapped to the whole target net. CON1 BOD locked key?

ROL2 unlock

lock key?

unlocked

open_door

open_door ack_key_unlock fin_key_check

ROL1

key_checked

key_checked

ROL2 POR2

locked key?

sec1?

unlock

lock

unlocked

Figure 9.

open_door

key_checked

Connector1

open_door

sec1_checked

Figure 10. Connection of CON1 and DOOR

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

13

The DOOR component, depicted in Fig. 11, consists of a body net BOD and three ports POR1, POR2, and POR3. The three ports describe the behavior of the door at an abstract level. In particular, the first port, POR1, describes that one may open the door when is closed and, conversely, one may close it when is open. This port is not used in this small example. It might be used by other applications, e.g. some control system that keeps track of the state of all doors in a building. The transformation relating POR1 to BOD is depicted in Fig. 12. The main issue here is that the transition open door is transformed into the subnet consisting of the transitions check sec and move doors together with the corresponding places. The two other ports, POR2, and POR3, are essentially identical. They describe that when the corresponding security checks have been passed then the door may be opened. Their relation to BOD is similar to the previous transformation. In particular, the transition open door is also mapped to the subnet of BOD consisting of the transitions check sec and move doors together with the corresponding places. The second port POR2 is connected to the role ROL2 of the connector CON1, presented above. The more abstract names (e.g. sec1?, sec1 checked) in the component DOOR are meant to document the genericity of the door with respect to the used security devices. This also applies for the port for the second security device, POR3. Initially the door is closed, which is specified by a token on the place door closed. In Fig. 12 we show how this port is transformed into the body net. The places are simply embedded, the transition close is mapped to the subnet containing the transition close and the two related places. The transition opendoor is mapped to the subnet in the hatched area. The other transformations are simple embeddings of the ports. The body net works as follows. Provided that both security checks are done, the initial token changes to the place sec. Now, the doors can be moved and are open afterwards. This is represented by a token on the place door open. Moreover, the tokens for the security check are returned to the two devices. The closing of the door takes place in a single step, represented by the transition close.

DOOR

POR1

POR1

POR2

door_closed

POR3

door_closed sec2?

sec1? open_door

close

open_door

open_door

close

open_door door_open

door_open

sec1_checked

sec2_checked

BOD door_closed

BOD

sec1?

sec2? check_sec

close

sec

move_doors

sec1_checked

sec2_checked door_open

Figure 11. Specification of the Door

door_closed 1111111111111111111111 0000000000000000000000 0000000000000000000000 1111111111111111111111 0000000000000000000000 1111111111111111111111 0000000000000000000000 1111111111111111111111 sec1? sec2? 0000000000000000000000 1111111111111111111111 0000000000000000000000 1111111111111111111111 0000000000000000000000 1111111111111111111111 check_sec 0000000000000000000000 1111111111111111111111 0000000000000000000000 1111111111111111111111 0000000000000000000000 1111111111111111111111 sec 0000000000000000000000 1111111111111111111111 0000000000000000000000 1111111111111111111111 0000000000000000000000 1111111111111111111111 0000000000000000000000 1111111111111111111111 move_doors 0000000000000000000000 1111111111111111111111 0000000000000000000000 1111111111111111111111 0000000000000000000000 1111111111111111111111 sec1_checked sec2_checked 0000000000000000000000 1111111111111111111111 0000000000000000000000 1111111111111111111111 door_open 0000000000000000000000 1111111111111111111111 0000000000000000000000 1111111111111111111111 0000000000000000000000 1111111111111111111111

close

Figure 12. Transformation POR1 =⇒ BOD

14

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

The component KEY in Fig. 13 contains a body net and a single port, which is connected to the role ROL1 of the connector CON1 via the obvious identity transformation. With the initial token at the place locked in the body net, the only possibility is to insert a key. Afterwards, the key can can be removed without unlocking the door, or it can be turned, which produces a token at the place unlocked. Turning the key back and removing it leads to the original situation. Fig. 14 shows how the port of the component is transformed to the body. The places are simply embedded, while the transition lock is mapped to the subnet in the hatched area and the transition unlock is mapped to the area framed by the dashed line. KEY POR1

POR1 locked

locked unlock

unlock

lock

lock unlocked

unlocked

BOD locked

ins_key

rem_key

key_in

trn_key

retrn_key

unlocked

Figure 13. Specification of the Keylock

111111111 000000000 000000000 111111111 locked 000000000 111111111 000000000 111111111 000000000 111111111 000000000 ins_key111111111 rem_key 000000000 111111111 000000000 111111111 000000000 111111111 key_in 000000000 111111111 000000000 111111111 000000000 111111111 trn_key111111111 retrn_key 000000000 000000000 111111111 000000000 111111111 000000000 111111111 unlocked 000000000 111111111

BOD

Figure 14. Transformation POR1 =⇒ BOD

The connector CON2, shown in Fig. 15, connects the second security device of the architecture to the door component. Thus, the connector assumes a role ROL1 with a transition scan, that represents the event of a successful scan at the device. Moreover, the connector assumes a role ROL2, which is meant to be connected with the door. The body of the connector then synchronizes the two events, such that the door can only be opened, if a successful scan has been reported. When the doors are open, the scanning device returns into the state ready.

The scanner component, whose port POR1 is meant to realize the role ROL1 of CON2, describes the Scanner in more detail. The transition scan is refined to a subnet, which contains a simple failure handling, i.e. to return to the the state ready in case of not recognizing a known pattern. The body has no possibility to re-initialize itself. This synchronization task is directly handled by the connector CON2. Let us now see what is the semantics of the secure door system. According to the results in the first part of this work, we know that the order in which we compute the compositions in a given architecture does not affect the final result. Thus, we show only one way of defining the semantics of the secure door system.

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

15

SCAN POR1 ready

CON2 BOD

scan ready

fin_scan_check

scan_checked scan_suc

scan

open_door

BOD ready

scan_suc

ack_scan

scan? start_scan

ROL1

failure

ROL2 ready

scan

scan_checked open_door

scan_suc

scan?

Figure 15. Connector2

scanned rec_pattern

scan_suc

Figure 16. Specification of the Scanner

In a first step, we compose the components KEY and DOOR along the connector CON1 to a net KEY&DOOR. Fig. 17 shows in the first line the body of the connector CON1 and it’s two roles ROL1 and ROL2 with the corresponding embeddings. The connecting transformation of ROL1 to the port POR1 of the KEY component is an identity transformation, while the transformation of ROL2 to POR2 of the DOOR component is already shown in Fig. 10. These connecting transformations are composed with the transformations in the components that refine the used ports into the corresponding body net. The resulting composed transformations now turn out to be parallel consistent w.r.t. the span of embeddings ROL1 → BOD ← ROL2, which is a requirement for the composition operation. More exactly, the conditions in Def. 3.7 are satisfied, because there are no overlappings of the embedded nets. Since the body nets of the KEY and DOOR component are disjoint, also condition three and four are valid. Conditions five and six are fulfilled since the two body nets of components KEY and DOOR do not add existing places nor transformations. At this point we are able to apply Thm. 3.1 and obtain the composed net KEY&DOOR. Intuitively, all transitions and places of the body net of CON1 are replaced according to their transformation in the roles. If there is not such a role, e.g. in the case of the transitions ack key unlock and fin key check, the transition remains unchanged, but it’s pre and post functions might need adaption according to possible place renamings. This is the case for the places key? and key checked, which are renamed but are in the pre and post sets of transitions that are not changed. Moreover, the transformed roles can also add parts, that are not image of a transition substitution. E.g. the marked place door closed is added to the body of the DOOR component, and thus, also to the result of this composition step. The so far unused other two ports of the DOOR component, not shown in the figure, are preserved by the composition operation. More exactly, the transformation induced by the embedding of the body of the DOOR component into the body of the composed component is composed with the original transformations of the roles into the DOOR body. Thus, the resulting component, depicted in Fig. 18, has two ports, equal to the ports POR1 and POR3 of the DOOR component. Thus, the transformation between the connector CON2 and the port POR3 can be reused unchanged. In connection with the transformation between the connector CON2 and the SCAN component, we get a second parallel extension, with the result shown in Fig. 19, which is also the semantics of the given architecture. As mentioned before, the remaining port can be used for a further extension of the architecture.

16

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

CON1 BOD locked key? unlock

lock

unlocked

ROL1 locked

unlock

open_door

ROL2

ack_key_unlock

key?

fin_key_check

lock

key_checked

open_door

unlocked

key_checked

POR1

POR2 locked sec1?

unlock

lock

open_door

unlocked

sec1_checked

KEY

DOOR

BOD

BOD door_closed locked sec1?

ins_key

sec2?

rem_key close

check_sec key_in sec trn_key

retrn_key move_doors unlocked sec2_checked

sec1_checked

door_open

KEY&DOOR BOD locked

ins_key

door_closed

rem_key

sec1?

sec2? close

check_sec

key_in

sec trn_key

unlocked

retrn_key

ack_key_unlock

move_doors

fin_key_check sec2_checked sec1_checked door_open

Figure 17. Parallel Extension for CON1

4. Architectural connectors based on CSP In [1] Allen and Garlan introduced the notion of architectural connector that has been a source of inspiration for the work in this paper. In particular, in that paper, the architecture of a system is described as consisting of three parts: The first part of the description defines a set of components and connectors (types). A component type is described as a set of ports together with the specification of its functionality, that is what we call the body of the component. A connector type is defined as a set of roles and a glue specification. The roles describe the expected local behavior of each of the interacting parties. That is, they act as a specification that determines the obligations of each component participating in the interaction. The glue specification describes how the activities of the connected components are coordinated. All these specifications are written using CSP [16] as a modelling language The second part of the system definition is a set of components and connector instances. These specify the actual entities that appear in the configuration. Finally, the third part establishes which component ports are linked to which connector roles. That paper, in addition to providing interesting conceptual and methodological discussions, from a

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

KEY&DOOR POR1

17

POR3 door_closed sec2?

open_door

close

open_door

door_open

sec2_checked

BOD locked

ins_key

door_closed

rem_key

sec1?

sec2? check_sec

key_in

close

sec trn_key

unlocked

retrn_key

ack_key_unlock

move_doors

fin_key_check sec2_checked sec1_checked door_open

Figure 18. Specification of the Key Composed with the Door

technical point of view it concentrates on studying only the connectors, their semantics and the operation for attaching ports to roles for the interconnection of components and connectors. Moreover, their main aim is on ensuring deadlock freeness of architectural systems. As a consequence, no technical details are provided about the semantics of architectures, nor about the semantics of components and their interconnection through connectors. In this sense, our paper extends [1] in two senses. On one hand, our constructions and results provide the technical details about architectures and components lacking in [1]. On the other, we provide some additional detail and insight to the concepts introduced in that paper, making explicit some conditions which in [1] are only implicit. However, as pointed out in the introduction and discussed below, we cannot use the compatibility relation between ports and roles introduced in [1], since it is not transitive.

4.1. Basics on CSP CSP [16] is a language (or a process algebra) introduced by Hoare for describing communicating entities. In [1] Allen and Garlan used a subset of this language to specify/describe the behavior of components and connectors as interacting protocols. In what follows, we use the same subset including: • Processes and events: A process describes an entity that can engage in communicating events. The simplest process ST OP is one that engages in no events. On the contrary, the process CHAOS is one that behaves chaotically, that is, that can have any arbitrary behavior. The event √ is used to represent the success event. The set of events with which a process P can communicate, that is, its alphabet, is denoted by αP. • Prefixing: A process that engages in event e and becomes process P is denoted e → P. • Named processes: Process names can be associated with a possibly recursive process expression. For instance, P = (e → P)|(c → Q) being Q = (d → Q).

18

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

KEY&DOOR&SCAN POR1 door_closed

open_door

close

door_open

BOD locked

door_closed ready

ins_key

rem_key

sec1?

sec2? check_sec

key_in

start_scan

failure

close

ack_scan sec trn_key

unlocked

retrn_key

ack_key_unlock

scanned move_doors

fin_key_check

rec_pattern sec2_checked fin_scan_check

sec1_checked

scan_suc

door_open

Figure 19. Specification of the Key Composed with Door and Scanner

• Parallel composition: Processes can be composed using the operator k. Processes P and Q in PkQ interact by synchronously engaging in events from the intersection of their alphabets, so that the behavior of the process PkQ is that permitted by both P and Q. For instance, (e → P)k(e → Q) = (e → PkQ) but (e → P)k(c → Q) = ST OP. • Choice: A process that can behave like P or Q is denoted by P|Q. When the process P|Q is observed in a given environment, that is, in a context where other processes can interact with it, then we can distinguish two different behaviors so that they must be denoted differently: – External choice: P[]Q means that the choice is made by the environment, so that its behavior is deterministic. – Internal choice: P ⊓ Q means that the choice is made internally by the process itself, so that its behavior is nondeterministic from the environment point of view. For instance, if e 6= d then – ((e → P)[](d → Q)) k (e → R) = (e → P)k(e → R) = (e → (PkR))

– ((e → P) ⊓ (d → Q)) k (e → R) = ((e → P)k(e → R)) ⊓ ((e → P)k(d → Q)) = (e → (PkR)) ⊓ ST OP

• Labelling: Events and processes may be labelled. An event e labelled with ℓ is denoted ℓ.e. The operator : is used to label all the events in a process P, so that ℓ : P is the same process P but with each of its events labelled with ℓ. The semantics of a process P is defined in CSP as a triple Sem(P) = (ΣP , FP , DP ) such that i) ΣP is the alphabet of P, i.e. αP,

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

19

∗

ii) FP is set of failures of P, where a failure is a pair of the form (t, X ) where t ∈ ΣP is a trace of P and X ⊆ ΣP is a set of events that P can refuse to participate after executing t, and ∗

iii) DP ⊆ ΣP is a set of divergences, that is, traces of P after which P can behave chaotically (essentially, with arbitrary behavior). See [16] Chapter 3. for more details on the mathematical theory defining the semantics of nondeterministic processes.

4.2. Connectors and components based on CSP As said above, to describe a connector type, Allen and Garlan provide process descriptions for each of the roles and its glue using CSP notation. In order to illustrate this, we revisit the example, borrowed from [1], describing a Pipe connector for a simple Pipe-Filter system, already shown in the Introduction of the first part of this work: Example 4.1. (Pipe connector) The following connector specification shows the basic behavior of a pipe in a pipe-filter systems1 connector Pipe = √ role Writer = write → Writer ⊓ close → √ √ role Reader = (read → Reader [] eof → close → ) ⊓ (close → ) glue = Writer.write → glue [] Reader.read → glue [] Writer.close → ReadOnly [] Reader.close → WriteOnly where ReadOnly = Reader.read → ReadOnly √ [] Reader.eof → Reader.close → √ [] Reader.close → √ WriteOnly = Writer.write → WriteOnly [] Writer.close → The pipe connector has two roles, a Writer and a Reader, that can determine when and how many times it will write and read, respectively. When done writing or reading, each role closes their side of the pipe. In addition, when a Writer closes its end of a pipe, there must be a way to inform the reader that there will be no more data. This makes the specification of the Reader slightly more complex, so that the end of data can be controlled. Note that the glue coordinates the interaction in such a way that it causes the close event of the Writer to appear as a eof event for the Reader. Furthermore, the meaning of a connector description with roles R1 , . . . , Rn and glue G, is defined in [1], as the process GkR1 : R1 k . . . kRn : Rn where Ri : Ri stands for the labelling of the event names in Ri with the distinct name of the role Ri (as can be seen in the above example). Note that this means that the sets of event symbols of the roles in a connector are considered to be disjoint. From our point of view, we consider that the specification GkR1 : R1 k . . . kRn : Rn is the body of the connector. Then, an embedding of a role into the body corresponds to an inclusion of the role expression within a parallel composition expression, as the one above. To be more precise, if we 1 However,

at this level of abstraction the example is not directly modelling, for instance, the FIFO discipline of the pipe.

20

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

analyze the expression GkR1 : R1 k . . . kRn : Rn in more detail, we may notice two things. On one hand, as said above, by definition, the alphabets of the processes R1 : R1 , . . . Rn : Rn are disjoint. Actually, they need to be disjoint since, otherwise, the roles processes would interfere each other. On the other hand, the glue should interact with each of the roles in a proper way. In particular, it makes no sense that a given role could accept a trace that the glue would not accept. In particular, this means that the failures and divergences of this parallel composition, when restricted to the alphabet of each role, should be a subset of the failures and divergences of that role. These considerations yield to the following definitions: Definition 4.1. (CSP specifications) A CSP specification is a pair P = (ΣP , ExpP ) where ΣP is the process signature consisting of a set of event symbols and ExpP is a CSP process expression built over ΣP . If we would follow [1] faithfully then we would define embeddings in terms of signature inclusions that satisfy some additional conditions. However, for technical reasons, we provide a slightly more general definition, allowing the renaming of signatures. As a consequence, before defining our notion of embedding, we need to provide some notation. In particular, given an injective mapping between two process signatures h : Σ1 → Σ2 , although the abuse of notation, we also denote by h the mapping that transforms any Σ1 -expression into a Σ2 -expression, by replacing every event symbol p by the corresponding symbol h(p). Conversely, given a set of Σ2 -traces T , we denote by T |h the largest set of Σ1 -traces whose translation through h is included in T . According to the above intuitions we define CSP embeddings as follows: Definition 4.2. (CSP embeddings) Given two CSP specifications P1 and P2 , an embedding e : P1 ֒→P2 is an injective mapping from the corresponding signatures, e : ΣP1 → ΣP2 that satisfies that there are two processes G and Q such that: i) ExpP2 ≡ ExpG ke(ExpP1 )kExpQ . ii) ΣP2 = ΣG , / iii) e(ΣP1 ) ∩ ΣQ = 0. iv) FExpP2 |e ⊆ FExpP1 and DExpP2 |e ⊆ DExpP1 . Intuitively, the process G corresponds to the glue of the connector and Q to the parallel composition of the rest of the roles. Then, in this framework, an n-ary CSP connector specification, can be represented as a set of n + 1 CSP specifications together with n embeddings: con = (R1 , . . . , Rn , B, {ei : Ri ֒→B}1≤i≤n ) such that a) ExpB = ExpG kExpR1 k . . . kExpRn , and / for every 1 ≤ i, j ≤ n with i 6= j. b) ei (Ri ) ∩ e j (R j ) = 0, provided that the glue and the roles satisfy the above conditions. It is easy to see that the identity is an embedding and that embeddings are transitive: Proposition 1. (Properties of embeddings in CSP) 1. Given a process specification P, we have that P֒→P

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

21

2. If e1 : P1 ֒→P2 and e2 : P2 ֒→P3 then e2 ◦ e1 : P1 ֒→P3 . Proof: 1. It is enough to note that, according to the laws of parallel composition [16], ExpP ≡ ExpRUNΣP kExpP kExpRUN0/ where RU NΣ is a process over the alphabet Σ that can always engage in any event of its alphabet. / process (it does nothing over the empty alphabet). Obviously, ΣP ⊆ ΣRUNΣP ; ΣP ∩ ΣRUN0/ = 0; and FRUNΣP ⊆ FExpP and DRUNΣP ⊆ DExpP . 2. If P1 ֒→P2 and P2 ֒→P3 then this means that ExpP2 ≡ ExpG1 ke1 (ExpP1 )kExpQ1 and, similarly, ExpP3 ≡ ExpG2 ke2 (ExpP2 )kExpQ2 . Therefore, ExpP3 ≡ ExpG2 ke2 (ExpG1 ke1 (ExpP1 )kExpQ1 )kExpQ2 but this implies that ExpP3 ≡ (ExpG2 ke2 (ExpG1 ))ke2 (e1 (ExpP1 ))k(e2 (ExpQ1 )kExpQ2 ) Now, ΣP3 = e1 (ΣG1 ) ∪ ΣG2 , since e2 is an embedding and hence we have that ΣP3 = ΣG2 . / since e1 (ΣP1 ) ∩ ΣQ1 = 0/ by hypothesis, and In addition, e2 (e1 (ΣP1 )) ∩ (e2 (ΣQ1 ) ∪ ΣQ2 ) = 0, / Finally, if FExpP2 |e1 ⊆ e2 (e1 (ΣP1 ) ∩ ΣQ2 = 0/ because e1 (ΣP1 ) ⊆ ΣP2 and e2 (ΣP2 ) ∩ ΣQ2 = 0. FExpP1 and FExpP3 |e2 ⊆ FExpP2 then FExpP3 |e2 ◦e1 ⊆ FExpP1 . Similarly, if DExpP2 |e1 ⊆ DExpP1 and DExpP3 |e2 ⊆ DExpP2 then DExpP3 |e2 ◦e1 ⊆ DExpP1 . ⊓ ⊔ Now, we have to define the notion of transformation for this kind of specifications. In principle, an obvious choice would be to use the notion of process refinement for CSP [16]: Definition 4.3. (CSP refinement [16]) A process Q is a refinement of a process P, denoted P⊑CSP Q if ΣP = ΣQ , FQ ⊆ FP and DQ ⊆ DP . In [1] the relation between the ports and the body of a component is not considered. However, Allen and Garlan discuss the possible use of CSP refinements for describing when it is possible to attach a role R to a port P in a given connection and they conclude that refinements are not adequate for modelling these attachments. The first problem that they point is that, in most cases, the event symbols used in R and P do not coincide, which is not possible for CSP refinements. For instance, the event symbols used in R may be a subset of those used in P if a given port offers possibilities that are not used by an interaction. Similarly, the set of event symbols used in P may not include some of the symbols used in R if the component do not take advantage of parts of the interaction. The solution is quite simple, it is enough to augment the alphabets of the two processes so that they become identical. There is another aspect in CSP refinements that Allen and Garlan consider a limitation in this context. In particular, they considere that, in the context of a refinement of a role R by a port P, P may include failures or divergences which are not included in R as long as these anomalous behaviors are excluded by the connector. Technically, this is defined as follows: [1]: P compat R iff R+(αP\αR)⊑CSP P+(αR\αP) kdet(R)

22

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

where R+(αP\αR) is the process R increased with the alphabet of P,2 and vice versa, and det(R) is the deterministic version of process R, that is, it has the same alphabet, it does not have divergences and its failures are only those produced by its refusals3 . This notion of compatibility is certainly the most general notion that can be used for describing when one can consider adequate the replacement of a role by a port. However, we cannot use it in our framework because, as the counter-examples below show, compatibility is not transitive. This means that, if we use the same kind of notion for defining the relation between a port and the body of a component, then a role may be incompatible with the body of a component even if the role is compatible with a given port of that component and the port is compatible with the body. Counterexample 1. (Composition does not preserve compatibility) In both of the following examples we have that P1 compat P2 and P2 compat P3 but P1 compat P3 does not hold. Let Q = b → Q and consider the processes: P1 = (a → Q) ⊓ (b → Q) P2 = (a → Q) P3 = (a → Q)[](b → CHAOS) The trace b is a divergence of P3 because its behavior becomes chaotic after executing b. It is not difficult to see that it is also a divergence of P3 kdet(P1 ) because P3 and P1 can synchronize on b and then proceed chaotically. However, b is not a divergence of P1 . A similar situation arises in the following example: √ P1 = (a → Q) ⊓ (b → ) P2 = (a → Q) √ P3 = (a → Q)[](b → b → ) √ Now, the problem is that (b, {b, }) is a failure of P3 kdet(P1 ) because after synchronizing in b the process would deadlock. However, notice that it is not a failure of P1 . We think that this limitation is the price to pay for the generality of the approach. Nevertheless, we think that we could overcome this problem at the cost of making our framework more complex. In particular, what we would need is to consider that models are not just related by means of embeddings and transformations, but also by port-role connections, which would not need to be transitive. Then we would have to modify some of the basic assumptions of our framework. For instance, we would need that a port-role connection composed with a transformation is a port-role connection. And we would also have to reformulate the extension and parallel extension constructions along the same direction. However, we think that this kind of additional complication is not worth, since this kind of situation is not very frequent. As a consequence, we consider that, to define the notion of transformation between this kind of specifications, in our context it is more adequate to use CSP refinements, but allowing the processes involved to use different sets of event symbols. In particular, we just consider that certain event symbols in both processes are identified through a partial injective mapping between their corresponding sets of symbols, t : Sigma1 → Σ2 , or equivalently through a span of injective morphisms t : Σ1 ← Σ0 → Σ2 , where Σ0 is the domain of t, i.e., the intersection of Σ1 and Σ2 . 2 That is, R

+(αP\αR) = RkST OPαP\αR, the process that has the same traces as R but a bigger set of failures due to the presence of new event symbols. 3 That is, f ailures(det(R)) = {(t, X) | t ∈ traces(R) and ∀e ∈ X,t · hei ∈ / traces(R)}

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

23

Definition 4.4. (Transformations) Given two process specifications P1 and P2 and a partial injective (labelling) mapping t : ΣP1 ← Σ0 → ΣP2 . If Σ is the signature resulting from the pushout diagram4 in figure 20 and if t(ExpP1 ) stands for the (partially) renamed process expression obtained by applying t to every event symbol occurring in ExpP1 , Then, we say that t : P1 =⇒ P2 is a transformation (or P2 is a transformation of P1 if the mapping t is implicit) if (Σ,t(ExpP1 ))⊑CSP (Σ, ExpP2 ). / ΣP 3

t2−1 (ΣP3 ) p.o.

Σ0

/ ΣP 2

t1−1 (ΣP2 )





p.o.



ΣP1



2

p.o.

/Σ

Figure 20. Sum of ΣP1 and ΣP1 via t.

ΣP1

 / Σ23

/ ΣP

p.o.



/ Σ12

 / Σ123

Figure 21. Sum of Σ1 , Σ2 and Σ3 via t1 and t2 .

Now, it should be obvious that the identity is a transformation and that embeddings are transformations, since property iv) of the definition of embeddings trivially implies that an embedding is a transformation. Let us now see that transformations are closed under composition: Proposition 2. (Composition of transformations) Given CSP process specifications P1 , P2 and P3 , if t1 : P1 =⇒ P2 and t2 : P2 =⇒ P3 are transformations then t2 ◦ t1 : P1 =⇒ P3 is a transformation. Proof: First of all, it is trivial that t2 ◦t1 is a partial injection if t1 and t2 are partial injections. Let Σ12 , Σ23 and Σ13 be the signature extensions defined via t1 , t2 and t2 ◦ t1 , respectively, as defined in Fig. ??. Then, we have to prove that, (Σ13 ,t2 ◦ t1 (Exp1 ))⊑CSP (Σ13 , Exp3 ) if (Σ12 ,t1 (Exp1 ))⊑CSP (Σ12 , Exp2 ) and (Σ23 ,t2 (Exp2 ))⊑CSP (Σ23 , Exp3 ). For this purpose, one may recall that adding new events to processes just changes its semantics by adding new refusals (but not traces) on the new events. As a direct consequence, it is easy to see that the following statement holds: Given process specifications (Σ, Exp1 ) and (Σ, Exp2 ) then, for every signature Σ′ such that Σ ⊆ Σ′ , (Σ, Exp1 )⊑CSP (Σ, Exp2 ) if, and only if, (Σ′ , Exp1 )⊑CSP (Σ′ , Exp2 ). Then, it is enough to prove that (Σ123 ,t2 ◦ t1 (Exp1 ))⊑CSP (Σ123 , Exp3 ) as a consequence of (Σ123 ,t1 (Exp1 ))⊑CSP (Σ123 , Exp2 ) and (Σ123 ,t2 (Exp2 ))⊑CSP (Σ123 , Exp3 ) is the sum of signatures ΣP1 and ΣP2 with respect to its shared (via t) event symbols: Σ = (ΣP1 \ t −1 (ΣP2 )) ∪ ΣP2 (up to isomorphism).

4 That

24

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

being Σ123 the signature that extends Σ1 , Σ2 and Σ3 via t1 and t2 . That is, the signature resulting from the following composition of pushout diagrams in figure 21. Finally, the above transitivity statement is a direct consequence of the facts that labelling is monotonic with respect to ⊑CSP . ⊓ ⊔ To end, we have to prove that we can define parallel extensions associated to these notions of embedding and transformation, provided that the adequate notion of parallel consistency is satisfied. In particular, our notion of parallel consistency may be considered a bit restrictive since it requires the specifications Ri to be pairwise disjoint. Actually, we could have weakened these properties. However, we have just followed the definitions in [1], where all the roles are pairwise disjoint: Definition 4.5. (Parallel Consistency) Given the CSP specifications Ri , 1 ≤ i ≤ n, and B, where ei : Ri ֒→B are embeddings and ExpB ≡ ExpG kExpR1 k . . . kExpRn kExpQ , and given the specifications Pi , 1 ≤ i ≤ n together with the transformations ti : Ri =⇒ Pi . We say that the transformations ti are / parallel consistent with respect to these embeddings if for every i, j, 1 ≤ i 6= j ≤ n, ei (Σi ) ∩ e j (Σ j ) = 0. Now, we have to prove that parallel consistency also satisfies the parallel extension propery: Theorem 4.1. (Parallel extension for CSP specifications) Given a family of transformations ti : Ri =⇒ Pi and a family of embeddings ei : Ri ֒→B, with 1 ≤ i ≤ n, such that they are parallel consistent, we can define their parallel extension t ′ : B ⇒ B′ with embeddings e′i : Ri ֒→B′ for i = 1, . . . , n according to Fig. 22.

ΣR 1  p C

...

n Rn }N } } tn t1 }} } }   ~} P1 Ap B n Pn AA }N } AA } t A }} e′1 AA  ~}}} e′n

R1 Ap

AA e AA 1 AA A

en

|> || | || . || Σ1 Bp BB BB BB B

Σ Nn Rn `BB BB {{ { BB { BB {{ { 0P }{ t t1 n ΣB N n Σn || | | || ~|| ΣP1  p n ΣPn CC {N CC { { CC {{ e′1 CC!  }{{{ e′n ...

CC e CC 1 CC C!

en

B′

ΣB ′

Figure 22. Parallel extension diagram for CSP.

Figure 23. Parallel extension of signatures.

Proof: Given the family of embeddings ei : Ri ֒→B, with 1 ≤ i ≤ n, it is easy to see that there should be processes G and Q such that ExpB ≡ ExpG ke1 (ExpR1 )k . . . ken (ExpRn )kExpQ , and such that the rest of the properties for the embeddings hold.

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

25

Let B′ = (ΣB′ , ExpG ke′1 (ExpP1 )k . . . ke′n (ExpPn )kExpQ , where ΣB′ is the result of putting together the signatures of all the processes involved. That is, technically, ΣB′ is the colimit of the diagram in Fig. 23. In this context, it is routine to check that for every i, Pi ֒→B′ . Now, we define the transformation t : B =⇒ B′ in terms of the (total) injective mapping from ΣB to ΣB′ in Fig. 23 Then, we have to prove that (ΣB′ ,t(ExpB ))⊑CSP (ΣB′ , ExpB′ ). Now, we know that: (ΣB′ ,t(ExpB )) = (ΣB′ ,t(ExpG ke1 (ExpR1 )k . . . ken (ExpRn )kExpQ )) ⊑CSP (ΣB′ , t(ExpG )kt(e1 (ExpR1 ))k . . . kt(en (ExpRn ))kt(ExpQ )) because k and relabelling distribute. On the other hand we know that for every i t1 : Ri =⇒ Pi is a transformation, i.e.: (Σi ,ti (ExpRi )) ⊑CSP (Σi ,ti (ExpPi )), where Σi is the signature extending ΣRi and ΣPi with respect to the transformation ti . Then, for every i, (ΣB′ ,t(ei (ExpRi ))) ⊑CSP (ΣB′ , e′n (ExpPn )). So, (ΣB′ , t(ExpG )kt(e1 (ExpR1 ))k . . . kt(en (ExpRn ))kt(ExpQ )) ⊑CSP (ΣB′ , t(ExpG )ke′1 (ExpP1 )k . . . ke′n (ExpPn )kt(ExpQ )) = (ΣB′ ,t(ExpB′ )), since parallel composition preserves refinement. One may see that, assuming that all injective mappings are inclusions, our parallel extension construction corresponds to the construction used in [1] to describe the meaning of attaching ports to roles of a given connector. In particular, in that paper this is defined as follows: [1]: The meaning of attaching ports P1 . . . Pn as roles named R1 . . . Rn of a connector with glue G is the process: GkR1 : P1 k . . . kRn : Pn . To end, we have to prove that the rest of the properties of parallel extension are satisfied by our definition. The first one is that parallel extension diagrams are closed under vertical composition. More precisely, let us suppose that B′ is the parallel extension of ti : Ri =⇒ Pi , with 1 ≤ i ≤ n, with respect to ei : Ri ֒→B and B′′ is the parallel extension of ti′ : Pi =⇒ Pi′ , with 1 ≤ i ≤ n, with respect to e′i : Pi ֒→B′ , as in Fig. 24, then B′′ is the parallel extension of ti′ ◦ ti : Ri ⇒ P′i with respect to e′i ◦ ei : Ri ֒→B. ...

n Rn }N } }} tn t1 }}   ~}} P1 @o B o Pn @@ e′ ~O ′ ~ e @ n 1 ~ @@ ~ t1′ tn′ @@ t ~~~     ~ ′ P1′ @o B′ oO Pn @@ e′′ ~ ′′ en ~~ @@ 1 @@ t ′ ~~~ @  ~~~

R1 Ap

AA e AA 1 AA A

en

B′′

Figure 24. Vertical composition of parallel extensions

The proof is quite simple. Assuming that ExpB ≡ ExpG ke1 (ExpR1 )k . . . ken (ExpRn )kExpQ , it is enough to note that the result specification B′′ is equal to (ΣB′′ , ExpG ke′′1 (ExpP1′ )k . . . ke′′n (ExpPn′ )kExpQ ,

26

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

independently of whether we perform one parallel extension after the other or if we directly compute the parallel extension of ti′ ◦ ti : Ri ⇒ P′i with respect to Ri ֒→B. The second property that we must prove is that a family of transformations consisting of a single P transformation t : P1 =⇒2 , which moreover is an embedding, is always parallel consistent with any embedding e : P1 → P3 . But this is obvious from the definition of parallel consistency. The last property that we have to prove is that given the extension diagram in Fig. 25, where t0 and t ′ are embeddings, then for all embeddings ek : Rk → M, 1 ≤ k ≤ n the diagram in Fig. 26 is a parallel extension diagram.

... GgR oO R1 _ iiii n _ i @@ e ~ i i e1 ~~ en iii @@ 0 t0 id @@ ~~ idiiiiiii ~ @ i   ~~~iiii  i t ... P0 @ o B _ o R1 iG g Rn iiii ~O @@ e′ ′ ′ i i e e ~ i n iii @@0 t ′ 1 ~~ @@ ~ iiiiiii ~ i  ~~tiiii

R0 _ @o R0 _ 



e0

/ B _ t′

t0

 

P0

e′0



/ B′

Figure 25. Extension of embeddings

B′

Figure 26. Extension of embeddings as parallel extension

To prove this property it is enough to notice that, if ExpB ≡ ExpG ke1 (ExpR1 )k . . . ken (ExpRn )kExpQ , then according to the above definitions, the result of the extension in Fig. 25 and of the parallel extension in Fig. 26 is in both cases the process B′ = (ΣB′ , ExpG ke′j (ExpPj )ke1 (ExpR1 )k . . . e j−1 (ExpR j−1 )ke j+1 (ExpR j+1 )k . . . ken (ExpRn )kExpQ ) up to a signature renaming

⊓ ⊔

As a consequence, we have shown that CSP specifications are a component framework: Theorem 4.2. The class of CSP processes together with the notions introduced above of embedding, transformation, parallel consistency, and parallel extension form a component framework.

5. Related work There has been several approaches to define module or component constructions to Petri Nets. However, in our opinion, most of them have have a limited interest to be used, in a straightforward way, as a basis to define architectural connectors and components. More precisely, many modular or component approaches to Petri Nets are just based on the use of hierarchical Petri Nets (e.g. [18, 8, 14, 13]) or of open nets where a given set of open places serves as interface (e.g. [27]), or on adding to nets explicit mechanisms for communication, coordination or cooperation (e.g. [9, 26, 11, 10]), without defining proper module or component concepts including general and well-defined notions of interfaces. In other approaches Petri net components are just nets where a set of places and transitions is implicitly considered as an interface and where they are merged by well-defined operations (e.g. [5, 4, 7, 19, 2, 15]). The work which is, obviously, more related to the instantiation that we present in

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

27

this paper is [23, 24]. However, in these papers modules can only have one import and one export interface, which means that the only possible architectures that one can model consist just of a sequence of modules. In addition to Wright, there are also several approaches that use different kinds of process algebras for the modeling of architectures (e.g., [21, 6, 3, 22]). For instance, the languages Darwin and π-ADL[21, 22]) are based on the π-calculus; PADL [6] is defined over a process algebra tailored for that language, and AEMILIA [3] can be seen as a stochastic extension of PADL. However, the kind of aspects of architectural design that are highlighted by these approaches is quite different to the aspects studied in this paper. More precisely, we are especially interested in the modeling of components, what is the compatibility relation that allow us to connect ports and roles (or required and provided interfaces) and what is the overall semantics of a component-based system. However, in these approaches, the main aim is to describe the runtime behavior of architectural systems in order to develop methods and tools to prove some properties related with this behavior. For this reason, the functionality of components can be abstracted away, the components may be seen just as a given process, and the interfaces are just the communication channels, i.e. no specific notion of connector as a first class citizen is needed.

6. Conclusion In this paper we have shown how we can instantiate the generic framework introduced in the first part of this work to define architectural component and connector notions for a given modeling framework. In particular, This has been done for Petri Nets and for CSP. Defining these instantiations has meant defining some given constructions, in particular extensions and parallel extensions, in terms of the given formalisms and showing that they satisfy the axioms presented in the generic framework. Then, the instantiation to these formalisms of the framework presented in the first part means that we have notions of components and architectural connectors for Petri nets and for CSP and we are able to interconnect them to form architectures. Moreover, the results in the first part, provide the semantics for these architectures. To give the intuition about how our framework works , we have presented a small case study modelling a door security system. Acknowledgements: This work is partially supported by the Spanish project GRAMMARS (TIN2004-07925-C03-01) supported by FEDER, and by the CIRIT Grup de Recerca Consolidat 2001SGR 00254

References [1] R. Allen, D. Garlan. A Formal Basis for Architectural Connection. In ACM Trans. on Software Engineering and Methodology 6(3): 213–249, 1997. [2] N. Aoumeur, G. Saake. A component-based Petri net model for specifying and validating cooperative information systems. Data Knowl. Eng. 42(2): 143–187, 2002. [3] S. Balsamo, M. Bernardo, M. Simeoni. Performance evaluation at the software architecture level. In Formal Methods for Software Architecture, (Bernado, M. and Inveradi, P., eds.), volume 2804 of Lecture Notes in Computer Science, pages 207–258. Springer, 2003. [4] E. Battiston, F.D. Cindio, G. Mauri. OBJSA nets: a class of high-level nets having objects as domains. In G. Rozenberg (Ed.), Advances in Petri Nets, volume 340 of Lecture Notes in Computer Science, pages 20–43. Springer, 1988.

28

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

[5] E. Battiston, F.D. Cindio, G. Mauri, L. Rapanotti. Morphisms and minimal models for OBJSA nets. In 12th International Conference on Application and Theory of Petri Nets, volume 524 of Lecture Notes in Computer Science, pages 455–476. Springer, 1991. [6] M. Bernardo, P. Ciancarini, Lorenzo Donatiello: Architecting families of software systems with process algebras. ACM Trans. Software Engineering and Methodology 11(4): 386–426, 2002. [7] M. Broy, T. Streicher. Modular functional modelling of Petri nets with individual tokens. In Advances in Petri Nets, volume 609 of Lecture Notes in Computer Science, pages 70–88. Springer, 1992. [8] P. Buchholz. Hierarchical high level Petri nets for complex system analysis. In Application and Theory of Petri Nets, volume 815 of Lecture Notes in Computer Science, pages 119–138. Springer, 1994. [9] S. Christinsen, N. Hansen. Coloured Petri nets extended with channels for synchronous communication. In Application and Theory of Petri Nets, volume 815 of Lecture Notes in Computer Science, pages 159–178. Springer, 1994. [10] W. Deiters, V. Gruhn. The FUNSOFT net approach to software process management. International Journal on Software Engineering and Knowledge Engineering 4(2): 229–256, 1994. [11] J. Desel, G. Juhs, R. Lorenz. Process semantics of Petri nets over partial algebra. In Proceedings of the XXI International Conference on Applications and Theory of Petri Nets, volume 1825 of Lecture Notes in Computer Science, pages 146–165. Springer, 2000. [12] H. Ehrig, K. Ehrig, U. Prange, G. Taentzer. Fundamentals of Algebraic Graph Transformation. EATCS Monographs in Theoretical Computer Science. Springer, 2006. [13] R. Fehling. A concept of hierarchical Petri nets with building blocks. In Advances in Petri Nets93, volume 674 of Lecture Notes in Computer Science, pages 148–168. Springer, 1993. [14] X. He. A formal definition of hierarchical predicate transition nets. In Application and Theory of Petri Nets, volume 1091 of Lecture Notes in Computer Science, pages 212–229. Springer, 1996. [15] J. F. Groote, M. Voorhoeve. Operational semantics for Petri net components. Theor. Comput. Sci. 379(1-2): 1–19, 2007. [16] C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985. [17] P. Inverardi, A. L. Wolf: Formal Specification and Analysis of Software Architectures Using the Chemical Abstract Machine Model. IEEE Trans. Software Engineering 21(4): 373-386, 1995. [18] K. Jensen. Coloured Petri nets. Basic concepts, analysis methods and practical use. EATCS Monographs in Theoretical Computer Science. Springer, 1992. [19] E. Kindler, Modularer Entwurf verteilter Systeme mit Petrinetzen, Ph.D. thesis, Technische Universit¨at M¨unchen, Institut f¨ur Informatik, 1995. [20] M. Klein, Transformation-Based Component Architectures – General Framework, Instantiations and Case Study. Ph.D. thesis, Technische Universit¨at Berlin, 2006. [21] J. Magee, J. Kramer. Dynamic Structures in Software Architecture. In David Garlan (Ed.), Proc. 4th ACM SIGSOFT Symposium on the Foundations of Software Engineering, ACM SIGSOFT Software Engineering Notes 21(6): 3–14, 1996. [22] F. Oquendo: pi-ADL: an Architecture Description Language based on the higher-order typed pi-calculus for specifying dynamic and mobile software architectures. ACM SIGSOFT Software Engineering Notes 29(3): 1–14, 2004. [23] J. Padberg. Place/transition net modules: Transfer from specification modules. Forschungsbericht 2001/05, Fakult¨at IV – Elektrotechnik und Informatik, TU Berlin, 2001. [24] J. Padberg, H. Ehrig. Petri net modules in the transformation-based component framework. J. Log. Algebr. Program. 67(1-2): 198–225, 2006.

F. Orejas, H. Ehrig et al / A Generic Approach. Part II

29

[25] W. Reisig. Petri Nets. EATCS Monographs in Theoretical Computer Science. Springer, 1985. [26] C. Sibertin-Blanc. Cooperative nets. In Application and Theory of Petri Nets, volume 815 of Lecture Notes in Computer Science, pages 471–490. Springer, 1994. [27] F. L. Tiplea, A. Tiplea: Petri net reactive modules. Theor. Comput. Sci. 359 (1-3): 77–100, 2006. [28] M. Urbasek and J. Padberg. Preserving liveness with rule-based refinement of place/transition systems. In Proc. of Sixth World Conference on Integrated Design and Process Technology, Pasadena, USA, 2002.