Francisco Durán

Gwen Salaün

Ajay Krishna

Automated Composition, Analysis and Deployment of IoT Applications

Building IoT applications of added-value from a set of available devices with minimal human intervention is one of the main challenges facing the IoT. This is a difficult task that requires models for specifying objects, in addition to user-friendly and reliable composition techniques which in turn prevent the design of erroneous applications. In this work, we tackle this problem by first describing IoT applications using abstract models obtained from existing models of concrete devices. Then, we propose automated techniques for building compositions of devices using a repository of available devices, and an abstract goal of what the user expects from such compositions. Since the number of possible solutions can be quite high, we use both filtering and ranking techniques to provide the most pertinent solutions to users. The provided solutions satisfy the given goal and may be analysed with respect to properties such as deadlock-freeness or unmatched send messages. Finally, the application can be deployed using existing execution engines.

Introduction

The Internet of Things (IoT) is a network of physical devices and software entities that interact together for fulfilling an overall objective. Although the devices are already available and omnipresent in our daily lives, the software allowing us to easily connect and manipulate those objects is still under development. Composition of devices and objects is a difficult and error-prone task for several reasons. First, there is a need for languages and models for describing (heterogeneous) objects or object interfaces. Several levels of expressiveness can be considered depending on the characteristics of the object (signature, behaviour, semantics, quality of service). Once a model of objects is properly defined, one can design a composition by specifying how these objects interact. This composition process should be as automated as possible to make it usable in practice by any end-user. Moreover, when building such a composition, several kinds of mismatch can arise resulting in an erroneous application. Finally, the goal is to deploy and run IoT applications with minimal human intervention.

In this paper, we propose techniques for supporting end-users during the composition and deployment tasks. We have a specific focus in this work on behavioural models for objects, that is, each object must exhibit the actions or messages it can execute as well as the order in which these actions must be triggered. Given such models, our techniques aim at automatically building satisfactory compositions given a repository of available objects and a description of the result that we call goal. The goal is an abstract specification of what the user expects from the resulting composition. A composition is satisfactory if it conforms to the goal requirements. Moreover, a composition can be analysed to check whether some additional correctness properties are verified. For example, such a property can state that each reachable send message has a matching receive message in another object. Finally, when a satisfactory composition is obtained, it is deployed by relying on existing execution engines.

Our solution consists of several consecutive steps for computing satisfactory compositions. First, we extract from the repository relevant objects wrt. the goal of the composition. For those objects, we compute all combinations and apply filtering techniques for keeping only objects exhibiting expected interactions according to the goal. We then check whether the remaining candidate compositions respect a defined compatibility notion. In this paper, we use a notion based on the equivalence of the intended goal with a candidate composition of objects. Additional properties can be verified on the resulting compositions, such as, e.g., the absence of deadlocks. If there are several compositions that satisfy the goal, we use ranking techniques for presenting the results in a specific order according to several possible relevance criteria.

The whole composition process is automated by an implementation in Maude [START_REF] Clavel | All About Maude[END_REF]. We also propose full automation of the deployment of the designed application, which allows our approach to support the development of IoT applications from the selection of a subset of satisfactory objects to their final deployment. In this work, we rely on Mozilla Project Things as execution and deployment platform, although other IoT platforms could have been used (Home Assistant, IFTTT, OpenHAB, etc.). We assume that objects are described using the Web Thing Description format by Mozilla. We also assume that the objects available in a given context (room, house, building, etc.) can be discovered using a search service, resulting in what we call a repository of objects. The goal provided by the end-user is described using a set of rules IF event THEN action representing what is expected from the generated composition.

Our prototype tool was applied to several examples for validation purposes. Since we target in this work applications at the level of a building (private house, office, nurse home, etc.), we made experiments with repositories consisting of about one hundred objects, for which the approach was able to compute compositions satisfying a given goal within a reasonable amount of time.

The rest of this paper is organized as follows. Section 2 introduces the model we use for objects and other notions (repository, goal, environment). Section 3 first presents the different steps that constitute our approach for automated composition of objects, and then describes our implementation and some experiments we carried out on several examples. Section 4 presents how IoT applications can be deployed in practice. Section 5 compares our approach to related work and Section 6 concludes the paper.

Models

In this section, we first introduce the model we use for describing devices and objects. Note that in the paper, for the sake of simplicity, we mainly use object as a common term for both devices and software elements. A repository is a set of objects, each object belonging to a family (TV, camera, light bulb, software app, window, etc.). We Listing 1. An excerpt from the JSON Thing Description of Hue temperature sensor then present our notion of composition, which relies on implicit bindings. Finally, we define the notion of goal that is used in this work for guiding the composition process and the notion of environment for modelling open systems.

In this work, we assume that objects are described using Mozilla's Web Thing Description format, 3 which provides a vocabulary for describing objects in a machine readable format with a JSON encoding. The description is complementary to the current W3C Web of Things (WoT) Working Group's abstract data model. WoT architectural style uses foundations of Web technology to build IoT in a decentralised, inter-operable, and scalable fashion [START_REF] Guinard | From the Internet of Things to the Web of Things: Resource-oriented Architecture and Best Practices[END_REF]. Our choice of WoT-based description is guided by the fact that things in WoT are backed by a standard data model and APIs which help in realworld deployment of objects. However, for designing the composition, we prefer to rely on an abstract model for objects, where we just keep the two most important attributes from a composition perspective, namely Event and Action. An event is emitted by a device (e.g., a room becomes too dark) whereas an action can be carried out on a device (e.g., turn on a light). The properties attribute in a Thing Description provides information on the type of event or action the device supports. Listing 1 shows an excerpt of the Hue temperature sensor description which describes a temperature sensor property. Since an order is possible between several events/actions (e.g., turn on a light and then turn off the light), we also keep this order in the model. To sum up, we describe an object using a Labelled Transition System (LTS) where labels either correspond to events or actions. Definition 1. An object is an LTS (S , s 0 , Σ, T ) where S is a finite set of states, s 0 ∈ S is the initial state, Σ = Σ ! ∪ Σ ? ∪ {τ} is a finite alphabet partitioned into a set of events, a set of actions, and the internal action τ, and T ⊆ S × Σ × S is a transition relation.

