Simon Robillard

Hélène Coullon

SMT-Based Planning Synthesis for Distributed System Reconfigurations

Keywords: reconfiguration, planning, synthesis, component models, distributed systems

Large distributed systems with an emphasis on adaptability are now considered a necessity in many domains, yet reconfiguration of these systems is still largely carried out in an ad hoc fashion, a process that is both inefficient and error-prone. In this paper, we tackle the planification problem for the reconfiguration of distributed systems in the component-based reconfiguration model Concerto. Specifically, given some tasks to execute and a desired final state of the system, we show how to compute a reconfiguration plan that guarantees satisfaction of intercomponent dependencies and is also optimized for parallel execution. Our technique relies on an SMT solver to compute the required dependencies between components and ultimately schedule the reconfiguration. We illustrate the use of this technique on a variety of synthetic examples as well as a real use case in the context of an OpenStack system.

Introduction

Large distributed software systems are now ubiquitous, with component-based systems (e.g., service-oriented architectures or microservices) offering a convenient way to structure large applications. Indeed, isolating functionalities in components and building systems through composition greatly enhances adaptability and scalability of applications, two important requirements for many organizations. This approach is also promoted by the massive adoption of highlydistributed computing infrastructures such as cloud and edge computing.

However, the advantages of distributed architectures come at the price of increased complexity and technical challenges related to observability, coordination, maintenance, etc. Notably, the system reconfigurations that are required to achieve adaptability commonly lead to faults. For example, a study of 597 unplanned outages that affected popular cloud services between 2009 and 2015 found that 16% of them were caused by a software or hardware upgrade [START_REF] Gunawi | Why does the cloud stop computing? lessons from hundreds of service outages[END_REF]. The study concludes that "the complexity of cloud hardware and software ecosystem has outpaced existing testing, debugging, and verification tools". Indeed, testing and debugging methods are largely inadequate in the context of distributed systems, while the adoption of more suitable formal methods remains marginal in industry. The latter can be attributed to the difficulty of using formal methods and tools. Yet formal methods can lighten the burden of program developers and system administrators instead of adding to it, with synthesis techniques used to generate correct-by-construction programs. In that spirit, we propose to employ a Satisfiability Modulo Theories (SMT) solver to automate the planning of reconfigurations (deployment, migrations, software updates, etc.) of componentbased systems, i.e., to generate programs that coordinate the non-functional operations required to perform such reconfigurations. There have been some attempts to synthesize reconfiguration programs for component-based systems (some of them relying on an SMT solver), but they either target ad hoc, nonexecutable models [START_REF] Kikuchi | Synthesis of configuration change procedure using model finder[END_REF], or are limited to specific cases such as deployment [START_REF] Lascu | A planning tool supporting the deployment of cloud applications[END_REF], where the problem of executing parallel tasks is reduced to finding a precedence order. In contrast, our work targets the full scope of the component-based reconfiguration model Concerto [START_REF] Chardet | Toward safe and efficient reconfiguration with Concerto[END_REF], which provides a formally-defined execution model with expressive constraints on parallelism, as well as a concrete execution engine, making it suitable for formal analysis and experimental work.

In Concerto, reconfigurations are driven by asynchronous behavior requests to components. The execution of a behavior may depend on the state of other components: such dependencies are denoted by ports that form the interface of components, indicating their provisions and requirements towards each other. Section 2 gives an overview of Concerto, for a more complete presentation, the reader can refer to [START_REF] Chardet | Toward safe and efficient reconfiguration with Concerto[END_REF]. Our goal with this work is to automatically generate reconfiguration scripts for systems of Concerto components, i.e., determine required behaviors and coordinate their execution. We take as starting point a reconfiguration goal composed of behaviors to execute over some components and a specification of the final state of the system, particularly the statuses of ports. That goal may be provided by a system administrator, or could have been generated in the context of an autonomic control loop [START_REF] Kephart | The vision of autonomic computing[END_REF]. Importantly, it is a partial specification that typically only mentions parts of the system. For example, an administrator may specify only that a certain utility component should execute a behavior to update its software, whereas the completion of this task actually requires other components to suspend and later resume their activity.

Since a reconfiguration goal can require changes in any component of a system, the search space for reconfiguration scripts grows rapidly with the number of components. To synthesize reconfigurations for large systems, we propose a novel technique that takes advantage of the nature of component-based models. It first solves the problem for each component individually, by considering the internals of the component to find relevant behaviors, under the simplifying assumption that external requirements are all satisfied. Later the method coordinates behaviors over the whole system, relying on a first-order encoding of the scheduling problem and making use of the model-finding capabilities of an SMT solver. If this step fails due to unsatisfied dependencies, individual component reconfiguration goals are refined and the process iterated. Section 3 describes this method, and Section 4 measures its performance and scalability on a variety of synthetic examples, and illustrates its applicability on a real use case.

Reconfiguration With Concerto

Components and Assemblies. A distributed system in Concerto is represented as an assembly, i.e., a collection of components that correspond to control entities for the elements of the system. Components are not intended to represent the functional aspects of those elements, but instead to pilot the actions (installation, maintenance, suspension of service, etc.) required to operate them during their lifespan. In other words, a Concerto component is a wrapper around a new or legacy piece of software (e.g., service, module), typically written by its developer, that acts as replacement for scripts to install and maintain it.

The structural interface of a component is provided by its provide ports and use ports. Provide ports denote services or data provided by that component when those ports are active, while use ports denote requirements that the component has when those ports are active. Ports can be connected in an assembly to allow the satisfaction of component requirements. Connected ports impose synchronization rules between their components: a use port cannot be activated unless connected to an active provide port (the user component may have to wait for that requirement to be fulfilled in order to continue its internal activity) and a provide port cannot be deactivated while connected to an active use port.

Internally, components are characterized by places representing milestones in the life cycle, and transitions between places, mapped to concrete reconfiguration actions (e.g., starting a virtual machine, downloading an image, etc.). The internal state of a component is given by its places: at any point during execution, one or more places are active. While a place π is active, transitions originating from it can be (simultaneously) fired, after which π ceases to be active. Conversely, a place π becomes active after the completion of all the transitions that reach it. The completion of a transition takes a non-deterministic duration after firing, modeling the execution of the associated action. Active places also determine the statuses of ports: each port is bound to a set of places, and is active whenever one of them is active. Thus the status of ports changes according to the life cycle of the component. In graphic representations, ports are linked to the place (or set of places, denoted by rounded boxes) to which they are bound.

The last characteristic attribute of a component is its set of behaviors. A behavior is a subset of the transitions in a component, such that the associated subgraph is acyclic. At any point in an execution, a component may execute one behavior. Only then can the transitions in that behavior be fired. The behaviors of a component serve as its operational interface: a component may have one behavior including the actions to start it, another including the actions to update it, etc. A component can be requested to execute a behavior, which will determine its evolution and the actions that it performs. Graphically, different behaviors are represented by depicting transitions in different colors.

Figure 1 gives a graphic representation of an assembly. Component dep1 includes three places (uninstalled, installed and running) and three transitions (arrows between places) that belong to three behaviors (deploy, update, and uninstall). Place running is active (denoted by a token) and bound to pro-vide port service, whereas places installed and running are bound to provide port config. Both ports are connected to use ports belonging to server. Reconfiguration Scripts. Concerto is equipped with a simple language to execute reconfigurations. Whereas a Concerto component is written by a developer, the reconfiguration language is intended to be used by system administrators or DevOps engineers. Components are piloted through asynchronous requests via the command pushB(id, b) that asks the component identified by id to execute behavior b. The command takes its name from the fact that requests received by a component are queued and asynchronously executed by that component in the order in which they were received. While a component executes a behavior request, transitions in that behavior are fired until the component reaches a state where none of them can be fired. The behavior request is then considered complete, and the component executes the next one, until no more requests remain. The Concerto language also provides synchronization commands: wait(id) blocks the execution of the reconfiguration program until the component identified by id has executed all behaviors requests submitted to it, and waitAll() blocks the execution until all components have executed all pending behavior requests. These three commands allow parallel asynchronous execution in Concerto, leading to more efficient reconfigurations. Based on the description of the components provided by their developers, Concerto can execute reconfiguration scripts , allowing for empirical performance comparisons [START_REF] Chardet | Predictable efficiency for reconfiguration of service-oriented systems with Concerto[END_REF].

The goal of this work is to generate a reconfiguration script using the three aforementioned commands to execute behaviors over components and bring them to a desired state. In addition to those three commands, the Concerto language also provides four usual commands to modify the topology of an assembly: create and delete components, connect and disconnect them. These operations are out of the scope of reconfiguration planning as we define it. Indeed, the decision to modify the topology of the assembly is usually taken by the same entity that determines reconfiguration goals (system administrator or autonomic analysis tool) [START_REF] Fischer | Engage: A deployment management system[END_REF][START_REF] Hewson | A declarative approach to automated configuration[END_REF] rather than left to the planning phase. Furthermore, if topological changes in the assembly are deemed necessary, they can almost always be implemented through a reconfiguration script with the following steps: (i) creations of components, (ii) creations of connections, (iii) changes in component states, (iv) deletions of connections and (v) deletions of components [START_REF] Boyer | Robust reconfigurations of component assemblies[END_REF][START_REF] Cansado | A formal framework for structural reconfiguration of components under behavioural adaptation[END_REF]. The main difficulty is to determine the operations of the third step that take the components to a safe state, in particular ensuring that none of the connections that will be deleted include an active use port. Computing a reconfiguration program to lead components to a desired state (or to have them perform some required operations) is the focus of this paper.

