Maria Pittou
email: mpittou@math.auth.gr

George Rahonis
email: 2grahonis@math.auth.gr

Architecture Modelling of Parametric Component-Based Systems

Keywords: Architecture modelling, Parametric component-based systems, First-order extended interaction logic

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

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 [START_REF] Bliudze | The algebra of connectors -structuring interaction in BIP[END_REF]. Componentbased design lies in constructing multiple components which coordinate in order to generate the global model for a system [START_REF] Bliudze | The algebra of connectors -structuring interaction in BIP[END_REF][START_REF] Giusto | Revising glue expressiveness in component-based systems[END_REF]. 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 [START_REF] Mavridou | Configuration logics: Modelling architecture styles[END_REF][START_REF] Sharmaa | A complete survey on software architectural styles and patterns[END_REF]. 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 [START_REF] Bliudze | Verification of concurrent design patterns with data[END_REF][START_REF] Bozga | Checking deadlock-freedom of parametric component-based systems[END_REF][START_REF] Mavridou | Configuration logics: Modelling architecture styles[END_REF].

In this paper we provide a formal framework for the architecture modelling of parametric component-based systems using a first-order logic. Parametric sys- tems represent a wide class of component-based systems including communication protocols and concurrent and distributed algorithms [START_REF] Abdulla | Parameterized verification[END_REF]9,[START_REF] Deniélou | Parameterised multiparty session types[END_REF]. Parametric systems are constructed by a finite number of component types each consisting of an unknown number of instances [START_REF] Aminof | Parameterized model checking of rendezvous systems[END_REF]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 [START_REF]Service Design Patterns: Fundamental Design Solutions for SOAP/WSDL and RESTful web services[END_REF][START_REF] Zhang | Total order in contentbased Publish/Subscribe systems[END_REF]. 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. [START_REF] Alagar | The B-Method[END_REF][START_REF] Amaro | REO based interaction model[END_REF][START_REF] Bliudze | The algebra of connectors -structuring interaction in BIP[END_REF][START_REF] He | Component-based design and verification in X-MAN[END_REF]) 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 [START_REF] Mavridou | Configuration logics: Modelling architecture styles[END_REF] 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 [START_REF] Corkill | Blackboard systems[END_REF], Request/Response [START_REF]Service Design Patterns: Fundamental Design Solutions for SOAP/WSDL and RESTful web services[END_REF], and Publish/Subscribe [START_REF] Eugster | The many faces of Publish/Subscribe[END_REF] 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.

(3) We show the expressiveness of FOEIL by examples for architectures of parametric component-based systems. Specifically, we consider the architectures Blackboard, Request/Response, and Publish/Subscribe, that impose orders on the implementation of their interactions.

Related work

In [START_REF] Mavridou | Configuration logics: Modelling architecture styles[END_REF] 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 [START_REF] Konnov | Parameterized systems in BIP: design and model checking[END_REF] 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. [START_REF] Bliudze | The algebra of connectors -structuring interaction in BIP[END_REF]). FOIL applied for modelling classical architectures (Star, Ring etc.) and contributed to model checking of parametric systems. Monadic Interaction Logic (MIL) was introduced in [START_REF] Bozga | Checking deadlock-freedom of parametric component-based systems[END_REF] 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 [START_REF] Bozga | Structural invariants for parametric verification of systems with almost linear architectures[END_REF], 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. [START_REF] Bliudze | The algebra of connectors -structuring interaction in BIP[END_REF]). 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 [START_REF] Attie | A general framework for architecture composability[END_REF] 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 [START_REF] Bliudze | Verification of concurrent design patterns with data[END_REF] 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. [START_REF] Hennessy | Algebraic laws for nondeterminism and concurrency[END_REF]) a logic, called HML, as a calculus for the specification of concurrent programs and their properties. In [START_REF] Francalanza | Monitorability for Hennessy-Milner logic with recursion[END_REF] 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 pro-cesses but it is far from describing complex architectures. Specifically our shuffle operator cannot be described in µHML.

In [START_REF] Giusto | Revising glue expressiveness in component-based systems[END_REF] 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 [START_REF] Guanciale | Realisability of pomsets[END_REF] (cf. also [START_REF] Tuosto | Semantics of global view of choreographies[END_REF]) 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 [START_REF] Honda | Multiparty asynchronous session types[END_REF][START_REF] Hüttel | Foundations of session types and behavioural contracts[END_REF]). The relation among multiparty session types and communicating automata was studied in [START_REF] Deniélou | Multiparty session types meet communicating automata[END_REF]. Parameterized multiparty session types were investigated in [START_REF] Charalambides | Parameterized, concurrent session types for asynchronous multi-actor interactions[END_REF][START_REF] Deniélou | Parameterised multiparty session types[END_REF]. Nevertheless, the work of [START_REF] Deniélou | Parameterised multiparty session types[END_REF] did not study the implementation order of the parameterized interactions and the models of [START_REF] Charalambides | Parameterized, concurrent session types for asynchronous multi-actor interactions[END_REF][START_REF] Deniélou | Multiparty session types meet communicating automata[END_REF][START_REF] Honda | Multiparty asynchronous session types[END_REF][START_REF] Hüttel | Foundations of session types and behavioural contracts[END_REF] 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 [START_REF] Bruni | Service oriented architectural design[END_REF]. Though, no order of interactions' execution was considered.

Preliminaries

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 w ¡ u = {w 1 u 1 . . . w m u m | w 1 , . . . , u m ∈ A * and w = w 1 . . . w m , u = u 1 . . . u m }.

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 [START_REF] Bliudze | The algebra of connectors -structuring interaction in BIP[END_REF], REO [START_REF] Amaro | REO based interaction model[END_REF], X-MAN [START_REF] He | Component-based design and verification in X-MAN[END_REF], and B [START_REF] Alagar | The B-Method[END_REF].

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) [START_REF] Bozga | Checking deadlock-freedom of parametric component-based systems[END_REF][START_REF] Bozga | Structural invariants for parametric verification of systems with almost linear architectures[END_REF][START_REF] Mavridou | Configuration logics: Modelling architecture styles[END_REF]. 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 φ ::= true | p | ¬φ | φ ∨ φ where p ∈ P . We set false = ¬true and ¬(¬φ) = φ, φ ∧ φ := ¬(¬φ ∨ ¬φ ), φ → φ := ¬φ ∨ φ for PIL formulas φ, φ over P . 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:

a |= PIL true, a |= PIL ¬φ iff a |= PIL φ, a |= PIL p iff p ∈ a, a |= PIL φ 1 ∨ φ 2 iff a |= PIL φ 1 or a |= PIL φ 2 .
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.

Specifically for γ = {a 1 , . . . , a m }, the PIL formula φ γ of γ is φ γ = φ a1 ∨. . .∨φ am . Let B = {B(i) | i ∈ [n]} 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.,

I B = {a ∈ I(P B ) | |a ∩ P (i)| ≤ 1 for every i ∈ [n]} . Definition 1. A component-based system is a pair (B, γ) where B = {B(i) | i ∈ [n]} is a set of components, with B(i) = (Q(i), P (i), q 0 (i), R(i)) for every i ∈ [n], 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. [START_REF] Bozga | Checking deadlock-freedom of parametric component-based systems[END_REF][START_REF] Bozga | Structural invariants for parametric verification of systems with almost linear architectures[END_REF][START_REF] Mavridou | Configuration logics: Modelling architecture styles[END_REF]).

Extended propositional interaction logic

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. Definition 2. 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

