Ajay Krishna

Michel Le Pallec

Radu Mateescu

Ludovic Noirie

Gwen Salaün

Rigorous Design and Deployment of IoT Applications

Keywords: IoT, behavioural modelling, composition, formal verification, deployment

Internet connected devices are becoming increasingly common in consumer homes. These devices combined with software entities are used to build Internet of Things (IoT) applications. As democratization of IoT takes shape, developing reliable IoT applications remains a challenge for consumers because these applications exhibit characteristics such as distribution, dynamicity, and heterogeneity, which make their design, development and maintenance difficult. In this paper, we use formal methods to ensure correct composition of objects and propose a reliable deployment mechanism in the context of an IoT application. Objects are modelled using an interface description model integrating a behavioural specification of the object functionality. We provide formal validation techniques for verifying that the composition is correct. A deployment plan is generated for automating the instantiation of all objects involved in a valid composition. All the proposals have been implemented as a prototype tool and experiments were carried out for evaluating the tool performance and usability.

I. INTRODUCTION

The Internet of Things (IoT) aims at sensing and altering our surrounding environment through connected devices to improve everyday life. Nowadays, the IoT specific hardware, especially to collect the information, are already in place, but there is still room for improvement regarding support on building of IoT applications, which are supposed to empower interconnected objects in order to build powerful and addedvalue services. Designing, developing, and maintaining IoT applications are difficult tasks, because such applications are highly distributed, data-centric, dynamic, and heterogeneous. First, IoT applications induce a high level of concurrency, distribution, and collaboration. Designing concurrent applications is a tedious and error-prone task, in particular because software is more and more complex. Complexity is intrinsic to IoT scenarios where we can imagine in a short-term future thousands of interconnected objects [START_REF] Sanchez | SmartSantander: IoT experimentation over a smart city testbed[END_REF]. Further, modern systems are no longer designed and implemented once-for-all, they can evolve over time. Last, there are multiple standards for communication protocols and technologies. Therefore, IoT applications have to deal with heterogeneous IoT hardware and communication layers.

The focus in this paper is on IoT object composition in order to build an application relying on objects and to provide a composite service of value for smart home users. Composition of objects is however a difficult task for several reasons. First of all, composition relies on models of the devices to be composed. Several levels of expressiveness can be considered [START_REF] Beugnard | Making components contract aware[END_REF] (signature, behaviour, semantics, quality of service) and each facet brings different issues from a composition perspective. Once a model of objects is properly defined, one can design a composition by specifying connections or bindings among the involved objects. Yet, building such a composition is error-prone because the objects might not have been connected correctly by the developer. Depending on the object description model, several kinds of mismatch can arise. So there is a need for analysis techniques in order to validate the composition and ensure that before the composition is deployed it works correctly. Lastly, tool support should be available in order to help the end-user during the composition and deployment tasks and make them as automated as possible.

In this paper, we propose various techniques to support the composition and deployment of objects in the context of an IoT application (Figure 1). The description model we consider for objects integrates the signature and behaviour levels. Our approach aims at supporting the IoT object composition via a user-friendly web application which helps the end-user to choose and connect the objects. The composition solution also provides validation techniques for verifying its correctness. Finally, a deployment plan is generated, which guides the automated instantiation of all objects involved in the composition in a certain order.

More precisely, the model consists of a set of signatures (interfaces) and a behavioural model (Labelled Transition System) giving the order in which these interfaces must be called. Given the models of a set of objects, the end-user can define how these objects are supposed to interact with one another. Once these bindings are defined, we propose automated analysis techniques in order to check whether the composition under construction satisfies some properties of interest, called compatibility notions in the rest of this paper.

As an example, we can check that every binding can be executed, meaning that a pair of objects which are bound through given application interfaces can execute its complete behaviour, i.e., none of the objects lose any of its capabilities. Those checks are achieved using process algebra [START_REF] Champelovier | Reference Manual of the LNT to LOTOS Translator (Version 6[END_REF] encodings and equivalence checking techniques [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF]. If the execution is not satisfied, this results in an erroneous composition. When the composition is valid, a deployment plan is generated and can be run to effectively interface and execute these objects. The plan is applied in a certain order to respect the dependency graph inherent to the composition model. The underlying idea is that if an object O 1 depends on an object O 2 , we start first O 2 and then O 1 . We implemented a web application for simplifying the use of our approach and we applied it successfully to several real-world applications.

To summarize, these are the main contributions of this paper: i) a formal model for objects and their composition. ii) compatibility notion and encoding into process algebra for automating these checks. iii) deployment plan generation and execution for running composition of objects. iv) tool support for helping the end-user during the composition and deployment steps. v) application to real-world use-cases in smart homes for validation purposes.

The organization of this paper is as follows. Section II introduces the model of objects and composition we rely on in this paper. Section III defines compatibility notions and how we check them in this work. Section IV focuses on deployment plan and its execution. In Section V, we describe our tool support and experiments. Section VI overviews related work and Section VII concludes the paper.

II. MODELS

In this section, we present a model for IoT objects, and use it to define a composite IoT service. This model provides a formal basis for reasoning about the behaviour of IoT objects, by allowing one to describe the behaviour of IoT objects in an abstract way, independent from implementation details, and to represent only the features necessary for correct object composition and deployment.

A. IoT Object

The behaviour of an IoT object is modelled as a Labelled Transition System (LTS), i.e., a state-transition graph representing the states of the object and its interactions with the environment.

Definition 1 (Labelled Transition System): An LTS is a tuple S, A, T, s 0 , where S is a set of states, A is a set of actions (labels) associated to transitions, T ⊆ S × A × S is the transition relation, and s 0 ∈ S is the initial state. A transition (s 1 , a, s 2 ) ∈ T (also noted s 1 a → s 2 ) indicates that the system can move from state s 1 to state s 2 by performing action a. The set A includes the internal action τ , which denotes unobservable behaviour.

An IoT object (also referred to as object or device in the sequel) contains physical, network, and application interfaces, which are used to physically connect the object (to a network or to its environment), to provide network access to the object, and to define its behaviour, respectively. When the object is connected to a network, we refer to it as a Connected Object (CO). Given the application context, we focus here on application interfaces. However, if we are to extend the model with information pertaining to physical interfaces, a more detailed model like the one in [START_REF] Pallec | Physical-interface-based IoT service characterization[END_REF] can be integrated with the proposed model. Definition 2 (IoT Object): An IoT object O = I in , I out , LTS consists of a set of input (application) interfaces I in , a set of output (application) interfaces I out , and an LTS S, A, T, s 0 describing the object behaviour, where

A ⊆ I in ∪ I out ∪ {τ }.
We assume in our approach that each object comes with an object model. These models 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].

B. Object Composition

Composition aims at connecting various objects through their application interfaces, resulting in a composite service. The objects involved in a composition interact with each other through bindings in a binary synchronous manner. Definition 3 (Binding): Given two objects O 1 and O 2 , a binding is an ordered pair β = (i O1 out , i O2 in ) specifying the connection between the output interface i O1 out of O 1 and the

input interface i O2 in of O 2 . For a binding β = (i O1 out , i O2 in ), we note in(β) = i O2
in and out(β) = i O1 out . From the composition perspective, we distinguish between strong and weak bindings. In our setting, strong bindings are functionally mandatory connections, without which a correct service cannot be achieved by the composition. On the other hand, weak bindings are optional for a correct functioning, but provide additional features to the composite service. Some auxiliary notation is needed before defining composition. An action renaming ρ = [b 1 /a 1 , ..., b n /a n ] is a partial function that maps each action a i to another action b i for 1 ≤ i ≤ n, i.e., ρ(a) is equal to b i if a = a i and is equal to a otherwise. The renaming induced by a set of bindings B = {β 1 , ..., β m }, which maps the input and output interfaces of each binding β i to the name β i , is defined as

ρ B = [β 1 /in(β 1 ), β 1 /out(β 1 ), ..., β m /in(β m ), β m /out(β m )].
For simplicity, we denote by β the name of a binding β. The notations in and out are extended to sets of bindings: in(B) = {in(β 1 ), ..., in(β m )} and out(B) = {out(β 1 ), ..., out(β m )}. The renaming of an LTS by ρ is defined as ren ρ ( S, A, T, s 0 ) = S, {ρ(a) | a ∈ A}, {s

ρ(a) → s | s a → s ∈ T }, s 0 . The parallel composition of LTS 1 = S 1 , A 1 , T 1 , s 01 and LTS 2 = S 2 , A 2 , T 2 , s 02 with synchronization on a set of actions A ⊆ A 1 ∪ A 2 is written as LTS 1 ⊗ A LTS 2 . This parallel composition is itself an LTS S = S 1 × S 2 , A = A 1 ∪ A 2 , T ⊆ S × A × S, s 0 = (s 01 , s 02 ) ,
where the transitions in T are defined as follows:

(i) (s 1 , s 2 ) a → (s 1 , s 2 ) if a ∈ A and s 1 a → s 1 ∈ T 1 ; (ii) (s 1 , s 2 ) a → (s 1 , s 2 ) if a ∈ A and s 2 a → s 2 ∈ T 2 ; (iii) (s 1 , s 2 ) a → (s 1 , s 2 ) if a ∈ A and s 1 a → s 1 ∈ T 1 and s 2 a → s 2 ∈ T 2 .
This LTS, called the synchronous product between LTS 1 and LTS 2 , can be constructed starting at the initial state s 0 = (s 01 , s 02 ) and exploring the transitions according to the three rules above.

Definition 4 (Composition

): A composition is a tuple C = B, Σ, I U in , I U out , LTS , W , where B = {β 1 , ..., β m } is a set of bindings, Σ = {O 1 , ..., O n } is a set of objects, I U in = (I in 1 ∪ ...∪I in n )\in(B) is the set of unbound input interfaces, I U out = (I out 1 ∪ ... ∪ I out n ) \ out(B) is the set of unbound output interfaces, LTS = ren ρ B (LTS 1 ) ⊗ B ... ⊗ B ren ρ B (LTS n ) is
the LTS of the composition, and W ⊆ B is the set of weak bindings.