We write m! for an action m ∈ Σ ! and m? for an event m ∈ Σ ? . We also call them as send and receive messages, respectively, for homogeneity reasons. We use the symbol τ for representing internal activities (variable assignment, internal computation, local decision, etc.). A transition is represented as s l --→ s ∈ T where l ∈ Σ.

This abstract model presents two advantages. First, it allows us to support any concrete model for a Thing Description in a uniform way. Second, it is simple and expressive enough for designing a composition consisting of several objects.

We assume that each object comes with a defined model that can be automatically obtained from its JSON description. As far as the behavioural part is concerned (LTS), this can be defined by an expert who has the knowledge of the device (i.e., device manufacturers can provide the model along with the datasheet) or they can be built by learning the behaviour of these devices [START_REF] Raffelt | LearnLib: A Framework for Extrapolating Behavioral Models[END_REF].

We call repository a set of objects available, for example, in a room, a house or a building, depending on the context of the application. In practice, these objects are discovered using a search functionality that allows to identify all objects available on a given network. Search can be implemented using the mDNS protocol on the network or via Bluetooth Eddystone beacon for devices in close physical proximity. Each object is defined by its concrete model in JSON format. As far as composition is concerned, abstract models introduced before are enough, and therefore we assume that each object is defined by its abstract model (LTS) and is associated to a family. Definition 2. A repository is a set of couples (F, O) where F is a family name and O is a set of objects defined by their abstract model.

A composition is defined as a set of objects described by their abstract models. We assume the objects involved in a composition interact using binary communication. This means that one interaction occurs between one send message (action) and one receive message (event) of two different objects on the same message name. Additionally, we consider a synchronous communication model, that is, two objects involved in an interaction evolve at the same time when communicating (a.k.a. handshake communication). Considering asynchronous communication (communication via message buffers or publish-subscribe) is part of the perspectives of this work.

A goal is an abstract description of what the end-user expects from the compositionto-be. To define this goal, we take inspiration into recent languages proposed for connecting devices and software (IFTTT) or for smart home software automation (Open-HAB). A goal is thus defined as a set of rules IF x THEN y, where x and y correspond to interactions between two objects. A goal is also defined by a set of family names, which gives an information about the objects to participate in the composition. E.g., the user can write that she wants three objects in the composition: a TV, a camera and a motion sensor. Family names can be derived from the @type member annotation of the Web Thing Description model. This annotation describes the device capabilities and required properties which is the basis for defining families. E.g., the Hue temperature sensor description in Listing 1 belongs to the TemperatureSensor family of devices. Definition 3. A goal is a couple (R, FS ) where R is a set of rules and FS is a set of family names.

Since a set of rules directly translates to an LTS (each rule transforms to a sequence of two transitions outgoing from the initial state and coming back to it), goals can also be designed as LTSs (as shown in the running example at the end of this section). Last, it is worth observing that, given the dynamicity of IoT applications, we cannot assume that compositions of objects are built once and for all. They can evolve over time and objects can be added/removed for several reasons (replacement, loss of connectivity, upgrade, failure, etc.). Therefore, an IoT application can be seen like an open system where all messages are not necessarily bound and can be kept open for further addition of objects. Unbound messages can also correspond to external behaviours (a motion or an action of a human being). In our approach, we consider these actions to be part of the environment. The environment can be initially empty and enriched throughout the composition process, if necessary. Definition 4. An environment is a set of send and receive messages.

Example. As a running example, we use a smart home application, which aims at automatically regulating the temperature and brightness in a house. To do so, we require five objects, namely a temperature sensor, a connected window, a brightness sensor, a light, as well as a piece of software, namely a smart home application running on a smartphone and acting like an orchestrator. We now define the goal of the composition using the rules (and corresponding LTS) given in Fig. 1. As described in this figure, the end-user expects two behaviours from the composition-to-be: (i) when a temperature sensor detects a too-high temperature with respect to human standards (say 20 degrees Celsius), a window should be opened; (ii) when a brightness sensor detects a too low level of luminosity, a light should be turned on. We will present in the next section the techniques we propose for automatically computing compositions satisfying the goal from a set of objects available in the repository.

Composition and Analysis

In this section, we present our techniques for automatically computing IoT applications by composition of available objects. Fig. 2 presents an overview of the different steps of our approach, which takes as input a repository of objects, a goal and an environment. As output, we generate a list of resulting compositions satisfying the goal (also called compatible compositions) and possibly satisfying additional properties of interest such as deadlock freeness. This list can be empty if there is no solution. If there is more than a solution, the solutions are ranked with respect to some quality criterion. Note that human intervention is required only at the beginning of the composition process to define the goal and if necessary, the environment. Each step of our approach refines the Fig. 2. Overview of the approach number of candidate compositions (C' ⊆ C and C" ⊆ C'), but for the last step (ranking) that only orders the compositions taken as input without discarding any of them.

In the rest of this section, we first present with more details each step of the approach. Then, we introduce the implementation of these techniques using Maude. Finally, we describe some experiments we carried out for validating our approach.

Steps of our Approach

Combine & filter. The first step of our approach takes as input the part of the goal corresponding to the set of family names and the repository, and generates all possible combinations. For example, if the composition needs a temperature sensor and a connected window, and there are two different temperature sensors and three windows in the repository, we generate all possible combinations (six possible couples in that specific case). For each combination, we apply some filtering techniques to discard it if we know beforehand that this composition will not be able to satisfy the given goal. To do so, we rely on static analysis of the alphabets of the objects involved in a candidate composition. We do not want to build the result of the composition (the LTS corresponding to all possible executions of a set of interacting objects) because this would be too costly computationally speaking. This composition LTS will be built in the next step only for candidate compositions that are not discarded by the filtering process.