As an example, consider the assembly in Figure 1, where all the components are running. We wish to run software updates on dep1 and dep2, but this will deactivate their provide port service. To carry out the updates, component server must first deactivate its corresponding use ports, which is accomplished by executing its behavior suspend. Figure 2a depicts a reconfiguration script that performs this, then returns the components to a running state. No explicit synchronization is needed between the suspension of server and the updates: the execution model of Concerto ensures that the updates cannot be executed as long as the provide ports are in use. An explicit synchronization is however needed before re-deploying the server, to prevent it from reactivating its use ports before the updates start. As a side note, the ports config (that represent configuration information that is not affected by the update, such as connection information) remain active throughout the reconfiguration: the fine-grained management of dependencies in Concerto avoids a full restart of the system. This assembly also illustrates the capacity of Concerto components to execute actions in parallel: for example, after server has reached place allocated, it can fire multiple transitions, corresponding to independent reconfiguration actions.

Concerto provides structured semantic tools to design efficient reconfiguration plans with highly parallel, asynchronous execution. However, taking full advantage of these features adds complexity to the internal structure of components and to associated reconfiguration scripts. Automated synthesis of reconfiguration scripts is therefore particularly useful in this context.

Reconfiguration Script Synthesis

This section describes the synthesis process used to generate reconfiguration scripts. This process takes as input a description of the current state of the system, namely the topology of the assembly (components and their connections) and the active places. We assume that the system is in a state where no component has pending behavior requests or ongoing transitions. Besides that information, the synthesis process also depends on a reconfiguration goal that is composed of (i) constraints Γ ports on the final state of ports and (ii) a set of behaviors Γ bhv to execute on designated components.

The constraints Γ ports are given by a partial function that maps specific instances of component ports to a boolean indicating whether that port is required to be active or inactive. A reconfiguration satisfies that goal if it ends in a state such that for any component c and port p, if Γ ports (c, p) is defined, the port p of component c is active if and only if Γ ports (c, p) = . Where the value of Γ ports is undefined, any status of the port satisfies the constraint. This means that a reconfiguration goal does not have to specify a unique final state for components, but instead allows for multiple target states. It may appear tedious to specify constraints for all components of an assembly when a reconfiguration is specifically aimed at a subset of it, but in practice the current state of the assembly can be used to guide the choice of Γ ports for those other components. A reasonable strategy might specify that provide ports active before the reconfiguration should remain active, and leave other ports unspecified.

The other element of the reconfiguration goal is the set Γ bhv , where each element is a pair composed of a component and a behavior. The reconfiguration satisfies it if it executes at least all these behaviors on the corresponding components. The set Γ bhv alone may not correspond to a feasible reconfiguration. For example, a system administrator wishing to update the components of Figure 1 might give a behavior goal Γ bhv = {(dep1, update), (dep2, update)} and a port goal Γ ports that maps every port instance to . The behaviors listed in that reconfiguration goal are not enough to carry it out, as it lacks a behavior to deactivate the use ports of the server prior to the update, and behaviors to reactivate all ports after the update. The synthesis process must therefore deduce necessary behaviors to carry out the reconfiguration goal, then schedule their executions in a suitable order. It proceeds as follows:

1. for each component independently, we find a sequence of behaviors that satisfies the goal, assuming that ports requirements are fulfilled (Subsection 3.1); 2. we find a global schedule for these sequences of behaviors (Subsection 3.2); 3. if the scheduling problem is found unsatisfiable, we analyze the incomplete schedule to deduce unsatisfied port requirements, compute additional reconfiguration sub-goals and iterate the process (Subsection 3.3); 4. once a feasible solution has been found, we attempt to optimize it by relaxing synchronization conditions (Subsection 3.4).

Determining Sequences of Component Behaviors

A procedure localSeq(c, act c , Γ bhv , Γ ports ) finds a sequence of behaviors that satisfies a reconfiguration goal Γ for a single component c starting in a state with active places act c . This is achieved by enumerating all sequences of behaviors with at most one occurrence of any behavior, and selecting one that satisfies the goal constraints. In practice, this enumeration is short because the number of behaviors of a component is usually small. More importantly, for a given component state (denoted by its active places), many behaviors do not have transitions originating from the active places. Since executing these behaviors would not have any effect, they can be ignored during the enumeration. Consequently, the number of useful sequences of behaviors to analyze is often much lower than the number of permutations. If no satisfying sequence is found by localSeq, then the problem has no solution, and the whole synthesis process fails. However, if multiple solutions are returned, the best possible sequence is picked, according to some (possibly user-defined) selection criterion. Some interesting optimization criteria are: the length of a sequence, its execution time (if time estimations are available for individual transitions, this may be computed with great accuracy [START_REF] Chardet | Predictable efficiency for reconfiguration of service-oriented systems with Concerto[END_REF]), the number of transitions it executes sequentially, or the number of ports it (de)activates. In our experiments, we used this last criterion, as it picks the component reconfiguration that is least likely to induce changes in other components, leading to simpler and potentially faster reconfiguration plans.

In order to coordinate sequences or behaviors across the assembly, we keep track of ports requirements and activity during each behavior of a sequence. In particular, for each behavior in a sequence, we record use ports of the component that are activated at least once by the behavior (they must be connected to an active provide port during the execution of the behavior), and provide ports that are deactivated at least once (they must not be connected to an active use port). In addition, we also record the status of each port at the end of the behavior. This information is computed with a simple traversal of the behavior graph, starting from the places that are active at the beginning of the behavior.

In the example of the update for the assembly in Figure 1, localSeq determines that components dep1 and dep2 should each execute the sequence [update, deploy]: the first behavior is included in Γ bhv and the second is required to take the components to a state that satisfies Γ ports .

Assembly-Level Reconfiguration Scheduling

Once sequences of behaviors to execute over each component have been determined, we turn our attention to the whole assembly and attempt to compute a sequence of reconfiguration commands (specifically, behavior requests and synchronization requests) that execute these behaviors. The challenge is to coordinate these behaviors in a way that satisfies all port requirements. To facilitate coordination and to restrict the search space, we specifically try to generate a reconfiguration composed of steps, such that each component executes at most one behavior per step, and each step is followed by a global synchronization request. This assumption on parallelism is reminiscent of the BSP model [START_REF] Bisseling | Parallel Scientific Computation: A Structured Approach Using BSP[END_REF]. Figure 2b gives an example of such a reconfiguration, to be compared with Figure 2a, which achieves the same result with fewer synchronization points. Fig. 2: A reconfiguration plan to perform updates on components dep1 and dep2 of the assembly in Figure 1, then restore the system to a working state.

SMT Constraints To find a reconfiguration plan, ordering constraints and port requirements are encoded as a problem in a many-sorted first-order logic (i.e., the logic is equipped with sorts that partition the domain, similarly to a simple type system), and an SMT solver is used to obtain a solution. That encoding of the scheduling problem centers around a sort Behavior, with a finite number of elements that represent the behaviors to schedule. The main task of the SMT solver is to find an interpretation for a function schedule that maps behaviors to a reconfiguration step during which to execute them. Conceptually, schedule could range over natural numbers, with behavior b executed at the ith step if i = schedule(b). However, such a model would require constraints with universal quantifiers over natural numbers, which pose a challenge for SMT solvers. It is also unnecessary, since there are only a finite number of behaviors to schedule: the number of steps required is at most the number of behaviors, when only one component executes a behavior at each step. If behaviors are executed in parallel over different components, fewer steps are required. Consequently, to improve the performance of the solver, the different steps of the reconfiguration are represented by another finite-domain sort Step, with elements step 1 , . . . step n , step final . The element step final represents the ultimate state of the system rather than a reconfiguration step. Accordingly, the scheduling function has the signature schedule : Behavior → Step, and the problem contains the constraint schedule(b) = step final for each behavior b.

A successor function succ :

Step → Step is needed to describe the effect of a reconfiguration step on the subsequent state of the system. Constraints succ(step i ) = step i+1 (for 0 i < n), succ(step n ) = step final and succ(step final ) = step final define the interpretation of succ. Likewise, to easily express sequentiality constraints, a function int : Step → Int maps each step to its step number, as defined by constraints int(step i ) = i. With this function, sequentiality is easily expressed: for any two consecutive behaviors b 1 and b 2 in the sequence of behaviors to schedule for a given component, the constraint int(schedule(b 1 )) < int(schedule(b 2 )) is added. This function reintroduces an infinite domain, which we sought to eliminate with the sort Step. However, since the problem contains no quantifiers over integers, the solver only has to check that the aforementioned formula is satisfied by a speculated interpretation of schedule. This limited form of integer reasoning has a negligible impact on the search.

