key: cord-0045115-kbyq2la0 authors: Pittou, Maria; Rahonis, George title: Architecture Modelling of Parametric Component-Based Systems date: 2020-05-13 journal: Coordination Models and Languages DOI: 10.1007/978-3-030-50029-0_18 sha: ecae59b239f5b91739b317bc01a7bf8c44bb21e9 doc_id: 45115 cord_uid: kbyq2la0 We study formal modelling of architectures applied on parametric component-based systems consisting of an unknown number of instances of each component. Architecture modelling is achieved by means of logics. We introduce an extended propositional interaction logic and investigate its first-order level which serves as a formal language for the interactions of parametric systems. Our logic effectively describes the execution order of interactions which is a main feature in several important architectures. We state the decidability of equivalence, satisfiability, and validity of first-order extended interaction logic formulas, and provide several examples of formulas describing well-known architectures. Developing well-founded modelling techniques is a challenging task for large and complex systems. Rigorous formalisms in systems engineering are mainly component-based that allow reconfigurability and validation [8] . Componentbased design lies in constructing multiple components which coordinate in order to generate the global model for a system [8, 20] . Therefore, defining the communication patterns of systems is one of the key aspects in modelling process. Coordination principles can be specified by means of architectures that characterize the permissible interactions and their implementation order as well as the topology, of the system's components [28, 34] . Architectures have been proved important in systems modelling since they enforce design rules on the components, and hence ensure correctness by construction with respect to basic properties such as deadlock freedom and mutual exclusion [7, 10, 28] . In this paper we provide a formal framework for the architecture modelling of parametric component-based systems using a first-order logic. Parametric systems represent a wide class of component-based systems including communication protocols and concurrent and distributed algorithms [1, 9, 17] . Parametric systems are constructed by a finite number of component types each consisting of an unknown number of instances [4, 9] . We address the problem of modelling the ordering restrictions for the components' connections, an important aspect of several parametric architectures, including Publish/Subscribe and Request/Response [15, 38] . For instance, in a Request/Response architecture a service needs firstly to enroll in the service registry and then receives requests from the interested clients. On the other hand, several services fulfilling the same task, maybe be enrolled in the registry in any order. We model components with the standard formalism of labelled transitions systems (cf. [2, 3, 8, 22] ) where communication is performed by their set of labels, called ports, and is defined by interactions, i.e., sets of ports. Then, architectures are modelled by logic formulas encoding allowed interactions and their execution order. Briefly, the contributions of our work are the following: (1) We introduce Extended Propositional Interaction Logic (EPIL for short) over a finite set of ports, which augments PIL from [28] with two operators namely the concatenation * and the shuffle operator . In contrast to PIL, where the satisfaction relation is checked against interactions, EPIL formulas are interpreted over finite words whose letters are interactions. Intuitively, the semantics of concatenation and shuffle operator specifies the execution of consecutive and interleaving interactions, respectively. We apply EPIL formulas for formalizing Blackboard [14] , Request/Response [15] , and Publish/Subscribe [18] architectures. (2) We introduce First-Order Extended Interaction Logic (FOEIL for short), as a modelling language for the architectures of parametric systems. The syntax of FOEIL is over typed variables and is equipped with the syntax of EPIL, the common existential and universal quantifiers, and four new quantifiers, namely existential and universal concatenation and shuffle quantifiers. The new quantifiers achieve to encode the partial and whole participation of component instances in sequential and interleaved interactions of parametric architectures. In [28] the authors introduced a Propositional Configuration Logic (PCL) as a modelling language for the description of architectures. First-and second-order configuration logic was considered for parametric architectures (called styles of architectures in that paper). PCL which was interpreted over sets of interactions has a nice property: for every PCL formula an equivalent one in full normal form can be constructed. This implied the decidability of equivalence of PCL formulas in an automated way. Though PCL does not describe the order of interactions required by architectures as it is done by our logics, EPIL and FOEIL. In [26] the first-order level of PIL, namely First-Order Interaction Logic (FOIL) was introduced to describe finitely many interactions, for parametric systems in BIP (cf. [8] ). FOIL applied for modelling classical architectures (Star, Ring etc.) and contributed to model checking of parametric systems. Monadic Interaction Logic (MIL) was introduced in [10] as an alternative logic for the interactions of parametric systems. MIL was used for the description of parametric rendezvous and broadcast communication and applied for developing an automated method for detecting deadlocks. In the same line, in [11] , an Interaction Logic with One Successor (IL1S) was developed for describing rendezvous and broadcast communications, and the architectures of parametric systems. IL1S was proved to be decidable and used for checking correctness of safety properties of parametric systems. FOIL, MIL, and IL1S, have been proved satisfactory for formalizing communication and architectures in parametric systems, though without capturing any order restrictions, as required by each architecture. One of the main features in BIP framework is "priorities among interactions" (cf. [8] ). A priority system is determined by a strict partial order ≺ among the set of permitted interactions. If a ≺ a for two interactions a and a , then a must be implemented before a since it has bigger priority. Clearly the set of strings of interactions satisfying an EPIL sentence containing a shuffle operator, cannot be obtained by any strict partial order among the set of interactions. In [5] the authors established a strict framework for architectures composability. There, architectures were considered as operators enforcing properties to semantics of systems' components. Preservation of safety and liveness properties was also studied for composed architectures. The subsequent work in [7] investigated architectures of composed-based systems with data and conditions under which safety properties are preserved. In both works the required order of the interactions' execution in architectures has not been considered. Hennessy and Milner introduced in 1985 (cf. [23] ) a logic, called HML, as a calculus for the specification of concurrent programs and their properties. In [19] the authors studied μHML, i.e., HML with least and greatest fixpoints and focused on a fragment of that logic that is monitored for runtime verification of programs' execution. μHML succeeded to describe simple client/server processes but it is far from describing complex architectures. Specifically our shuffle operator cannot be described in μHML. In [20] the authors introduced the Components and Behaviors (CAB) process calculus which extended BIP with dynamic capabilities and showed the expressiveness of its priorities. The paper studied dynamic composition of subcomponents based on the calculus language which though does not cover the architecture of the compound system. Distributed systems were investigated in the setup of pomsets in [21] (cf. also [36] ) where the execution order of interactions was considered. Though, due to the imposed orders of pomsets, our shuffle operation cannot be sufficiently described in this framework. For instance, the subfomula ϕ 1 ϕ 2 of the EPIL formula ϕ describing the Publish/Subscribe architecture (cf. Example 3) cannot be described by means of pomsets. Multiparty session types described efficiently communication protocols and their interactions patterns (cf. for instance [24, 25] ). The relation among multiparty session types and communicating automata was studied in [16] . Parameterized multiparty session types were investigated in [13, 17] . Nevertheless, the work of [17] did not study the implementation order of the parameterized interactions and the models of [13, 16, 24, 25] did not consider the architectures of the systems. Finally, an architectural design rewriting model for the development and reconfiguration of software architectures was introduced in [12] . Though, no order of interactions' execution was considered. For every natural number n ≥ 1 we denote by [n] the set {1, . . . , n}. For every set S we denote by P(S) the powerset of S. Let A be an alphabet, i.e., a finite nonempty set. We denote by A * the set of all finite words over A and we let A + = A * \ {ε} where ε denotes the empty word. Given w, u ∈ A * , the shuffle product w u of w and u is a language over A defined by A component-based system consists of a finite number of components of the same or different type. We define components by labelled transition systems (LTS for short) like in well-known component-based modelling frameworks including BIP [8] , REO [3] , X-MAN [22] , and B [2] . Formally, an atomic component is an LTS B = (Q, P, q 0 , R) where Q is a finite set of states, P is a finite set of ports, q 0 is the initial state and R ⊆ Q × P × Q is the set of transitions. We call an atomic component B a component, when we deal with several atomic components. For every set B = {B(i) | i ∈ [n]} with B(i) = (Q(i), P (i), q 0 (i), R(i)), i ∈ [n], we assume that (Q(i)∪P (i))∩(Q(i )∪P (i )) = ∅ for every 1 ≤ i = i ≤ n. Here we focus only on the communication patterns of systems' components, using the terminology of BIP for the basic notions. Communication is achieved through components' interfaces. The interface of an LTS corresponds to its set of labels, called ports. Then, communications of components are defined by interactions, i.e., sets of ports, that can be represented by formulas of propositional interaction logic (PIL for short) [10, 11, 28] . Hence, firstly we need to recall PIL. Let P be a nonempty finite set of ports. Then I(P ) = P(P ) \ {∅} is the set of interactions over P . The syntax of PIL formulas φ over P is given by the grammar φ : PIL formulas are interpreted over interactions in I(P ). For every PIL formula φ and a ∈ I(P ) we define the satisfaction relation a |= PIL φ by induction on the structure of φ as follows: Note that PIL differs from propositional logic, since it is interpreted over interactions, and thus the name "interaction" is assigned to it. Two PIL formulas φ, φ are called equivalent, denoted by φ ≡ φ , when a |= φ iff a |= φ for every a ∈ I(P ). For every a = {p 1 , . . . , p l } ∈ I(P ) we consider the PIL formula φ a = p 1 ∧ . . . ∧ p l . Then, a |= PIL φ a , and for every a, a ∈ I(P ) we get a = a iff φ a ≡ φ a . We can describe a set of interactions as a PIL formula. } and set P B = i∈[n] P (i). An interaction of B is an interaction a ∈ I(P B ) such that |a ∩ P (i)| ≤ 1, for every i ∈ [n]. We denote by I B the set of all interactions of B, i.e., , and γ is a set of interactions in I B . The set γ of interactions of (B, γ) specifies the architecture of the system. Obviously, we can replace γ by its corresponding PIL formula φ γ , i.e., in a logical directed notation. Expression of software architectures by logics has been used in several works and gave nice results (cf. [10, 11, 28] ). PIL describes nicely several architectures but its semantics does not capture the execution order of the interactions imposed by each architecture. Ordered interactions occur in common architectures, including Request/Response and Publish/Subscribe. In this section, we introduce a propositional logic that extends PIL with two operators, the concatenation * and the shuffle operator , and we model architectures of component-based systems with order restrictions. Let P be a finite set of ports. The syntax of extended propositional interaction logic ( EPIL for short) formulas ϕ over P is given by the grammar The binding strength, in decreasing order, of the EPIL operators is: negation, shuffle, concatenation, conjunction, and disjunction. Negation is applied only in PIL formulas and EPIL formulas of type ζ. The latter ensures exclusion of erroneous interactions in architectures. The restricted use of negation allows a reasonable complexity of translation of FOEIL formulas to finite automata. This in turn implies the decidability of equivalence, satisfiability, and validity of FOEIL sentences (cf. Sect. 6). Our assumption has no impact in expressiveness of EPIL formulas, since they can efficiently model most known architectures. EPIL formulas are interpreted over finite words w ∈ I(P ) * . Intuitively, a word w encodes each of the distinct interactions within a system as a letter. Moreover, the position of each letter in w depicts the order in which the corresponding interaction is executed in the system, in case there is an order restriction. Let ϕ be an EPIL formula over P and w ∈ I(P ) * . If w = ε and ϕ = true, then we set w |= true. If w ∈ I(P ) + , then we define the satisfaction relation w |= ϕ by induction on the structure of ϕ as follows: If ϕ = φ is a PIL formula, then w |= φ implies that w is a letter in I(P ). Two EPIL formulas ϕ, ϕ are called equivalent, denoted by ϕ ≡ ϕ , when w |= ϕ iff w |= ϕ for every w ∈ I(P ) * . Now, we define an updated version of componentbased systems by replacing the PIL formula by an EPIL formula. Specifically, a component-based system is a pair (B, ϕ) } is a set of components and ϕ is an EPIL formula over P B . The investigation of semantics and verification of component-based systems is a part of future work. Next we present three examples of component-based models (B, ϕ) whose architectures have ordered interactions encoded by EPIL formulas satisfied by words over I B . Clearly, there exist several variations of the following architectures and their order restrictions, that EPIL formulas could also model sufficiently by applying relevant modifications. We need to define the following macro EPIL formula. Let P = {p 1 , . . . , p n } be a set of ports. Then, for p i1 , . . . , p im ∈ P with m < n we let Example 1 (Blackboard). We consider a component-based system (B, ϕ) with the Blackboard architecture. The latter is applied in planning and scheduling [35] as well as in artificial intelligence [6] . Blackboard architecture involves a blackboard, a controller and the (knowledge) sources components [14, 29] . Blackboard presents the state of the problem to be solved and sources provide partial solutions without knowing about the existence of other sources. When there is enough information for a source to provide its partial solution, the source is triggered, i.e., is keen to write on the blackboard. Since multiple sources may be triggered, a controller component is used to resolve any conflicts. We consider three knowledge sources components. Hence, (1), . . . , B(5) refer to blackboard, controller and the sources components, respectively ( Fig. 1 ). Blackboard has two ports p d , p a to declare the state of the problem and add the new data as obtained by a source, respectively. Sources have three ports p n k , p t k , p w k , for k = 1, 2, 3, for being notified about the existing data on the blackboard, the trigger of the source, and for writing on the blackboard, respectively. Controller has three ports, p r used to record blackboard data, p l for logging the triggered sources, and p e for their execution to blackboard. Here we assume that all sources are triggered, i.e., that they participate in the architecture. The EPIL formula ϕ for Blackboard architecture is The first PIL subformula encodes the connection among blackboard and controller. The EPIL subformula between the two * operators represents the connections of knowledge sources to blackboard. The last part of ϕ captures the connection of some of knowledge sources with controller and blackboard. The use of * operator in ϕ ensures that the controller is informed before the sources, and that sources are triggered before writing on blackboard. The shuffle operator in ϕ captures any possible order, among the sources, for connecting with controller and blackboard. Before our second example we show the expressive difference among EPIL and PCL formulas of [28] . Remark 1. Consider the Blackboard architecture presented in the previous example. Then the corresponding PCL formula ρ (cf. [28] ) describing that architecture is where + denotes the coalescing operator, denotes the union operator, and φ i = #(p l ∧ p ti ) + #(p e ∧ p wi ∧ p a ) for i = 1, 2, 3. Then, the PCL formula ρ is interpreted over sets of interactions in P(I(P ))\ {∅} which trivially cannot express the required order of the execution of the interactions. For instance the set of interactions , p a } satisfies ρ but represents no order of the interactions' execution. Example 2 (Request/Response). Request/Response architectures refer to services and clients, and are classical interaction patterns widely used for web services [15] . Services become available to clients by enrolling in the so-called service registry. Then clients scan the registry and choose a service. Each client that is interested in a service sends a request and waits until the service's respond. Meanwhile no other client is connected to the service. To achieve this, in [28] a third component called coordinator was added for each service. For our example we consider seven components, namely the service registry, two services with their coordinators, and two clients. (Fig. 2) . Service registry has the ports p e , p u , and p t , for the services' enrollment and for allowing a client to search and take the service's address, respectively. Services have the ports p r k , p g k , p s k , for k = 1, 2, for enrolling to service registry, and connecting to a client (via coordinator) for receiving a request and responding, respectively. Clients have the ports p l k , p o k for connecting with service registry to look up and obtain a service's address, while the ports p n k , p q k and p c k express the connection of the client to coordinator, to service (via coordinator) for sending the request and for collecting its response, respectively, for k = 1, 2. Coordinators have three ports, p m k for controlling that only one client is connected to a service, p a k for acknowledging that the connected client sends a request, and p d k that disconnects the client when the service responds to the request, for k = 1, 2. The EPIL formula ϕ for the Request/Response architecture equals to The subformulas at the left of the first two concatenation operators encode the connections of the two services and the two clients with registry. Then, each of the three subformulas connected with the big disjunctions expresses that either one of the two clients or both of them (one at each time) are connected with the first service only, the second service only, or both of the services, respectively. IoT applications (cf. [30, 31] ), and recently in cloud systems [37] and robotics [27] . It involves publishers, subscribers, and topics components. Publishers advertise and transmit to topics the type of messages they produce. Then, subscribers are connected with topics they are interested in, and topics in turn transfer the messages from publishers to corresponding subscribers. Once a subscriber receives the requested message, it is disconnected from the relevant topic. Publishers cannot check the existence of subscribers and vice-versa [18] . We consider two publisher, two topic and three subscriber components (Fig. 3) . Publishers have two ports, p a k and p t k , for k = 1, 2, for advertising and transferring their messages to topics, respectively. Topics are notified from the publishers and receive their messages through ports p n k and p r k , for k = 1, 2, respectively. Ports p c k , p s k and p f k , for k = 1, 2, are used from topics for the connection, the sending of a message, and disconnection with a subscriber, respectively. Subscribers use the ports p em , p gm , p dm , for m = 1, 2, 3, for connecting with the topic (express interest), getting a message from the topic, and disconnecting from the topic, respectively. The EPIL formula for the Publish/Subscribe for i ∈ {1, 2} (topics) and ξ 1 = ξ 11 ∨ ξ 12 ∨ (ξ 11 ξ 12 ), ξ 2 = ξ 21 ∨ ξ 22 ∨ (ξ 21 ξ 22 ) encode that each of the two topics connects with the first publisher, or the second one, or with both of them, where ξ ij = #(p ni ∧ p aj ) * #(p ri ∧ p tj ) for i, j ∈ {1, 2}, and ϕ ij = #(p ci ∧ p ej ) * #(p si ∧ p gj ) * #(p fi ∧ p dj ) for i ∈ {1, 2} and j ∈ {1, 2, 3}, describes the connections of the two topics with each of the three subscribers. The presented examples demonstrate that EPIL formulas can encode the order restrictions within architectures and also specify all the different instantiations for the connections among the coordinated components in the system. In this section we deal with the parametric extension of component-based systems defined by a finite number of distinct component types whose number of instances is a parameter for the system. In real world applications we do not need an unbounded number of components. Though, the number of instances of every component type is unknown or it can be modified during a process. Next we consider parametric component-based systems, i.e., component-based systems with infinitely many instances of every component type. } be a set of component types. For every i ∈ [n] and j ≥ 1 we consider a copy B(i, j) = (Q(i, j), P (i, j), q 0 (i, j), R(i, j)) of B(i), namely the j-th instance of B(i). Hence, for every i ∈ [n] and j ≥ 1, the instance B(i, j) is also a component and we call it a parametric component or a component instance. We assume that (Q(i, j) ∪ P (i, j)) ∩ (Q(i , j ) ∪ P (i , j )) = ∅ whenever i = i or j = j for every i, i ∈ [n] and j, j ≥ 1. This restriction permits us to use, without any confusion, the notation P (i, j) = {p(j) | p ∈ P (i)} for every i ∈ [n] and j ≥ 1. We set pB = {B(i, j) | i ∈ [n], j ≥ 1} and call it a set of parametric components, with P pB = i∈[n],j≥1 P (i, j). Since parametric systems consist of an unknown number of component instances, we need a symbolic representation to describe their architectures. For this, we introduce the first-order extended interaction logic whose semantics describes the order of interactions implemented in a parametric architecture. Our logic is proved sufficient to model several complex architectures. This is important because parametric systems based on well-defined architectures satisfy most of their requirements [4, 9] . We introduce the first-order extended interaction logic as a modelling language for describing the interactions of parametric component-based systems. For this, we equip EPIL formulas with variables. Due to the nature of parametric systems we need to distinguish variables referring to different component types. , j ≥ 1} and X (1) , . . . , X (n) be pairwise disjoint countable sets of first-order variables referring to instances of component types B(1), . . . , B(n) , respectively. Variables in X (i) , for every i ∈ [n], are denoted by small letters with the corresponding superscript, i.e., x (i) ∈ X (i) , i ∈ [n], is a first-order variable referring to an instance of component type B(i). Let X = X (1) ∪ . . . ∪ X (n) and set P pB(X ) = p x (i) | i ∈ [n], x (i) ∈ X (i) , and p ∈ P (i) . , j ≥ 1} be a set of parametric components. Then the syntax of first-order extended interaction logic (FOEIL for short) formulas ψ over pB 1 is given by the grammar where ϕ is an EPIL formula over P pB(X ) , i ∈ [n], x (i) , y (i) are first-order variables in X (i) , ∃ * denotes the existential concatenation quantifier, ∀ * the universal concatenation quantifier, ∃ is the existential shuffle quantifier, and ∀ the universal shuffle quantifier. Furthermore, we assume that whenever ψ contains a subformula of the form ∃ * x (i) .ψ or ∃ x (i) .ψ , then the application of negation in ψ is permitted only in PIL formulas and formulas of the form x (j) = y (j) . Let ψ be a FOEIL formula over pB. We denote by free(ψ) the set of free variables of ψ. If ψ has no free variables, then it is a sentence. We consider a mapping r : [n] → N. The value r(i), for every i ∈ [n], represents the finite number of instances of the component type B(i) in the parametric system. We let pB(r) = {B(i, j) | i ∈ [n], j ∈ [r(i)]} and call it the instantiation of pB w.r.t. r. Also P pB(r) = i∈[n],j∈[r(i)] P (i, j) and I pB(r) = {a ∈ I(P pB(r) ) | |a ∩ P (i, j)| ≤ 1 for every i ∈ [n] and j ∈ [r(i)]}. Let V ⊆ X be a finite set of first-order variables and set P pB(V) = {p(x (i) ) ∈ P pB(X ) | x (i) ∈ V}. A (V, r)-assignment is a mapping σ : V → N such that σ(V ∩ X (i) ) ⊆ [r(i)] for every i ∈ [n], and σ[x (i) → j] is the (V ∪ {x (i) }, r)assignment which acts as σ on V \ {x (i) } and assigns j to x (i) . If ϕ is an EPIL formula over P pB(V) , then σ(ϕ) is an EPIL formula over P pB(r) which is obtained by ϕ by replacing every port p(x (i) ) in ϕ by p(σ(x (i) )). We interpret FOEIL formulas ψ over triples consisting of a mapping r : [n] → N, a (V, r)-assignment σ, and a word w ∈ I * pB(r) . The semantics of formulas of the form ∃ * x (i) .ψ and ∀ * x (i) .ψ (resp. ∃ x (i) .ψ and ∀ x (i) .ψ) refer to satisfaction of ψ by subwords of w. The subwords correspond to component instances which are determined by the application of the assignment σ to x (i) , and w results by the * (resp. ) operator among the subwords. Let ψ be a FOEIL formula over a set pB = {B(i, j) | i ∈ [n], j ≥ 1} of parametric components and V ⊆ X a finite set containing free(ψ). Then for every r : [n] → N, (V, r)-assignment σ, and w ∈ I * pB(r) we define the satisfaction relation (r, σ, w) |= ψ, inductively on the structure of ψ as follows: By definition of parametric systems, all instances of each component type are identical, hence the order specified above in the semantics of ∃ * , ∀ * , ∃ , ∀ quantifiers causes no restriction in the derived architecture. If ψ is a FOEIL sentence over pB, then we write (r, w) |= ψ. Let also ψ be a FOEIL sentence over pB. Then, ψ and ψ are called equivalent w.r.t. r when (r, w) |= ψ iff (r, w) |= ψ , for every w ∈ I * pB(r) . In the sequel, we shall write also x (i) = y (i) for ¬(x (i) = y (i) ). Let β be a boolean combination of atomic formulas of the form x (i) = y (i) and ψ a FOEIL formula over pB. Then, we define β → ψ ::= ¬β ∨ ψ. For simplicity we denote boolean combinations of formulas of the form x (i) = y (i) as constraints. For instance we write ∃x (i) Note that in [28] the authors considered a universe of component types and hence, excluded in their logic formulas the erroneous types for each architecture. Such a restriction is not needed in our setting since we consider a well-defined set [n] of component types for each architecture. A parametric component-based system is a pair (pB, ψ) where pB = {B(i, j) | i ∈ [n], j ≥ 1} is a set of parametric components and ψ is a FOEIL sentence over pB. In the sequel, we refer to parametric component-based systems simply as parametric systems. We remind that in this paper we focus on the architectures of parametric systems. The study of parametric systems' behavior is left for investigation in subsequent work as a part of parametric verification. For our examples in the next subsection, we shall need the following macro FOEIL formula. Let pB = {B(i, j) | i ∈ [n], j ≥ 1} and 1 ≤ i 1 , . . . , i m ≤ n be pairwise different indices. Then We present examples of FOEIL sentences describing parametric architectures, where the order of interactions is a main feature. We should note that FOEIL describes effectively as well, architectures with no order restrictions. Due to space limitations, we refer the reader to [32] for such examples. Example 4 (Blackboard). The subsequent FOEIL sentence ψ encodes the interactions of Blackboard architecture, described in Example 1, in the parametric setting. We let X (1) , X (2) , X (3) to be set of variables for blackboard, controller, and knowledge sources component instances, respectively. ψ = ∃x (1) ∃x (2) . . We present a FOEIL sentence ψ for Request/Response architecture, described in Example 2, in the parametric setting. Let X (1) , X (2) , X (3) , and X (4) refer to instances of service registry, service, client, and coordinator component, respectively. Then, ψ = ∃x (1) . (∀ x (2) .#(p e (x (1) ) ∧ p r (x (2) ))) * (1) )))) * ∃ y (2) ∃x (4) ∃ * y (3) .ξ ∧ ∀y (4) ∀z (3) ∀z (2) . θ ∨ ∀t (3) ∀t (2) (z (2) = t (2) ).θ where the EPIL formulas ξ, θ, and θ are given respectively, by: ξ = #(p n (y (3) ) ∧ p m (x (4) )) * #(p q (y (3) ) ∧ p a (x (4) ) ∧ p g (y (2) )) * #(p c (y (3) ) ∧ p d (x (4) ) ∧ p s (y (2) )), θ = ¬(true * #(p q (z (3) ) ∧ p a (y (4) ) ∧ p g (z (2) )) * true), and θ = (true * #(p q (z (3) ) ∧ p a (y (4) ) ∧ p g (z (2) )) * true) ∧ ¬(true * #(p q (t (3) ) ∧ p a (y (4) ) ∧ p g (t (2) )) * true). The subformula ∀y (4) ∀z (3) ∀z (2) . θ ∨ ∀t (3) ∀t (2) (z (2) = t (2) ).θ in ψ serves as a constraint to ensure that a unique coordinator is assigned to each service. Example 6 (Publish/Subscribe). We consider Publish/Subscribe architecture, described in Example 3, in the parametric setting. In the subsequent FOEIL sentence ψ, we let variable sets X (1) , X (2) , X (3) correspond to publisher, topic, and subscriber component instances, respectively. ψ = ∃ x (2) . ∃ x (1) . #(pa(x (1) ) ∧ pn(x (2) )) * #(pt(x (1) ) ∧ pr(x (2) )) * ∃ x (3) . #(pe(x (3) ) ∧ pc(x (2) )) * #(pg(x (3) ) ∧ ps(x (2) )) * #(p d (x (3) ) ∧ p f (x (2) )) . In [28] a simpler version of Request/Response and Blackboard architectures is described where the resulting sets of interactions do not depict any order. Publish/Subscribe architecture has not been studied in [10, 26, 28] . Observe that in the presented examples, whenever is defined a unique instance for a component type we may also consider the corresponding set of variables as a singleton. In this section, we prove that the equivalence and validity problems for FOEIL sentences are decidable in doubly exponential time, whereas the satisfiability problem is decidable in exponential time. For this, we establish an effective translation of every FOEIL formula to an expressive equivalent finite automaton, and hence we take advantage of well-known computational results for finite automata. We refer the reader to [32] for detailed proofs of our results. Theorem 1. Let ψ be a FOEIL sentence over a set pB = {B(i, j) | i ∈ [n], j ≥ 1} of parametric components and r : [n] → N. Then, we can effectively construct a finite automaton A ψ,r over I pB (r) such that (r, w) |= ψ iff w ∈ L(A ψ,r ) for every w ∈ I * pB(r) . The worst case run time for the translation algorithm is exponential and the best case is polynomial. We prove Theorem 1 using the subsequent proposition. Let V ⊆ X be a finite set of variables. For every i ∈ [n] and x (i) ∈ V, we define the set P (i)(x (i) ) = {p(x (i) ) | p ∈ P (i) and x (i) ∈ V} and let I pB(V) = {a ∈ I(P pB(V) ) | |a ∩ P (i)(x (i) )| ≤ 1 for every i ∈ [n] and x (i) ∈ V}. Next let σ be a (V, r)assignment and L a language over I pB (V) . We denote by σ(L) the language over I(P pB(r) ) 2 which is obtained by L by replacing every variable x ∈ V by σ(x). , j ≥ 1} of parametric components. Let also V ⊆ X be a finite set of variables containing free(ψ) and r : [n] → N. Then, we can effectively construct a finite automaton A ψ,r over I pB (V) such that for every (V, r)-assignment σ and w ∈ I * pB(r) we have (r, σ, w) |= ψ iff w ∈ σ(L(A ψ,r )) ∩ I * pB(r) . The worst case run time for the translation algorithm is exponential and the best case is polynomial. Proof. We prove our claim by induction on the structure of the FOEIL formula ψ. The input of the translation algorithm is the FOEIL formula ψ and the complexity measure refers to the set of states of the derived finite automaton A ψ,r . Proof (of Theorem 1). We apply Proposition 1. Since ψ is a sentence it contains no free variables. Hence, we get a finite automaton A ψ,r over I pB(r) such that (r, w) |= ψ iff w ∈ L(A ψ,r ) for every w ∈ I * pB(r) , and this concludes our proof. Next, we deal with the decidability of satisfiability and validity results for FOEIL sentences. For this, we recall firstly these notions. A FOEIL sentence ψ over pB is called satisfiable w.r.t. r whenever there exists a w ∈ I * pB(r) such that (r, w) |= ψ, and valid w.r.t. r whenever (r, w) |= ψ for every w ∈ I * pB(r) . , j ≥ 1} be a set of parametric components and r : [n] → N a mapping. Then, the satisfiability problem for FOEIL sentences over pB w.r.t. r is decidable in exponential time. 2 σ(L) is not always over I pB (r) . For instance, assume that a ∈ L with a ∈ I pB(V) , p(x (i) ), p (y (i) ) ∈ a for some i ∈ [n], p, p ∈ P (i), and σ(x (i) ) = σ(y (i) ). Then σ(a) / ∈ I pB(r) . Proof. Let ψ be a FOEIL sentence over pB. By Theorem 1 we construct, in exponential time, a finite automaton A ψ,r such that (r, w) |= ψ iff w ∈ L(A ψ,r ) for every w ∈ I * pB(r) . Then, ψ is satisfiable iff L(A ψ,r ) = ∅ which is decidable in linear time [33] , and thus satisfiability of FOEIL sentences over pB is decidable in exponential time. Proof. Let ψ be a FOEIL sentence over pB. By Theorem 1 we construct, in exponential time, a finite automaton A ψ,r such that (r, w) |= ψ iff w ∈ L(A ψ,r ) for every w ∈ I * pB(r) . Then, ψ is valid iff L(A ψ,r ) = I * pB(r) which is decidable in exponential time [33] . Hence, we can decide whether ψ is valid or not in doubly exponential time. In this paper we deal with the formal study of architectures for parametric component-based systems. We introduce a propositional logic, EPIL, which augments PIL from [28] with a concatenation and a shuffle operator, and interpret EPIL formulas over finite words of interactions. We also study FOEIL, the firstorder level of EPIL, as a modelling language for the architectures of parametric systems. EPIL and FOEIL encode the permissible interactions and the order restrictions of complex architectures. Several examples are presented and we show the decidability of equivalence, satisfiability and validity of FOEIL sentences. Ongoing work involves the verification of parametric systems against formal properties, and specifically the application of architectures modelled by FOEIL, for studying the behavior and proving properties (such as deadlock-freedom) of parametric systems. Several architectures, like Ring and Linear [28] cannot be formalized by FOEIL sentences. For this, the study of second-order level of EPIL is needed which is left as future work. Another direction is the extension of our framework for modelling architectures with data applied on parametric systems. Also, it would be interesting to investigate in our setting the architecture composition problem (cf. [5] ). Finally, in a forthcoming paper we study parametric component-based systems and FOEIL in the weighted setup. Parameterized verification Specification of Software Systems. Texts in Computer Science REO based interaction model Parameterized model checking of rendezvous systems A general framework for architecture composability Handbook of Artificial Intelligence Verification of concurrent design patterns with data The algebra of connectors -structuring interaction in BIP Decidability in parameterized verification Checking deadlock-freedom of parametric component-based systems Structural invariants for parametric verification of systems with almost linear architectures Service oriented architectural design Parameterized, concurrent session types for asynchronous multi-actor interactions Blackboard systems Service Design Patterns: Fundamental Design Solutions for SOAP/WSDL and RESTful web services Multiparty session types meet communicating automata Parameterised multiparty session types The many faces of Publish/Subscribe Monitorability for the Hennessy-Milner logic with recursion Revising glue expressiveness in component-based systems Realisability of pomsets Component-based design and verification in X-MAN Algebraic laws for nondeterminism and concurrency Multiparty asynchronous session types Foundations of session types and behavioural contracts Parameterized systems in BIP: design and model checking How do you architect your robots? State of the practice and guidelines for ROS-based systems Configuration logics: modelling architecture styles Blackboard Systems, chap A publish-subscribe approach to IoT integration: the smart office use case Publish/Subscribe mechanism for IoT: a survey of event matching algorithms and open research challenges Architecture modelling of parametric component-based systems Elements of Automata Theory A complete survey on software architectural styles and patterns The use of the blackboard architecture for a decision making system for the control of craft with various actuator and movement capabilities Semantics of global view of choreographies Privacy-preserving attributekeyword based data publish-subscribe service on cloud platforms Total order in content-based Publish/Subscribe systems We are deeply grateful to Simon Bliudze for discussions on a previous version of the paper.