The composition takes into account the future extensions to the service. It is an open-ended system, wherein every interface in an object O i is not expected to be bound to another object O j . The unbound (without active binding) input and output interfaces I U in and I U out can be used to bind other objects when the service is extended. This is typically the case in IoT service scenarios, where all features of an IoT device are not used in a given scenario. In certain cases, unbound input interfaces can interact with the real-world environment. Environment can be a human, a physical object or an event in the real world. We can define these interactions by modelling the behaviour of the environment as a specific object and establish bindings between the environment model and other objects in the composition. In other words, these environment bindings close the open-ended composition. Further, a composition C = B, Σ, I U in , I U out , LTS , W can be seen itself as an IoT object C = I U in , I U out , hide B (LTS ) , where hide B (LTS ) = ren [τ /β1,...,τ /βm] (LTS ) is the hiding of actions B in the LTS. This enables a hierarchical composition of services from individual devices and existing composite services.

Example 1: Consider an IoT composition scenario involving three objects, namely a smartphone app, a media device and an external speaker, illustrated in Figure 2 (input and output interfaces are represented by donuts and triangles, respectively). The smartphone app can connect to the media device and view the videos available on the phone screen. The media device can also be connected to an external speaker. These objects are modelled as follows:

Smartphone= {P VIDEO}, {P ON}, LTS Smartphone MediaDevice= {M ON, M AUX}, {M VIDEO, M AUDIO}, LTS Media Speaker = {S AUDIO}, ∅, LTS Speaker
The connections between objects are modelled by the bindings ON = (P ON, M ON), VIDEO = (M VIDEO, P VIDEO), and AUDIO = (M AUDIO, S AUDIO). The composition is defined as

C = {ON, VIDEO, AUDIO}, {Smartphone, MediaDevice, Speaker }, {M AUX}, ∅, LTS , {VIDEO}
The LTSs of individual objects are shown in Figure 2 (for the sake of simplicity, we have avoided loops in the behaviour), and the LTS of the overall composition is shown in Figure 3 (left). Notice that even though the media device provides an interface to add an auxiliary input, the composition does not support the operation. So, the interface M AUX is unbound in the given composition, i.e., I U in = {M AUX}.

III. COMPATIBILITY

In Section II, we modelled a composition formally, here we investigate how to ensure its correctness from an interaction perspective. We first propose a notion of compatibility assessing that the bindings present in a composition do not alter the behaviour of the objects in the given setting. Then, we show how this compatibility is checked via an encoding into process algebra and an analysis based on equivalence checking.

A. Compatibility Notion

Intuitively, a composition involving a set of objects and a set of bindings is correct if all bindings can effectively be executed and if all reachable actions unbound in the composition do not prevent the bindings to be executed. We define this notion of compatibility using classic concurrency concepts introduced in Section II: parallel composition of LTSs with synchronization on a set of actions A (LTS 1 ⊗ A LTS 2 ), hiding of a set of actions A in an LTS (hide A (LTS )), and branching equivalence [START_REF] Van Glabbeek | Branching Time and Abstraction in Bisimulation Semantics[END_REF] of two LTSs (≡ br ).

Definition

(Compatibility):

Let C = B, Σ, I U in , I U out , LTS , W be a composition involving a set of objects Σ = {O 1 , ..., O n } with LT S i = S i , A i , T i , s 0i for 1 ≤ i ≤ n. The composition C is correct with respect to compatibility iff: hide I U in ∪I U out (LTS ) ≡ br LTS ⊗ A chaos B where A = A 1 ∪...∪A n and chaos B = {s}, B, {s β → s | β ∈ B},
s is the LTS consisting of a single state and having, for each binding, one self-loop transition labelled by the identifier of that binding. Definition 5 expresses that, when put in an environment that blocks the execution of the unbound interfaces (right hand side of the equivalence), the composition still behaves as defined by the LTSs of the objects and the bindings, with the unbound interfaces made unobservable (left hand side of the equivalence). Similar compatibility notions between behavioural interfaces were defined in the services domain [START_REF] Ouederni | Comparator: A tool for quantifying behavioural compatibility[END_REF].

Example 2: Consider again the composition described in Example 1 and Figure 2, which involves a phone, a media device, and an external speaker. Although the bindings are valid from an interface point of view, the overall composition is not able to provide the desired service. Indeed, as defined by its LTS, the media device requires an auxiliary input on interface M AUX for an audio M AUDIO to be sent out. Since interface M AUX is not bound in the composition (i.e., I U in = {M AUX}), the environment may prevent it to occur, which in turn will make the action M AUDIO (bound by AUDIO) unreachable. This is captured by the compatibility check, as illustrated in Figure 3. In the broad sense, incompatible object compositions result in missing features in an IoT application. According to Definition 4, the LTS of the composition (leftmost in Fig. 3) synchronises on the bindings ON, AU-DIO, and VIDEO, whereas M AUX would evolve as an independent transition. Composing the LTS in parallel with chaos {ON,AUDIO,VIDEO} with synchronization on all actions {ON, AUDIO, VIDEO, M AUX} would eliminate the right branch of the LTS, resulting in the sequential system shown in Figure 3. This is clearly not branching equivalent to hide {M AUX} (LT S) (rightmost in Fig. 3), because the latter system can silently perform the τ -step, followed by action AUDIO.

This notion of compatibility ensures that the LTSs hide I U in ∪I U out (LTS ) and LTS ⊗ A chaos B have the same observational behaviour. However, it does not guarantee that this behaviour indeed corresponds to the desired service implemented by the composition. The intended behaviour can be ensured by verifying relevant functional properties (e.g., absence of deadlocks and livelocks, safety, liveness, fairness, etc.) on either LTS using, e.g., temporal logic and model checking techniques.

B. Analysis

The compatibility check is achieved using an encoding into process algebra. This allows us to rely on existing verification tools for process algebra and avoids developing new ad-hoc tools for automating this check. More precisely, we use here the LNT process algebraic language [START_REF] Champelovier | Reference Manual of the LNT to LOTOS Translator (Version 6[END_REF], [START_REF] Garavel | From LOTOS to LNT[END_REF] and the CADP toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF], which accepts LNT as main specification language and supports different kinds of verification, such as model and equivalence checking.

LNT allows the definition of data types, functions, and processes. LNT processes are built from actions, choices (select), parallel composition (par), action hiding (hide), looping behaviours (loop), and sequential composition (;).

The communication between parallel processes takes place by rendezvous on a set of synchronized actions specified in the parallel composition. To carry out the compatibility check, we need to generate several LTSs as specified in Definition 5. We first encode each object LTS in LNT by associating an LNT process to each state of the LTS. The process body consists of a choice (select) specifying all transitions going out of that state, each one being followed by a call to the process associated to its target state, as shown in Listing 1 for the Media LTS. Then, the overall LTS of the composition is obtained by putting all object processes in parallel and synchronizing them on all binding names, as illustrated in Listing 2. Next, chaos B is encoded as an LNT process consisting of a cycle (loop) that chooses at each step (select) one of the binding names in B. Finally, the two processes hide I U in ∪I U out (LTS ) and LTS ⊗ A chaos B are encoded in LNT using the hiding operator (hide) and the parallel composition with synchronization on all actions, respectively. We generate the LTSs hide I U in ∪I U out (LTS ) and LTS ⊗ A chaos B by invoking the CADP compilers on the corresponding LNT processes, and we apply the CADP equivalence checker to compare these LTSs modulo branching equivalence. The LTS generation and comparison steps are automated using SVL scripts [START_REF] Garavel | SVL: A scripting language for compositional verification[END_REF].

IV. DEPLOYMENT

This section describes the deployment of applications. The modelling and verification techniques proposed in the previous sections ensure that the object composition provides a correct IoT service. Further, we propose to generate a deployment plan based on the bindings. The plan aims at orchestrating the IoT service deployment which involves the control and configuration of objects and network layer.

By binding objects in a composition, we create dependencies among the objects. These dependencies must be taken into account during deployment in order to fulfil the service level agreements such as order of execution, availability, etc. A composition can be represented naturally as a directed graph, whose nodes are objects and whose directed edges are the bindings between objects. Using this directed graph, the dependency chain can be deduced using inverse topological sorting [START_REF] Tarjan | Depth-first search and linear graph algorithms[END_REF]. The limitation of this technique is that it works only on directed acyclic graphs (DAGs). If the graph of the composition contains cycles, we need to break these cycles (feedback arc set) and thus transform the graph into a DAG. It is here that the notion of weak and strong bindings comes into play. The edges corresponding to weak bindings that are present on cycles are discarded by the sorting algorithm, as they do not impede the primary service goal. At this point, we do not handle bindings involving strong cyclic dependencies. Definition 6 (Deployment Plan): A deployment plan P consists of a sequence of steps involving three operations -[ADD, BIND, START] on an IoT object O.

ADD operation takes object O as input. BIND takes two different objects O 1 and O 2 and establishes a binding β in the composition. Similarly, START operation takes the object O to be started as input. More specifically, ADD refers to the provisioning of required application interfaces (e.g., 'motion detection' for a camera). BIND refers to the configuration of the network layer to allow the communication between application interfaces. START enables application interfaces of objects. The deployment plan dictates the order in which these operations are applied.

Example 3: As an illustration, consider a use case involving three devices: a baby monitor (dlink50201), a smartphone (phoneapp), and a TV (Chromecast). In this scenario, the baby monitor and the TV are co-located in a smart room whereas the smartphone is located in a remote environment. Assume that the TV (or any device screen) is installed in the baby's room. The user would like to turn on the screen and play baby's favourite show on the screen, when he/she wakes up. It will keep the baby engaged for a while until he/she is attended by his/her parents or caretaker. The use case composition is shown in Figure 4. In order to restrict the unbound behaviour, we have defined the environment in the use case as shown in far left of Figure 4. A deployment plan as shown in Listing 3 is generated for this composition.