The filtering process aims at traversing the alphabet of the goal and at checking whether, for each element of the goal alphabet, there are two objects in the composition with matching messages on that message, that is, one send message and one receive message with that label in two different objects. This is mandatory, otherwise no interaction would be possible on that message, resulting in a deadlock. This approach is purely syntactic, so it is very efficient, but we may still have unsatisfactory candidate compositions. The next step builds the behavioural composition for this set of candidate objects and explores all possible executions to verify that the aforementioned interactions can effectively occur according to the behavioural models of the involved objects.

Definition 5. Given a goal (G, FS ) with G = (S G , s 0 G , Σ G , T G
) and a set of n object LTSs (S i , s 0 i , Σ i , T i ) corresponding to a candidate composition according to the family names given in FS , this composition is not filtered out iff for each m ∈ Σ G , ∃i, j ∈ {1, . . . , n}, such that m ∈ Σ ! i and m ∈ Σ ? j .

Fig. Compose & check compatibility. This step takes as input all combinations of objects obtained using the family names defined in the goal and the repository, which have been kept after application of the filtering techniques. For each combination, we first build the resulting LTS corresponding to the composition a.k.a. synchronous product [START_REF] Arnold | Finite Transition Systems -Semantics of Communicating Systems[END_REF] in the automata-based terminology. This LTS is built independently of the goal. It considers the objects involved in the combination and the environment. All synchronize on the intersection of their alphabets (no independent evolution of observable messages).

We recall that the communication model is synchronous, binary, and matches two transitions with the same label and opposite directions (sender and receiver).

Definition 6. Given a set of n object LTSs (S i , s 0 i , Σ i , T i ), the synchronous composition is the labelled transition system CLTS = (S c , s 0 c , Σ c , T c ) where: Once the composition LTS is built, we first hide all interactions in the composition LTS that do not belong to the alphabet of the goal. Then, we need to compare both LTSs (goal LTS and composition LTS) to check if they produce the same observational behaviours. Since there are possibly hidden (or τ) transitions in the composition LTS, we need to use a comparison notion that takes these specific transitions into account. This is the case of the branching bisimulation [START_REF] Van Glabbeek | Branching Time and Abstraction in Bisimulation Semantics[END_REF] (≡ br ), which is one of the finest bisimulation notions to compare LTSs in presence of hidden actions. Definition 7. Given a goal LTS G and a composition LTS CLTS build from a set of object LTSs, these objects satisfy the goal iff: hide Σ G (CLTS) ≡ br G.

-S c = S 1 × . . . × S n -s 0 c ∈ S c such that s 0 c = (s 0 1 , . . . , s 0 n ) -Σ c = ∪ i Σ i -T c ⊆ S c × Σ c × S c , and for s = (s 1 , . . . , s n ) ∈ S c and s = (s 1 , . . . , s n ) ∈ S c : (interact) s m --→ s ∈ T c if ∃i, j ∈ {1, . . . , n} where i j : m ∈ Σ ! i ∩ Σ ? j where ∃ s i m! ---→ s i ∈ T i , and s j m? ---→ s j ∈ T j such that ∀k ∈ {1, . . . , n}, k i ∧ k j ⇒ s k = s k (internal) s τ --→ s ∈ T c if ∃i ∈ {1, . . . , n}, ∃ s i τ --→ s i ∈ T i such that ∀k ∈ {1, . . . , n}, k i ⇒ s k = s k
These two steps are applied to all candidate compositions issued from the combine and filter step. Each composition respecting the above criterion is part of the resulting set of compatible compositions. Example. Going back to the running example and particularly to the result obtained in the previous step to compose objects temp. sensor, window (v2), and smartapp (Fig. 3), we first build the composition of those three objects. We assume the environment is empty in that case. Fig. 4 shows the resulting composition LTS where we can see that there are four possible interactions in a loop. Note that this loop exists because the window can alternatively be opened and closed in sequence. Moreover, there are two other interactions ('cold' and 'warm') corresponding to messages exchanged between the temperature sensor and the smart application. Therefore, as far as compatibility is concerned, when we compare the goal (half of it to be precise) with the composition LTS where we hide interactions 'cold' and 'close' (dashed transitions) that do not belong to the alphabet of the goal, these two LTSs are not bisimilar and the candidate composition is not a compatible composition.

Assume now a slightly different version of the temperature sensor where the model actually alternates between warm and cold messages as shown in Fig. 5 (left). When composing this temperature sensor with the connected window (v2) and the smart app given in Fig. 3, we obtain the composition LTS given in Fig. 5 (middle) where only four possible interactions in a loop are maintained. This LTS turns out to be bisimilar then compatible when focusing on the goal alphabet only. Check properties. After compatibility checking, we keep only compositions that satisfy the goal as explained beforehand. However, these compositions may not satisfy Fig. 5. Running example: (left) temperature sensor (v2) and (right) composition and compatibility additional properties. In this paper, we focus on properties that are independent of the application. Properties that depend on the application (e.g., a specific message never occurs after another one) can be specified using temporal logic and verified using model checking techniques [START_REF] Baier | Principles of Model Checking[END_REF] for instance. As far as independent properties are concerned, we present two examples of such properties in this paper, namely deadlock freeness and unmatched send messages.

In our context, a deadlock occurs when there is a (global) state in the composition LTS without outgoing transition and there is one object that could evolve independently from its (local) state because in its own model there is an outgoing transition. If we put it in another way, this object has a possible behaviour to move on in its model but this transition cannot be executed in the context of the composition. Definition 8. Given a set of object LTSs (S i , s 0 i , Σ i , T i ) and the corresponding composition LTS CLTS = (S c , s 0 c , Σ c , T c ), the composition is deadlocking if there is a global state s = (s 1 , . . . , s n ) ∈ S c such that s l --→ s ∈ T c but ∃ j ∈ {1, . . . , n}, s j ∈ S j and s j l --→ s j ∈ T j where l is either a send or receive message.