The main difficulty in scheduling a reconfiguration lies in ensuring that ports requirements are satisfied for each behavior of a component. A predicate act p : Step → Bool is introduced for each (use or provide) port p to indicate the activity status of the port at the beginning of reconfiguration steps. The status of each port p after each behavior b is uniquely defined, as determined during the computation of the sequences of behaviors of the component to which the port belongs. Correspondingly, a constraint [¬]act p (succ(schedule(b))) is added to reflect that status. The square brackets denote the absence or presence of the negation, depending on whether the port is inactive or active at the end of the behavior. Conversely, the status of a port cannot change if its component is not executing a behavior. For a component with behaviors b 1 , . . . , b n , the constraint schedule(b

1 ) = step i ∧ • • • ∧ schedule(b n ) = step i =⇒ (act p (step i ) ⇐⇒ act p (succ(step i ))
) is added for every step i such that 0 i < n. Ports requirements can then be modeled. Let u be a use port that needs to be provided (i.e., connected to an active provide port) during behavior b, and p the provide port to which it is connected, the constraint act p (schedule(b)) ensures that p is active (and u provided) when b begins. Conversely, for a provide port p deactivated by a behavior b and connected to a use port u, ¬act u (schedule(b)) ensures that u is inactive when b begins. Furthermore, for any behavior b that activates a use port u and any behavior b that deactivates the connected provide port p, the constraint schedule(b) = schedule(b ) ensures that the behaviors are executed at different steps, hence separated by a synchronization barrier.

The problem3 is passed to an SMT solver. If satisfiable, the interpretation found for schedule is used to build a reconfiguration script such as in Figure 2b.

Note that the scheduling problem could be encoded as a SAT problem. However, SMT solvers can reason about the theory EUF (equality and uninterpreted functions) using a dedicated congruence algorithm. We also use (non-recursive) data types, for which some SMT solvers have a dedicated reasoning algorithm [START_REF] Barrett | An abstract decision procedure for a theory of inductive data types[END_REF], to represent the domains of Behavior and Step. These capabilities allow us to encode the problem straightforwardly and obtain solutions efficiently. Also note that the size of the scheduling problem is only a function of the number of behaviors to schedule and the number of component ports, but does not depend on the internal complexity of components, so that optimized components with several parallel transitions will not adversely affect the synthesis method.

Determining Missing Behaviors

Until now, we have considered the scheduling problem under the assumption of a fixed sequence of behaviors to schedule for each component. In general, a set of behaviors may have no feasible schedule. For example, it is not possible to fully execute the behavior update on components dep1 and dep2 of the assembly in Figure 1 without first deactivating the use ports service1 and service2 of component server, i.e., executing its behavior suspend. To plan reconfigurations for an incomplete set of behaviors, we use our SMT encoding of the scheduling problem to detect the point in the reconfiguration at which additional changes must be performed, then we create new component reconfiguration sub-problems and use the solutions to augment the sequences of behaviors to schedule.

Let S be a mapping that associates to each component a sequence of behaviors (i.e., the sequence to be executed by that component, as determined in Subsection 3.1), a maximal executable schedule S of S is a mapping that associates to each component c a prefix of S(c), such that (i) the scheduling problem corresponding to the sequences in S has a solution (ii) no reconfiguration problem built by extending a prefix in S with one behavior has a solution. Intuitively, a maximal executable schedule is a point up to which the reconfiguration S can be carried out, before unsatisfied port requirements prevent further execution.

Procedure 1 iteratively computes a maximal executable schedule S and uses the resulting information to refine the sequences of behaviors to execute for each component, until a solution is found that executes them all. By analyzing the statuses of ports in the assembly at the end of the execution of S (which depend only on the last behavior in each sequence), and comparing them to the requirements of the first unscheduled behaviors in S, we deduce a set of provide ports to activate and use ports to deactivate to allow further scheduling of S, and compute intermediary ports constraints Γ' ports . For each component c that does not have unscheduled behaviors in S, we determine a sequence s 1 of behaviors that satisfies this intermediate goal (assuming that the component starts with active places act c S corresponding to its state after executing the last behavior in S (c)) and a sequence s 2 that takes the component from its state after executing s 1 (active places act c s1 ) to one that satisfies the port constraints Γ ports of the original goal. Sequences of behaviors to execute are thus extended ([ ] denotes the empty sequence, and s 1 • s 2 the concatenation of two sequences). To ensure a monotonic search, sequences are extended only for components c without unscheduled behaviors in S, i.e., not the components that brought about the intermediary goal Γ' ports . If no such extension can be found (¬progress), the scheduling of S is blocked by a circular dependency between components and the synthesis process fails. If the procedure terminates, it returns a reconfiguration script corresponding to a solution of the scheduling problem of S.

Consider the example of running updates in the assembly of Figure 1. Initially (see Subsection 3.1), the mapping S of sequences of behaviors computed with localSeq is defined by S(dep1) = S(dep2) = [update, deploy], and S(server) = [ ], because Γ bhv does not include any behavior for that component, and the component is already in a state that satisfies Γ ports . This combination of sequences of behaviors has no feasible schedule. In particular, the mapping S that associates to every component the empty sequence is found to be a maximal executable schedule of S. The first unscheduled behaviors in S are two instances of update, they require use ports service1 and service2 of component server to be deac- The first requires it to reach a state where the two ports are deactivated, a call to localSeq returns the solution s 1 = [suspend]. From the resulting component state, the second reconfiguration sub-goal requires server to go to a state that satisfies Γ ports , in this case localSeq returns the sequence s 2 = [deploy]. S is updated so that S(server) = [suspend, deploy]. At this point, S is found to be a maximal executable schedule of itself, and the corresponding solution is returned, i.e., the reconfiguration plan in Figure 2b. Note that Procedure 1 is not guaranteed to terminate, nor is it a complete search algorithm. In particular, it relies on two heuristics: the selection function used when localSeq finds multiple candidate sequences, and the choice of maximal executable schedule for a given mapping S.

Computing a Maximal Executable Schedule Procedure 1 relies on a function findMaxExecSchedule to compute a maximal executable schedule of a mapping S, illustrated in Procedure 2, that maintains a mapping containing prefixes of elements in S (initially mapping every component to the empty sequence) and incrementally extends those prefixes, checking every time the satisfiability of the corresponding scheduling problem. This procedure calls the SMT solver to check the satisfiability of the scheduling problems. In the actual implementation, some simple checks are also used to quickly detect some trivially unsatisfiable or satisfiable instances of the scheduling problem, although these are left out of Procedure 2 for clarity. The procedure continues until all behaviors have been included or no additional behavior can be scheduled. A maximal executable schedule always exists (the mapping that associates every component to the empty sequence always has a satisfiable scheduling problem, and may be maximal), and findMaxExecSchedule always finds one. However maximal executable schedules are not unique, and a bad choice may result in an ineffective reconfiguration plan. In the example above, during the second iteration, the mapping S of sequences to schedule is defined by S(server) = [suspend, deploy] and S(dep1) = S(dep2) = [update, deploy]. S itself is a maximal executable schedule of S, but so is the mapping S defined by S (server) = [suspend, deploy] and S (dep1) = S (dep2) = [ ]. S corresponds to the case where the server is restarted too early. Picking this maximal executable schedule will ultimately lead to a reconfiguration that stops the server at least twice. To avoid this, a good heuristic for findMaxExecSchedule is to extend in priority the prefixes for which the added behavior is least likely to affect other components, i.e., those that deactivate the fewest provide ports and activate the fewest use ports.

Relaxation of Synchronization Barriers

The assumption that reconfigurations should proceed in globally synchronized steps, although useful to find a solution, severely limits the potential for intercomponent parallelism, a key feature of Concerto. A final optimization stage takes the reconfiguration plan with synchronized steps and relaxes synchronization where possible. First, every command waitAll() is replaced with a sequence of commands wait(c) for every component c that executes a behavior in the preceding step. This preserves the semantics of the reconfiguration and makes the targets of synchronization explicit. Then, for a given step i and a given command wait(c) after this step, we apply the following rule: if for all behaviors executed by c since the last command wait(c) up to step i, no provide (resp., use) port is deactivated (resp., activated) and connected to a use (resp., provide) port that is activated (resp., deactivated) at step i + 1, then wait(c) can be delayed until after step i + 1. This rule is applied for every step in order, delaying barriers as late as possible and removing duplicates. This transformation reduces the number of barriers yet ensures that behaviors with conflicting effects on ports remain separated by an explicit synchronization. Port requirements for behaviors do not have to be taken into account, as the Concerto execution model ensures implicit synchronization for those. As an example, this optimization applied to the reconfiguration plan in Figure 2b yields the one in Figure 2a.