In this use case, the composition is without cycles. So, the dependency chain is pretty clear: the smartphone interfaces S TVON and S TVOFF depend on the TV (T TVON, T TVOFF) and the baby monitor B ALERT depends on S ALERT interface of the smartphone.

The devices are deployed in the following order: first, the TV is deployed, then the smartphone, and finally the babymonitor is deployed thereby preventing send-receive mismatch at the interface level. Further, in Section V, we detail how the deployment plan is leveraged by an existing platform for network level deployment.

V. TOOL SUPPORT AND EXPERIMENTS

In this section, we describe our tool implementing the approach. The implementation is available online on Github 1 . Further in the section, we validate the approach using experiments involving composition and deployment of real-world IoT use cases.

A. IoT Service Assistant

The target users of the tool may not have the required skills to generate correct compositions and deployments. So, the tool aims at guiding the user towards deployment by hiding the underlying complexities. The user-base that we are targeting is home users, who have the basic understanding of IoT devices, but they do not want to get into API-level programming to get things working. A short training session may be required for the users to familiarise themselves with the tool features.

The tool is hosted as a web application on an Apache Tomcat server with an intuitive user interface based on jQuery and Semantic UI. The data format used is JSON and the integration with other services is done via REST API calls. The assistant performs these major functions: i) initial recommendation of devices for composition, ii) object composition by allowing users to compose IoT services through binding devices spread over different smart environments, iii) compatibility check to ensure correctness of the designed IoT service at the application level, iv) automated deployment of the validated composition.

Recommendation: First step in the tool workflow is recommendation. In [START_REF] Pallec | Digital assistance for the automated discovery and deployment of IoT services[END_REF], the authors proposed an automated recommendation of IoT services based on the physical interaction between objects and their environments. We build upon their work and use the recommendation service to get a set of objects available for a possible composition. From the set of objects, users can choose the subset of objects to be involved in the composition. Next, the tool loads the corresponding object models (described in Section II), which are specified in JSON. Users can view the chosen objects on the web interface, along with their application interfaces.

Composition: In the composition step, users can graphically define a set of bindings between application interfaces of objects to generate a composition. Then, the defined bindings are stored in a JSON file, which is used to generate a deployment plan as described in Section IV. The web interface provides an option to graphically view the dependencies among devices in the form of a directed graph.

Compatibility: Next, the user is provided with an option to check the compatibility of the proposed composition. The tool connects to the backend formal verification toolset CADP to check the compatibility of the composition. Internally, the tool takes JSON models corresponding to the objects and the file containing the JSON bindings as input and performs a model-to-model transformation to generate the required LNT code and SVL [START_REF] Garavel | SVL: A scripting language for compositional verification[END_REF] scripts for automating the analysis steps. The result of the compatibility check is returned to the user. In case of an incompatible composition, the user may want to restart the composition process. S/he can update the bindings or choose a new set of devices and check if they are compatible. Once a compatible solution is found, s/he can proceed to the deployment step.

Deployment: Finally, in the deployment step, the tool connects to Majord'Home [START_REF] Boussard | The Majord'Home: a SDN approach to let ISPs manage and extend their customers'home networks[END_REF], a modular IoT platform to configure the network layer. Majord'Home is a Software Defined Network (SDN) [START_REF]Software-defined networking: The new norm for networks[END_REF] based platform, which offers simplified interfaces for the network configuration of IoT services across multiple smart environments. Majord'Home is used as a deployment platform as it offers a finer degree of control to dictate the deployment leveraging specific features provided by the platform in terms of service isolation and device sharing. However, any IoT platform that provides APIs for network control can be used for deployment. Deployment is based on the plan described in Section IV. The network at SDN level is configured accordingly. In a composition, there may be one or more bindings between a pair of objects. For each set of bindings between a pair of objects, a Software-Defined LAN (SD-LAN) is set up by configuring the Residential Gateways. Using this setup, COs spread across different smart environments can communicate as they were in a same smart environment [START_REF] Boussard | Software-defined lans for interconnected smart environment[END_REF]. Additionally, the SD-LAN solution allows a CO to interact with different IoT services yet preserves the network isolation and discovery properties. The designed IoT assistant manages and controls SD-LANs by using custom REST APIs. The overall integration of the assistant with Majord'Home is shown in Figure 5. A CO controller is required in the architecture to facilitate the control and configuration of COs. Also, the network elements are treated as COs. This abstraction is due to the fact that there is a strong inter-working between configuration of COs and the network layer in efficiently deploying IoT services.

The tool screenshot is shown in Figure 6. Initially, the service recommendation assistant suggests the following devices: A DLink camera, an Android 7.0 tablet, and a Chromecast device. These devices can be used to setup a baby monitoring service in a smart home. In Figure 6 (top left), we can see the device list on the web interface along with available application interfaces. The output interfaces are highlighted using a ribbon with a triangle in the device list. Further in Figure 6 (bottom left), we can see the user established bindings. The dependency graph of the objects' is displayed to the user (Figure 6, top right). The compatibility checks are successful for the given scenario and also we can notice the SD-LAN creation in the screenshot (Figure 6, bottom right). More details regarding the tool and its implementation are available in the companion tool paper [START_REF] Krishna | IoT Composer: Composition and deployment of IoT applications[END_REF].

B. Experiments

In order to validate our approach, we considered various IoT objects available in a smart home environment and composed a number of use cases involving these objects. We focus on performance and usability aspects of the tool. Some of the experiment results for measuring the performance are shown in Table I. The host machine used was running Xubuntu 18.04 on a hardware consisting of Core i7-7600U processor, 256GB M.2 PCIe SSD, and 16GB of RAM. In Table I, Objs denotes the number of IoT objects used in the composition (environment included). Bind refers to the number of bindings. The next two columns denote the number of states and transitions in the composition LTS. The time taken to generate the LTS in seconds (rounded off to nearest integer) and the time taken to perform the compatibility check (in seconds) are shown in the last two columns. We have not shown the deployment plan generation time as it is the time required for topological sorting, which is linear with respect to the number of objects and bindings. Moreover, it is negligible considering the context of a smart home. The time taken for deployment is negligible with respect to analysis steps as it predominantly involves establishing network connections between objects.

In Table I, the time taken to generate the LTS and check the compatibility does not proportionally increase with the number of objects and bindings, as the size of the composition LTS depends not only on the number of objects, but also on the complexity of their individual behaviours. The Multi prefix refers to use cases where objects are replicated in the scenario (e.g., a pair of smart doors in MultiDoor use case). We can also observe that use cases IndepCase1 and IndepCase2 involve many objects and consequently, the generated LTS is quite large. In these two use-cases, we simulated multiple instances of compositions running independently to introduce a high level of concurrency. IndepCase2 takes about 12 seconds to perform the compatibility check. This time is satisfactory considering the fact that the check is done at design time where there is no tight time constraints. To sum up, the results of the experiments confirm our understanding that the modelling and analysis approach scales well and can be used for correct IoT deployments in the context of a smart home.

In addition to performance, the tool usability was measured by involving three end-users. The users were of different ages ranging from 21 to 50 years old. Users were provided a short 20 minute walkthrough of the tool and they were explained briefly the underlying techniques (behavioural models, formal verification etc.). Generally, when carrying out the experiments we observed that an average time of 4 minutes was taken to visually build a realistic composition (select interfaces and bind) using 4 objects. Interestingly, all the users had a clear goal in mind when they began their compositions. A common feedback among the users was to reduce the number of click interactions in the tool. It is true that with the current UI, building a composition involving more than 10 objects can take a bit longer. But, as we target smart homes, where a given IoT application does not involve all the objects in the home (often less than 10 objects), we expect the composition to be built in a reasonable amount of time.

Finally, if we are to scale this approach for large IoT systems like smart cities, it would require a redesign of the UI and binding techniques. Nevertheless, the verification and deployment steps are likely to scale as the compositional verification capabilities of CADP can handle systems with hundreds of parallel components [START_REF] Bouzafour | Model-checking synthesizable systemverilog descriptions of asynchronous circuits[END_REF].

VI. RELATED WORK

In this section, we will review the state of the art on three aspects: compatibility of behavioural models, compositiondeployment of IoT applications and deployment of distributed applications.

Compatibility: Compatibility has been studied in different areas such as software architectures, software components, or Web services, but has not been the source of research yet in the IoT community. [START_REF] Brand | On communicating finite-state machines[END_REF], [START_REF] Yellin | Protocol specifications and component adaptors[END_REF] use an automata-based formalism as model and rely on a notion called unspecified receptions stating that every send message must have a corresponding receive message. [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. 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] Durán | A Generic Framework for Nprotocol Compatibility Checking[END_REF] proposes a generic framework for verifying several notions of compatibility between behavioural models. The analysis is achieved using the rewriting logic based Maude's toolset. [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 web services can cooperate safely. The compatibility between two services is defined by the soundness property on open workflow nets. Compared to these works, our approach proposes a new compatibility notion in the context of IoT objects composition. The verification of this compatibility notion is fully automated using an encoding into process algebra and LTS traversal techniques.

Composition (Tools): We review 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 (IFTTT)[END_REF] are two tools that provide graphical support for visually building applications consisting of IoT objects. SmartThings [START_REF] Smartthings | Smartthings: Add a little smartness to your things[END_REF] platform provides ability to write compound rules for home automation using SmartRules app [START_REF] Smartrules | Smartrules: Rule your smart home[END_REF]. Sharp Tools [START_REF] Tools | Sharp tools: Visualize and automate your smart home[END_REF] has a visual builder and dashboard to automate and monitor smart homes. Stringify [START_REF] Stringify | Stringify: Change your life by connecting every thing[END_REF] uses Flows similar to IFTTT to build automation. webCoRE [START_REF] Webcore | webcore: The web community's own rule engine[END_REF] is a community rule engine that allows users to create scripts that are interpreted and executed by SmartThings. openHAB [START_REF] Openhab | openhab: Empowering the smart home[END_REF] is an open source home automation software that allows to define rules based on events, time and other triggers. These rules are executed by the openHAB engine. The home automation products in the industry help users build automation scenarios but they do not fully take into account the dependencies among devices at the behavioural level.