ζ ::= φ | ζ * ζ ϕ ::= ζ | ¬ζ | ϕ ∨ ϕ | ϕ ∧ ϕ | ϕ * ϕ | ϕ ¡ ϕ
where φ is a PIL formula over P .

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. Section 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. - 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 #(p i1 ∧ . . . ∧ p im ) ::= p i1 ∧ . . . ∧ p im ∧ p∈P \{pi 1 ,...,pi m } ¬p.

w |= φ iff w |= PIL φ, -w |= ζ 1 * ζ 2 iff there exist w 1 , w 2 ∈ I(P ) * such that w = w 1 w 2 and w i |= ζ i for i = 1, 2, -w |= ¬ζ iff w |= ζ, -w |= ϕ 1 ∨ ϕ 2 iff w |= ϕ 1 or w |= ϕ 2 , -w |= ϕ 1 ∧ ϕ 2 iff w |= ϕ 1 and w |= ϕ 2 , -w |= ϕ 1 * ϕ 2 iff
Example 1. (Blackboard) We consider a component-based system (B, ϕ) with the Blackboard architecture. The latter is applied in planning and scheduling [START_REF] Straub | The use of the blackboard architecture for a decision making system for the control of craft with various actuator and movement capabilities[END_REF] as well as in artificial intelligence [START_REF]Handbook of Artificial Intelligence[END_REF]. Blackboard architecture involves a blackboard, a controller and the (knowledge) sources components [START_REF] Corkill | Blackboard systems[END_REF]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, B = {B(i) | i ∈ [5]} where B(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

ϕ = #(p d ∧ p r ) * #(p d ∧ p n1 ) ¡ #(p d ∧ p n2 ) ¡ #(p d ∧ p n3 ) * ϕ 1 ∨ ϕ 2 ∨ ϕ 3 ∨ (ϕ 1 ¡ ϕ 2 ) ∨ (ϕ 1 ¡ ϕ 3 ) ∨ (ϕ 2 ¡ ϕ 3 ) ∨ (ϕ 1 ¡ ϕ 2 ¡ ϕ 3 )
where ϕ i = #(p l ∧ p ti ) * #(p e ∧ p wi ∧ p a ) for i = 1, 2, 3. 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 [START_REF] Mavridou | Configuration logics: Modelling architecture styles[END_REF].

Remark 1. Consider the Blackboard architecture presented in the previous example. Then the corresponding PCL formula ρ (cf. [START_REF] Mavridou | Configuration logics: Modelling architecture styles[END_REF]) describing that architecture is

ρ = #(p d ∧ p r ) + #(p d ∧ p n1 ) + #(p d ∧ p n2 ) + #(p d ∧ p n3 )+ φ 1 φ 2 φ 3 (φ 1 + φ 2 ) (φ 1 + φ 3 ) (φ 2 + φ 3 ) (φ 1 + φ 2 + φ 3 )
where + denotes the coalescing operator, denotes the union operator, and Example 2. (Request/Response) Request/Response architectures refer to services and clients, and are classical interaction patterns widely used for web services [START_REF]Service Design Patterns: Fundamental Design Solutions for SOAP/WSDL and RESTful web services[END_REF]. 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 [START_REF] Mavridou | Configuration logics: Modelling architecture styles[END_REF] a third component called coordinator was added for each service.

p d p a Blackb. B (1
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 #(p e ∧p r1 )¡#(p e ∧p r2 ) * ξ 1 ¡ξ 2 * ϕ 11 ∨ϕ 21 ∨(ϕ 11 * ϕ 21 )∨(ϕ 21 * ϕ 11 )

ϕ 12 ∨ ϕ 22 ∨ (ϕ 12 * ϕ 22 ) ∨ (ϕ 22 * ϕ 12 ) ϕ 11 ∨ ϕ 21 ∨ (ϕ 11 * ϕ 21 ) ∨ (ϕ 21 * ϕ 11 ) ¡ ϕ 12 ∨ ϕ 22 ∨ (ϕ 12 * ϕ 22 ) ∨ (ϕ 22 * ϕ 12 )
where ξ i = #(p li ∧ p u ) * #(p oi ∧ p t ) for i = 1, 2, and ϕ ij = #(p ni ∧ p mj ) * #(p qi ∧ p aj ∧ p gj ) * #(p ci ∧ p dj ∧ p sj ) for i = 1, 2 (clients) and j = 1, 2 (services). 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. Example 3. (Publish/Subscribe) Publish/Subscribe architecture is used in IoT applications (cf. [START_REF] Olivieri | A Publish-Subscribe approach to IoT integration: the smart office use case[END_REF][START_REF] Patel | Publish/Subscribe mechanism for IoT: A survey of event matching algorithms and open research challenges[END_REF]), and recently in cloud systems [START_REF] Yang | Privacy-preserving attributekeyword based data publish-subscribe service on cloud platforms[END_REF] and robotics [START_REF] Malavolta | How do you architect your robots? State of the practice and guidelines for ROS-based systems[END_REF]. 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 [START_REF] Eugster | The many faces of Publish/Subscribe[END_REF]. 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 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.

architecture is ϕ = ϕ 1 ∨ ϕ 2 ∨ (ϕ 1 ¡ ϕ 2 ) with ϕ i = ξ i * ϕ i1 ∨ ξ i * ϕ i2 ∨ ξ i * ϕ i3 ∨ ξ i * (ϕ i1 ¡ϕ i2 ) ∨ ξ i * (ϕ i1 ¡ϕ i3 ) ∨ ξ i * (ϕ i2 ¡ ϕ i3 ) ∨ ξ i * (ϕ i1 ¡ ϕ i2 ¡ ϕ i3 ) for i ∈ {1, 2} (
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.

Parametric component-based systems

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.

Let B = {B(i) | i ∈ [n]
} 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).

p
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 [START_REF] Aminof | Parameterized model checking of rendezvous systems[END_REF]9].

First-order extended interaction logic

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. Let pB = {B(i, j) | i ∈ [n], 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) . Definition 4. Let pB = {B(i, j) | i ∈ [n], 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

ψ ::= ϕ | x (i) = y (i) | ¬(x (i) = y (i) ) | ψ ∨ ψ | ψ ∧ ψ | ψ * ψ | ψ ¡ ψ | ∃x (i) .ψ | ∀x (i) .ψ | ∃ * x (i) .ψ | ∀ * x (i) .ψ | ∃ ¡ x (i) .ψ | ∀ ¡ x (i) .ψ
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.

Definition 5. 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:

-(r, σ, w) |= ϕ iff w |= σ(ϕ), -(r, σ, w) |= x (i) = y (i) iff σ(x (i) ) = σ(y (i) ), -(r, σ, w) |= ¬(x (i) = y (i) ) iff (r, σ, w) |= x (i) = y (i) , -(r, σ, w) |= ψ 1 ∨ ψ 2 iff (r, σ, w) |= ψ 1 or (r, σ, w) |= ψ 2 , -(r, σ, w) |= ψ 1 ∧ ψ 2 iff (r, σ, w) |= ψ 1 and (r, σ, w) |= ψ 2 , -(r, σ, w) |= ψ 1 * ψ 2 iff there exist w 1 , w 2 ∈ I * pB(r) such that w = w 1 w 2 and (r, σ, w i ) |= ψ i for i = 1, 2, -(r, σ, w) |= ψ 1 ¡ψ 2 iff there exist w 1 , w 2 ∈ I * pB(r) such that w ∈ w 1 ¡w 2 and (r, σ, w i ) |= ψ i for i = 1, 2, -(r, σ, w) |= ∃x (i) .ψ iff there exists j ∈ [r(i)] such that (r, σ[x (i) → j], w) |= ψ, -(r, σ, w) |= ∀x (i) .ψ iff (r, σ[x (i) → j], w) |= ψ for every j ∈ [r(i)], -(r, σ, w) |= ∃ * x (i) .ψ iff there exist w l1 , . . . , w l k ∈ I * pB(r) with 1 ≤ l 1 < . . . < l k ≤ r(i) such that w = w l1 . . . w l k and (r, σ[x (i) → j], w j ) |= ψ for every j = l 1 , . . . , l k , -(r, σ, w) |= ∀ * x (i) .ψ iff there exist w 1 , . . . , w r(i) ∈ I * pB(r) such that w = w 1 . . . w r(i) and (r, σ[x (i) → j], w j ) |= ψ for every j ∈ [r(i)], -(r, σ, w) |= ∃ ¡ x (i) .ψ iff there exist w l1 , . . . , w l k ∈ I * pB(r) with 1 ≤ l 1 < . . . < l k ≤ r(i) such that w ∈ w l1 ¡...¡w l k and (r, σ[x (i) → j], w j ) |= ψ for every j = l 1 , . . . , l k , -(r, σ, w) |= ∀ ¡ x (i) .ψ iff there exist w 1 , . . . , w r(i) ∈ I * pB(r) such that w ∈ w 1 ¡ . . . ¡ w r(i) and (r, σ[x (i) → j], w j ) |= ψ for every j ∈ [r(i)].
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) ∀y (i) ∃x (j) ∀y (j) ((x (i) = y (i) ) ∧ (x (j) = y (j) )).ψ for ∃x (i) ∀y (i) ∃x (j) ∀y (j) .(((x (i) = y (i) ) ∧ (x (j) = y (j) )) → ψ).

Note that in [START_REF] Mavridou | Configuration logics: Modelling architecture styles[END_REF] 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. Definition 6. 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 # p i1 (x (i1) ) ∧ . . . ∧ p im (x (im) ) ::= p i1 (x (i1) ) ∧ . . . ∧ p im (x (im) ) ∧ j=i1,...,im p∈P (j)\{pj } ¬p(x (j) ) ∧ j=i1,...,im ∀y (j) (y (j) = x (j) ). ∀x (k) .¬p(x (k) ) .

The first m -1 conjunctions express that the ports in the argument of # participate in the interaction. The double indexed conjunctions in the first pair of big parentheses disable all the other ports of the participating instances of components of type i 1 , . . . , i m described by x (i1) , . . . , x (im) , respectively; conjunctions in the second pair of parentheses disable all ports of remaining instances of component types i 1 , . . . , i m . The last conjunct in the third line ensures that no ports in instances of remaining component types participate in the interaction.

Examples of FOEIL sentences for parametric architectures

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 [START_REF] Pittou | Architecture modelling of parametric component-based systems[END_REF] 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) . #(p d (x (1) ) ∧ p r (x (2) ))