Experiments

The implementation described here, the examples, and the experimental results are available at https://doi.org/10.5281/zenodo.5820571.

Implementation

We implemented the synthesis process in a Python tool that attempts to produce a reconfiguration script for a given assembly and reconfiguration goal. The process is entirely automated. Given a description of an assembly and a reconfiguration goal, it generates relevant scheduling problems and interacts with an SMT solver to generate reconfiguration programs. Intermediate scheduling problems can be output in the SMT-LIB file format, the standard used by most SMT solvers [START_REF] Barrett | The satisfiability modulo theories library (SMT-LIB)[END_REF], and can be solved using any solver that complies with version 2.6 of the SMT-LIB standard. The preferred mode of operation for our tool does not output files, but interacts with the SMT solver Z3 [START_REF] De Moura | Z3: An efficient SMT solver[END_REF] through the Z3 Python API. This interface makes it easy to analyze interpretations returned by the solver for satisfiable problems, and thus to reconstruct schedules. This is the mode of operation used to conduct the experiments described below.

Results Over Synthetic Examples

To test our technique on a variety of cases, we devised assemblies with four types of topology. In central-user assemblies, a set of provider components, each with a pair of provide ports, is connected to different use ports of one central user component. In central-provider assemblies, one central provider component has a pair of provide ports that is connected to (a pair of use ports of) multiple other components. In linear assemblies, components form a chain such that each component has a pair of provide ports connected to the pair of use ports of the next component. In stratified architectures, components are organized in levels containing up to three components, such that each component in a level has a pair of provide ports connected to use ports on every component in the level above (i.e., a provide port can be connected to up to three use ports). Every component in these assemblies is equipped with behaviors to deploy it, update or suspend it, and uninstall it. Figure 3 depicts those four topologies, with internal nets of components omitted for clarity. As an example of the internal structure of components, Figure 1 shows the central-user assembly with three components. For other types and sizes of assembly, components follow similar internal structures, adapted to offer adequately many ports.

For each architecture, we generated assemblies with 10, 30 and 100 components (scaling the number of providers for central-user, the number of users for central-provider, the length of the chain for linear or the number of levels for stratified ), and ran three scenarios. The deployment scenario starts with all components uninstalled, Γ ports requires the activation of a provide port on the last component(s) in the dependency order, while Γ bhv is empty. The update scenario starts with all components running, Γ ports requires a similar final state, and Γ bhv includes update behaviors for components that are first in the dependency order and no behavior for the others. The uninstall scenario starts with all components running, Γ ports requires the deactivation of all ports, while Γ bhv is empty. Each scenario affects every component of the assembly. Table 1 describes the solving process and resulting solution for these 36 examples. Experiments were executed on a computer with an 8-core 1.6GHz processor and 16 GiB of RAM. Solutions were successfully generated for all but 4 examples (the process was aborted after one hour). For 21 of them, the process took less than a minute. Results indicate that the solving time, and ultimately the success of the method, depend on the topology of the assembly: the assemblies for which some reconfigurations could not be computed within one hour are those with long chains of dependencies (linear and stratified assemblies with 100 components). This can be explained in two ways: firstly, the propagation of port requirements and the deduction of missing behaviors requires a number of iterations of the main loop of Procedure 1 proportional to the length of the longest chain of dependency. Secondly, architectures with long chains of dependencies are less conducive to parallel execution of behaviors, and therefore the instances of scheduling problems solved have a high number of steps, leading to a large search space and long solving times. For example, the deployment of 100 component in the linear architecture ultimately requires 100 steps. For each of the 17 instances of the scheduling problem solved to compute that reconfiguration, the SMT solver took on average 147 seconds to return a solution. In contrast, to deploy 100 components in the central-user architecture, the reconfiguration script requires only 2 steps, as a result the SMT solver was able to return a solution after only 0.21 seconds on average each time it was called. For difficult problems, the solving time is dominated by calls to the SMT solver as shown in the solving time column of Table 1 (in parentheses, the cumulated time taken by the SMT solver). Overall, these examples show that our method is able to plan reconfigurations affecting large number of components. Furthermore, architectures with a very large number of components, such as microservice architectures, typically have a shallow depth rather than long chains of dependencies, and scale horizontally [START_REF] Kratzke | Understanding cloud-native applications after 10 years of cloud computing -a systematic mapping study[END_REF][START_REF] Nadareishvili | Microservice Architecture[END_REF][START_REF] Taibi | Architectural patterns for microservices: A systematic mapping study[END_REF], similarly to our central-user and central-provider architectures. Our method scales well in those conditions.

Writing a correctly coordinated reconfiguration plan with tens of asynchronous behaviors is a non-trivial task. It is particularly difficult when explicit synchronizations commands are needed in the reconfiguration script. The execution model of Concerto ensures that this is seldom necessary, but some synchronization barriers are required, e.g., in the update scenarios to prevent early restarts that would block the updates. Our synthesis technique determines synchronization points required for completion of the reconfigurations, but it also avoids synchronization points that would slow the execution unnecessarily. It performs these tasks quickly, with a time gain that is especially significant when compared to the service interruption that an incorrect reconfiguration would cause.

OpenStack Use Case

We also tested our method on a real OpenStack system. OpenStack is the de facto standard open-source solution to address the IaaS level of the cloud paradigm, it can be seen as the open-source operating system of the cloud.

In previous work [START_REF] Chardet | Enhancing separation of concerns, parallelism, and formalism in distributed software deployment with Madeus[END_REF], Madeus, a subset of Concerto restricted to deployment, was used to deploy an OpenStack system. Following the deployment strategy of the reference production deployment tool Kolla, 11 components were specified, resulting in a real OpenStack deployment up to 70% faster than Kolla. Here we use the same components, extended with behaviors for reconfiguration. We analyzed the official installing, updating and uninstalling procedures of OpenStack to design the associated internal nets. Figure 4 depicts those components and their connections, with details of the internal structure depicted for the four main components, and omitted for clarity on seven others. The reconfiguration starts with all components running. The reconfiguration scenario requires an update of the database component (Γ bhv = {(mariadb, update), (mariadb, deploy)}) and Γ ports specifies that all ports must eventually return to their initial (active) state. Our method generates a reconfiguration plan in 1.95 seconds, correctly deducing ) its number of components (size), the number of problems solved by the SMT solver (smt) followed in parentheses by the number of those that were found satisfiable, the total solving time in seconds followed in parentheses by the cumulated time taken by the SMT solver (time), the number of steps in the solution before relaxation of the synchronization barriers (steps), and the number of behaviors executed in that solution (bhvs). missing behaviors for mariadb as well as components affected by the interruption of its service, i.e., keystone, nova, neutron, and glance. The generated plan coordinates 12 behaviors on these 5 components. After optimization, it includes only 2 synchronization points needed to ensure the complete re-deployment of mariadb and keystone, whose services are required by other components.

While the scale of this use case may seem limited, its architecture is not trivial. This real-world scenario leads to a complicated synchronization problem. The 12 behaviors in the reconfiguration program require 8 global synchronization steps before optimization. The optimization phase reduces this to 2 individual synchronization points, thus enhancing the level of parallelism and asynchrony of the reconfiguration program, while preserving its correctness. A DevOps engineer or system administrator would be challenged to write such a program without errors or unnecessary synchronization points, whereas our solution only requires them to specify a reconfiguration goal.

Related work

For models with fixed component life cycles, planning and scheduling techniques have been used to plan reconfigurations [START_REF] Arshad | Deployment and dynamic reconfiguration planning for distributed software systems[END_REF][START_REF] El Maghraoui | Model driven provisioning: Bridging the gap between declarative object models and procedural provisioning tools[END_REF]. Pre-established protocols can also be used: while such solutions are in general less flexible, they have desirable features such as decentralized coordination [START_REF] Etchevers | Self-configuration of distributed applications in the cloud[END_REF] or recovery policies [START_REF] Boyer | Robust reconfigurations of component assemblies[END_REF]. Comparatively fewer works study the problem of reconfiguration planning in models with programmable component life cycles, such as Concerto. Kikuchi et al. [START_REF] Kikuchi | Synthesis of configuration change procedure using model finder[END_REF] synthesize reconfiguration plans with a model finder. Unlike us, they assume that all available reconfiguration operations are given in the input of the scheduling problem, which may limit scalability. Operations and reconfiguration goal are encoded in the Alloy specification language, and synthesis is performed by the Alloy Analyzer. This work relies on a simple ad hoc component-based model, with reconfiguration operations that must be sequentially ordered. The model does not have specific execution semantics, instead the list of operations has to be given by the user, with their effects described as constraints on the states before and after the operations. Therefore the correctness of the correspondence between the synthesized procedure and its executable counterpart depends on the user. Metis [START_REF] Lascu | A planning tool supporting the deployment of cloud applications[END_REF] closes that gap between planning and execution, as it schedules deployment plans for distributed systems in the Aeolus model [START_REF] Di Cosmo | Aeolus: A component model for the cloud[END_REF], which has formal execution semantics. The authors first describe the problem as a generic planning problem and use standard planners to solve it, then present a specialized solving algorithm. Metis is limited to deployment rather than general reconfiguration, making the computation of dependencies more straightforward. Aelous shares many similarities with Concerto, but lacks intra-component parallelism and asynchronous commands in its reconfiguration language. These features improve the efficiency of reconfigurations but also make them more difficult to plan. Note that these features can also be represented through planning and scheduling problems [START_REF] Keller | The CHAMPS system: Change management with planning and scheduling[END_REF], typically solved by approximation.