Composition (Techniques):

The work presented in [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. The authors in [START_REF] Tata | Formal model and method to decompose process-aware IoT applications[END_REF] present 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. In our approach, we preferred semi-automated composition techniques (bindings required as input) to keep the user in the loop and we provide automated techniques for verifying correctness of the composition. We also propose full automation of the deployment of the final application, which makes our approach supporting the development of IoT applications from selection to final deployment.

Deployment: Finally, deployment of distributed applications has mainly been investigated in the cloud computing area. There are several configuration management tools, such as Puppet or Chef, which allow one to automatically configure new machines as described in dedicated files called manifests or recipes. Industrial technologies, such as BOSH, Cloudify, and Heat, help to create, deploy, and orchestrate applications in multiple cloud infrastructures. As far as the configuration steps are concerned, these technologies rely on the aforementioned configuration management tools (e.g., Puppet or Chef). [START_REF] Lascu | Automatic deployment of component-based applications[END_REF] presents a formal model of components and a sound and complete algorithm for computing the sequence of actions that permits the deployment of a desired configuration even in the presence of circular dependencies among components. In [START_REF] Brogi | Modelling and analysing cloud application management[END_REF], the authors present an extension of the TOSCA standard in order to specify the behaviour of a cloud application's management operations. They also propose several kinds of analysis for checking, e.g., the validity of a management plan or the possibility to reach a certain configuration given a plan. [START_REF] Etchevers | Reliable self-deployment of distributed cloud applications[END_REF] presents a self-deployment protocol that aims at configuring a set of software components distributed over a set of virtual machines. This protocol works in a fully automated and decentralized way while supporting VM failures. Compared to these works, we propose an automated deployment solution for IoT applications, which is formally verified through abstract models and relies on SDN-based deployment.

VII. CONCLUSION

This paper has presented a solution for supporting the design and deployment of IoT applications. We first propose to support the correct construction of compositions of servicebased devices by using behavioural models and automated verification techniques. Our proposed interface-based model for IoT objects, provides a generic view of the device and its behaviour, thereby making the composition agnostic to heterogeneity found across different device manufacturers. The compatibility analysis ensures that all the bindings defined in the composition can effectively be executed when the application is deployed. Once the composition is validated, a deployment plan is generated and can be executed in order to effectively configure and run the application. All the steps of our approach are supported by a prototype tool we implemented and that allows users to graphically compose, validate, and deploy IoT services. This tool has been interfaced with the Majord'Home platform and several case studies were used for validating our solution which turns out to be very helpful in practice.

Moving forward, the presented work offers several perspectives. First, our deployment approach can be extended to deal with object compositions containing cycles of strong bindings. A possible solution is to identify bindings that can be considered as weak (and hence enable the application of our current deployment scheme) and have a minimal impact on the service during its deployment. The second one relates to the extension of the presented composition framework to support the reconfiguration process (removing or adding new devices to running applications) preserving the level of correctness ensured during the deployment phase. The final perspective relates to extending the formal models of IoT objects and composition with value-passing communication and quantitative information (e.g., probabilities, costs, etc.) to carry out QoS analysis and performance evaluation of the IoT applications.

Figure 1 .

 1 Figure 1. Verified IoT composition and deployment.

Figure 2 .

 2 Figure 2. An IoT composition using three connected objects.

Figure 3 .

 3 Figure 3. LTSs underlying the compatibility check for Example 1.

  module m e d i a d e v i c e i s p r o c e s s m e d i a d e v i c e i d l e [ on , v i d e o , aux , a u d i o : any ] i s s e l e c t on ; m e d i a d e v i c e v i d e o [ on , v i d e o , aux , a u d i o ] [ ] aux ; m e d i a d e v i c e a u d i o [ on , v i d e o , aux , a u d i o ] end s e l e c t end p r o c e s s p r o c e s s m e d i a d e v i c e v i d e o [ on , v i d e o , aux , a u d i o : any ] i s v i d e o ; m e d i a d e v i c e e x i t [ on , v i d e o , aux , a u d i o ] end p r o c e s s p r o c e s s m e d i a d e v i c e a u d i o [ on , v i d e o , aux , a u d i o : any ] i s a u d i o ; m e d i a d e v i c e e x i t [ on , v i d e o , aux , a u d i o ] end p r o c e s s p r o c e s s m e d i a d e v i c e e x i t [ on , v i d e o , aux , a u d i o : any ] i s s t o p end p r o c e s s end module Listing 1. LNT processes specifying the Media Device LTS.

  module p r o d a l l ( phone , m e d i a d e v i c e , s p e a k e r ) i s p r o c e s s p r o d [ on , v i d e o , aux , a u d i o : any ] i s par on , v i d e o -> p h o n e i d l e [ on , v i d e o ] | | on , v i d e o , a u d i o -> m e d i a d e v i c e i d l e [ on , v i d e o , aux , a u d i o ] | | a u d i o -> s p e a k e r i d l e [ a u d i o ] end par end p r o c e s s end module Listing 2. LNT process specifying the composition of objects.

  1 https://ajaykrishna.github.io/iotcomposer/

Figure 4 .

 4 Figure 4. IoT use case showing model behaviour and bindings.

Figure 5 .

 5 Figure 5. Tool integration with Majord'Home platform.

Figure 6 .

 6 Figure 6. Screenshot of the web interface.


Ajay Krishna

Michel Le Pallec

Radu Mateescu

Ludovic Noirie

Gwen Salaün

IoT Composer: Composition and Deployment of IoT Applications

Keywords: IoT, behavioural models, composition, formal verification, deployment

The Internet of Things (IoT) consists of interconnected physical devices and software components. These connected things or objects exchange information in order to provide an end-user service. To fulfil this objective, such applications have to be designed by composing existing objects. However, this is a very difficult task mostly due to the heterogeneity and diversity of available objects. The IoT Composer tool was developed for supporting the development of IoT applications by first providing a behavioural model for objects and their composition. IoT Composer is developed as a web application that provides graphical support for composing available objects. The tool also provides automated validation techniques for verifying that the composition behaves correctly. Finally, a deployment plan is generated and can be run for effectively binding and instantiating all objects involved in the composition. IoT Composer was applied successfully to several real-world case studies.

I. INTRODUCTION

The Internet of Things (IoT) is a network of physical devices and software components that are connected together in order to exchange information and to fulfil an IoT service. IoT applications are supposed to empower interconnected objects in order to build powerful and added-value services. The hardware devices used for building IoT applications are already available, but there are only a few management systems that support the design, deployment and maintenance of such applications. These tasks are particularly ambitious due to the specificities of IoT applications that are by nature highly distributed, heterogeneous and dynamic. Indeed, IoT applications induce a high level of concurrency, distribution, and collaboration. Designing concurrent applications is by nature a difficult and error-prone task. Moreover, IoT applications have to deal with heterogeneous IoT hardware and communication layers. Therefore, there is a need for a common model for specifying all objects and the way they interact altogether. Last but not least, modern systems are no longer designed and implemented once-for-all, but they may evolve over time, which requires simple techniques for updating and changing those applications.

In this paper, we present the IoT Composer tool, which supports all the steps of the design, composition, and deployment of an IoT application by selecting, configuring and binding available objects. Figure 1 gives an overall view of the IoT Composer functionalities. Given a repository of objects, the first step is to select some objects as candidates to participate in the composition-to-be. This part of the approach is achieved by relying on an existing recommendation system [START_REF] Pallec | Digital assistance for the automated discovery and deployment of IoT services[END_REF]. Then, IoT Composer graphically exposes the interfaces of the selected objects and allows the user to bind interfaces with respect to the IoT service expected from the composition. It is worth noting that only this first step of the approach requires human intervention, all the following steps being fully automated. In a second step, given a set of selected objects and a set of bindings, we generate code in the LNT process algebraic specification language [START_REF] Garavel | From LOTOS to LNT[END_REF]. This specification is fed as input to the CADP verification toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF] in order to check several properties of interest. The most important one is compatibility, which consists in checking whether the set of objects and bindings will behave correctly, avoiding erroneous situations. The tool also allows the verification of other properties such as the absence of deadlocks. If the selected objects and bindings are not satisfactory, the user can return to the first step to update the selection or bindings wrt. the feedback given during the verification step. The final step of the approach aims at generating a deployment plan that is executed for effectively configuring and running the application. IoT Composer is a web application with an intuitive user interface. It has been applied to several real-world case studies 1 for validation purposes and it turns out to be very useful as it simplifies the design of new IoT applications. Note that our approach supports the development of IoT applications from the beginning (selection) to the end (deployment). In doing so, it also ensures reliability of the applications by formally verifying the proposed solution in the background. The targeted users are any end-users who may want to deploy reliable added-value IoT services on top of objects available in their smart homes. The tool is available as open source online 1 with several examples we used during its evaluation.

The rest of this paper is organized as follows. Section II introduces the models used for specifying objects and their composition. This section also presents the notion of compatibility that allows one to check that the composition executes as expected. Section III describes the IoT Composer tool. Section IV presents experiments performed on several realworld smart home use-cases. Section V overviews related work and Section VI concludes the paper.

II. MODELS AND COMPATIBILITY

As far as models are concerned, an IoT object is modelled as a Labelled Transition System (LTS), i.e., a state-transition graph representing the states of the object and its interactions with the environment. Each transition is labelled by an action corresponding to an input or output message. An LTS can be viewed as a behavioural interface description language.