This notion of deadlock is quite strong, because we focus on global states without outgoing transitions. There is another similar case in which there is a global state with at least one outgoing transition, and there is one object with a local transition outgoing from that state labelled with a send message that does not appear in the composition LTS. This property allows one to detect unmatched send messages. Definition 9. Given a set of object LTSs (S i , s 0 i , Σ i , T i ) and the corresponding composition LTS CLTS = (S c , s 0 c , Σ c , T c ), there is unmatched send messages if ∃s = (s 1 , . . . , s n ) ∈ S c , such that ∃s l --→ s ∈ T c and ∃ j ∈ {1, . . . , n}, s j ∈ S j and s j m! ---→ s j ∈ T j and ∀s l --→ s ∈ T c , l m.

Example. For illustration purposes, let us focus on the part of the running example that aims at lighting up/down the room depending on the level of brightness. To do so, we present three objects in Fig. 6 (left) resulting in a compatible composition: the composition LTS (middle) and the goal (right) are bisimilar. The resulting composition (middle) is free of deadlocks, but is not free of unmatched send messages because in both global states in the composition, the brightness sensor can always send a 'bright!' message, which is not caught in the composition because there is no counterpart ('bright?') in Fig. 6. Running example: (left) objects, (middle) composition and (right) goal any other object. In such a situation, the user can either decide to move on because this is not a problem (can be amended, for example, by adding 'bright?' to the environment) or to choose another compatible composition satisfying this property.

Rank. In its current version, we rank satisfactory compositions according to their complexity. As complexity criterion, we consider the size of the composition LTS in terms of number of transitions. The composition ranked first corresponds to the solution that can satisfy the expected goal with the lowest number of interactions.

Implementation

We have developed the techniques presented in the former section using Maude's rewriting logic framework [START_REF] Clavel | All About Maude[END_REF]. We chose Maude for implementing the composition techniques because its declarative style facilitates program writing, and specifically, it is quite simple to implement filtering techniques, composition or compatibility analysis. Moreover, Maude is adequate to specify concurrent systems and is equipped with a large variety of analysis tools.

Maude is a high-level language and a high-performance system that supports membership equational logic, and rewriting logic specification and programming of systems. Rewriting logic [START_REF] Meseguer | Conditional Rewriting Logic as a Unified Model of Concurrency[END_REF] is a logic of change that can naturally deal with state and with highly nondeterministic concurrent computations. Rewriting logic is parameterised by an equational logic, and therefore, Maude integrates an equational style of functional programming with rewriting logic computation. In the Maude implementation of rewriting logic, the equational logic is membership equational logic [START_REF] Bouhoula | Specification and Proof in Membership Equational Logic[END_REF]. Membership equational logic is a Horn logic whose atomic sentences are equalities t = t and membership assertions of the form t : S , stating that a term t has sort S . Such a logic extends order-sorted equational logic, and supports sorts, subsort relations, subsort polymorphic overloading of operators, and the definition of partial functions with equationally defined domains. Further details may be found in [START_REF] Clavel | All About Maude[END_REF].

The Maude's implementation consists of different modules. Unfortunately, for the sake of space, we cannot present in detail the contents of these modules. The interested reader should look at the Maude specification, together with a set of examples, which is available online [START_REF] Durán | A Note on Automated Composition, Analysis and Deployment of IoT Applications[END_REF].

1 ----seeks a global state corresponding to a deadlock 2 op deadlock : LTS Set { Device } -> Bool .

3 ----checks whether there is a transition outgoing of that state 4 op deadState : State Set { Transition } -> Bool .

Listing 2. Equations for deadlock checking in the Maude implementation

A first module defines all necessary data types presented in Section 2 (object model, repository, goal, environment). Then, we have one module for each step of the approach presented in Section 3.1 and summarized in Fig. 2. Finally, we use a couple of additional modules for defining concrete objects grouped in a repository and several examples of goals for making experiments that we will present in Section 3.3.