The problem of determining reconfiguration goals (i.e., the analysis phase) is complementary to the planning problem. Engage [START_REF] Fischer | Engage: A deployment management system[END_REF] uses a SAT solver to build a complete target configuration (a set of components to deploy) from a partial specification, based on a hierarchical specification of a distributed software stack. It also performs limited planning, namely sequentially ordering deployments. Engage does not account for the state of the system, and is thus limited to initial deployments or reconfigurations from the ground up. Zephyrus [START_REF] Di Cosmo | Automated synthesis and deployment of cloud applications[END_REF] and ConfSolve [START_REF] Hewson | A declarative approach to automated configuration[END_REF] are two tools to infer, from the state of the system/environment, a target configuration that could be used as an entry of our planning tool.

Conclusion

We have described a synthesis method for reconfiguration plans of componentbased systems, that relies on (i) finding local solutions at the component level, (ii) finding a schedule that coordinates those solutions at the assembly level, with the help of an SMT solver, (iii) determining unsatisfied dependencies to refine the reconfiguration goal until it becomes satisfiable, and (iv) optimizing the synthesized reconfiguration plan to improve its level of parallel and asynchronous execution. Dividing the problem in this manner, as opposed to attempting to solve it at once with an SMT solver, is a key to solving large instances, although it leads to incompleteness (the third step relies on an incomplete search guided by some heuristic choices). This design decision does not appear to affect the success of the method or the quality of synthesized plans, and allows the technique to scale to applications with large number of components, as demonstrated in our experiments on synthetic examples and a real use case. To improve scalability on complex architectures, this technique could be adapted to a hierarchical composition model, which would lend itself to a recursive resolution algorithm. components are used in the central-provider and linear architectures, and parallel user components are used in central-user and stratified architectures. Parallel user components can be scaled to offer p pairs of use ports, to accommodate the architecture. The internal net is adapted accordingly with p places suspended and sconf. Recall that the internal structure of components does not affect the complexity of scheduling problems, and that the time required for synthesis is dominated by the solving of these problems.

For some instances of user and parallel user components in the assemblies, the provide ports are not connected to other components (and not shown in Figure 3). All other component ports are connected in the assemblies.

Fig. 1 :

 1 Fig.1: A Concerto assembly with three components. For readability, the bindings of ports config1 and config2 are only partially depicted: they also contain places configured, running, s1 and s2.

  Procedure globalSolution(A, Γ bhv , Γports ) is for c ∈ A do S(c) ← localSeq(c, act c A , Γ bhv , Γports ); while findMaxExecSchedule(S) = S do S ← findMaxExecSchedule(S) ; Γ'ports ← port conditions required to execute, for every component c, the first behavior in S(c) that is not in S (c); progress ← false ; for c ∈ A such that S (c) = S(c) do s1 ← localSeq(c, act c S , Γ bhv \S (c), Γ'ports ) ; s2 ← localSeq(c, act c s 1 , ∅, Γports ) ; if s1 = [ ] or s2 = [ ] then S(c) ← S (c) • s1 • s2 ; progress ← true ; end end if ¬ progress then fail ; end return reconfigurationScriptOfSolution(S) ; end Procedure 1: Synthesizes a reconfiguration script. tivated. Consequently, two new reconfiguration sub-goals are created for server.

Procedure 2 :

 2 Procedure findMaxExecSchedule(S) is suffixes ← S ; for c such that suffixes(c) is defined do prefixes(c) ← [ ]; progress ← true ; while progress do progress ← false ; for c such that suffixes(c) = [ ] do b ← head (suffixes(c)) ; if the scheduling problem for prefixes extended with b is satisfiable then progress ← true ; prefixes(c) ← prefixes(c) • [b] ; suffixes(c) ← tail (suffixes(c)) ; end end end return prefixes ; end Computes a maximum executable schedule for sequences of behaviors S.

Fig. 3 :

 3 Fig. 3: The four assembly topologies in synthetic examples.

Fig. 4 :

 4 Fig. 4: A Concerto assembly for an OpenStack system.

Fig. 5 :

 5 Fig. 5: The components used in synthetic benchmarks.