A composition of objects, also referred to as a composite service, is then built by combining various objects, which are bound to each other relying on their LTS interfaces. The interfaces in the LTS are derived from the application interfaces of IoT objects. Given two objects, a binding aims at connecting one output message of one object with one input message of another object. A composition is thus defined by a set of objects and a set of bindings relating these objects. In this work, we assume that the objects involved in a composition interact using binary communication: an interaction occurs between one output message and one input message (same message name) belonging to two different objects. Additionally, we consider handshake communication, also known as synchronous communication model. This means that the sender is blocked until the receiver is able to interact with it. Then, both objects synchronize at the same time.

Compatibility checking aims at ensuring that a service composition involving a set of objects and a set of bindings is correct, i.e., all bindings can effectively be executed and all reachable actions unbound in the composition do not prevent the bindings to be executed (Unbound interfaces refer to the interfaces which are not involved in the composition). This compatibility notion is checked by first automatically encoding the set of behavioural models and the set of bindings into the LNT process algebraic specification language [START_REF] Champelovier | Reference Manual of the LNT to LOTOS Translator (Version 6.7)[END_REF]. Then, we make use of the existing tools available in the CADP toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF], which accepts LNT as input, for (i) compiling the LNT specification into an LTS describing all the possible 1 https://ajaykrishna.github.io/iotcomposer/ executions of the composition (called composition LTS), and for (ii) traversing this LTS in order to verify that all bindings do appear in the composition LTS.

Note that we take advantage of this LNT encoding for verifying other properties of interest. This is the case, for instance, of the absence of deadlocks, which can be automatically analyzed using model checking techniques available in CADP.

III. IOT COMPOSER

The IoT Composer tool aims at assisting the user during the composition and deployment tasks when developing a new IoT application. Indeed, end-users may not have the required skills to build reliable and bug-free compositions of objects. The tool guides the user towards reliable application design by hiding the underlying complexities. It is hosted as a web application on an Apache Tomcat server with a simple user interface based on jQuery and Semantic UI. The data format used is JSON and the integration with other services is achieved via REST API calls.

IoT Composer performs three major functions: (i) composition by allowing users to compose IoT objects through binding devices spread over different smart environments, (ii) compatibility check to ensure correctness of the designed IoT application, and (iii) automated deployment of the validated composition. Figure 2 shows a screenshot of the web application and of its functionalities on a simple example involving four objects. The very first step (object composition) relies on the recommendation service presented in [START_REF] Pallec | Digital assistance for the automated discovery and deployment of IoT services[END_REF]. The authors proposed an automated recommendation of IoT objects based on the interaction between objects and their environments. We use this approach for an early identification and selection of objects suitable for the design of an IoT service. When the user has selected some of the objects suggested by the recommendation system, the tool loads in the web interface this list of objects with the set of input/output messages provided in their respective application interfaces. From this set of recommended objects, the user can then graphically define a set of bindings between these interfaces to generate a composition (selected objects + bindings). The defined bindings are stored in a JSON file. The web interface provides an option to display in the web application the graph making explicit the dependencies among objects.

In the next step, the tool connects to the backend formal verification toolset (CADP) to check the compatibility of the composition. Internally, the tool takes JSON models corresponding to the objects and the file storing the JSON bindings as input. Then, it performs a model-to-model transformation to generate the required LNT code and Script Verification Language (SVL) [START_REF] Garavel | SVL: A scripting language for compositional verification[END_REF] scripts for automating the whole analysis step. The result of the compatibility check (true or false) is returned to the user. In case of an incompatible composition, the user is able to restart the composition process. (S)He can update the bindings or choose a new set of objects and check if they are compatible. When a compatible solution is found, (s)he can proceed to the (final) deployment step.

In the final step, a deployment plan is first generated by relying on a set of defined actions involving both application and network layers. This set of actions (add object, bind objects and start object) must be applied in a specific order for respecting the objects' functional dependencies. This plan is obtained considering the composition as a directed graph (objects as nodes and bindings as edges) and applying topological sorting in order to extract the sequence of operations to apply. Given such a plan, the tool is interfaced with Majord'Home [START_REF] Boussard | Software-Defined LANs for Interconnected Smart Environment[END_REF], [START_REF] Boussard | The Majord'Home: a SDN approach to let ISPs manage and extend their customers'home networks[END_REF], a modular IoT platform to deploy IoT applications. Majord'Home follows the Software Defined Network (SDN) [START_REF]Software-Defined Networking: The New Norm for Networks[END_REF] paradigm, which offers simplified interfaces for the network configuration of IoT services involving multiple smart environments. For each IoT service, a Software-Defined LAN (SD-LAN) is setup by configuring the residential gateways which delineate different local networks. Using this SD-LAN functions, connected objects spread across different smart environments can communicate as if they were in a same smart environment. Additionally, the SD-LAN solution allows a connected object to interact with different IoT services, yet preserves network isolation and discovery properties. IoT Composer manages and controls SD-LANs by using custom REST APIs. The overall integration of the IoT Composer components with other services (recommendation system, CADP, Majord'Home) is shown in Figure 3. Each component or service indicates its inputs and outputs as well as its implementation technology stack.

IV. EVALUATION

In order to validate our approach, we relied on various IoT objects available in a smart home environment and designed several IoT services by composing these objects. Some of the experimental results are shown in Table I. The host machine was running Xubuntu 18.04 on a hardware consisting of Core i7-7600U processor, 256GB M.2 PCIe SSD, and 16GB of RAM. In Table I, Objs denotes the number of IoT objects used in the composition. Bind refers to the number of bindings. The next two columns denote the number of states and transitions in the composition LTS. The time taken to generate the LTS (in seconds) and the time taken to perform the compatibility check (in seconds) are shown in the last two columns. The deployment time is not shown in this table. The plan generation time is negligible for dozens of objects since it is the time required for topological sorting, which is linear with respect to the number of objects and bindings. The deployment itself is achieved via the Majord'Home platform [START_REF] Boussard | The Majord'Home: a SDN approach to let ISPs manage and extend their customers'home networks[END_REF]. It takes a few seconds and this time does not depend on the number of objects.

As it can be observed in Table I, the time taken to generate the LTS and check the compatibility does not proportionally increase with the number of objects and bindings. It takes at most 12 seconds for the most complex example (20 objects), which is reasonable since this check is performed at designtime before deploying the IoT application. The final examples in Table I take more time because they involve more objects and therefore generating the corresponding composition LTS and checking compatibility are more time-consuming. We originally targeted to compose and deploy IoT services in the residential context (smart homes). In such a context, one may have a home with dozens or even hundreds of objects, but for a given concrete application it would barely need more than a few objects. To sum up, the results of these experiments confirm that, as far as scalability is concerned, the approach is satisfactory for IoT deployments in the smart home context.

V. RELATED WORK

In this section, we compare IoT composer with existing tools supporting the design of new applications by composition of IoT objects.

Node-RED [START_REF] Js-Foundation | Node-RED: Flow-based Programming for the IoT[END_REF] is a programming tool for wiring together hardware devices, APIs and online services. It provides a browser-based editor that makes it easy to wire together flows using a wide range of nodes. The final application can be deployed to its runtime in a single-clic. The light-weight runtime environment is built on Node.js, and can be run at the edge of the network on low-cost hardware (such as Raspberry Pi) or in the cloud. IFTTT [START_REF] Ovadia | Automate the internet with if this then that (IFTTT)[END_REF] (If This Then That) is a free web-based service to graphically create chains of simple conditional statements, called applets. An applet is triggered by changes that occur within other web services. In addition to the web-based application, the service runs on iOS and Android. Zenodys [START_REF] Zenodys | IoT Platform[END_REF] proposes a visual IoT platform for easily building IoT applications. Their approach relies on connectors for collecting and binding data sources. Deployment is supported as well as a set of data analytics in order to monitor running applications. Compared to these three tool-supported solutions, a first difference concerns modelling aspects. None of them assume that objects can be described using behavioural models whereas in our approach some services provided by an object should be executed in a certain order. This assumption particularly makes sense when focusing on composite applications. In addition, these solutions do not provide any support for checking that the application preserves some correctness criteria before deployment.

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] 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. In our approach, we preferred semi-automated composition techniques (bindings required as input) to keep the user in the loop and we provide automated techniques for verifying correctness of the composition. We also propose full automation of the final application deployment, which makes our approach supporting the development of IoT applications from the selection of objects to their deployment.

VI. CONCLUDING REMARKS

IoT Composer provides a solution for supporting the design and deployment of IoT applications. It allows developers to build correct compositions of software objects and devices by using behavioural modelling languages and automated verification techniques. The compatibility check ensures that all the bindings defined in the composition can effectively be executed when the application is deployed. It also checks that the composition is free of deadlocking situations. Once the composition is validated, a deployment plan is generated and can be executed in order to effectively configure and run the application. The IoT Composer tool is available online and has been applied successfully on several real-world case studies.

In the future, we first plan to extend the IoT composer tool to provide new functionalities supporting the reconfiguration (addition and removal of objects) of a deployed and running application. This should be possible via the web application and must preserve the level of correctness ensured during the deployment phase. A second perspective of this work concerns the verification step. Beyond analysis of compatibility and other properties of interest, we would like to provide quantitative verification techniques to carry out QoS analysis and performance evaluation of the IoT applications. This would require extending the models of IoT objects and composition with quantitative information (e.g., probabilities, costs, etc.).

Fig. 1 .

 1 Fig. 1. Overview of the tool functionalities.

Fig. 2 .

 2 Fig. 2. Screenshots of the web interface.

Fig. 3 .

 3 Fig. 3. Tool components and integration with various services.


Nicolás Espitia
email: nicolas.espitia-hoyos@inria.fr.

Andrey Polyakov
email: andrey.polyakov@inria.fr.

Denis Efimov
email: denis.efimov@inria.fr.

Wilfrid Perruquetti
email: wilfrid.perriquetti@ec-lille.fr.

Some characterizations of boundary time-varying feedbacks for fixed-time stabilization of reaction-diffusion systems

Keywords: Reaction-diffusion equations, time-varying feedbacks, fixed-time convergence, exponential Bell polynomials, generalized Laguerre polynomials