* ∀ ¡ x (3) .#(p d (x (1) ) ∧ p n (x (3) )) * ∃ ¡ y (3) . #(p l (x (2) ) ∧ p t (y (3) )) * #(p e (x (2) ) ∧ p w (y (3) ) ∧ p a (x (1) )) .
Example 5. (Request/Response) 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) ))) * (∀ ¡ x (3) .(#(p l (x (3) ) ∧ p u (x (1) )) * #(p o (x (3) ) ∧ p t (x (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) . #(p a (x (1) ) ∧ p n (x (2) )) * #(p t (x (1) ) ∧ p r (x (2) )) * ∃ ¡ x (3) . #(p e (x (3) )∧p c (x (2) )) * #(p g (x (3) )∧p s (x (2) )) * #(p d (x (3) )∧p f (x (2) )) .
In [START_REF] Mavridou | Configuration logics: Modelling architecture styles[END_REF] 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 [START_REF] Bozga | Checking deadlock-freedom of parametric component-based systems[END_REF][START_REF] Konnov | Parameterized systems in BIP: design and model checking[END_REF][START_REF] Mavridou | Configuration logics: Modelling architecture styles[END_REF].

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.

Decidability results for FOEIL

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 [START_REF] Pittou | Architecture modelling of parametric component-based systems[END_REF] 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).

Proposition 1. Let ψ be a FOEIL formula over a set pB = {B(i, j) | i ∈ [n], 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.

Theorem 2. Let pB = {B(i, j) | i ∈ [n], j ≥ 1} be a set of parametric components and r : [n] → N a mapping. Then, the equivalence problem for FOEIL sentences over pB w.r.t. r is decidable in doubly exponential time.

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) .

Theorem 3. Let pB = {B(i, j) | i ∈ [n], 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.

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 [START_REF] Sakarovitch | Elements of Automata Theory[END_REF], and thus satisfiability of FOEIL sentences over pB is decidable in exponential time.

Theorem 4. Let pB = {B(i, j) | i ∈ [n], j ≥ 1} be a set of parametric components and r : [n] → N a mapping. Then, the validity problem for FOEIL sentences over pB w.r.t. r is decidable in doubly 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 valid iff L(A ψ,r ) = I * pB(r) which is decidable in exponential time [START_REF] Sakarovitch | Elements of Automata Theory[END_REF]. Hence, we can decide whether ψ is valid or not in doubly exponential time.

Conclusion

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 [START_REF] Mavridou | Configuration logics: Modelling architecture styles[END_REF] 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 [START_REF] Mavridou | Configuration logics: Modelling architecture styles[END_REF] 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. [START_REF] Attie | A general framework for architecture composability[END_REF]). Finally, in a forthcoming paper we study parametric component-based systems and FOEIL in the weighted setup.

  The research work was supported by the Hellenic Foundation for Research and Innovation (HFRI) under the HFRI PhD Fellowship grant (Fellowship Number: 1471).

( 4 )

 4 We state an effective translation of FOEIL formulas to finite automata and prove the decidability of equivalence, validity and satisfiability for FOEIL sentences.The structure of the paper is as follows. In Section 2 we discuss related work and in Section 3 we recall the basic notions for component-based systems and interactions. Then, in Section 4 we introduce the syntax and semantics of EPIL and present three examples of architectures defined by EPIL formulas. In Section 5 we introduce the syntax and semantics of our FOEIL and provide examples of FOEIL sentences describing concrete parametric architectures. Section 6 deals with the decidability results for FOEIL sentences. Finally, in Conclusion, we present open problems and future work.

Definition 3 .

 3 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:

  there exist w 1 , w 2 ∈ I(P ) * such that w = w 1 w 2 and w i |= ϕ i for i = 1, 2, -w |= ϕ 1 ¡ ϕ 2 iff there exist w 1 , w 2 ∈ I(P ) * such that w ∈ w 1 ¡ w 2 andw i |= ϕ i for i = 1, 2.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, ϕ) whereB = {B(i) | i ∈ [n]} is a setof 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 .

Fig. 1 .

 1 Fig. 1. Blackboard architecture. A possible execution for the interactions.

φ

  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 d , p r }, {p d , p n1 }, {p d , p n2 }, {p d , p n3 }, {p l , p t2 }, {p e , p w2 , p a } satisfies ρ but represents no order of the interactions' execution.

  p

Fig. 2 .

 2 Fig. 2. Request/Response architecture. The omitted interactions are derived similarly.

  topics) and ξ 1 = ξ 11 ∨ ξ 12 ∨ (ξ 11 ¡ξ 12 ), ξ 2 = ξ 21 ∨ ξ 22 ∨ (ξ 21 ¡ξ 22 )