Table 1 :

 1 Results of the synthesis process on synthetic examples. For each problem, the table indicates the architecture of the assembly and (arch.

		assembly		solving	plan
		arch. size smt	time (s)	steps bhvs
			10 2 (2)	0.25 (0.02)	2	10
		c-user	30 5 (5)	1.99 (0.18)	2	30
			100 17 (17)	23.94 (3.59)	2 100
	deployment	c-provider linear	10 2 (2) 30 5 (5) 100 17 (17) 10 2 (2) 30 5 (5)	0.33 (0.08) 3.95 (1.80) 93.07 (68.67) 0.40 (0.08) 9.19 (4.27)	2 2 2 100 10 30 10 10 30 30
			100 17 (17) 2689.86 (2512.22) 100 100
			10 3 (3)	0.64 (0.09)	5	10
		stratified	30 6 (6)	12.04 (5.28)	12 30
			100 18 (18) 1274.52 (1121.40) 35 100
			10 6 (5)	1.69 (0.78)	4	20
		c-user	30 12 (11)	25.07 (18.59)	4	60
			100 36 (35) 1737.29 (1654.67) 4 200
			10 13 (4)	1.79 (0.41)	4	20
	update	c-provider	30 40 (11) 100 133 (34) 685.54 (541.69) 22.98 (9.97) 10 50 (5) 12.72 (3.26)	4 4 200 60 20 20
		linear	30 446 (11) 1388.50 (825.06) 60 60
			100	-	-	-	-
			10 20 (6)	14.55 (5.82)	13 26
		stratified	30 147 (16) 2306.85 (1885.17) 34 86
			100	-	-	-	-
			10 3 (3)	0.54 (0.14)	3	11
		c-user	30 6 (6)	6.01 (2.76)	3	31
			100 18 (18) 162.51 (125.51)	3 101
	interruption	c-provider linear	10 4 (4) 30 10 (10) 100 34 (34) 571.73 (514.48) 0.91 (0.30) 12.36 (7.25) 10 10 (10) 1.30 (0.19) 30 30 (30) 39.31 (13.69)	3 3 3 199 19 59 10 10 30 30
			100	-	-	-	-
			10 4 (4)	2.50 (1.10)	9	19
		stratified	30 11 (11) 132.59 (108.53) 23 59
			100	-	-	-	-

Illustrating instances for the running example, in the SMT-LIB file format, can be found at https://doi.org/10.5281/zenodo.5820571.

Appendix A Algorithm to find a sequence of behaviors for a single component Procedure 3: Finds a sequence of behaviors that satisfies the reconfiguration goal for a component c.

Procedure 3 shows how a sequence of behavior that satisfies a goal for a single component c is found: enum recursively enumerates sequences of behaviors, it returns the set of sequences that include requested behaviors and ensure that the component finishes in a state that satisfies the port constraints. The argument seq denotes the sequence being analyzed, act denotes the active places after the execution of that sequence, bhvs is the set of candidate behaviors whose permutations remain to be tested, Γ' bhv denotes the behaviors that remain to be included in the sequence to satisfy the goal, and Γ' ports the port conditions to satisfy. bestSolution return the best sequence in a set, according to some (possibly user-defined) optimization criterion. Solutions returned by localSeq are valid under the assumption that all ports requirements are eventually satisfied by the other components connected to those ports, hence Procedure 1 may call localSeq multiple times with refined reconfiguration goals for a component c.

Appendix B Internal structure of components used in synthetic benchmarks

Figure 5 describes the three types of components used in the synthetic benchmarks of Section 4.2. Provider components are used in all four architectures, user


Alexandre De Bernardinis
email: alexandre.de-bernardinis@univ-lorraine.fr

Richard Lallemand
email: richard.lallemand@univ-eiffel.fr

Abdelfatah Kolli
email: abdelfatah.kolli@gmail.com

Highly efficient bidirectional Silicon Carbide power converter for Electric Vehicle flywheel emulator

Keywords: DC/AC Converter, Electric Vehicle, Flywheel, MOS Field Effect Transistor, Pulse Width Modulation, Silicon carbide

Flywheels are nowadays a solution for the dynamic charging of electric vehicles since they act as transient energy storage. The need of a top efficient reversible power converter for the flywheel system is crucial to assure high dynamic performance. The paper presents the design of a 50kW highly efficient bidirectional three-phase DC-AC inverter involving most recent Silicon carbide metal oxide semiconductor field effect transistors and its experimental validation on home-made emulator. Highest efficiency in reversible mode, compactness and thermal enhancement are the target objectives that have been achieved. The converter prototype is evaluated on an original Pulse Width Modulation testing-bench able to emulate the working of the flywheel system. High frequency Pulse Width Modulation switching, speed cycle operating and thermal losses are evaluated. Also an efficiency above 99% for the converter has been attained, enabling a robust functioning of the flywheel system emulator able to perform specific charging profiles.

INTRODUCTION

Among recent developments in energy storage techniques cited by [START_REF] Amirante | Overview on recent developments in energy storage: Mechanical, electrochemical and hydrogen technologies[END_REF], Flywheel Energy Storage System (FESS) is an electromechanical energy storage system which can exchange electrical power with the electric network [START_REF] Khodadoost Arani | Review of Flywheel Energy Storage Systems structures and applications in power systems and microgrids[END_REF]. It consists in an electrical machine, DC-AC converter, DC link capacitor and a massive (steel or composite materials) disk. Unlike other storage systems such as the Battery Energy Storage System (BESS), FESS is an environmentally-friendly short-or medium-term energy storage system, which has the capability of numerous charge and discharge cycles. These characteristics make the FESS a suitable choice for different applications in the power system such as power quality improvement, power smoothing, renewable energies integration support, stability improvement, etc. Flywheel Energy Storage System (FESS) can hence be applied in various domains, from very small micro-satellites to huge power networks as reported by [START_REF] Mousavi | A comprehensive review of Flywheel Energy Storage System technology[END_REF]. Energy storage systems (ESS) with ultra-long lifetime of over twenty years using matrix converters and flywheels to compensate frequency and voltage fluctuations for the power grid are solutions to be considered [START_REF] Kato | Loss evaluation of matrix converters using SiC-MOSFETs for flywheel energy storage systems[END_REF][START_REF] Kato | Ultra Long Lifetime Energy Storage System using Flywheels and Matrix Converters[END_REF]. Flywheels have the advantage of providing maintenance-free for over twenty years. Also flywheels sometimes involve the use of superconductor materials dedicated for high speed devices as stated in [START_REF] Guettafi | Modelling and simulation of an association magnetmultifilamentaries superconductors as spherical bearing for an inertial flywheel with high speed[END_REF], and behave as dynamic energy storage systems for residential microgrids and for power management in electric vehicles (EVs) as recovering the braking energy [START_REF] Wang | Optimization and control of battery-flywheel compound energy storage system during an electric vehicle braking[END_REF][START_REF] Barelli | Comparative analysis of AC and DC bus configurations for flywheel-battery HESS integration in residential micro-grids[END_REF], for the control and stability of the grid voltage involving specific control laws and strategies. There are three main devices composing a FESS, including the AC machine as Permanent Magnet Synchronous Motor (PMSM), bearing, and power electronics interface which technology can be based on Silicon carbide (SiC) devices, alike SiC MOSFETs, or JFET body diodes [START_REF] Ben Salah | Modelling, analysis, and experimental study of SiC JFET body diode[END_REF] for attaining highest efficiency, compactness and thermal enhancement. The manuscript is a post IEEE ITEC 2017 contribution for which a first approach of the work has already been published by authors [START_REF] Bernardinis | High efficiency Silicon carbide DC-AC inverter for EV-charging Flywheel system[END_REF]. The present manuscript focuses on a progress of the previously published work, including novel achieved results in particular, the calculation of the electro thermal highest efficiency of the SiC power inverter for usage profiles, and the dynamic evaluation of the converter on a homemade emulator that reproduces in laboratory the technological behavior of a flywheel energy storage system (FESS) dedicated to electric vehicle recharging. The purpose of this paper is to propose the concept and realization of an originally-designed bidirectional 50kW three-phase DC-AC inverter with novel Silicon carbide (SiC)-based MOSFETs transistors technology used for the power supply of a flywheel energy storage system dedicated to electric vehicles charging. The research work, which is mainly experimental, provides real technological innovation, in both designs the power converter itself and the hardware emulator since they utilize the most recent wide band-gap silicon carbide semiconductors, and original robust control strategy. The work is carried-out in the framework of the French "VIVE" project supported by the French ministry of Industry and Region of Paris-Île de France. Highest efficiency in reversible mode, compactness and thermal enhancement are the target objectives and research highlights for the converter prototype. The three-phase DC-AC Silicon carbide inverter prototype is tested on an original home-made PWM test-bench which semiconductor switches are controlled using the modulated hysteresis controller and which is able to emulate the working of the PMSM -flywheel system. High frequency PWM tests, design aspects for the DC busbar, speed cycle operating and thermal losses are evaluated. Adopted design for realization and control strategy should permit to reach the highest efficiency for the DC-AC inverter. The paper is organized as follows: In section II a recent literature overview is proposed on Flywheel energy storage systems and Silicon carbide converters used as power electronics supply for FESS. Section III focuses on the SiC-based DC-AC inverter design for EVcharging Flywheel system. Section IV presents experimental pulse width modulated (PWM) switching tests, interface driver card design for the SiC MOSFETs switches and DC Bus hardware design. Section V deals about the experimental validation for the SiC DC-AC inverter implemented on the original, and modular, double-converter PWM test bench controlled using the modulated hysteresis method. Finally section V ends with the evaluation of static, then speed cycle thermal losses and calculation of SiC DC-AC inverter efficiency.

II. LITERATURE SURVEY

This section describes a literature overview on Flywheel Energy Storage Systems (FESS) and Silicon carbide power converters. It starts with power electronics topologies feeding FESS, and 3 then enumerates any applications of the Flywheel technology as energy storage device in several domains. Examples of research works and realizations is this field are given hereafter. A bidirectional converter (BDC) is essential in applications where energy storage devices are involved. Such applications include transportation, battery less uninterruptible power system, flywheel energy storage systems, etc. Bidirectional power flow through buck and boost modes of operation along with high power density and efficiency is an important requirement of such systems. A novel BDC topology using a combination of fast turn-off Silicon controlled rectifier (SCR) and Insulated-gate bipolar transistor (IGBT) with a novel control logic implementation to achieve zero switching losses through zero voltage transition and zero current transition techniques has been designed by [START_REF] Salinamakki Ramabhatta Gurumurthy | High-Efficiency Bidirectional Converter for Flywheel Energy Storage Application[END_REF]. According to [START_REF] Amodeo | High-performance sensorless nonlinear power control of a flywheel energy storage system[END_REF], Flywheel energy storage systems (FESS) can be used to store and release energy in high power pulsed systems. Based on the use of a homopolar synchronous machine driving a FESS, a high performance model-based power flow control law has been developed by S.J. Amodeo et al. using the feedback linearization methodology. To reduce the magnetic losses, a pulse amplitude modulation driver for the armature is more adequate. The restrictions in amplitude and phase imposed by the driver are also included. A full order Luenberger observer for the torque angle and rotor speed is developed to implement a sensorless control strategy. In [START_REF] Salinamakki Ramabhatta Gurumurthy | A Novel Dual-Winding BLDC Generator-Buck Converter Combination for Enhancement of the Harvested Energy From a Flywheel[END_REF] a novel flywheel energy storage system is proposed which results in up to 20% enhancement in the harvested energy from the flywheel, in comparison with the existing systems. Generally, boost converters are used for boosting the voltage in such systems. Major limitation of a boost converter is the dependency of its maximum achievable voltage gain on the ratio of its source resistance to load resistance which limits the amount of harvested energy from a flywheel and lowers the efficiency at low input voltages. In [START_REF] Koos Van Berkel | Topology and Flywheel Size Optimization for Mechanical Hybrid Powertrains[END_REF] Koos van Berkel et al. state that mechanical hybrid powertrains have the potential to improve the fuel economy of passenger vehicles at a relatively low cost, by adding a flywheel and only mechanical transmission components to a conventional powertrain. This paper presents a systematic approach to optimizing the topology and flywheel size, which are the key design parameters of a mechanical hybrid powertrain. The topology is optimized from a limited set of over twenty existing mechanical hybrid powertrains described in the literature. After a systematic classification of the topologies, a set of four competitive powertrains is selected for further investigation. The fuel-saving potential of each hybrid powertrain is computed using an optimal energy controller and modular component models, for various flywheel sizes and for three certified driving cycles. The hybridization cost is estimated based on the type and size of the components. Other criteria, such as control complexity, clutch wear, and driving comfort are qualitatively evaluated to put the fuel-saving potential and the hybridization cost into a wider perspective. Results show that, for each of the four investigated hybrid powertrains, the fuelsaving benefit returns the hybridization investment well within (about 50%) the service life of passenger vehicles. The optimal topology follows from a discussion that considers all the optimization criteria. The associated optimal flywheel size has an energy storage capacity that is approximately equivalent to the kinetic energy of the vehicle during urban driving (50 km/h). Fast charging stations (FCS) are able to recharge plug-in hybrid electric vehicles (pHEVs) in less than half an hour, thus representing an appealing concept to vehicle owners since the off-road time is similar as for refueling at conventional public gas stations [START_REF] Rafi | A Comprehensive Review of DC Fast-Charging Stations With Energy Storage: Architectures, Power Converters, and Analysis[END_REF]. However, since these FCS plugs have power ratings of up to 100 kW, they may expose the utility mains to intolerable stresses in the near future scenario where there will be a large number of public FCS spread across the network. Authors of paper [START_REF] Rafi | A Comprehensive Review of DC Fast-Charging Stations With Energy Storage: Architectures, Power Converters, and Analysis[END_REF] proposes a comprehensive review of DC Fast-Charging Stations with Energy Storage: Architectures, Power Converters, and Analysis. In [START_REF] Sun | A Control Algorithm for Electric Vehicle Fast Charging Stations Equipped With Flywheel Energy Storage Systems[END_REF] authors proposes a control strategy for plug-in electric vehicle (PEV) fast charging station (FCS) equipped with a flywheel energy storage system (FESS). The main role of the FESS is not to compromise the predefined charging profile of the PEV battery during the provision of a hysteresis-type active power ancillary service to the overhead power system. In that sense, when 0219-3 the active power is not being extracted from the grid, an FESS provides the power required to sustain the continuous charging process of the PEV battery. A key characteristic of the whole control system is that it is able to work without any digital communication between the grid-tied and FESS converters. The presented experimental results have proved the high accuracy of the theoretical analysis. In [START_REF] Noppakunkajorn | Analysis of High-Speed PCB With SiC Devices by Investigating Turn-Off Overvoltage and Interconnection Inductance Influence[END_REF] Silicon (Si) carbide (SiC)-based power switching devices provide significant performance improvements compared to conventional Si devices. The superior characteristics enable considerable loss, size, and weight reduction of power converters in the powertrain of hybrid/electric vehicles. However, the fast switching capability of SiC devices renders them more vulnerable to parasitic inductances in the circuit. Hence, the impact of interconnection inductances to overvoltage during turn-OFF transient of SiC devices should be taken into account.

III. SILICON CARBIDE DC-AC INVERTER FOR EV FLYWHEEL CHARGING SYSTEM

As stated in Section II in the review, Flywheels energy storage systems (FESS) are also nowadays becoming more and more potential candidates for utilization as hybrid-storage sources in association with batteries within electric cars. As an example, the active electromagnetic slip coupling kinetic energy recovery system is potentially a cost-effective, yet efficient method for energy transfer between a vehicle and a lightweight flywheel, presented by [START_REF] Ershad | Development of a Kinetic Energy Recovery System Using an Active Electromagnetic Slip Coupling[END_REF]. According to the authors, the proposed kinetic energy recovery system (KERS) may be less costly and less complex than flywheel-batteries as it needs only one electrical machine and one power electronic converter. Moreover, the storage system is capable of recovering much more mechanical power than its electrical ratings. Furthermore, since a great part of the energy exchange takes place in mechanical form, only a fraction of the captured energy needs to be processed by the power electronic converter. Also, the research described in [START_REF] Tang | Novel Torsional Vibration Modeling and Assessment of a Power-Split Hybrid Electric Vehicle Equipped With a Dual-Mass Flywheel[END_REF] is aimed at exploring the effect of a dual-mass flywheel on the torsional vibration characteristics of a power-split hybrid powertrain. Other recent research works presented by authors themselves concern two front wheel-motor drives [START_REF] Itani | Comparative analysis of two hybrid energy storage systems used in a two front wheel driven electric vehicle during extreme startup and regenerative braking operations[END_REF], the dynamic recharging of electric vehicles, or for their use as reversible dynamic power sources for EV recharging stations. The work presented in this paper is part of the French VIVE project (VIVE: "Volant d'Inertie pour Véhicules Electrifiés") coordinated by AER-Atmostat Company, with the supports of the French ministry of Industry and Region of Paris-Île de France in the framework of the FUI (Fonds Unique Interministériel) grant agreement, which objective is to realize, characterize, and implement a flywheel system from AER-Atmostat for EV-charging [START_REF] Bernardinis | High efficiency Silicon carbide DC-AC inverter for EV-charging Flywheel system[END_REF]. From the general powertrain shown in Fig. 1, the presented study concerns the three-phase interface DC-AC inverter (in dashed red lines in Fig. 1), connected to the variable DC bus (580V up to 620V) and supplying the 60kW-Neodymium Iron Boron Permanent magnet synchronous motor (PMSM), 8 poles, whose frequency of the fundamental voltage varies in the range of 100 Hz to 400 Hz depending on the rotor mechanical speed (3.000 to 6.000 rpm). The Flywheel system with its PMSM motor/generator, and interface inverter is connected through the DC bus to a 3-phase reversible converter ensuring current reinjection/supply with the 380V/ 50Hz grid network and connected to a mixed DC-AC 3-phase plant for EV-dynamic recharging. A 2-level control strategy is used for the powertrain control. Level 1 deals with supervision, security issues, having as inputs the different use-case scenarios (named as macroscopic level). Level 0 (close-up control level) includes the control strategy in (d,q) Park reference frame for the three-phase PMSM currents and provides through a Real-Time prototyping system the PWM signals to the gates of the 3-phase DC-AC inverter transistors. DC voltage security limit up to VDCmax = 700V is added for the inverter protection.

0219-4

In the FESS a three-phase resistive bloc (named security resistors) has been added at the input stage of the motor-flywheel system (Fig. 1), enabling the flywheel energy discharge in case of emergency situation, in twelve minutes approximately. For designing the DC-AC inverter prototype and meet the research objectives, Silicon carbide (SiC) MOSFETs in a 1200V/300A Half-Bridge configuration have been chosen from the newest market technology. The goal is to have a high efficiency, compactness and thermal performance for the DC-AC power converter solution, in order to meet industrial challenges for the civil implementation of the EV-charging Flywheel energy storage system. The objective is to reach the highest efficiency in both reversible energy flows for the 60 kW Flywheel/PMSM/inverter system. For switching constraints, up to 100 kHz (max) driver card have been used.

IV. PWM SWITCHING CHARACTERISTICS AND TESTS

The layout of the paper should follow the style of this document, starting with a title, name(s) of author(s) and affiliation(s).

Experimental switching tests for the SiC MOSFETs Figures 5a) and 5b

) respectively present the switching ON (a) and OFF (b) waveforms for 20kHz frequency performed on the SiC MOSFETs devices. Oscillations amplitude phenomena, in particular for turn-off, have been attenuated using a 2µF snubber capacitor connected in parallel to the MOSFETs Half-Bridge. Turn-On time is 300ns, turn-off about 400ns. Losses and efficiency for the DC-AC inverter will be given in Section 5.3. Numerical acquisitions have been done using oscilloscope Lecroy Wave runner HRO64i, the Vds measurement with sensor PM9100, Ids measure using shunt LEM25 10mΩ, and Vgate with Tektro P5050 recorder. Laboratory experimental test bench equipment permits to reproduce high frequency PWM control signals applied to the SiC MOSFET Half-Bridge. Figure 7 shows PWM gate control signals, and focus on the AC-phase current. Picture denotes that the current is accurately controlled without any disturbances. First, to be operated, the OCP (Over Current Protection) mode of the driver card should be deactivated, then the driver card is supplied in 24VDC and the waveforms are acquired on the digital Yokogawa© high speed scope recorder. The yellow waveform in Fig. 6b) represents the control signal injected in the HCPL-3120 optocouplers, the green curve represents the input voltage of the LS (Low side) driver card and is between 1.5 V and -2 V. The purple curve is the HS (High side) part of the driver (2 V). Finally the red waveform highlights the MOSFET voltage of the LS part of SiC module, it should be noted we obtain +20V for the ON state and -6 V for the OFF state. We should however notice that there appears a phaseshift between the input of the driver card and the output gate control signal of LS MOSFET.