Some characterizations of boundary time-varying feedbacks for fixed-time stabilization of reaction-diffusion systems

Nicolás Espitia * , Andrey Polyakov * , Denis Efimov * , Wilfrid Perruquetti * *

INTRODUCTION

Finite/fixed-time stabilization and estimation have been widely considered for many years in the framework of linear and nonlinear ordinary differential equations (ODEs) [START_REF] Bhat | Finite time stability of continuous autonomous systems[END_REF]; [START_REF] Polyakov | Finite-time and Fixed-time Stabilization: Implicit Lyapunov Function Approach[END_REF]; [START_REF] Lopez-Ramirez | Finite-time and fixed-time observer design: Implicit lyapunov function approach[END_REF]). The need to meet some performance, time constraints and precision has highly motivated the stabilization and estimation in finite/fixed time. The concept of fixed-time differs from finite-time whenever the settling time is independent of the initial condition. More recent contributions deal with prescribedtime stabilization for nonlinear ODEs in normal form [START_REF] Song | Time-varying feedback for regulation of normalform nonlinear systems in prescribed finite time[END_REF]. For partial differential equations (PDEs), on the other hand, finite/fixed-time concepts have become a relevant research area (see e.g. [START_REF] Polyakov | On Homogeneous Finite-Time Control For Evolution Equation in Hilbert Space[END_REF], [START_REF] Pisano | Tracking control of the uncertain heat and wave equation via power-fractional and sliding-mode techniques[END_REF]). The motivations for finite/fixedtime control and estimation for PDEs are in the same way of those for the finite-dimensional systems. In particular, since many complex systems are described by PDEs (e.g. hydraulic networks, tubular chemical reactors, etc), convergence while meeting time constraints or just realizing the well-known separation principle are central issues, which can be coped when exploiting finite-time concepts.

For hyperbolic PDEs, on the one hand, there are few contributions in the literature (e.g. [START_REF] Perrollaz | Finite-time stabilization of 2×2 hyperbolic systems on tree-shaped networks[END_REF]; Coron et al. (2017)) for the stabilization in finite- time with boundary control; however for parabolic PDEs, on the other hand, the scenario is even more demanding and only few works have addressed some relevant issues on null controllability and finite-time stabilization (e.g. [START_REF] Coron | Null controllability and finite time stabilization for the heat equations with variable coefficients in space in one dimension via backstepping approach[END_REF]) by making use of the backstepping approach to design time-varying feedbacks; although with discontinuous kernels. Based on that work, this topic is moved forward for continuous time-varying feedbacks in [START_REF] Espitia | On continuous boundary time-varying feedbacks for fixed-time stabilization of coupled reaction-diffusion systems[END_REF] and [START_REF] Espitia | Boundary time-varying feedbacks for fixed-time stabilization of constant-parameter reactiondiffusioniffusion systems[END_REF] where the backstepping approach with continuous time-varying kernels is studied. In both of these works, the main idea relies on selecting a suitable target system that meets the fixedtime stability property. To that end, a blow-up function in time is used as reaction term which makes the target systems fixed-time stable. The approach leads to build on time-varying kernels allowing closed-form analytical solutions. Furthermore, the bounded invertibility is guaranteed and the fixed-time stability property is preserved for the closed-loop system.

In this work, and as a part of the perspectives in [START_REF] Espitia | Boundary time-varying feedbacks for fixed-time stabilization of constant-parameter reactiondiffusioniffusion systems[END_REF], we consider target systems with more general blow up functions where the power degree is left arbitrary.

The main contribution relies on more general characterizations of kernel solutions. It is proved that using the Faà di Bruno formula we can express the resulting kernels in rather closed-form in terms of the the exponential complete Bell polynomials which have plenty of properties and relations with special functions within the framework of hypergeometric functions and orthogonal polynomials. The fixed-time stability property is guaranteed for both the target system and the original system due to the bounded invertibility of the backstepping transformation.

When particularizing the degree of blow up function, one can recover the main results in [START_REF] Espitia | Boundary time-varying feedbacks for fixed-time stabilization of constant-parameter reactiondiffusioniffusion systems[END_REF].

This paper is organized as follows. In Section 2, we present the problem and the backstepping approach with timevarying kernels. Section 3 presents some characterization for kernel solutions. Section 4 provides the main result on fixed-time stabilization. Section 5 provides a numerical example to illustrate the main result. Finally, conclusions and perspectives are given in Section 6.

Notations R + will denote the set of nonnegative real numbers. The set of all functions g : [0, 1] → R such that 1 0 g(x) 2 dx < ∞ is denoted by L 2 ((0, 1), R) and is equipped with the norm • L 2 ((0,1),R) . Γ(•) denotes the Gamma function. I m (•), J m (•) with m ∈ Z, denote the modified Bessel and (nonmodified) Bessel functions of the first kind, respectively. L

PROBLEM DESCRIPTION

Let us consider the following scalar reaction-diffusion system with constant coefficients:

u t (t, x) = θu xx (t, x) + λu(t, x)
(1)

u(t, 0) = 0 (2) u(t, 1) = U (t)
(3) and initial condition: u(0, x) = u 0 (x) (4) where θ > 0 and λ ∈ R, u : [0, T ) × [0, 1] → R is the system state. The time T > 0 is given, and will be called from now the prescribed time or fixed time. In addition, U (t) ∈ R is the control input which will be a time-varying feedback having the functional form

U (t) = K(t)[u(t, •)](1) (5) with K(t)[u(t, •)](1) = 1 0 k(1, y, t)u(t, y)dy (6)
yet to be characterized. The existence and uniqueness of classical solutions of ( 1)-( 4) is assumed for initial conditions u 0 ∈ H 2 ((0, 1), R) satisfying the zero order compatibility conditions u(0, 0) = 0 and u(0, 1) = U (0). Without imposing compatibility condition, solutions u ∈ C 0 ([0, T ); L 2 ((0, 1), R)) can be understood in the weak sense (see [START_REF] Coron | Null controllability and finite time stabilization for the heat equations with variable coefficients in space in one dimension via backstepping approach[END_REF]).

Backstepping transformation and time-varying kernel equations

In this work, we build on the backstepping approach in order to come up with a boundary time-varying feedback that steers the state of the system (1)-( 4) to zero in a prescribed time T . To that end, the invertible Volterra integral transformation is chosen to depend on time. It is given as follows,

w(t, x) = u(t, x) - x 0 k(x, y, t)u(t, y)dy = K(t)[u(t, •)](x) (7)
The aim is to transform the system (1)-( 4) into the following target system:

w t (t, x) = θw xx (t, x) -c(t)w(t, x) (8)
w(t, 0) = 0 ( 9)

w(t, 1) = 0 (10)
with initial condition:

w 0 (x) = u 0 (x) - x 0 k(x, y, 0)u 0 (y)dy ( 11
)
where w : [0, T ) × [0, 1] → R is the state of the target system whose reaction term is a time-dependent parameter c(t) that needs to be designed to achieve fixed-time stability.

Following the standard methodology to find the kernel equations and by taking into account the time-varying dependence, it can be shown that the original system is transformed into the target system with the kernel of the transformation (7) satisfying the following PDE system:

k xx (x, y, t)-k yy (x, y, t) = γ(t)k(x, y, t)+ 1 θ k t (x, y, t) (12) k(x, 0, t) = 0 (13) d dx k(x, x, t) = -1 2 γ(t) (14) provided that c(t) = -λ + γ(t)θ (15)
where k is defined on the domain T = {(x, y, t) ∈ R 2 × [0, T ) : 0 ≤ y ≤ x ≤ 1} and γ can be chosen to be a smooth positive time-varying scalar function defined on [0, T ). Under a suitable characterization of γ, the fixed-time stabilization problem relates to the problem of solvability of kernel equations ( 12)-( 14). Solving them and choosing U (t) given in (5) we realize the backstepping transformation. Remark 1. The right-hand side of (12) contains the partial derivative of the kernel w.r.t time. For more general cases, where the reaction term is both space-and timevarying dependent, the well-posedness has been rigorously addressed in e.g. [START_REF] Colton | The solution of initial-boundary value problems for parabolic equations by the method of integral operators[END_REF], [START_REF] Meurer | Tracking control for boundary controlled parabolic PDEs with varying parameters: Combining backstepping and differential flatness[END_REF] and [START_REF] Vazquez | Control for fast and stable laminar-to-high-reynolds-numbers transfer in a 2D Navier-Stokes channel flow[END_REF]. Furthermore, the problem with time-dependent reaction term has been already addressed in [START_REF] Smyshlyaev | On control design for pdes with space-dependent diffusivity or timedependent reactivity[END_REF] where power series solutions are obtained. As in [START_REF] Espitia | On continuous boundary time-varying feedbacks for fixed-time stabilization of coupled reaction-diffusion systems[END_REF][START_REF] Espitia | Boundary time-varying feedbacks for fixed-time stabilization of constant-parameter reactiondiffusioniffusion systems[END_REF], here we intend to exploit the power series representations. •

Inverse transformation and time-varying kernel equations

The inverse of the backstepping transformation is given by

u(t, x) = w(t, x) + x 0 l(x, y, t)w(t, y)dy = L(t)[w(t, •)](x) (16)
whose kernel l(x, y, t), can be shown to satisfy the following PDE system:

l xx (x, y, t) -l yy (x, y, t) = -γ(t)l(x, y, t) + 1 θ l t (x, y, t) (17) l(x, 0, t) = 0 (18) d dx l(x, x, t) = -1 2 γ(t) (19)
provided that c(t) = -λ + γ(t)θ and l is defined on the domain

T = {(x, y, t) ∈ R 2 × [0, T ) : 0 ≤ y ≤ x ≤ 1}.
As before, γ can be chosen to be a smooth positive time-varying scalar function defined on [0, T ). The timevarying feedback (5) can equivalently be written under the following functional form