Fig. 3 .

 3 Fig. 3. Publish/Subscribe architecture. A possible execution for the interactions.

  p∈P (j) ¬p(y (j) ) ∧ k∈[n]\{i1,...,im} p∈P (k)

  m 1 p a 1 p d 1

	Client 2 B(7)	p l 2 p o 2	p u p t	S. Registry B(1)	p e	p r 2	Service 2 B(3)
	p n 2 p q 2 p c 2				p g 2	p s 2
	Client 1 B(6)	p l 1 p o 1				p r 1	Service 1 B(2)
	p n 1 p q 1 p c 1				p g 1	p s 1
				p m 2 p a 2 p d 2
					Coord. 2		Coord. 1
					B(5)		B(4)

  a 1

						p e 1	Subs. 1 B(5)
						p g 1
	Publ. 1 B(1)		p n 1	Topic 1 B(3)	p c 1	p d 1
					p s 1
		p t 1	p r 1		p f 1	p e 2	Subs. 2 B(6)
						p g 2
						p d 2
	Publ. 2 B(2)	p a 2	p n 2	Topic 2 B(4)	p c 2	p e 3	Subs. 3 B(7)
					p s 2	p g 3
		p t 2	p r 2		p f 2	p d 3

According to our terminology for EPIL formulas, a FOEIL formula should be defined over the set of ports of pB. Nevertheless, we prefer for simplicity to refer to the set pB of parametric components.

Acknowledgement. We are deeply grateful to Simon Bliudze for discussions on a previous version of the paper.


Leonardo Frittelli
email: leonardofrittelli@mcafee.com

Facundo Maldonado
email: facundomaldonado@mcafee.com

Hernán Melgratti

Emilio Tuosto
email: emilio.tuosto@gssi.it

A Choreography-Driven Approach to APIs: the OpenDXL Case Study

We propose a model-driven approach based on formal datadriven choreographies to model message-passing applications. We apply our approach to the threat intelligence exchange (TIE) services provided by McAfee through the OpenDXL industrial platform. We advocate a chain of model transformations that (i) devises a visual presentation of communication protocols, (ii) formalises a global specification from the visual presentation that captures the data flow among services, (iii) enables the automatic derivation of specifications for the single components, and (iv) enables the analysis of software implementations.

Introduction

We propose a methodology for the modelling and analysis of (part of) OpenDXL, a distributed platform that embraces the principles of the API-economy [START_REF]The API-economy[END_REF][START_REF] Doerrfeld | The API Economy Disruption and the Business of APIs. Nodic APIs (nordicapis.com)[END_REF]. In this context applications are services built by composing APIs and made available through the publication of their own APIs. In fact, the APIs of OpenDXL are paramount for enabling the openness of the platform, its growth in terms of services (currently the platform offers hundreds of different services), and its trustworthiness. The overall goal of OpenDXL is to provide a shared platform for the distributed coordination of security-related operations. A key aspect of the platform is to foster public APIs available to stakeholders for the provision or consumption of cyber-security services.

A well-known issue in API-based development is that APIs interoperability heavily depends on the (quality of) documentation: "An API is useless unless you document it" [30]. Proper documentation of APIs is still a problem. The current practice is to provide informal or semi-formal documentation that makes it difficult to validate software obtained by API composition, to establish their properties, and to maintain and evolve applications [START_REF] Ariola | Testing in the API Economy. Top 5 Myths[END_REF]. The OpenDXL platform is no exception. The APIs of the platform is mostly described in plain English.

We advocate a more systematic approach that, turning informal documentation of APIs in precise models, enables the application of formal methods to develop and analysis services. We focus on threat intelligence exchange (TIE) [START_REF]Threat intelligence exchange recommended workflow[END_REF], one of the OpenDXL APIs for the coordination of activities such as assessment of security-related digital documents or reaction to indicators flagging suspicious behaviour or data. The API of TIE is part of OpenDXL and it has been designed to enable the coordination of distributed security-related activities. More precisely, TIE APIs support the management of crucial cyber-security information about assets (digital or not) of medium-size to big organisations.

Components for TIE developed by third-party stakeholders sometimes exhibit unexpected behaviour due to the ambiguity of the documentation of communication protocols. In fact, TIE relies on an event-notification communication infrastructure to cope with the high number of components and the volume of the communication. This asynchronous communication mechanism requires the realisation of a specific communication protocol (an application-level protocol) for the various components of the architecture to properly coordinate with each other. To address these issues, we propose a more rigorous approach to the development and documentation of the APIs. We adopt a recent behavioural type system [START_REF] Bruni | Data-driven choreographies à la klaim[END_REF] to give a precise model of some TIE services. Besides the resolution of ambiguities in the API documentation, our model enables some static and run-time verification of TIE services. We will discuss how these models could be used to check that the communication pattern of components is the expected one. Also, we will show how our behavioural types can be used to automatically verify logs of executions that may flag occurrences of unexpected behaviour.

Summary of the contributions Our overall contribution is a methodology for the design, rigorous documentation, and analysis message-passing applications. We firstly introduce our methodology and describe the model-transformations it entails. An original aspect of our approach is the combination of two models conceived to tackle different facets of message-passing applications. More precisely we rely on global choreographies (g-choreographies, for short; see e.g., [START_REF] Guanciale | Realisability of pomsets via communicating automata[END_REF][START_REF] Tuosto | Semantics of global view of choreographies[END_REF] and references therein) to specify the communication pattern of a message-passing system and on klaimographies [START_REF] Bruni | Data-driven choreographies à la klaim[END_REF] to capture the data-flow and the execution model of our application domain.

We aim to show how a model-driven approach can be conducive of a fruitful collaboration between academics and practitioners. We draw some considerations about this in Section 6. Our approach consists of the following steps:

1. Device a graphical model G representing the coordination among the components of the application; for this we use global choreographies (cf. Section 2.1). 2. Transform G into behavioural types formalising the protocol into a behavioural type K representing the global behaviour of the application; for this we use klaimographies (cf. Section 2.2)

3. Transform K into specifications of each component of the application; for this we project K on local types (cf. Section 4). 4. Transform the local types into state machines from which to derive monitors to check for possible deviations from expected behaviour and verify implementations of components (cf. Section 5).

Although, g-choreographies are crucial to settle a common ground between academics and practitioners, they do not capture the data-flow and the execution model of OpenDXL. To cope with this drawback we formalise TIE with klaimographies, a data-driven model of choreographies.

Structure of the paper An overview of the TIE and an informal account of our behavioural types system is given in Section 2.1 (we refer the reader to [START_REF] Bruni | Data-driven choreographies à la klaim[END_REF] for the full details). The behavioural types of TIE are reported in Section 3; there we clarify that our model falls in the setting of "top-down" choreographic approaches. This amounts to say that we first give global specification that formally captures the main aspects of the communication protocol of all TIE from a holistic point of view. Then, in Section 4 we discuss how to automatically derive (by projection) the local behaviour of each component of TIE. We consider a few real scenarios in Section 5 and draw some conclusions in Section 6.

Preliminaries

We survey the two main ingredients of this paper, OpenDXL and klaimographies. We focus on the part of OpenDXL relevant to our case study and only give an informal account of klaimographies (see [START_REF] Bruni | Data-driven choreographies à la klaim[END_REF] for details).

An informal account of OpenDXL