Let us illustrate our Maude implementation with the verification of compositions. Listing 2 gives the equations used for identifying that a (global) state corresponds to a deadlock state. The deadlock operation takes as input the composition LTS and the set of device models. The first equation (line 6) applies when the composition LTS does not contain any state. The second equation is the most interesting. It says that if there is one global state (line 8) in the composition LTS corresponding to a deadlock state (line 11) that is a state without outgoing transition, and if there is one device with one possible transition from that local state (line 9), then this means that this behaviour cannot be executed in the context of this composition, and the equation returns true (line 10). The deadState operation (lines 14-20) takes a state and an LTS as input and checks whether from that state there is an outgoing transition. The first equation (lines 14-15) applies to simple devices. The second equation (line [START_REF] Js-Foundation | Node-RED: Flow-based Programming for the IoT[END_REF][START_REF] Klai | Checking Compatibility of Web Services Behaviorally[END_REF][START_REF] Marconi | Automated Composition of Web Services: the ASTRO Approach[END_REF][START_REF] Martens | Analyzing Web Service Based Business Processes[END_REF] applies to composition LTSs. Both equations correspond to the case in which there is such a transition and return false. The final equation (line 20) applies otherwise and returns true.

Experiments

The final part of this section presents some experiments we carried out to see how our approach scales with respect to the number of objects available in the repository and with respect to the size of the goal. The experiments were run on a macOS Mojave machine with a 2.8 GHz Intel Core i7 processor, 16GB of DDR3 RAM and 256GB PCIe-based flash storage. We recall that our approach targets small to medium-size applications, corresponding to a number of objects available in a smart home or building. 1. Experimental results (∼ 0 for values smaller than 0.1 sec.) Table 1 presents the results obtained for seven different goals. G2 corresponds to the goal of the running example given in Fig. 1. For the first four goals, we vary the size of the repository, that is, the number of objects available in the repository. More specifically, we use three repositories of different sizes (30 objects, 80 objects, and 150 objects). As for the three last goals (G5 to G7), we only use the largest one (150 objects). Table 1 then gives the number of possible combinations according to the list of family names given in the goal (combine), the number of compositions selected after application of the filtering techniques (filter), the number of compatible compositions satisfying the goal (compose and check compatibility), and the time it takes to compute all these steps. When a time is smaller than 0.1 sec., we use ∼ 0.

∼ 0 ∼ 0 ∼ 0 ∼ 0 G1 3 6 80 220 1 1 ∼ 0 ∼ 0 ∼ 0 ∼ 0 G1 3 6 150 5,544 13 12 ∼ 0 ∼ 0 ∼ 0 ∼ 0 G2 5 4 30 288 18 1 ∼ 0 ∼ 0 ∼ 0 ∼ 0 G2
∼ 0 ∼ 0 ∼ 0 ∼ 0 G3 5 8 80 119 0 0 ∼ 0 ∼ 0 ∼ 0 ∼ 0 G3 5 8 150 218 1 1 ∼ 0 ∼ 0 ∼ 0 ∼ 0 G4 8 10 30 336 0 0 ∼ 0 ∼ 0 ∼ 0 ∼ 0 G4 8
First of all, it is worth noting that for all these small and medium size (yet realistic) compositions, the results are computed in a reasonable time (about a total of four minutes for all the examples given in Table 1).

The increase in terms of computational time mainly comes from the number of possible combinations. It takes more time to compute and explore all possible combinations to see whether they are possible candidates (kept after filtering) and finally solutions wrt. the expected goal. The number of combinations augments for three reasons. The first factor is the number of objects in the repository. When looking at G2 in the table for instance, one can see that the number of combinations and the computation times increase when considering a repository with 30, 80 or 150 objects. The second factor is the number of objects involved in the composition. Goals G5, G6 and G7 show compositions involving 10, 15 and 20 objects. Here again, the number of objects induces a larger number of combinations and an increase in computation time. The third reason is not obvious because it concerns the number of objects in each family. If we look at goals G2 or G4 in the table with a repository of 150 objects, we can see that even for a limited number of objects (5 and 8), the number of combinations is rather high. This is because in both cases, the families of objects specified in the goal have many instances of objects in the repository (more than 10 concrete objects for each family), resulting in many combinations. In contrast, if the goal has many objects, but families with fewer instances, as it is the case for goal G5 for example, there are not so many combinations.

Once all combinations are computed, filtering is applied on all those combinations. Obviously, the more combinations, the costlier is filtering. This is why these two numbers (time for generating combinations and for applying filtering) are related and usually quite close. The final step computes the synchronous composition of all objects for each remaining combination and checks whether the resulting composition LTS matches the goal. This step is definitely the costliest. As an example, for G2 (150 objects), after filtering there still are 11,000 possible candidates, and it takes about 25 secs. to generate the compositions and analyse them, whereas it takes less than 10 secs. to generate all combinations (about 400,000) and apply filtering on them.

As a conclusion, it is worth noting the importance of the filtering techniques that can avoid the unnecessary and costly computation of some candidate compositions as well as their compatibility analysis. All the times given in the table are reasonable because the filtering techniques return a low number of candidate compositions.

Deployment

This section details the real-world deployment of IoT devices using an execution platform. We use the Mozilla Project Things as it is open-source and one of the feature-rich implementations of WoT. However, any standard IoT platform, such as OpenHAB or Home Assistant, can also be used for deployment. Specifically from our point interest, Things Gateway from Mozilla has a unified Web interface to monitor and control devices. It also provides REST APIs to create and deploy rules.

Given a set of available objects (repository) and a set of abstract rules (goal), after the application of the process presented in Section 3, we obtain a subset of these objects satisfying the rules. This section explains how this application can be deployed on the platform. Recall that the events and actions in the abstract rules are associated with the properties attribute of the Thing Description. Therefore, in order to deploy each abstract rule, we first map the events and actions of the abstract rules to its corresponding properties in the JSON Thing Description. An action or an event relates to a change in property values. Using this idea, we generate a rule in JSON format for each abstract rule. Further, we use the gateway API provided by the platform, which takes a JSON rule as input, to deploy each newly created rule.

Example. We have deployed our running example using the following devices: Philips Hue Play Light, Philips Motion Sensor which has a built-in ambient light sensor and a temperature sensor. As our device repository did not have smart window, we created virtual Things adapters to emulate the smart window. We use the TemperatureProperty of the Philips Hue temperature sensor as shown in Fig. 1 to build the concrete rule "IF warm THEN open". The deployable rule is shown in Listing 3, where we notice that warm translates to temperature greater than 20 degrees Celsius (value attribute set to { " enabled " : true , " trigger " : { " type " : " MultiTrigger " , " op " : " AND " , " triggers " : [ { " type " : " LevelTrigger " , " label " : " Temperature " , " property " : { " type " : " number " , " thing " : " hue-2 " , " id " : " temperature " , " unit " : " degree celsius " } , " value " : 2 0 , " levelType " : " GREATER " } ] } , " effect " : { " type " : " MultiEffect " , " effects " : [ { " type " : " SetEffect " , " label " : " On / Off " " property " : { " type " : " boolean " , " thing " : " virtual-env-1 " , " id " : " on " } , " value " : true } ] } } Listing 3. WoT rule JSON corresponding to abstract rule IF warm THEN open 20). Users can configure such or keywords to make the rules closer to the natural language. The action in the rule is described in the effect attribute, where a boolean property is set to on in the virtual environment thing.

Related Work

We discuss in this section some relate work on automated composition of Web services, compatibility of behavioural models, and (automated) composition of IoT objects. Automated composition was mainly studied in the Web services area. Several papers have been published on that problem, see, e.g., [START_REF] Narayanan | Simulation, Verification and Automated Composition of Web Services[END_REF][START_REF] Berardi | Automatic Composition of E-services That Export Their Behavior[END_REF][START_REF] Marconi | Automated Composition of Web Services: the ASTRO Approach[END_REF][START_REF] Bertoli | Automated Composition of Web Services via Planning in Asynchronous Domains[END_REF]. Most of these techniques rely on Web service languages, namely WSDL and BPEL, whereas we preferred to rely on generic behavioural models to make our solution more easily reusable in other application areas. These papers make use of existing planning techniques and tools. We preferred a different solution since we choose rule-based programming and rewriting logic for computing the resulting compositions. Our approach also provides (automated) verification techniques to check for compatibility and other properties of interest.

As far as compatibility checking is concerned, several works have focused on this problem assuming that entities are described using behavioural models, see, e.g. [START_REF] Brand | On Communicating Finite-State Machines[END_REF][START_REF] Yellin | Protocol Specifications and Component Adaptors[END_REF][START_REF] Canal | Compatibility and Inheritance in Software Architectures[END_REF][START_REF] Martens | Analyzing Web Service Based Business Processes[END_REF][START_REF] Attiogbé | Checking Component Composability[END_REF][START_REF] Durán | A Generic Framework for N-protocol Compatibility Checking[END_REF][START_REF] Klai | Checking Compatibility of Web Services Behaviorally[END_REF]. [START_REF] Canal | Compatibility and Inheritance in Software Architectures[END_REF] proposes the π-calculus as modelling language and defines a compatibility relation taking inspiration into Milner's bisimulation notion. [START_REF] Martens | Analyzing Web Service Based Business Processes[END_REF] presents a framework for modelling Web service with Petri nets and for analysing several properties on these models, the most important being the usability property, which is verified using the soundness criterion for workflow modules. In [START_REF] Attiogbé | Checking Component Composability[END_REF], the authors address the composability of components. They assume that two software components are composable if their respective services are pairwise compatible, where service compatibility is understood as deadlock-freeness. [START_REF] Klai | Checking Compatibility of Web Services Behaviorally[END_REF] proposes an approach based on Symbolic Observation Graphs (SOG) allowing one to decide whether two services can cooperate safely. The compatibility between two services is defined by the well-known soundness property on open workflow nets. Our approach proposes a notion of goal-based compatibility for IoT applications obtained by composition of available devices and its verification using rewriting logic and Maude's framework.

We finally introduce recent results and tools for the composition and configuration of IoT applications. From an industrial perspective, Node-RED [START_REF] Js-Foundation | Node-RED: Flow-based Programming for the IoT[END_REF] and IFTTT [START_REF] Ovadia | Automate the Internet with "If This Then That[END_REF] are two tools that provide graphical support for visually and manually building applications consisting of connected objects. We chose full automation and synthesis of the object composition in our approach. [START_REF] Felfernig | ASP-based Knowledge Representations for IoT Configuration Scenarios[END_REF] shows how to use Answer Set Programming (ASP) techniques to represent configuration scenarios for basic applications in the IoT. [START_REF] Alkhabbas | Enacting Emergent Configurations in the IoT Through Domain Objects[END_REF] proposes an approach that makes a set of things connect and cooperate temporarily to achieve a user goal. [START_REF] Tata | Formal Model and Method to Decompose Process-Aware IoT Applications[END_REF] presents a formal approach for the decomposition of process-aware applications to be deployed in IoT environments. These applications are modelled using Petri nets and correctness of the decomposition is proved with respect to language preservation. In [START_REF] Bucchiarone | A Context-aware Framework for Dynamic Composition of Process Fragments in the Internet of Services[END_REF], the authors present a solution to the dynamic composition of services. To do so, they rely on stateful models of services, contextual information, a goal description and planning techniques in order to generate automatically a resulting composition of services. Similarly to [START_REF] Tata | Formal Model and Method to Decompose Process-Aware IoT Applications[END_REF][START_REF] Bucchiarone | A Context-aware Framework for Dynamic Composition of Process Fragments in the Internet of Services[END_REF], we rely on behavioural models of objects with a specific focus here on the automated composition of objects. We provide additional techniques for facing the large number of solutions (filtering and ranking) as well as automated verification techniques for ensuring compatibility and additional properties. Last but not least, we also support the deployment of concrete applications.

Concluding Remarks

We have presented some automated techniques for generating and deploying satisfactory compositions given an abstract goal of the composition-to-be and a set of object families. Our approach works applying successively different steps. First, from a repository of available objects, we generate a set of candidate compositions statically filtering those that cannot satisfy the goal. Then, we check if these candidates satisfy the given goal and are therefore compatible compositions. The user can also decide to verify additional properties that are independent of the application such as deadlock freeness or the absence of unmatched send messages. If there is more than one solution, we rank them according to some complexity criterion. Finally, the resulting composition is deployed using an existing execution engine. The composition and analysis process are supported by an implementation in Maude. The deployment process is carried out using Mozilla's Project Things platform. We applied the whole approach on several case studies for validation purposes.

The first perspective of this work is to consider location of objects in the object model and composition goal. We believe that this information would allow us to make our approach scalable in order to target larger applications (at the level of a campus or a city for example). More precisely, this information would be used during the composition process for improving our filtering techniques and for finding the best combinations without exhaustively producing and analysing all of them. Considering asynchronous communication (communication via message buffers or publish-subscribe) is another perspective of this work.

Fig. 1 .

 1 Fig. 1. Running example: goal

Fig. 4 .

 4 Fig. 4. Running example: composition and compatibility

5 6 9 ( 10 = true 11 i

 591011 eq deadlock ( model ( St , empty , empty ) , Devices ) = true . 7 ceq deadlock ( 8 model ( St , ( s ( ( DId | -> St1 , ISM ) ) , States ) , Transitions ) , dev ( DId , model ( St2 , States1 , ( ( St1 -I -> St3 ) , Transitions1 ) ) ) , Devices ) ) f deadState ( s ( ( DId | -> St1 , ISM ) ) , Transitions ) . 12 eq deadlock ( Mod , Devices ) = false [ owise ] .

13 14 18 (

 1318 eq deadState ( St , ( St -I -> St1 , Transitions ) ) 15 = false . 16 eq deadState ( 17 s ( ( DId | -> St , ISM ) ) , s ( ( DId | -> St , ISM ) ) -Str -> s ( ( DId | -> St1 , ISM1 ) ) , Transitions ) ) 19 = false . 20 eq deadState ( St , Transitions ) = true [ owise ] .

  3. Running example: filtering techniquesExample. Let us illustrate filtering techniques on the running example, and more particularly on the bottom half of the goal given in Fig.1, which focuses on temperature and windows. In this part of the goal, we need one temperature sensor, one window and one smart app. The smart app acts like an orchestrator and is usually defined by end-users or reused from existing applications proposing common scenarios for them. The smart app may provide many functionalities, but we focus on those of interest with respect to the current goal. Fig.3gives four possible objects that match the required family names. Consider successively the two following combinations (temp. sensor, window

(v1), smartapp) and (temp. sensor, window (v2), smartapp). The first composition is discarded by our filtering techniques, because there is one interaction appearing in the goal ('open') that is not possible in the composition (missing 'open?' message). The second composition is preserved by our filtering techniques because both 'warm' and 'open' interactions are possible.

Project Things by Mozilla: https://iot.mozilla.org/wot/.

https : / / iot . mozilla . org / schemas


Francisco Durán

Camilo Rocha

Gwen Salaün

Analysis of Resource Allocation of BPMN Processes

come   L'archive ouverte pluridisciplinaire

Introduction

This work presents first steps towards the development of a formal and automatic approach to resource allocation analysis for business process models. The approach comprises a formal yet executable specification in rewriting logic [START_REF] Meseguer | Conditional Rewriting Logic as a Unified Model of Concurrency[END_REF], a logic of concurrent computation, of a significant and expressive subset of the Business Process Model and Notation (BPMN) extended with time features and resources. By being executable in the Maude system [START_REF] Clavel | All About Maude[END_REF], the specification supports the concurrent simulation of a process with different types of resources and with multiple replicas for any given workload. The analysis techniques for resource allocation use Maude's rewriting tools for evaluating expected values in the executable model -such as charge, occupancy, and usage percentage -by mechanically generating automatic simulations. The output of the automatic analysis can then be used to quantitatively assess the efficiency of the business process model, and thus guide a re-design or re-allocation of resources.

The overall idea is that multiple concurrent executions of a process compete for shared resources. Models are analyzed by observing how the resources' usage evolve over time when varying the workload and the number of available resources. This is done without an implementation of the system running on real resources: the input to the automatic analysis task is a BPMN model of the process workflow, enriched with a description of its timing behavior and resource availability. The BPMN models are described by means of activity and collaboration diagrams, four types of gateways (namely, inclusive, exclusive, parallel, and event-based), loops, unbalanced processes, event handling, and message-passing. The timing aspects of the models are specified by associating durations to each flow and task in the workflow, which can be sampled F. Durán was partly funded by projects PGC2018-094905-B-I00 (Spanish MINECO/FEDER) and UMA18-FEDERJA-180 (J. Andalucía/FEDER), and by U. Málaga, Andalucía Tech. C. Rocha was partly supported by Colciencias-EcosNord project "FACTS: Foundational Approach to Cognition for Today's Systems" (63561). from a probability distribution function. Resource usage is specified by providing the amount of resources available and the resources required for the execution of tasks.

The usefulness of the approach is illustrated with an experiment, which supports the claim that such an analysis can help in detecting resource usage problems, thus ultimately leading to the improvement of the business process by optimizing its resource allocation. In particular, the experiment presented in this paper identifies low-level occupancy of resources and undesirable patterns of resource usage. They encompass sequential dependencies and bottlenecks provoked by some highly used resources that may induce performance fall-downs.

Business Process Model and Notation

Figure 1 presents a process describing a parcel ordering and delivery by drones. This BPMN process is presented as a collaboration diagram consisting of two pools, one for the client and another one for the order management and the delivery process; they are represented as lanes. This process includes different kinds of gateways, probabilities for choice gateways, stochastic functions for time associated to tasks, a loop, and unbalanced structures.

As usual, start and end events are used, respectively, to initialize and terminate processes. A task represents an atomic activity that has exactly one incoming and one outgoing flow. A task may have a duration (expressed as a stochastic expression) and may produce an event message. A sequence flow describes two nodes executed one after the other, i.e., by imposing an execution order with possible delays.

The timing information associated to tasks and flows (durations or delays) is described either as a literal value or sampled from a probability distribution function. Gateways (exclusive, inclusive, parallel, and event-based) are used to control the divergence and convergence of the execution flow. Gateways with one incoming (resp., outgoing) branch and multiple outgoing (resp., incoming) branches are called splits (resp., merges). Event-based split gateways may have a default branch fired by a timeout. Workflows with looping behavior are supported, as well as unbalanced workflows.

Data-based conditions for split gateways are modeled using probabilities associated to outgoing flows of exclusive and inclusive split gateways. For instance, notice the exclusive split after the Search products task in the Client lane of the running example, which has outgoing branches with probabilities 0.6, 0.2, and 0.2, specifying the likelihood of following each corresponding path.

Instead of implicitly associating resources to lanes, resources are explicitly defined at the task level, which is more general. A task that requires resources can include, as part of its specification, the number of required instances (or replicas) of a resource. The process in Figure 1 relies on employees for parcel packing and drones for parcel delivery. Notice the colored circles at the bottom-right corner of the Prepare parcel and Deliver parcel tasks, indicating that one instance of the employee resource and another one of the drone resource are required, respectively, for the tasks completion. Several tasks could compete for the same resources (not the case in this example). Furthermore, since multiple instances of a process may be executed concurrently, all instances also access and compete for the shared resources. At the bottom-right corner of Figure 1, a total of two employees and three drones are specified as the available resources.

Resource Allocation Analysis

This section illustrates how resource allocation analysis can be performed with the proposed approach using the running example. Given a process description, a specification of resources, and a workload, the experiments illustrate how information on execution times and resource usage is collected. This information is used to find the optimal allocation of resources that minimizes costs and execution times relative to an optimization goal. The interested reader is referred to [START_REF] Durán | A Note on Resource Allocation Analysis of BPMN Processes[END_REF] for further details on the experiments.

The BPMN subset encoded in Maude is quite expressive and several kinds of properties can be computed, including timing and resource-based ones. These properties are meaningful when executing multiple instances of a process that compete for the shared resources. As for timing properties, the approach presented in this paper allows the computation of average execution times (AET) of a process, its variance (Var), and the average synchronization time (AST) for merge gateways, representing the time elapse from the arrival of the first token through one of its incoming flows to its activation. Synchronization times make sense only for parallel and BPMN 1.0 inclusive gateways, since there is no waiting / synchronization time for the other gateways.

The following resource-based properties are computed: -The global time usage of all replicas of each resource R (GTU R ).

-The average GTU of resource R (GTU 1 R ). -The average usage percentage for a resource R (UP 1 R ). To quantify these properties, Maude rewriting capabilities are used in order to simulate and extract analysis results on a given BPMN process.

Table 1 summarizes experimental results on execution times and resource usage on the parcel order and delivery example (Figure 1). They were carried out on an iMac with 3,2GHz Intel Core i5 and 8GB. All simulations were performed assuming a given workload with a number of instances (1st column) and an exponentially distributed interarrival time (λ = 4). Columns 2-6 contain, resp., the average execution time (AET), its variance (Var), the average synchronization time for the parallel merge at the end of the delivery process lane (AST g8 ), the average synchronization time for the end events (AST ee ), and the total time to complete the execution of all instances. The next six columns show results on resource usage for employees and drones. The final column gives the overall time needed to complete the analysis. All times are logical units, except the ones in the last column that are given in seconds. Other information, such as the duration of each task and the synchronization time of merge gateways, is also collected. These experiments consist of 100, 200, 400, 800, and 1600 instances for 2 employees and 3 drones. Note that the average execution and synchronization times, as their variance, clearly increase with the number of instances. This is because the more tokens compete for resources, the more time it takes to execute the process and for the tokens to reach the synchronization points. Note the relationship between AET and AST ee times, showing an unbalance between the two lanes: the client lane terminates earlier than the other lane, which exhibits a bottleneck because of the demand on the resources.

The GTU increases with the number of executed instances. These times are particularly interesting because they can be materialized as costs (e.g., cost of a resource, salary of an employee/all employees). In relation with usage percentage (UP), the results indicate that the employees are "underused" since they work around 40% of the time, in contrast to the drones that are constantly busy and used about 90% of the time for delivering parcels. This may suggest an inappropriate allocation of resources. It is worth observing that, although the number of instances clearly affects all computed times, the results for resource usage (UP) are quite stable and a small number of instances is enough for obtaining a good approximation of these percentages.

Resource allocation impacts execution times (AET) and resource usage (UP) of a process. Figure 2 focuses on average execution time and depicts the results when the number of employees and drones vary for a fixed number of executions (400). The objective here is to reduce the average execution time for completing the process: the quicker the parcel is delivered, the more satisfied the client is. It can be observed that, independently of the number of employees, execution times are not satisfactory with 1 or 2 drones (between 400 and 800 time units). The time becomes reasonable for more than 3 drones (less than 300 time units) and tends to stabilize. It is also worth noting that, given its low usage rate, the number of employees does not impact significantly the execution time. For more than six drones, only going from one to two employees makes a significant impact in the AET values. Figure 3 gives a different point of view of resource usage by concentrating on each resource replica. Figure 3 (left) shows that employees are close to 100% usage only if there is 1 or 2 instances of that resource and at least 4 or 8 drones, respectively. If the number of employees increases, the usage percentage quickly drops, reaching a low level (e.g., 14% for 4 employees and 2 drones). This percentage slightly increases with the number of drone replicas (e.g., 34% for 4 employees and 5 drones), but remains low (around 30%). Figure 3 (right) shows that the drone usage is always quite high whatever the number of employees is. With only 1 or 2 drones, the usage percentage is almost at 100% and slightly decreases with 4 drones. When there are 6 drones and 1 employee, the percentage is still about 60%. Another interesting fact is that the number of employees barely impacts the drone usage percentage. For example, with 4 drones, the usage percentage is around 90% for any number of employees.

Fig. 1 .

 1 Fig. 1. Running example: parcel delivery by drones.

Fig. 2 .

 2 Fig. 2. Average execution time (400 instances)

Fig. 3 .

 3 Fig. 3. Average percentage usage per employee (left) and drone (right) (400 instances)

Table 1 .

 1 Experimental results for the running example (2 employees, 3 drones)

	Num. AET Var AST g8 AST ee inst.	Total time GTU e GTU 1 e UP 1 Resources e GTU d GTU 1 d UP 1 d	Anal. time
	100 106 72	58	58	326 271	135	41 853	284	87	5s
	200 185 134 71	139 670 514	257	38 1892 630	94 26s
	400 284 173 98	237 1132 994	497	43 3270 1089 96 189s
	800 506 294 145	459 2217 1867 933.6 42 6525 2171 98 1233s
	1600 891 473 240	844 4187 3714 1857 44 12428 4142 98 7909s