U (t) = L(t)[w(t, •)](1) (20) with L(t)[w(t, •)](1) = 1 0 l(1, y, t)w(t, y)dy (21)

CHARACTERIZATIONS OF THE PDE KERNELS

3.1 Solution of the PDE kernel (12)-( 14)

Let us choose γ in ( 12)-( 14) to be the solution that satisfies the following scalar nonlinear ordinary differential equation:

γ(t) = 1 + ǫ γ 0 T γ (2+ǫ)/(1+ǫ) (t), γ(0) = γ 1+ǫ 0 > 0 (22)
where ǫ > 0 is a design parameter, T is given and is going to be the prescribed time. The solution to ( 22) is as follows:

γ(t) = (γ 0 T ) 1+ǫ (T -t) 1+ǫ (23)
This solution is monotonically increasing and blows up at time T . In order to characterize the solution of ( 12)-( 14), let us briefly introduce some relevant results within the framework of special functions and advanced combinatorics.

Preliminaries on exponential Bell polynomials. The exponential (partial) Bell polynomials are defined by the series expansion [START_REF] Comtet | Advanced Combinatorics[END_REF]):

∞ n=k B n,k (x 1 , x 2 , ..., x n-k+1 ) t n n! = 1 k! ∞ m=1 x m t m m! k
The exponential (complete) Bell polynomials are defined by

B n (x 1 , x 2 , ..., x n ) = n k=1 B n,k (x 1 , x 2 , ..., x n-k+1 ), B 0 = 1 (
B n,k (abx 1 , ab 2 x 2 , ..., ab n-k+1 x n-k+1 ) = a k b n B n,k (x 1 , x 2 , ..., x n-k+1 ) (25)
Property 2. Relation to the Lah numbers (Comtet, 1974, Section 3.3):

B n,k (1!, 2!, .., (n -k + 1)!) = n -1 k -1 n! k! (26)
Property 3. Recurrence relation for the complete Bell polynomials (Bell, 1934, p. 270):

B n+1 (x 1 , x 2 , ..., x n+1 ) = n k=0 n k x n-k B k (x 1 , x 2 , ..., x k ) (27)
Let us recall the Faà di Bruno formula in terms of Bell polynomials as follows: Definition 1. [The Faà di Bruno formula] If g and h possess derivatives up to order n, then

d n dx n g(h(x)) = n k=0 g (k) (h(x))B n,k (h ′ , h ′′ , ..., h (n-k+1) )
(28) Theorem 1. Let T > 0 be given and γ satisfy (22). The problem (12)-( 14) has a well-posed solution on T , given by k(x, y, t)

= - y 2 γ 1/(ǫ+1) (t) T γ 0 θ ∞ n=0 (γ 1/(ǫ+1) (t)(x 2 -y 2 )) n 4 n (T γ 0 θ) n n!(n + 1)! × B n+1 (ǫ + 1) 0 (T γ 0 θ)γ ǫ/(ǫ+1) (t), (ǫ + 1) 1 (T γ 0 θ)γ ǫ/(ǫ+1) (t), ..., (ǫ + 1) n+1 (T γ 0 θ)γ ǫ/(ǫ+1) (t) (29)
Proof. We recall that we look for a solution of the form [START_REF] Smyshlyaev | On control design for pdes with space-dependent diffusivity or timedependent reactivity[END_REF]:

k(x, y, t) = -y 2 e -θ t 0 γ(τ )dτ f (z, t), z = x 2 -y 2 θ (30)
Introducing ( 30) into ( 12)-( 14), we straightforwardly obtain that f (z, t) satisfies the following nonlinear parabolic PDE:

f t (z, t) = f zz (z, t) + 3 z f z (z, t) (31
) with boundary conditions,

f z (0, t) = 0, f (0, t) = γ(t)e θ t 0 γ(τ )dτ := F (t) (32) where F (t) is a C ∞ function (whose n-th derivative w.r.t time is denoted by F (n) (t) := d n dt n F (t)
). Since we deal with an infinitely differentiable function γ(t), the solution to (31)-( 32) can be found in [START_REF] Polianin | Handbook of linear partial differential equations for engineers and scientists[END_REF] and it is as follows:

f (z, t) = ∞ n=0 z 2n 4 n n!(n + 1)! F (n) (t) ( 33
)
The task is to characterize F (n) (t). To that end, note that F (t) is just a product with composite functions. Therefore, using the general Leibniz rule, we have

F (n) (t) = n k=0 n k γ (n-k) (t) d k dt k e θ t 0 γ(τ )dτ (34)
and then, by applying the the Faà Di Bruno formula (see (28)) to (34), we get

F (n) (t) = n k=0 n k γ (n-k) k j=0 B k,j (θγ, θ γ, .., θγ (k-j) ) × e θ t 0 γ(τ )dτ
(35) By ( 22) and computing iteratively its (kj)-th derivative, (35) is reformulated as follows:

F (n) (t) = n k=0 n k (1 + ǫ) n-k (T γ 0 ) n-k γ(γ 1/(ǫ+1) ) n-k × k j=0 B k,j θγ, θ (1+ǫ) T γ0 γγ 1/(ǫ+1) , θ (1+ǫ)(2+ǫ) (T γ0) 2 γ(γ 1/(ǫ+1) ) 2 , ..., θ (1+ǫ) k-j (T γ0) k-j γ(γ 1/(ǫ+1) ) k-j e θ t 0 γ(τ )dτ
From Property 1 and the definition of the complete Bell polynomials (24), we get

F (n) (t) = n k=0 n k (1 + ǫ) n-k (T γ 0 ) n γγ n/(ǫ+1) × B k (1 + ǫ) 0 (T γ 0 θ)γ ǫ/(1+ǫ) , (1 + ǫ) 1 (T γ 0 θ)γ ǫ/(1+ǫ) , ..., (1 + ǫ) k (T γ 0 θ)γ ǫ/(1+ǫ) e θ t 0 γ(τ )dτ
(36) which can further be rewritten as follows:

F (n) (t) = γ (n+1)/(ǫ+1) (T γ 0 ) n+1 θ n k=0 n k (1 + ǫ) n-k (T γ 0 θ)γ ǫ/(ǫ+1) × B k (1 + ǫ) 0 (T γ 0 θ)γ ǫ/(1+ǫ) , (1 + ǫ) 1 (T γ 0 θ)γ ǫ/(1+ǫ) , ..., (1 + ǫ) k (T γ 0 θ)γ ǫ/(1+ǫ) e θ t 0 γ(τ )dτ
(37) Then, by the recurrence relation in Property 3, we finally obtain the characterization for F (n) (t). That is,

F (n) (t) = γ (n+1)/(ǫ+1) (T γ 0 ) n+1 θ × B n+1 (1 + ǫ) 0 (T γ 0 θ)γ ǫ/(1+ǫ) , (1 + ǫ) 1 (T γ 0 θ)γ ǫ/(1+ǫ) , ..., (1 + ǫ) n+1 (T γ 0 θ)γ ǫ/(1+ǫ) e θ t 0 γ(τ )dτ (38)
Hence, replacing it into (33) and by virtue of (30), we obtain (29). This concludes the proof.

•

Let us particularize the case when ǫ = 1 from which it is possible to obtain closed-form solutions for the kernel in terms of generalized Laguerre polynomials and subsequently, in terms of the modified Bessel functions. Thus, we can alternatively but more rigorously recover the results of [START_REF] Espitia | On continuous boundary time-varying feedbacks for fixed-time stabilization of coupled reaction-diffusion systems[END_REF] and [START_REF] Espitia | Boundary time-varying feedbacks for fixed-time stabilization of constant-parameter reactiondiffusioniffusion systems[END_REF] Corollary 1. Let T > 0 be given and γ satisfy (22). If ǫ = 1, then the problem (12)-( 14) has a well-posed solution on T , given by

k(x, y, t) = - y 2 γ(t) ∞ n=0 (γ 1/2 (t)(x 2 -y 2 )) n 4 n (T γ 0 θ) n (n + 1)! × L (1) n -(T γ 0 θ)γ 1/2 (t) (39)
Before we get into the proof, let us first introduce some intermediary results from the theory of hypergeometric functions.

Kummer confluent hypergeometric functions and generalized Laguerre polynomials. The Kummer confluent hypergeometric function 1 F 1 (a; b; p) is defined as follows:

1 F 1 (a; b; p) = ∞ k=0 (a) k (b) k p k k! (40)
The Kummer function has the following property: Property 4.

e p 1 F 1 (a; b; -p) = 1 F 1 (b -a; b; p) (41)
A relation between the polynomials involving the Lah numbers and the Kummer function is as follows [START_REF] Qi | On the sum of the Lah numbers and zeros of the Kummer confluent hypergeometric function[END_REF], Theorem 1): Property 5.

n k=1 n -1 k -1 n! k! p k = n!e -p 1 F 1 (n + 1; 2; p) (42)
The generalized Laguerre polynomial expressed in terms of ( 40) is

L (α) k (p) = k + α k 1 F 1 (-k; α + 1; p) (43)
Proof.[ of Corollary 1] From (36) with ǫ = 1, we have that 32) is given by

F (n) (t) in (
F (n) (t) = γγ n/2 (T γ 0 ) n n k=0 n k (2) n-k e θ t 0 γ(τ )dτ × k j=0 (T γ 0 θ) j (γ 1/2 ) j B k,j (2) 0 , (2) 1 , (2) 2 , ..., (2) k-j (44)
Note that B k,j ((2) 0 , (2) 1 , (2) 2 , ..., (2) k-j ) = B k,j (1, 2!, 3!, ..., (k -j + 1)!).
Therefore, applying Properties 2, 4, 5 and (43) it holds that

F (n) (t) = n! γγ n/2 (T γ 0 ) n (n + 1) + ((T γ 0 θ)γ 1/2 ) × n k=1 (n + 1 -k) k L (1) k-1 -(T γ 0 θ)γ 1/2 e θ t 0 γ(τ )dτ
(45) For the next developments we need the following intermediate result [START_REF] Coffey | On finite sums of Laguerre polynomials[END_REF], Proposition 1):