The measured delay is Toff_fall= 250 ns, the manufacturer's data of the driver card estimates the Toff_fall between 250 and 300 ns, hence there is a good concordance. We also measured the Toff_rise = 610 ns. The manufacturer's data gives a Toff_rise between 400 and 500 ns.

We have hence validated the switching operating of a SiC Half-bridge and have realized the complete interface card design for the 3 legs.

V. EXPERIMENTAL VALIDATION

Original reversible PWM double-converter tester for hardware emulator

The proposed hardware emulator architecture is original, it has been completely home-made designed in the laboratory. It is composed of two bi-directional converter, the "tester" composed of 3 IGBT/Diode Silicon PWM half-bridges based on Infineon semiconductor technology EconoDUALTM FF450R12ME3 (1200V, 450A) with trench/fieldstop IGBT3 and emitter controlled high efficiency diode (Right side in Fig. 11), and the SiC CREE ® CAS300M12BM2 (1200V, 300A) DC-AC PWM inverter under test (DUT) (Left side in Fig. 9).

0219-8

2 1 V V . 2 1 d DC * mod + = (1)
The tester IGBT/diodes inverter is current controlled. The three phase currents (Ia, Ib, Ic) which represent the PMSM phase currents are controlled using an original modulated hysteresis current controller (HCC), as shown in Fig. 10a), based on the modulated hysteresis method, which is detailed hereafter. The switching frequency F is synchronized with the frequency Fs of the DUT SiC inverter, with a limitation up to Flim ≤ 50 kHz maximum. The output of the modulated hysteresis controller provides the gate duty cycles for the Infineon IGBTs semiconductors (ha, hb, hc, ha, hb, hc). Different load current cycles can be imposed thanks to the IGBT tester, and representative of motor behavior. In the studied flywheel emulator application, the fundamental modulation frequencies are imposed from 200 Hz to 400 Hz, emulating the motor speed (3000 to 6000 rpm). The principle of the testing bench is original; hence it enables the possibility to test all types of DUT inverters, and further to investigate the ageing mechanisms of the semiconductors under specific dynamic PWM constraints.