The Open Data Exchange Layer (OpenDXL, https://www.opendxl.com/) is an open-source initiative aiming to support the exchange of timely and accurate cyber-security information in order to foster the dynamic adaptation of interconnected services to security threats. OpenDXL is part of the McAfee Security Innovation Initiative [START_REF]Mcafee security innovation alliance[END_REF], a consortium of about hundred ICT companies including HP, IBM, and Panasonic. A main goal of OpenDXL is to provide a shared platform to enable the distributed coordination of security-related operations. This goal is supported by the threat intelligence exchange (TIE) reputation APIs [START_REF]Threat intelligence exchange recommended workflow[END_REF] designed to enable the coordination of activities involving the assessment of the security threats of an environment (configuration files, certificates, unsigned or unknown files, etc.); the prioritisation of analysis steps (focusing on malicious or unknown files); the customisation of security queries based on reputation-based data (such as product or company names); the reaction to suspicious indicators. A key aspect of OpenDXL lays in its service-oriented nature. Providers use the APIs to offer various services such as reporting services, firewalls, security analytics, etc. Consumers of these APIs (typically companies or large institutions) can either use existing services, or combine them to develop their own functionalities. The basic communication infrastructure features an event-notification architecture whereby participants subscribe to topics of interests to generate events or query services. Such topics are also used to broadcast security information of general interest. The main components of OpenDXL are clients (C), servers (S), and brokers (B). The latter mediate interactions among clients and servers in order to guarantee service availability. Brokers interact with each other to dynamically assign servers to clients when default servers are unavailable.

The high-level workflow of the TIE APIs is specified by the sequence diagram in Fig. 1 (borrowed from [START_REF]Threat intelligence exchange recommended workflow[END_REF]). Together with other informal documentation, the diagram guides the implementation of new components or the composition of services available in the platform. For instance, the documentation describing how clients can set the reputation of a file specifies that a client "must have permission to send messages to the /mcafee/service/tie/reputation/set topic".

Data-driven global types

Unlike "standard" behavioural types, klaimographies model data flows in a communication model not based on point-to-point interactions. Interactions in a klaimography happen through tuple spaces in the style of Linda-like languages [START_REF] Gelernter | Generative communication in Linda[END_REF]. Instead of relying on primitives for sending and receiving messages over a channel, here there are primitives for inserting a tuple on a tuple space, for reading (without consuming) a tuple from a tuple space, or for retrieving a tuple from a tuple space. We call these interactions data-driven, as the coordination is based on (the type of) the exchanged tuples and the roles played by components. In fact, the communication model uses pattern matching to establish when a message from a sender may be accessed by a receiver. Crucially, klaimographies also feature multi-roles, namely roles that may be enacted by an arbitrary number of instances. Let us discuss these points with a simple example:

K = C → S : (bool • int) @ . S → C : (int • str) @
The klaimography K specifies the communication protocol between (arbitrarily many) clients C and (arbitrarily many) servers S. More precisely, each client makes a request to a server by inserting a tuple consisting of a boolean and an integer at the tuple space , as indicated by the prefix C → S : (bool • int) @ . A server consumes the request and generates a response to be consumed by a client, as specified by S → C : (int • str) @ . Remarkably, K does not prescribe that the particular client and server involved in the first interaction are also the ones involved in the second interaction; K above establishes instead that every client starts by producing a tuple to be consumed by a server and then consumes a tuple generated by a server (also K stipulates that servers behave dually). As a consequence, the participants in K cannot correlate messages in different interactions. This can be achieved by using binders, e.g.,

K = C → S : (bool • νx : int) @ . S → C : (x : int • str) @
The first interaction in K introduces a new name x for the integer value exchanged in the first message. The use of x in the second interaction constraints the instances of S and C to share a tuple whose integer expression matches the integer shared in the first interaction. Consequently, the two messages in the protocol are correlated by the integer values in the two messages.

Tuple spaces may simulate other communication paradigms such as multicast or event-notification. For instance, a tuple space can be thought of as a topic; messages can be produced, read and consumed only by those roles that know such topic. Binders can also be used to ensure the creation of new topics. Consider the klaimography below:

K = C → S : (bool • int • ν : loc) @ . S → C : (int • str) @
K is similar to K but for the fact that each client communicates to the server a new tuple space known only to the particular client and server that communicate in the first interaction; the second interaction takes place by producing and consuming messages on such new tuple space.

Broadcast can be achieved by producing persistent messages, e.g.,

K = C → S : (bool • int) @ . S!int • str @ r
where S!int • str @ r states that servers insert their responses at locality r. The absence of round brackets around the tuple expresses that such tuple is read-only (i.e., they cannot be removed from the tuple space); the absence of a receiver expresses that any role can read the tuple; consequently, the generated tuple can be read by any role "knowing" the locality r.

Additionally, klaimographies provide operators for sequential composition (≺), choices (+) and recursion (µ ρ X.K), illustrated in the following section.

Klaimographies for OpenDXL

The first problem we had to face in the modelling of the protocol was to find a common ground between academic and industrial partners. This is important in

C-→S : MD(x) S-→C : Restt(x) C-→S : MD(x) C-→S : File(x) S-→C : Resft(x) C-→S : File(x) S-→C : Restf (x) C-→S : MD(x) S-→C : Resff (x) + + C-→S : Req(x) + (i) (ii) + KNR Fig. 2.
A g-choreography for TIE APIs order to have enough confidence that the produced formalisation faithfully represent the protocol. To attain this we gave a first approximation of the protocol as the g-choreography in Fig. 2 which we now describe. A client C and a server S engage in a protocol where C may (repeatedly) either (i) send S meta-data regarding some file x or (ii) request the analysis of a file x. A server S reacts to a request from a client in four possible ways depending on the information S may need to further acquire from the requesting client. In the protocol these alternatives are encoded with a message Res bb (x) where b and b are two boolean flags; the first boolean is set to true when the server needs meta-data related to the file x while b is set to true if more context information about the file is necessary.

The client reacts to this request from the sever as appropriate. For instance, if C receives the message Res tt (x) then it has to send both meta-data and context information, while only the latter are sent if Res ft (x) is received. Before iterating back, the server may publish a new report 4 ; this is modelled by the activity K NR which we leave unspecified. This activity consists of a possible emission of a new report about file x that the server S may decide to multi-cast to clients (not just to clients currently engaging with the server).

We remark that the g-choreography in Fig. 2 represents the interactions between clients and servers and has been introduced as a first step in the formalisation of the protocol to pave the way for its algebraic definition as klaimographies. Firstly, a graphical representation played a central rôle when validating protocol interactions with industrial partners. Secondly, the graph was used as a blueprint for the formalisation. Hence, we invite the reader to follow such graph as the formal definitions unroll.

In the OpenDXL platform several clients and servers may interact by exchanging messages. The interaction in TIE is always triggered by a client which, as seen in Section 2.1, iteratively decides to either send some metadata on a file or request for the reputation of a specific file. This can be defined as follows

K TIE µ C X.K Body ≺ X (1)
where µ C X.K Body ≺ X is the recursive type to express iterative behaviour; it indicates that role C is the one controlling the iteration. Namely, C decides whether to repeat the execution of the body K Body or to end it. The sequential composition K Body ≺ X is just syntax to express that, after the execution of K Body , the iteration restarts. Notation We write as "macros" so that occurrences of the left-hand side of the equation are verbatim replaced for its right-hand side. The body of the iteration in (1), defined as

K Body (K MD (x, ) + K REQ (x, )) ≺ K NR (x) (2)
specifies that each iteration consists of a choice between K MD (x, ) and K REQ (x, ) followed by K NR (x):

-The branch K MD (x, ) accounts for the case in which a client sends new metadata to a server. -The branch K REQ (x, ) describes the interaction for the case in which the client sends a reputation request. -The continuation K NR (x) describes the decision of the server of emitting a reputation report.

Notation In accordance with the previous notation, x and above are just metaidentifiers for the same syntactic identifier across equations.

Let b be a globally known location representing the public name on which a client sends requests to a server. The branches of the body are defined as:

K MD (x, ) C → S : (MD • νx : Dgt • ν : loc) @ b K req (x, ) C → S : (Req • νx : Dgt • ν : loc) @ b . K info (x, ) (3)
In both cases the first interaction takes place on the tuple space b.

In K MD (x, ), the client simply sends a tuple MD • νx : Dgt • ν : loc made of three fields. The first field has sort MD which is a tag for messages carrying metadata. The second field is a named sort νx : Dgt, where (i) the sort Dgt (after digest) types values that are hash codes of files and (ii) the identifier x is introduced to establish the correlation that will be used in the following interactions. This mechanism enables the tracking of data dependencies among interactions. Finally, the third field is another named sort : loc; basically, the client communicates also the name of a new tuple space, to be used in the subsequent communications. For instance, the continuation type

K NR (x) S!Report • x : Dgt @ b' + 0
describes the behaviour of a server that decides whether to emit a new report about the received metadata or not. Type K NR (x) consists of a non-deterministic choice between a branch S!Report • x : Dgt @ b' and the empty type 0. The former specifies that the server publishes a new report for the file by emitting a (persistent) tuple of type Report • x : Dgt on a publicly known5 tuple space b'. Note that the use of x constraints the new report produced by server S to be related to a file digest communicated earlier to S.

The interaction prefixes C → S : (...) @ are quite different than the prefix S!Report • x : Dgt @ . This is a remarkable peculiarity of klaimographies that is quite useful to model TIE. Firstly, the former kind of prefix describes an interaction between two roles: clients are supposed to produce messages of some sort for servers. Instead, the behavioural type S!Report • x : Dgt @ only prescribes the expected communication from a single role, the server. This allows any role to access the tuple types generated by this kind of prefixes.

Another important aspect is the other syntactic difference: the messages in round brackets are produced to be consumed, while the ones not surrounded by brackets are persistent and can only be read; moreover, the message can be read by any role able to access the tuple space . For instance, requests of clients are eventually handled by a server, while any role can read, but not remove, reports.

Let us now return to the comment on the other branch in (2). In the klaimography K REQ (x, ), a client sends a request for the reputation of a file by sending a message whose tag is of type Req. In that message, the client sends the digest Dgt that identifies the file and, analogously to K MD (x, ), a fresh locality ; the correlation x and the locality are used in the subsequent interactions, which are described by K info (x, ) below.

K info (x, ) S → C : (Res tt • x : Dgt) @ . K tt (x, ) + S → C : (Res tf • x : Dgt) @ . K tf (x, ) + S → C : (Res ft • x : Dgt) @ . K ft (x, ) + S → C : (Res ff • x : Dgt) @
This klaimography corresponds to the inner-most choice of the graph in Section 2.1; it prescribes the possible responses that the server may send to the client. We start commenting on the last branch. If the server does not require further information, it simply informs the client that the interaction for that request concludes. The remaining branches of K info (x, ) model the cases in which the server requests both the metadata and the file (first branch), just the metadata (second branch) or just the file (third branch). When both metadata and file are requested, then the protocol continues as follows

K tt (x, ) C → S : (MD • x : Dgt) @ . C → S : (File • x : Dgt) @
And, when the server asks for either the metadata or the file, then

K tf (x, ) C → S : (MD • x : Dgt) @ K ft (x, ) C → S : (File • x : Dgt) @
which is in accordance with the g-choreography in Section 2.1.

Projections

As commonplace in choreographic approaches, the description of the expected behaviour of each participant in a protocol can be obtained by projection. In our case, this is an operation that takes a klaimography and a role and generates a description, dubbed local type, of the flow of messages sent and received by that participant. Local types are meant to give an abstract specification of the processes implementing the roles of the klaimography. We write the projection of a klaimography K for the role ρ as K ρ . Note that the projection operation is completely automatic; given a klaimography the behaviour of each component is algorithmically derived. We omit here the formal definition of K ρ , which can be found at [START_REF] Bruni | Data-driven choreographies à la klaim[END_REF], and illustrate its application to K TIE in (1). We consider K TIE C first. The projection operation is defined by induction on the syntax of the klaimography; hence we focus on the constituent parts of K TIE . Consider the branch K MD (x, ), which is defined in (3) as the interaction C → S : (MD • νx : Dgt • ν : loc) @ b. The projection of this interaction on the client role just consists of the behaviour that generates a message of type MD • νx : Dgt • ν : loc on the locality b; formally, this is written

K MD (x, ) C = (MD • νx : Dgt • ν : loc)!b
Note (a) the use of the round brackets to represent message consumption, and (b) the projection is oblivious of the intended receiver (the server). In fact, the behavioural type system of klaimographies ensures that if the actual components abide by the klaimographies given in Section 3, then only components enacting the role of the server will access those kind of tuples.

The projection for K req (x, ) (and all its constituents) is analogous:

K req (x, ) C = (Req • νx : Dgt • ν : loc)!b . K info (x, ) C K info (x, ) C = (Res tt • x : Dgt)? . K tt (x, ) C + (Res tf • x : Dgt)? . K tf (x, ) C + (Res ft • x : Dgt)? . K ft (x, ) C + (Res ff • x : Dgt)? K tt (x, ) C = (MD • x : Dgt)! .(File • x : Dgt)! K tf (x, ) C = (MD • x : Dgt)! K ft (x, ) C = (File • x : Dgt)!
Observe that the projection for K info is a choice in which C expects (and consumes) one of the four possible messages produced by the server at locality . Finally, the projection of K NR (x) is

K NR (x) C = Report • x : Dgt?b' + 0
Differently from the projection of interactions in which the client consumes the messages, the first branch of the above projection just reads the message at the locality . Note the difference between (t)? (consumption) and t? (read), which reflects the usage of round bracket discussed in Section 3. Projection works homomorphically on choices and sequential composition, hence the projection of K body in (2) we have

K body C = (K MD (x, ) C + K req (x, ) C ) ≺ K NR (x) C
We now give the projection of K TIE , which is a recursive klaimography. Then,

K TIE C = µX(b) . stop !b . 0 + νy : loc !b . K body C ≺ X y b (4)
The projection of a recursive klaimography is also a recursive local type. However, the projection introduces auxiliary interactions to coordinate the execution of the loop. Since C is the role that coordinates the recursion in K TIE , in the projection C starts its body by communicating its decision to terminate or to continue. Namely, the body of K TIE C has two branches, stop !b communicates the termination of the recursion, while the other starting with νy : loc !b iterates (and distributes a fresh localities for the next iteration). Note that recursive variables X in the local types are parameterised variables X(b) and X b . In general, a klaimography µ ρ X.K is projected as a recursive local type µX( x) . L where the formal parameters x stand for the locations used for coordination and are the initial values, in this case, b. The projection for the behaviour of the server is obtained analogously.

Types at work

Like data types, behavioural types can be regarded as specifications of the intended behaviour of a system. As such they can check that the components implementing the protocol abide by their specifications. Customarily, approaches to behavioural types focus on static enforcement [START_REF] Honda | Multiparty asynchronous session types[END_REF][START_REF] Dezani-Ciancaglini | Sessions and session types: An overview[END_REF][START_REF] Hüttel | Foundations of session types and behavioural contracts[END_REF], i.e., the source code implementing a role is type-checked against its local type and the soundness of the type checking algorithm ensures that well-typed code behaves as prescribed by its type. Also the dynamic enforcement of protocols based on local types has been addressed in the literature [START_REF] Bocchi | Monitoring networks through multiparty session types[END_REF][START_REF] Neykova | Timed runtime monitoring for multiparty conversations[END_REF][START_REF] Francalanza | Reversible choreographies via monitoring in erlang[END_REF]. In most cases, monitors dynamically check that the messages exchanged by the components comply with the protocol. Deviations from the expected behaviour are singled out and offending components are blamed.

In this work we explore the usage of local types for the off-line monitoring of role implementations. In particular, we use projections to check that the different implementations of the multirole C in TIE follow the protocol. We take advantage of the fact that the communication infrastructure of TIE keeps a log with the communication messages generated by the different roles.

In Fig. 3 we show an anonymised (and simplified) version of a few entries of a real log. Each entry corresponds to an interaction between a client and a server and it consists of a record of comma-separated fields which we now describe: the first field is a global timestamp used to order the entries chronologically; the second field is the locality, which is encoded by a three-digits number; the third and fourth fields are the identity of the sender and of the receiver respectively (for obvious reasons, the real identities have been obfuscated; Fig. 3 uses symbolic names clientA, server1, etc.); the remaining fields are the payloads of the message, which varies depending on the type of the message.

The type of each message is identified by a tag: Req, MD, and File have analogous meaning to the ones used in the specification of the protocol in Sections 3 and 4. The sorts such as Res tf used in our specification are rendered in the implementation with a payload consisting of three parts: the tag Res and two binary digits; used to encode the subscript (with 1 representing true and 0 representing false); for instance, the subscript tf above is encoded as the pair 1, 0. We use file i to represent the different digests transmitted over the messages. The first entry in the log of Fig. 3 is generated by the interaction

C → S : (Req • νx : Dgt • ν : loc) @ b
executed by K req (x, ), where the instance clientA of the role C sends to the instance server1 of S a request for a reputation report about the file file1.

The second entry in the log corresponds to the selection of the branch

S → C : (Res tf • x : Dgt) @ . K tf (x, )
in K info (x, ) in which the server asks the client for the metadata of the file; the messages in which the client sends the metadata can be seen in the third line of the log. Obviously, the interactions among different instances need not to be consecutive, as it is the case for the entries at locality 340 which are on the lines 4, 5 and 7. Observe also that the last entry in Fig. 3 has broadcast as its receiver. This message corresponds to the publication of a reputation report by the server, which is defined in K NR (x) as Report • x : Dgt? . We have implemented in Python an off-line monitor that takes a log and a local type in input and checks whether the log faithfully follows behaviour described by the local type. Local types are turned into a textual representation of finite state automata that can be depicted as UML state machines. For instance, @startuml left to right direction [*] --> S0 S0 --> S0: 'MD'@l @Dgt S0 --> S1: 'Req'@l S1 --> S2: ('Res', '1', '1')@l -> @Dgt S1 --> S3: ('Res', '0', '1')@l -> @Dgt S1 --> S4: ('Res', '1', '0')@l -> @Dgt S1 --> S0: ('Res', '0', '0')@l S2 --> S3: 'MD'@l -> @Dgt S3 --> S0: 'File'@f S4 --> S0: 'MD'@l @enduml the local type K tie C is defined as shown in Fig. 4, which can be graphically represented as shown in Fig. 5.

These representations are obtained by "massaging" the projections defined in Section 4. The main difference between the UML representation and the local type (besides the obvious syntactic changes) is that the former does not contain the messages for coordinating the recursion in (4) (i.e., stop and νy : loc); those have been omitted because not explicitly exchanged by the components. As a consequence, we assume that the client continues the loop if it keeps sending messages and it finishes silently otherwise. Another simplification for the sake of the presentation is the omission of K NR (x) C , essentially because the observable behaviour of the client is unaffected if it reads or not a report. In fact, the log is not informative enough to discriminate on the choice made by the client.

Once such simplifications are in place, (4) can be easily matched with the graphical representation in Fig. 5. The state S0 represents K TIE C . The self-loop stands for the selection of the branch K MD (x, ) C , i.e., the client sends a message containing metadata, and then restart the loop. The transition from S0 to S1 represents instead the choice of the branch K req (x, ) C , i.e., the client request of a reputation report. The remaining states are in one-to-one correspondence with the following projections defined in the previous section: S1 stands for K info (x, ) C , S2 for K tt (x, ) C , S3 for K ft (x, ) C , and S4 for K tf (x, ) C . All the transitions are decorated with the associated messages sent or received by a client. Note also that S1, S3 and S4 have transitions to the state S0 meaning that execution of the body the is completed and that the body can be restarted.

With this implementation we have detected a few deviations from the expected behaviour. In particular, some clients exhibit the following violations:

files are sent for analysis without a prior request, requests for further information from the server are not honoured.

The first violation is detected by the presence of an entry of the log with a message tagged File without a previous message from the server with tag Res tt or Res ft . The second violation is due to the absence of an entry related to a given hash used by the server for asking further information.

Our implementation can also check other properties. For example, TIE clients should guarantee a so-called "time-window" property which requires that "a request for the analysis of the same file from a client must not happen before a given amount of time elapsed from the previous request from the client for the same file."

This property (as well as others) can be checked by monitor derived from the local types as done in the examples above.

Conclusions, Related & Future Work

Summary We reported on a collaboration between industrial and academic partners which applied formal methods to address a key problem affecting APIsbased software. More precisely, the problem that informal specifications of the behaviour of services may lead to errors in message-passing applications. For instance, third-party clients of TIE services exhibit anomalous when interacting with the services developed at McAfee. To overcome this problem, TIE services are engineered with a rather defensive approach to anticipate anomalous interactions. Unintended behaviours are reported to third-parties after a "post-mortem" analysis of execution logs.

We devised a model-driven approach to model and validate message-passing software. We applied the methodology in the context of the OpenDXL platform, an initiative of a consortium of industries conceived for the development of cyber-security functionalities. The platform provides an API to allow developers to access and combine the functionalities of a service-oriented architecture. In this context we applied the methodology to the threat intelligence exchange (TIE) service provided by McAfee Cordoba for the assessment of security threats, prioritisation of analysis steps, reputation-based data queries.

Related work

The use of behavioural types for the specification and analysis of message-passing application is widespread (see [START_REF] Hüttel | Foundations of session types and behavioural contracts[END_REF] for a survey). Semantics of behavioural types (operational or denotational) abstract the behaviour of systems and enables the use of formal methods and tools to check their properties.

Our proposal hinges on a form of choreographies in the vein of global type systems [START_REF] Honda | Multiparty asynchronous session types[END_REF], which formally capture the design of WSCDL [START_REF] Kavantzas | [END_REF]. In fact, the specification of a global view is the starting step of our methodology and the use of a projection operation to (automatically) derive local views is a paramount step in the model-transformation chain described in Section 1. The literature offers several variants of choreographic models [START_REF] Dalla Preda | Dynamic choreographies -safe runtime updates of distributed applications[END_REF][START_REF] Qiu | Towards the theoretical foundation of choreography[END_REF][START_REF] Bravetti | Contract compliance and choreography conformance in the presence of message queues[END_REF][START_REF] Busi | Choreography and orchestration conformance for system design[END_REF][START_REF] Tuosto | Semantics of global view of choreographies[END_REF][START_REF] Guanciale | Realisability of pomsets via communicating automata[END_REF] (to mention but a few). A common treat of those models is that they are grounded on pointto-point communication in traditional settings (such as the use of the actor model [START_REF] Agha | Actors: A Model of Concurrent Computation in Distributed Systems[END_REF] or π-calculus [START_REF] Sangiorgi | The π-Calculus: a Theory of Mobile Processes[END_REF][START_REF] Milner | Communicating and Mobile Systems: the π-calculus[END_REF][START_REF] Milner | A Calculus of Mobile Processes, I and II[END_REF]). A distinguished feature of OpenDXL is that it relies on event-notification mechanisms. This is the main motivation for the adoption of klaimographies [START_REF] Bruni | Data-driven choreographies à la klaim[END_REF]. In fact, unlike other choreographic approaches, klaimographies advocate a peculiar interpretation of interactions. More precisely, interactions A-→B : m are generally interpreted as "an instance of A and an instance of B exchange message m". The interpretation of A-→B : m drastically changes in klaimographies and becomes "any instance of A generates the message m expected to be handled by any instance of B". This interpretation is the cornerstone for a faithful modelling of OpenDXL.

Lesson learned Although we are at an early stage of the collaboration, we can draw some conclusions.

A first point worth remarking is about the effectiveness of our methodology. On the one hand, the academic partners were oblivious of several current practices (such as the continuous defensive patching TIE servers). On the other hand, the industrial partners acquired some notions about behavioural specifications during the participation of a school [25] organised by the academic partners as well as presented the OpenDXL platforms at the school. The methodology was applied immediately after the school and the bulk of modelling and analysis of TIE was concluded in about 3-persons month. In the chain of model transformations of our methodology, steps (1) and ( 4) were paramount for practitioners to apply this methodology: the use of visual, intuitive, yet formal models enabled a fruitful collaboration among stakeholders. In fact, g-choreographies were key to tune up the model and to identify the main aspects of the intended communication protocol as well as to ease the collaboration between practitioners and academics. Basically, g-choreographies gave a first intuitive presentation capturing the essential interactions of TIE. This has been instrumental for an effectual collaboration. Once the g-choreography expressing the intended behaviour has been identified, the academic partners have devised the klaimographies formalising the expected behaviour. The identification of the corresponding klaimographies allowed us to automatically derive local specifications (step (iii)) and use them as precise blue-prints of components as well as to automatically derive monitors (step (iv)). Remarkably, the transformation from local types to state machines was suggested by our industrial partners who saw it as a more streamlined way of sharing the specifications among practitioners (including those outside McAfee). At this stage we do not have data to measure the impact of the enhanced documentation on the quality of the software produced.

This experience also highlights the importance of non-deterministic abstractions and of visual tools in practice. We argue that these elements are paramount for collaborations that could be beneficial to both academics and practitioners. In fact, behavioural types (as many formal methods) may not be easy for practitioners to handle. To tackle this issue we opted for models offering a visual and intuitive presentations of the formal models used in the specifi-cations. The specification in terms of g-choreographies and klaimographies was attained in few days of man-power involving academics and practitioners. This hints that our model-driven methodology can significantly reduce the steepness of the learning curve that formal methods often require.

The problem of informal behavioural specification is ubiquitous in API-based software. The approach we followed aimed at some generality: instead of devising ad-hoc formal methods for the OpenDXL case study, we decided to apply existing frameworks. In fact, both g-choreographies and klaimographies had been developed before and independently of this collaboration. The methodology proposed here assumes only that components communicate through generative coordination mechanisms [START_REF] Gelernter | Generative communication in Linda[END_REF]. As noted by one of the reviewers, "tuple-semantics are well-suited not only for this use case but for the modern age of IoT, where event-based middlewares are becoming the norm."

A final note on the connection with other formal methods. Behavioural specifications offer also support to "bottom-up" engineering (see, e.g., [START_REF] Lange | Synthesising choreographies from local session types[END_REF][START_REF] Lange | From Communicating Machines to Graphical Choreographies[END_REF]). This would require to infer the behaviour to analyse from logs and, as noted by another reviewer, one could spare "to model the whole behaviour [...] and focus on specific components." We concur that our methodology can be complemented by such technique (and this is indeed one of the goals within the BehAPI project). Also, one may wonder if the methodology can be combined with model checking. This is indeed the case since our models feature operation semantics amenable to be model checked. A drawback of model checking is that practitioners would find it hard to express the properties to check. Instead the top-down approach allowed them to express such conditions in terms of state machines.

Future work Global graphs have been key to facilitate the collaboration between academics and industrial partners for the former can use g-choreographies precisely (since they come with a precise semantics) and the latter can use the visual and intuitive presentation of g-choreographies. It is in the scope of future work to use the formal framework of g-choreographies. In fact, we can use gchoreographies to verify liveness properties of the communication protocols, or to generate executable template code to be refined by practitioners. We plan to extend ChorGram [START_REF] Lange | ChorGram: tool support for choreographic deveelopment[END_REF], a tool based on g-choreographies, to support the methodology. For instance, projection operations from global to local views are a key feature of our choreographic framework. Here, we have manually given klaimographies and their projections. This can be automatised by algorithmically transforming g-choreographies into klaimographies. Another possibility is to exploit ChorGram to generate code; for instance, ChorGram can map g-choreographies to (executable) Erlang code. These sort of functionalities are highly appealing to industrial stakeholders due (a) to the "correct-by-construction" principle they support and (b) to the fact that each release of TIE services requires the realisation of in-house clients for many different languages and platforms. For instance, OpenDXL needs to develop several version of each component for different execution environments. Also, TIE clients have to be implemented in different programming languages or for operating systems; this could be done by devising each software component by projection from a global view. Having tools that generate template code for implementing the communication protocol of each component would speed up the development process and reduce the time of testing (which would not need to focus on communications which would be correct-by-construction). In order to attain this, it could be useful to "dress up" g-choreographies with existing industrial standards that practitioners may find more familiar (and may be more appealing). An interesting candidate for this endeavour is BPMN [START_REF]Object Management Group. Business Process Model and Notation[END_REF] since its coordination mechanisms are very close to those of g-choreographies. In fact, BPMN is becoming popular in industry and it has recently gained the attention of the scientific community which is proposing formal semantics of its constructs. For instance, the formal semantics in [START_REF] Corradini | Walking through the semantics of exclusive and event-based gateways in BPMN choreographies[END_REF] could be conducive of a formal mapping from BPMN to g-choreographies or global types. In this way practitioners may specify global views within a context without spoiling the rigour of our methodology.

For simplicity in this paper we abstracted away from some aspects of TIE. The extension of our approach to the complete protocol is not conceptually complex, but it is scope for future work. This will include the analysis to further properties expected of TIE components and that can be checked from the logs. Following our methodology, we plan to devise monitors for the run-time verification of those properties as well.

A final remark is about other advantages of behavioural types that we can exploit in the future. For instance, one goal is to device tools for checking the compliance of components to the TIE protocol. This can be achieved by typechecking components against their projections.

Fig. 1 .

 1 Fig.1. Documenting TIE[START_REF]Threat intelligence exchange recommended workflow[END_REF]

Fig. 3 .

 3 Fig. 3. A simplified snippet of a real (anonymised) log

Fig. 4 .Fig. 5 .

 45 Fig. 4. Kdxl C as UML diagram (textual representation)

The server is actually multi-threaded and could issue new reports about files other than x at any time; for simplicity, we do not model this aspect.

Here we simplify the actual implementation where the topic used to publish the report is related to the file used in the request.

Acknowledgments We thank the anonymous reviewers for their many insightful comments and suggestions.

Research partly supported by the EU H2020 RISE programme under the Marie Skodowska-Curie grant agreement No 778233, by UBACyT projects 20020170100544BA and 20020170100086BA, PIP project 11220130100148CO, and by MIUR project PRIN 2017FTXR7S IT MATTERS (Methods and Tools for Trustworthy Smart Systems)