n j=1 L (1) j-1 j (p) = 1 p (1 -L (0) n )(p) (46)
along with the following well-known recurrence relations of the generalized Laguerre polynomials (Szego, 1975, Section 5.1) :

p n k=0 L (α) k (p) = (n + α + 1)L (α) n (p) -(n + 1)L (α) n+1 (p) (47)
and

L (α) n (p) = L (α+1) n (x) -L (α+1)
n-1 (x) (48) Hence, from (45) combined with (46) yields

F (n) (t) = n! γγ n/2 (T γ 0 ) n (n + 1)L (0) n -(T γ 0 θ)γ 1/2 -(T γ 0 θ)γ 1/2 n k=1 L (1) k-1 -(T γ 0 θ)γ 1/2 e θ t 0 γ(τ )dτ (49)
Shifting the index in the above sum and using the first recurrence relation (47), we have

F (n) (t) =n! γγ n/2 (T γ 0 ) n (n + 1)L (0) n -(T γ 0 θ)γ 1/2 + (n + 1)L (1) n-1 -(T γ 0 θ)γ 1/2 -nL (1) n -(T γ 0 θ)γ 1/2 e θ t 0 γ(τ )dτ
Applying the second recurrence relation (48), we finally obtain

F (n) (t) =n! γ(t)γ n/2 (t) (T γ 0 ) n L (1) n -(T γ 0 θ)γ 1/2 (t) e θ t 0 γ(τ )dτ
Therefore, replacing it into (33) and by virtue of (30), we obtain (39). This concludes the proof.

• Corollary 2. [START_REF] Espitia | Boundary time-varying feedbacks for fixed-time stabilization of constant-parameter reactiondiffusioniffusion systems[END_REF]] The system (12)-( 14),( 22) with ǫ = 1 has a well-posed C ∞ solution on T , given by

k(x, y, t) = -yγ(t)e √ γ(t)(x 2 -y 2 ) 4T γ0θ I 1 γ(t)(x 2 -y 2 ) γ(t)(x 2 -y 2 ) (50)
3.2 Solution of the PDE kernel (17)-( 19)

Proceeding similarly as before, the characterizations for the time-varying kernel of the inverse transformation are given as follows:

Theorem 2. Let T > 0 be given and γ satisfy (22). The problem (17)-( 19) has a well-posed solution on T , given by l(x, y, t)=-y 2

γ 1/(ǫ+1) (t) T γ 0 θ ∞ n=0 (γ 1/(ǫ+1) (t)(x 2 -y 2 )) n 4 n (T γ 0 θ) n n!(n + 1)! ×(-1) n B n+1 (ǫ + 1) 0 (T γ 0 θ)γ ǫ/(ǫ+1) (t), -(ǫ + 1) 1 (T γ 0 θ)γ ǫ/(ǫ+1) (t),
..., (-1) n+1 (ǫ + 1) n+1 (T γ 0 θ)γ ǫ/(ǫ+1) (t) (51)

Corollary 3. Let T > 0 be given and γ satisfy (22). If ǫ = 1, then the problem (17)-( 19) has a well-posed solution on T , given by

l(x, y, t) = - y 2 γ(t) ∞ n=0 (γ 1/2 (t)(x 2 -y 2 )) n 4 n (T γ 0 θ) n (n + 1)! × L (1) n (T γ 0 θ)γ 1/2 (t) (52)
Corollary 4. [START_REF] Espitia | Boundary time-varying feedbacks for fixed-time stabilization of constant-parameter reactiondiffusioniffusion systems[END_REF]] The system (17)-( 19),( 22) with ǫ = 1 has a well-posed C ∞ solution on T , given by

l(x, y, t) = -yγ(t)e √ γ(t)(x 2 -y 2 ) 4T γ0θ J 1 γ(t)(x 2 -y 2 ) γ(t)(x 2 -y 2 ) (53)

FIXED-TIME STABILIZATION

Lemma 1. The target system (8)-( 10) with γ satisfying (22) is fixed-time stable, i.e. for any w 0 ∈ L 2 ((0, 1), R), it holds w(t, •) L 2 ((0,1),R) → 0 as t → T (54)

Proof. The proof essentially follows the same lines of [START_REF] Espitia | Boundary time-varying feedbacks for fixed-time stabilization of constant-parameter reactiondiffusioniffusion systems[END_REF] as we consider the Lyapunov function candidate, V : L 2 ((0, 1), R) → R + , V (w) = 1 2 1 0 w 2 (x)dx such that, for all t ∈ [0, T ), it holds that:

V (w(t, •)) ≤ζ(t)V (w 0 ) (55) where

ζ(t) := e -2 θγ 0 T ǫ γ(t) ǫ/(1+ǫ)
e 2 θγ 0 T ǫ γ(0) ǫ/(1+ǫ) +λt (with ǫ > 0) is monotonically decreasing with the properties ζ(0) = 1 and ζ(T ) = 0. Therefore, it is straightforward to obtain w(t, •) L 2 ((0,1),R) → 0 as t → T .

•

Since kernel k is continuous on T , it holds, for each t ∈ [0, T ), that K(t) ∞ ≤ M k (t) where K(t) ∞ = sup 0≤y≤x≤1 |k(x, y, t)|. Similarly, it holds, for each t ∈ [0, T ), that L(t) ∞ ≤ M l (t) where L(t) ∞ = sup 0≤y≤x≤1 |l(x, y, t)|.
In this paper, we state the following assumption on the characterization of M k (t) and M l (t). Assumption 1. There exist c k and c l > 0 depending on γ 0 such that M k (t) = e c k γ(t) ǫ/(1+ǫ) (56) and M l (t) = e c l γ(t) ǫ/(1+ǫ) (57) Remark 2. For ǫ = 1, M k (t) and M l (t) have been precisely characterized in [START_REF] Espitia | Boundary time-varying feedbacks for fixed-time stabilization of constant-parameter reactiondiffusioniffusion systems[END_REF]. The proof to verify that ( 56)-( 57) hold with ǫ = 1 requires long technical developments and is not provided here for space limitation.

• Theorem 3. Let θ, T > 0 be fixed. Under Assumption 1, if γ 0 is chosen such that c l -T γ0θ ǫ < 0 , then the timevarying feedback controller

U (t) = 1 0 k(1, y, t)u(t, y)dy (58)
with k(1, y, t) as in (29) (at x = 1), stabilizes the system (1)-( 4) in a prescribed T , i.e. for any initial condition u 0 ∈ L 2 ((0, 1), R), it holds u(t, •) L 2 ((0,1),R) → 0 as t → T (59) Moreover, U (t) remains bounded and |U (t)| → 0 as t → T .

Proof. It follows the same reasoning as in [START_REF] Espitia | Boundary time-varying feedbacks for fixed-time stabilization of constant-parameter reactiondiffusioniffusion systems[END_REF]. Thus, by Lemma 1 and Assumption 1 the bounded invertibility of the backstepping transformation can be verified as the estimate of the L 2 -norm of the original system, which is given by

u(t, •) L 2 ≤(1 + M l (t)) ζ(t)(1 + M k (0)) u 0 L 2 (60) goes to zero in a fixed time T since the term M l (t) ζ(t) = e (c l -θγ 0 T ǫ )γ(t) ǫ/(1+ǫ) e θγ 0 T ǫ
γ(0) ǫ/(1+ǫ) +λT decreases to zero as t goes to T . remaining part of the proof immediately follows.

•

SIMULATIONS

Let us illustrate the fixed-time stability result with ǫ = 1 by considering a scalar reaction-diffusion system with θ = 1, λ = 12 and initial condition u(0, x) = 1025x(1x). Note that, in open loop (e.g. U (t) = 0), the system is unstable. The continuous boundary time-varying feedback is implemented by using the obtained closed-form solution for the kernel gain (50). Figure 1 shows the time evolution of L 2 -norm of the closed-loop system plotted on a logarithmic scale. It illustrates that with the time-varying feedback, the closed-loop system converges in a prescribe time T = 0.6s. It can be observed that the convergence to zero is faster than using the traditional linear control (e.g. in [START_REF] Smyshlyaev | Closed-form boundary state feedbacks for a class of 1-d partial integrodifferential equations[END_REF]) for exponential stabilization (red-dashed line).

CONCLUSION

In this work we have obtained more general characterizations of the time-varying kernels whose solutions are given in terms of power series representation involving the exponential complete Bell polynomials. By particularizing the characterization, one can recover kernel solutions in terms of the Laguerre polynomials and the modified Bessel functions. The fixed-time stability property can be guaranteed for both the target system and the original one. For future works, we expect to study robustness analysis as well as feasibility issues. In addition, the main methodology for fixed-time stabilization of other classes of PDEs is going to be addressed.

  denotes the generalized Laguerre polynomial. 1 F 1 (a; b; p) denotes the (Kummer) confluent hypergeometric function. (a) k := a(a + 1)(a + 2) • • • (a+k-1) = Γ(a+k) Γ(a) denotes the Pochhammer symbol or rising factorial. n k := n! k!(n-k)! , k = 1, 2, .., n denotes the binomial coefficients. Finally, B n,k (•), B n (•) denote the incomplete and complete exponential Bell polynomials, respectively.

  24)Let us point out some relevant properties as follows: Property 1. (Homogeneity). The following identity holds for n ≥ k and a, b ∈ R(Comtet, 1974, Section 3.3):

Fig. 1 .

 1 Fig. 1. Evolution of the L 2 -norm of the closed-loop system (logarithmic scale) with time-varying feedback (blue line) for a prescribed time T = 0.6s and linear control feedback (red dashed line) for exponential stabilization.

ACKNOWLEDGEMENTS

Authors would like to thank Drew Steeves, Miroslav Krstic and Rafael Vazquez for fruitful discussions on the general backstepping kernel characterization.