Original reversible PWM double-converter tester for hardware emulator

In order to control the IGBT/Diode "tester" converter, playing the role of a PMSM emulator, the modulated hysteresis technique has been employed. The principle of this method is detailed and explained in the following paragraph. An adaptive hysteresis-band control method where the band is modulated with the system parameters in order to maintain the modulation frequency to be nearly constant is presented by B.K. Bose in [START_REF] Bose | An adaptive hysteresis-band current control technique of a voltage-fed PWM inverter for machine drive system, Industrial Electronics[END_REF]. Although the technique is applicable to general AC motor drives and other types of load, the modulated hysteresis method permits to impose the switching frequency of the IGBTs transistors. The hybrid controller, called "modulated hysteresis" controller, combines in one hand the robustness properties of a hysteresis controller and on the other hand the zero static error of a linear proportional integral (PI) controller. In addition, it allows the fixed frequency operation of the converter. It ensures high dynamic response with a fixed-frequency operation mode, a zero static error, and high robustness properties with respect to system parameters variations as shown in [START_REF] Bose | An adaptive hysteresis-band current control technique of a voltage-fed PWM inverter for machine drive system, Industrial Electronics[END_REF]. The principle of the method consists in superimposing to the reference current (iref*) a modulated triangular signal (itr) having adequate amplitude Atr and desired frequency ftr (Fig. 10b). We obtain then a modulated reference current (imod*), which constitutes the new reference for the current control loop as given by Equ. 2.

tr ref mod i * i * i + = (2)
A judicious choice for Atr and the hysteresis bandwidth Bh impose the switching frequency of the IGBTs transistors equal to that of the triangular signal one. It should be noted that the chosen switching frequency is a compromise between the current ripple rate and the switching losses. Indeed, a higher switching frequency value increases the switching losses of the transistors impacting negatively the global converter efficiency, and on the contrary, for a given "phaseinductance" value, a too small switching frequency creates an important current ripple, which can cause electrical constraints on the semiconductor switches. The modulated hysteresis method is robust, needs only a few parameters in order to be implemented (DC-link voltage source amplitude, the cyclic inductance of the PMSM machine and the desired switching frequency). Moreover the knowledge of a precise model for the PMSM machine is not necessary. Results of previous studies concerning the modulated hysteresis method in the motor operatingmode show that the sum (Atr + Bh) should verify inequality (3) in order to impose the switching frequency of the transistors equal to that of the triangular signal one:

tr DC h tr f L V B A . . 4  + (3)
When using these parameters, the dynamic of the phase current during the commutations is improved and becomes close to that of the current when the classical hysteresis method is applied. Moreover the modulated hysteresis method has still the advantage of a constant switching frequency for the IGBTs transistors. Concerning the modulated hysteresis method, M.A. Shamsi Nejad et al. in [START_REF] Bose | An adaptive hysteresis-band current control technique of a voltage-fed PWM inverter for machine drive system, Industrial Electronics[END_REF] exposed the modeling and study of this new hybrid current controller. It ensures high dynamic response with a fixed-frequency operation mode, a zero static error, and high robustness properties in regard to system parameters variations. To model the proposed nonlinear current controller, different modeling tools have been developed by the authors. In a first step, a high-frequency average model is proposed. It allows studying the average dynamic properties (bandwidth, time response, and overflow) of the method. To investigate the behavior of the current ripple due to the switching effect, a second model, based on the construction of a 3D bifurcation diagram and the definition of a form function, is established. This model allows studying the nature of the cycle described by the state trajectory and proving that the system operates with a fixed switching frequency. Design rules of the control parameters of this controller are explained and its robustness properties are tested by numerical simulations and validated by experimental tests. Fig. 11 shows the global testing bench: DC-AC SiC inverter connected to the IGBT/Diode tester, developed at SATIE laboratory.

Evaluation of the losses and SiC DC-AC inverter efficiency

The 3-phase DC-AC SiC inverter is water cooled. An appropriated heat-sink has been calculated. Thermal losses P (Watt) are given by the following Equation (4), = 2.9 l/mn is the water cooling flow, Cp the specific heat capacity of water = 4 180 J. kg-1.K-1, and (Two, Twi) resp. the output and input water temperatures.

( )

wi wo p f T T C m - = • . . P (4)
Analytical losses, including copper (Joule) losses and switching losses are deduced from SiC semiconductor datasheets and calculated using formula (5):

)

) ( . .( 3 P 2 off on s rms dsON E E F I R + + = (5)
Analytically, for 144Arms which is the maximal current constraint, for 24 kHz switching frequency, RdsON=3.5 mΩ at ambient temperature 25°C, RG = 5Ω (external gate resistance present on the driver card), Eon = 5.25 mJ, Eoff= 1.9 mJ, the calculated losses are 732 W which value is in accordance with the losses evolution at 3000 rpm (144A), see results in Fig. 12. For 20 kHz the losses are 647 W, and for 16 kHz the losses become 561 W. Efficiencies (in %) are calculated for static points, with Equation 6, for 50 kW transmitted power: Efficiencies of the SiC converter (from 16 kHz to 24kHz) are between 99,5% to 99,3%. Figure 13 represents the thermal losses for a speed up and down cycle from 3000 to 6000 rpm, then from 6000 down to 3000 rpm. The time for current injection is 2 x 9 min = 1080 sec with 1 min pause between the two transients. The average losses for the cycle at 24kHz is 461 W, which deduced efficiency is 99,1 % over the speed up -down cycle.

0219-13

CONCLUSION

The research work presented in this paper has concerned the design and experimental validation of a 50kW three-phase high efficiency DC-AC inverter with novel Silicon carbide (SiC)-based MOSFETs transistors technology, and used for the supply of an EV-Charging flywheel energy storage system. High frequency switching and PWM tests, and hardware realization have been presented and discussed. The three-phase DC-AC Silicon carbide inverter prototype has been characterized on an original homemade PWM test-bench controlled using a modulated hysteresis controller, and which is able to emulate the working of the motor-flywheel system. Static power tests up to 50kW have been performed, also up-down speed cycle operating and thermal losses have been evaluated. An efficiency above 99% has been reached for the DC-AC three-phase Silicon carbide converter prototype thanks to the adopted design and control strategy. As a further step, the SiC-based inverter prototype should be integrated together with the control master module in order to perform tests over the global motor-flywheel energy storage system, with scenarios representative of EV-charging use cases.

Figure 1 .Figure 2 Figure 3 .Fig. 3 :Figure 4 .

 12334 Figure 1. General overview of the FESS (Flywheel Energy Storage System) used for EVcharging

Figure 5 4 . 2 .Figure 6

 5426 Figure 5.a) SiC MOSFET switching ON state

Figure 6 .

 6 Figure 6.b) Driver card Prodrive® gate output Switching results up to 100 kHz

Figure 7 .Figure 8 .

 78 Figure 7. Focus on 20kHz PWM gate signal and AC phase current (view on digital scope recorder) Figure 8. DC-AC Inverter prototype on heatsink (with DC busbar, current LEM© sensors, capacitor's snubber and interface driver cards for CREE ProDrive ® ). The DC-AC inverter is water cooled

Figure 9 .

 9 Figure 9. Electrical topology for DC-AC SiC inverter connected to the double-converter architecture

Figure 10 .

 10 Modulated hysteresis method a) Hysteresis regulator b) Modulated hysteresis current

Figure 11 .

 11 Figure 11. Testing bench for SiC prototype inverter testing

Figure 12 .Figure 13 .

 1213 Figure 12. Experimental thermal losses for 50kW test

ACKNOWLEDGMENT

Authors gratefully thank the French ministry of Industry, and the Region of Paris Île-de-France, for financing of research within the FUI-13 N° 13021410 grant agreement, and greatest thanks to Dr. Ing. Jean-Pierre Ousten † , research engineer, for his precious assistance and contribution in the design and realization of the silicon carbide DC-AC reversible inverter prototype.