Feedback Stabilization of Switched Differential Algebraic Systems

Eduardo Mojica-Nava and Naly Rakoto-Ravalontsalama Abstract-A stabilization problem for a switched differential-algebraic system is investigated. We propose an approach for solving effectively the stabilization problem for an autonomous linear switched differentialalgebraic system based on projector and flow matrices. In switched DAEs, the switches can induce jumps in certain state-variables, and it has been shown that the formulation as a switched DAE already implicitly defines these jumps, no additional jump map must be given. These jumps can be calculated in terms of the consistency projectors. The essence of this method is to design a stabilizing controller for switched differentialalgebraic systems, i.e., the continuous dynamics of each subsystem are described by sets of differential-algebraic equations, using an averaging switched DAE model based on consistency projector and flow matrices to guarantee convergence towards an equilibrium point via fast switching Index Terms-Differential-algebraic equations, Moments, Optimal Control, Switched Systems

I. INTRODUCTION

In most all areas of electrical, mechanical, or chemical engineering the modeling and control of the dynamics of complex systems is nowadays highly modularized, thus allowing the efficient generation of mathematical models for substructures and link them together via constraints. Differential-algebraic equations (DAEs) arise in the modeling of physical systems where the state variables satisfy certain algebraic constraints alongside some differential equations that govern the evolution of these state variables. In complex systems naturally arise the switched control systems, which are characterized by a set of several continuous nonlinear state dynamics with a logic-based controller, which determines simultaneously a sequence of switching times and a sequence of modes [START_REF] Liberzon | Switching in systems and control[END_REF], [START_REF] Sun | Switched linear systems: control and design[END_REF], [START_REF] Mojica-Nava | A polynomial approach for stability analysis of switched systems[END_REF].

In the last years several researchers have considered the control of switched systems (see, for example [START_REF] Branicky | Algorithms for optimal hybrid control[END_REF], E. Mojica-Nava is with Electrical and Electronics Department, Universidad Nacional de Colombia, Bogotá, Colombia, eamojican@unal.edu.co, N. Rakoto-Ravalontsalama is with IMT Atlantique and LS2N, Nantes, France. naly.rakoto@mines-nantes.fr. and [START_REF] Branicky | A unified framework for hybrid control: Model and optimal control theory[END_REF], [START_REF] Xu | Optimal control of switched systems based on parameterization of the switching instants[END_REF], [START_REF] Bengea | Optimal control of switching systems[END_REF], [START_REF] Mojica-Nava | A polynomial approach for optimal control of switched nonlinear systems[END_REF]). In switched systems, a switching signal and an external control input may be designed together to guarantee closed-loop asymptotically stabilization [START_REF] Sun | Switched linear systems: control and design[END_REF], [START_REF] Mojica-Nava | A polynomial approach for stability analysis of switched systems[END_REF]. In the particular case of switched linear systems, several effective techniques have been presented and summarized in books such as in [START_REF] Liberzon | Switching in systems and control[END_REF], [START_REF] Sun | Switched linear systems: control and design[END_REF]. The research field of switched differential-algebraic systems has been growing in the last decade, some work has been done in stability analysis and numerical solutions, see e.g. [START_REF] Liberzon | On stability of linear switched differential algebraic equations[END_REF], [START_REF] Mehrmann | Hybrid systems of differential-algebraic equations-Analysis and numerical solution[END_REF], [START_REF] Tanwani | On observability of switched differential-algebraic equations[END_REF], [START_REF] Trenn | Switched differential algebraic equations[END_REF], and recently in [START_REF] Mostacciuolo | Averaging for switched daes: Convergence, partial averaging and stability[END_REF] it is presented an averaging model for a switched DAEs and it is studied convergence and stability of the proposed model. In switched DAEs, the switches can induce jumps in certain state-variables, and it has been shown that the formulation as a switched DAE already implicitly defines these jumps, no additional jump map must be given. These jumps can be calculated in terms of the consistency projectors. Control algorithm considering switched DAE systems has no been widely studied. In general, the work has been focus on constrained cases, such as switched DAEs with lower indexes (index-1 to index-3 DAE) [START_REF] Mehrmann | Hybrid systems of differential-algebraic equations-Analysis and numerical solution[END_REF] or stabilization via single switching signal based on a approximation parameter [START_REF] Mironchenko | Stabilization of switched linear differential algebraic equations and periodic switching[END_REF]. However, this condition is not satisfied because the averaging approach will result in switching signals depending on this parameter. The main limitation of the stabilizing algorithm proposed in [START_REF] Mironchenko | Stabilization of switched linear differential algebraic equations and periodic switching[END_REF] is the destabilizing effect of the consistency projectors, the nonexistence of an averaged model for the switched DAE is not considered [START_REF] Trenn | Stabilization of switched daes via fast switching[END_REF].

The main contribution of this paper is to design a stabilizing controller for switched differential-algebraic systems, i.e., the continuous dynamics of each subsystem are described by sets of differential-algebraic equations in general, using an averaging switched DAE model based on consistency projector and flow matrices to guarantee convergence towards an equilibrium point via fast switching. The proposed approach overcomes the limitation of the destabilizing effect of the consistency projector using the properly defined averaged model.

The rest of the paper is organized as follows. Section II presents a brief description of the main concepts of switched DAEs. In Section III, some theoretical results are shown for feedback stabilizing control design. Section IV presents simulation results and finally in Section V some conclusions and future work are drawn.

II. SWITCHED DIFFERENTIAL ALGEBRAIC SYSTEMS

A. Basic Definitions

The switched differential algebraic system adopted in this work is described by sets of differential algebraic equations for each mode of operation and a switching signal that determines which mode is operating at each point of time. Consider a general mathematical model described by switched differential algebraic equations (DAE) of the form

E σ ẋ(t) = A σ x 1 (t) + B σ u(t), ( 1
)
where x is the state, the switching signal σ

: [t 0 , t F ] → Q ∈ {1, 2, .
.., q} is a piecewise constant function of time, with t 0 and t F as the initial and final times respectively, and (q) is the number of subsystems. Every mode of operation corresponds to a specific subsystem (E i , A i ), for some i ∈ Q, and the switching signal σ determines which subsystem is followed at each point of time into the interval

[t 0 , t F ], E i , A i ∈ R n × R n , B i ∈ R n × R m
are constant matrices for each subsystem, and x(0) = x 0 are fixed initial values. In addition, we consider a non-Zeno behavior, i.e., we exclude an infinite switching accumulation points in time. In order to obtain a solution in the new mode, the initial value obtained by the algorithm have to be consistent with the DAE in the next mode. For each subinterval of [t 0 , t F ] we assume that consistent initial values for the currently mode exist, such that a solution exists. Furthermore, we assume that the integration interval have nonzero measure, i.e., an instantaneous multiple mode change is not allowed [START_REF] Mehrmann | Hybrid systems of differential-algebraic equations-Analysis and numerical solution[END_REF]. Finally, we assume that the state does not have jump discontinuities. Moreover, for the interval [t 0 , t F ], the control functions must be chosen such that the initial and final conditions are satisfied. Definition 1: A control for the switched differentialalgebraic system in (1) is a duplet consisting of (a) a finite sequence of modes, and (b) a finite sequence of switching times such that

t 0 < t 1 < • • • < t F .
Locally in each mode i ∈ Q and for every small subinterval of [t 0 , t F ], we consider the classical solution concept. The solution of a switched differentialalgebraic system depends on the initial mode, initial conditions, and mode switching control rule. We assume also that all solutions of each mode evolve within a consistency space [START_REF] Trenn | Solution concepts for linear daes: a survey[END_REF]. An important issue when dealing with switched DAEs is the possible jumps after a switch, which makes necessary to allow solutions with jumps leading to problems in obtaining the solution of (1). To handle this behavior we use the distributional solution space introduced in [START_REF] Trenn | Switched differential algebraic equations[END_REF] for switched DAEs.

Assumption 2: The matrix pairs (E i , A i ) are regular in the sense that each matrix pair are of the same dimension n and the characteristic polynomial det(sE i -A i ) ̸ = 0. In the next subsection, it is introduced the concept of regularity and consistency projector that are fundamental to guarantee existence and uniqueness of solution of the switched DAEs.

B. Regularity and Consistency Projectors

In Assumption 2 is presented the regularity conditions needed for each matrix pair (E i , A i ). Based on this assumption, the following result presents the characterization of regularity in terms of Quasi-Weierstrass form (it is not assumed that the matrices N i , and J i are in Jordan canonical form), which provides a decoupling of each DAE into purely differential and algebraic parts [START_REF] Trenn | Switched differential algebraic equations[END_REF] Proposition 3:

If each matrix pairs (E i , A i ) ∈ R n × R n is regular, then there exist invertible matrices S i , T i ∈ R n × R n such that each (E i , A i ) is transformed into a Quasi-Weierstrass form (S i E i T i , S i A i T i ) = ([ I 0 0 N i ] , [ J i 0 0 I ]) (2)
where I is the identity matrix of the appropriate dimension, N i are Nilpotent matrices, and J i are some matrices.

In [START_REF] Trenn | Switched differential algebraic equations[END_REF], it is presented a useful method to obtain matrices S i and T i using Wong sequences. Consider a regular matrix pair (E i , A i ) with index η, the associated Wong sequences of subspaces are as follows

υ 0 := R n , υ k+1 = A -1 k (E k υ k ), for k = 0, 1, ..., υ * , with υ * := ∩ k υ k ω 0 := {0}, ω l+1 = E -1 l (A l ω l ), for l = 0, 1, ..., ω * , with ω * := ∪ l ω l ,
then we choose full rank matrices V and W , such that imV = υ * and imW = ω * and obtain invertible matrices

T := [V, W ], S := [EV, AW ] -1 .
Wong sequences are nested and get stationary after exactly η steps. Once we have obtained the Quasi-Weierstrass form of regular matrices E i , A i , we can define the consistency projectors and flow matrices as follows Definition 4: For each pair (E i , A i ), the consistency projectors are given by

M i = T i [ I 0 0 0 ] T -1 i ,
the flow matrices are given by

A d i = T i [ J i 0 0 0 ] T -1 i ,
and the differential projectors are given by

M d i = T i [ I 0 0 0 ] S i , .
It should be guaranteed that the design is impulse and jump free. Assume that the matrix pair (E i , A i ) are regular and that there is a switch at time t from mode σ(t -) = p to mode σ(t

+ ) = r, with p, r ∈ Q. If for all p, r ∈ Q E r (I -M r )M p = 0
holds, then all distributional solutions x(t) of (1) are impulse-free for any switching signal. And if also (I -M r )M p = 0 holds, then all solutions are jump and impulse free for any switching time, i.e, x(t + ) = x(t -).

The solution of the switched DAE can now be characterized in terms of projectors and flow matrices as follows [START_REF] Mostacciuolo | Averaging for switched daes: Convergence, partial averaging and stability[END_REF].

Theorem 5: Consider the system (1) with Assumption 2 and consistency projectors, differential projectors, and flow matrices introduced in Definition 4. Then x(t) is the impulse free part of any distributional solution of (1) if and only if x(t) is a solution of the switched system with jumps given by

ẋ(t) = A d i x(t) + M d i B i u(t), ( 3
)
x(t + k,i ) = M i x(t - k,i ),
where t - k,i and t + k,i are the instant time before and after the switch, respectively. The initial conditions before the switched DAE is activated x(0 -) is assumed consistent and

x(0 -) = x 0 . Finally, the following projector assumptions are introduced. Consider the set of projectors {M i } q i=1 , then we have the following Projector Assumptions

• imM ∩ ⊆ imM i and • ker M ∩ ⊇ ker M i , ∀i ∈ Q,
where im and ker are the image and kernel of matrices, respectively. The product projector M ∩ is given by

M ∩ = q ∏ i=1 M i . ( 4
)
Theorem 5 provides tools to control design since using projectors and flow matrices we are able to use previous result for switched linear systems. In the next section, we extend available stabilization result for switched systems to switched DAEs systems.

III. STATE FEEDBACK SWITCHING CONTROL

In this section, we present a state feedback switching control algorithm for switched DAEs system [START_REF] Bengea | Optimal control of switching systems[END_REF]. The main objective is to design a feedback stabilizing control law, which involves finding appropriate switching signals as well as continuous state feedback controllers to make the closed-loop system asymptotically stable.

Consider the switched DAEs system (1), we propose a definition of stabilizability as follows Definition 6: System ( 1) is said to be linear feedback stabilizable, if there exist a switching signal σ, and state feedback control inputs

u i (t) = -K i x(t) (5)
such that the closed-loop switched DAEs system

E σ ẋ(t) = (A σ -B σ K σ )x(t)
is well-posed and uniformly asymptotically stable.

In order to develop a control algorithm to satisfy Definition 6, we apply the average technique to approximate the switching DAEs system based on Theorem 5. First, let us define the simplex set as

∆ = { α i ∈ R| q ∑ i=1 α i = 1, α i ≥ 0 } .
where q is the number of subsystems and the set of subsystems indexes is defined as i ∈ Q = {1, 2, . . . , q}. The average matrices are defined as convex combinations of the subsystems matrices. Recall that the solutions of the switched DAE (1) can be expressed by solutions of a switched system with jumps (3). Recently in [START_REF] Mostacciuolo | Averaging for switched daes: Convergence, partial averaging and stability[END_REF], it is proposed an averaged model that approximates the behavior of the switched DAE. Considering that a time-varying system can be viewed as a timeinvariant averaged system with a small perturbation, an averaging model has been proposed. Consider a periodic switching signal σ for the switched DAE system (1), the averaging model converges to the switched system for a fast switching with a small period. The proposed average model is as follows

ẋα (t) = M ∩ ( q ∑ i=1 α i A d i ) M ∩ + M ∩ ( q ∑ i=1 α i B d i ) x α (0) = M ∩ x 0 (6)
where i ∈ Q, α i are defined in the simplex, and M ∩ is defined in (4). Consider that assumptions in Theorem 5 are satisfied and there exists an average model ( 6), then we can establish the quadratically stabilization conditions for switched DAE.

Lemma 7: System (1) is quadratically stabilizable if there exist gain matrices

K i , i ∈ Q such that the matrix { M ∩ ( ∑ i∈Q α i M d i (A i -B i K i ) ) M ∩ : α i ∈ ∆ } contains a Hurwitz matrix. Let us define A Kα = M ∩ ( ∑ i∈Q α i M d i (A i -B i K i ) ) M ∩
as the average closed-loop matrix. The following proposition presents the stabilizability condition. Proposition 8: For system (A d i , B d i ), α i are given convex combination parameters, with i ∈ Q such that the pair (

∑ i α i A d i , ∑ i α i B d i ) is controllable.
Then, the switched affine system is quadratically stabilizable.

We present a state-feedback switching signal based on an appropriate partition of the state space. As a first approach, we assume that the system is single-input

B 1 = [1, 0, . . . , 0] ⊤
and in the controllable form. Then the single-input system (

∑ i α i A d i , B d 1 )
is also quadratically stabilizable. Considering the average matrix A α and B α = α 1 B d 1 , we can find a feedback K 1 such that

A Kα = A α -B α K 1 is Hurwitz with u 1 = u 2 = -K 1 x.
Supposing assumptions in Lemma ( 7) holds, we solve the Lyapunov equation

A ⊤ Kα P + P A Kα = -I n ,
and we obtain a symmetric positive definite matrix P , this matrix can be seen as a common Lyapunov function for the switched DAEs system. For each subsystem we denote

∀i ∈ Q, Q i = [M d i (A i -B 1 K 1 )] ⊤ P + P [M d i (A i -B 1 K 1 )]. (7)
which are positive definite matrices. The main result for the feedback switching algorithm is presented in the following theorem. Theorem 9: Consider the switched DAEs system (1). If there exist positive matrices Q i as in [START_REF] Mironchenko | Stabilization of switched linear differential algebraic equations and periodic switching[END_REF] such that V = x ⊤ P x. Then the state switching control

σ(x) = arg min i∈Q {x ⊤ Q i x}, (8)
and the feedback control u(x) = -K 1 x, asymptotically stabilize system (1).

Notice that arg min stands for the index which attains the minimum among Q = {1, 2, • • • , q}, and that the eigenvalues of the average matrix A Kα = A α -B α K 1 can be arbitrarily (symmetrically) assigned by appropriately choosing K 1 using techniques such as pole placement.

In this section, we have presented the main theoretical results for stabilization of switched DAE (1). In the next section, some simulation results are presented to illustrate the implementation of Theorem 9 and particularly the switching control [START_REF] Mojica-Nava | A polynomial approach for optimal control of switched nonlinear systems[END_REF].

IV. NUMERICAL EXAMPLE

A simple academic switched differential algebraic model is used as an example to illustrate the approach proposed in this paper. It is established that this system is asymptotically controllable and asymptotically stabilizable. The system has two operation modes described by the following matrices

A 1 = [ 1 -1 1 0 ] , E 1 = [ 1 -1 0 0 ] , A 2 = [ 1 1 0 -1 ] , E 2 = [ 1 1 0 0 ] ,
and the consistency projectors obtained by some method using Wong sequences are given by

M 1 = A d 1 = [ 0 0 -1 1 ] , M 2 = A d 2 = [ 1 1 0 0 ] ,
the convex combination parameter are α 1 = 0.3, α 2 = 0.7. We obtain the product projector

M ∩ = [ 0 0 -1 -1 ]
With these matrices, we choose appropriate eigenvalues for the closed loop system using a simple routine of pole placement following the indications of Theorem 9 and switching control [START_REF] Mojica-Nava | A polynomial approach for optimal control of switched nonlinear systems[END_REF].

Fig. 1 shows the trajectories and the switching signal for the switched DAEs applying one single continuous control and a switching signal based on the proposed methodology. It is shown that both controllers acting simultaneously drive the switched DAEs system to the equilibrium point.

V. CONCLUSIONS AND FUTURE WORK

We have presented preliminary results dealing with the stabilization problem of switched differentialalgebraic systems. We have introduced a useful tool to solve this problem based on consistency projector and flow matrices to guarantee convergence towards an equilibrium point via fast switching. Some simulation results allow us to observe the effectiveness of the proposed algorithm. There are several possible extension of this work. One direction is towards non-linear systems, in particular DAEs systems of polynomial form. On the other hand, the approach based on consistency projector can be used in linear optimal control problem such as a linear quadratic regulator for switched DAEs.

Fig. 1 .

 1 Fig. 1. States and switching signal

23rd International Symposium on Mathematical Theory of Networks and Systems Hong Kong University of Science and Technology, Hong Kong, July 16-20, 2018


Anne-Lise Courbis

Thomas Lambolais

Thanh-Hung Nguyen

Safe Incremental Design of UML Architectures

Keywords: UML composite components, BIP architectures, conformance analysis, safety analysis, refinement, incremental development, transformation of UML models into BIP models

come   L'archive ouverte pluridisciplinaire

Introduction

Designing UML models of software intensive reactive systems is recognized to be a tricky and crucial task. Reactivity means that such systems must continuously react to their environment, at a speed defined by this environment. It implies liveness properties, stating that the system will eventually react as it must. These systems are also dependable, so that reliability, availability and robustness are of primary importance. This implies safety properties, stating that undesired behaviors of the system will never happen.

Despite the increasing number of conferences and researches about UML, the use of UML is not yet fully accepted by industrialists [START_REF] Petre | UML in practice[END_REF]. The lack of a precise semantics and the numerous ambiguities of UML could explain this defeat. Another related main explanation is the lack of support for UML designers in the process for both setting up models and evaluating them. The rule of the thumb is that an architecture assessment should be held as soon as architecture decisions begin to be made and the cost of reversing those decisions would be more than conducing software architecture evaluation [2]. However, few methods of UML model development support model evaluation during the design phases. The novelty of our proposed approach is to consider at early steps of the design both liveness and safety properties.

In a previous work [START_REF] Lambolais | Designing and integrating complex systems: Be agile through liveness verification and abstraction[END_REF][START_REF] Lambolais | IDF: A framework for the incremental development and conformance verification of UML active primitive components[END_REF], we have presented our Incremental Development Framework (IDF) and its associated tool IDCM (Incremental Development of Conformance Models). IDF supports the development and the evaluation of UML models for reactive systems. It deals with UML primitive components whose behavior is represented by a state machine and UML composite components whose parts are primitive components or composite ones. IDF allows models to be developed step by step. At every step of the design, the model is verified as being consistent with the model obtained at the previous step, a step being a model evolution which can be of four kinds: extension, refinement, increment or substitution. The verification of these four kinds of model evolution is based on a conformance relation [START_REF] Luong | Implementation of the Conformance Relation for Incremental Development of Behavioural Models[END_REF] which verifies that liveness properties defined by a reference model are preserved. However, this work has its own shortcomings: explicit verification of safety properties is not addressed. This article aims at enhancing IDF in order to be able to model and check explicit safety properties. That is a way to cover the verification of the complete properties of a system since it has been proved that the safety/liveness spectrum covers all linear-time properties of a system under design [START_REF] Schneider | Decomposing Properties into Safety and Liveness using Predicate Logic[END_REF].

We present in section 2 an example pointing out an incremental development of a model whose liveness analysis is demonstrated using IDCM, but suffering from a lack of safety analysis. Section 3 presents the BIP meta-model that has been selected as an intermediate format to analyze models in order to use D-Finder tool to check safety analysis. The tool IDCM associated with IDF, as well as UML and BIP models presented in this article, may be downloaded on the website [START_REF]IDCM[END_REF]. Section 5 presents related works. We conclude in section 6 and present our future directions.

Motivating example

Let us consider MUTEX, a mutual exclusion system that can process two orders of task execution in parallel: it has two ports (see Fig. 1), each of them allowing the reception of a demand of task execution (operation start of interface IUserIn) and the transmission of an acknowledgement at the end (operation finish of interface IUserOut). The high level specification of MUTEX represents the system from an external point of view and does not yet represent the resource. It is modeled from a behavioral point of view by an atomic UML component whose behavior is specified by a state machine (see Fig. 1b). The next step of modeling aims at representing the internal view of the system, i.e. the shared resource and the two users. The interface provided by the resource offers two actions: take and release. The designer thus specifies the components SpecUser and SpecResource and their associated behaviors (cf. Fig. 2) in order to match MUTEX high level specification. The first model set up by this way is named MUTEXSpec: it is a composite component which assemblies two SpecUser components and one SpecResource component (see Fig. 3a).

A new modeling step is starting to set up a possible implementation of MUTEXSpec architecture (see Fig. 3b) based on components User and Resource. User is not detailed since it is not required to understand the example. Resource is presented in Fig. 5a. Both User and Resource have been checked by IDCM as extending and thus conforming their specification (Fig. 3c). The conformance relation [START_REF] Leduc | A framework based on implementation relations for implementing LOTOS specifications[END_REF] between an implementation model and a spec- ification model guarantees that actions that are mandatory after any trace of the specification must also be accepted by the implementation after the same trace. This relation has been implemented with its variant, refines and extends, in [START_REF] Luong | Implementation of the Conformance Relation for Incremental Development of Behavioural Models[END_REF]. It requires models to be transformed into LTS (Labelled Transition System) that is automatically achieved using IDCM and CADP toolbox [START_REF] Garavel | CADP 2011: a toolbox for the construction and analysis of distributed processes[END_REF] (see [START_REF] Lambolais | Designing and integrating complex systems: Be agile through liveness verification and abstraction[END_REF][START_REF] Lambolais | IDF: A framework for the incremental development and conformance verification of UML active primitive components[END_REF] for more details about the transformation). In the following, we give an interpretation of these relations on the MUTEX models.

For formal definitions, see [START_REF] Lambolais | IDF: A framework for the incremental development and conformance verification of UML active primitive components[END_REF]. MUTEX composite component conforms to MUTEXSpec component: it is a suitable implementation of the specification. MUTEXSpec architecture is a refinement of MUTEX behavioral specification: it has no extra traces and realizes all mandatory part of the specification. Resource component conforms to Resource-Spec and is an extension: Resource is able to behave like its specification but has also extra behavior which does not conflict with its specification. This example points out that MUTEX is a "good" realization of the initial specification from a liveness point of view as defined by the ISO standard [START_REF]Information technology -open systems interconnection -conformance testing methodology and framework -part 1: General concepts[END_REF]. However, we are not able to verify the safety property stating that the resource has to be exclusive. We may interpret this property in terms of states that the components of the system may or may not reach. If the resource R1 is exclusive, it means that U1 and U2, the two users of MUTEX may not be at the same time in state Starting, which is the output state of the transition start/takeResource, while R1 is in state Busy.

IDF relations cannot verify an explicit property such as this one. It is thus necessary to associate another tool with IDCM. IDF. The BIP (Behavior, Interaction and Priority) modeling and verification framework is based on several principles which match with IDF: development of correctness-byconstruction model, incrementality, compositionality and composability [START_REF] Bensalem | Incremental component-based construction and verification using invariants[END_REF]. It includes many tools for safety property analysis and model transformation from several languages such as AADL and Lustre. To the best of our knowledge, there is no available transformation tool from UML to BIP taking into account both primitive and composite component descriptions. We have thus developed a module of IDCM that may be uploaded on the IDCM website [START_REF]IDCM[END_REF]. The transformation principle is presented and illustrated in section 4.

BIP language

BIP is a powerful language for modeling heterogeneous real-time systems. We only focus on specific concepts useful to understand the safety analysis purpose and the transformation from UML to BIP. As we do not consider data analysis of UML models, we will not consider data modeling in BIP. In the same way, we will not deal with priority concepts of the BIP language. Refer to [START_REF] Basu | Modeling heterogeneous real-time components in BIP[END_REF] for detailed information about the BIP language. Fig. 4 gives an overview of the main classes of BIP meta-model corresponding to UML concepts we deal with.

BIP describes compound components by a set of interactions between atomic components whose behaviors are represented by LTS. Two kinds of interactions are possible: strong (also called rendezvous) and weak (broadcast). In this study, we restrict interactions to rendezvous which are defined on ports representing actions.

D-Finder: a toolbox for safety analysis

D-FINDER provides methods and tools to compute invariants of BIP models. Such invariants are interesting since they preserve safety properties. There are two kinds of invariants: component invariants which are over approximation of reachable states, and interaction invariants which define global boolean constraints dealing with the synchronization of components. D-FINDER is based on an abstraction technique allowing the state space to be reduced. Its strength is to perform incremental constructions of models and incremental computations of invariants [START_REF] Bensalem | Incremental component-based construction and verification using invariants[END_REF] allowing large-scale systems to be checked. D-Finder uses BDD library for the symbolic computation of interaction invariants, and then the SAT-solver tool Yices [START_REF] Dutertre | [END_REF] for checking satisfiability. Verifying a safety property consists in demonstrating using Yices that the negation of the property is unsatisfiable in a context defined by the set of invariant expressions generated by D-Finder. The invariants are expressed by Boolean Behavioral Constraints [START_REF] Nguyen | Constructive verification for componentbased systems[END_REF].

Illustration of a safety property for MUTEX

Let us consider the MUTEX specification and implementation architectures (Fig. 3a and3b). We aim at checking if the mutual exclusion property is satisfied. Equation 1expresses the non expected property: two users U1 and U2 can be both in Starting state while the shared resource R1 is in busy state. We have to demonstrate that this property can never be satisfied.

(and R1 busy-(and U1 Starting-U2 Starting-)) (1)

The following section focuses on UML model transformation into BIB and points out results of safefy analysis of MUTEX models after their transformation.

4 From UML to BIP architectures UML and BIP share the same view about component concepts: a UML component whose behavior is defined by a state machine matches the BIP atomic component concept, a UML composite component matches the BIP compound component (see Table 1). The concept of UML interface (set of visible operations) does not explicitly exist in BIP. However, it may be translated into exported ports. A matching is possible between operations belonging to interfaces associated with UML ports and the BIP ports. For instance, the port P of component User which is associated with the interface IResource will correspond to two BIP ports named P TAKE and P RELEASE since interface IResource contains the two operations TAKE and RELEASE. This is why the relation between UML port and BIP ports is of cardinality n in Table 1

Transformation of atomic components

We have given in [START_REF] Lambolais | IDF: A framework for the incremental development and conformance verification of UML active primitive components[END_REF] a LTS semantics to UML state machines. BIP atomic models have a LTS semantics [START_REF] Basu | Modeling heterogeneous real-time components in BIP[END_REF]. The mapping from UML to BIP is thus trivial. It is important to note that UML is more concrete than the LTS language and allows more complex structures to be modeled, such as actions on data or call events through ports. Hence, this semantics abstracts some concepts of UML like data, events, time, ports, guards, thanks to the intrinsic non-deterministic nature of LTS. The rules allowing the UML atomic transformation into LTS are detailed in [START_REF] Lambolais | IDF: A framework for the incremental development and conformance verification of UML active primitive components[END_REF]. Figure 5a represents the state machine of component Resource of MUTEX architecture and figure 6 gives the corresponding BIP model that is automatically generated by the module UMLtoBIP of IDCM.

Transformation of composite components

There is a direct mapping between UML composite component and BIP compound components (see Table 2): a UML composite component consists of a set of Parts which match BIP Components. A UML assembly Connector matches a set of BIP connectors. Indeed, a BIP connector is relative to the synchronization of a single operation shared by two interconnected ports, while a UML connector is relative to the synchronization of the set of operations belonging to interfaces associated with the interconnected ports. The Port of a Part belonging to a delegate connector will be exported and renamed by the name of the port of the compound component. Table 2 summarizes the matching of concepts between UML composite components and BIP compound components. To illustrate this transformation, we give in Figure 7 the BIP code of the MUTEX architecture represented in Figure 3b. This code is automatically generated by the transformation module UMLtoBIP of IDCM. the mutual exclusion whose negation is expressed in equation 1 of section 3.3. For SpecMUTEX, the property is unsatisfied: it means that the resource mutual exclusion has been properly implemented in this architecture. That is not the case for the MUTEX architecture. Indeed, the state machine associated with the Resource (see Fig. 5a) points out that it may be used concurrently by two users. On this example, the error is obvious, but it is not the case for large system for which components may be designed by third parties according to a high level specifications: conformance does not guarantee safety preservation and a complete specification has to define both the expected behavior (liveness properties) and unexpected states or sequence of events (safety properties). IDCM associated with BIP and its associated tools is a good way to cover all these aspects.

Safety analysis of MUTEX architecture

Discussion and Related work

Most of behavioral analyzes of UML models (75% according to [START_REF] Lucas | A systematic review of UML model consistency management[END_REF]) are done by transformation of UML models into formal languages that can be handled by model checkers or theorem provers. Some of them are referenced below. However, to the best of our knowledge, no framework support the incremental development of UML architecture models by analyzing both liveness and safety behavioral aspects. In particular, no framework is able to consider abstract and non-deterministic UML models and few frameworks are able to consider UML models partially covering the requirements. Hence, even if some work addresses refinement of models, they do not focus on the reduction of non-determinism, and most of them cannot analyze models the specification of which is extended, despite it is a key action for designing complex systems and managing model evolution. Refer to [START_REF] Lambolais | IDF: A framework for the incremental development and conformance verification of UML active primitive components[END_REF] to have more arguments and a complete state of the art about formal verification of models.

To argue this discussion, let us take some representative works about UML/SysML architecture model verification [START_REF] Kmimech | Checking component assembly in ACME: an approach applied on UML 2.0 components model[END_REF][START_REF] Pétin | Combining SysML and formal models for safety requirements verification[END_REF][START_REF] Chouali | Formal verification of components assembly based on SysML and interface automata[END_REF][START_REF] Ober | Unambiguous UML composite structures: the OMEGA2 experience[END_REF][START_REF] Baresi | Formal verification and validation of embedded systems: the UML-based MADES approach[END_REF]. Although [START_REF] Daw | UML-VT: A Formal Verification Environment for UML Activity Diagrams[END_REF] focuses on UML activity diagrams, we must pay attention to the sound discussion about model checking that is the base of our approach. [START_REF] Kmimech | Checking component assembly in ACME: an approach applied on UML 2.0 components model[END_REF] defines a UML profile to transform models into Wright for using the FDR model checker [START_REF]Failures-Divergence Refinement (FDR2 User Manual)[END_REF]. FDR focuses on liveness and safety. It deals with several refinements and provides deadlock detection. However, it does not support analysis of extended models and models are not verified under fairness assumption, which is the main drawback as pointed out in [START_REF] Lambolais | IDF: A framework for the incremental development and conformance verification of UML active primitive components[END_REF]: FDR can not distinguish between 'critical' livelocks (when there may exist executions where the system won't never exit some infinite internal paths) and 'false' livelocks, where under a fairness assumption, the system may leave internal infinite paths or loops. [START_REF] Chouali | Formal verification of components assembly based on SysML and interface automata[END_REF] defines and verifies component assemblies and performs a behavioral compatibility verification but extension and refinement techniques are not supported. [START_REF] Ober | Unambiguous UML composite structures: the OMEGA2 experience[END_REF] have extended the techniques proposed by [START_REF] Cuccuru | Meaningful composite structures[END_REF] who has defined the OMEGA 2, a UML profile. Architectures are translated into IF/IFx models [START_REF] Bozga | The IF Toolset[END_REF] allowing LTS models to be generated and analyzed by the CADP model checker [START_REF] Garavel | CADP 2011: a toolbox for the construction and analysis of distributed processes[END_REF]. [START_REF] Baresi | Formal verification and validation of embedded systems: the UML-based MADES approach[END_REF] uses a notation integrating concepts of both UML and MARTE [START_REF]OMG formal/2011-06-02. UML profile for MARTE -Modeling and Analysis of Real-time Embedded Systems[END_REF] and transforms models into temporal logic descriptions that can be analyzed by the model checker Zot [START_REF] Pradella | Bounded satisfiability checking of metric temporal logic specifications[END_REF]. Other approaches about AADL aims at transforming models into intermediate models such as FIACRE [START_REF] Chkouri | Prototyping of distributed embedded systems using AADL[END_REF][START_REF] Berthomieu | Formal Verification of AADL models with Fiacre and Tina[END_REF] or BIP [START_REF] Chkouri | Prototyping of distributed embedded systems using AADL[END_REF] to use appropriate model checkers such as TINA [START_REF] Berthomieu | The tool TINA: Construction of abstract state spaces for Petri nets and time Petri nets[END_REF] or Yices [START_REF] Dutertre | [END_REF]. These approaches are powerful from the safety point of view but they are not able to integrate liveness analysis for incremental development of models as it is done in IDCM.

Conclusion

In this article, we have pointed out the interest for incremental development of UML models and the complementarity between safety and liveness analyses. We have defined a transformation of UML models into the BIP formalism which is implemented into the tool IDCM we have developed. By this way, the liveness and safety analyses are automated. Safety properties are expressed by proposi-tional calculus and requires designers to manipulate a specific syntax. Further steps consist in developing a support to help designers to express the safety properties in terms of UML concepts regardless the theorem prover syntax, and studying their automatic rewording when UML models are refined or extended.

  (a) Interfaces. (b) MUTEX Atomic component.

Figure 1 :

 1 Figure 1: MUTEX Behavioral specification.

Figure 2 :

 2 Figure 2: (a) SpecUser and (b) SpecResource state machines

  (a) MUTEXSpec composite component (b) MUTEX composite component. (c) Liveness relations between MUTEX components.

Figure 3 :

 3 Figure 3: Incremental development of the MUTEX system.

Figure 4 :

 4 Figure 4: Main BIP classes.

( a )

 a Resource state machine. (b) Resource LTS.

Figure 5 :

 5 Figure 5: Resource component transformation into LTS.

Figure 6 :

 6 Figure 6: Resource BIP model.

Table 2 :

 2 Despite MUTEX architecture conforms to MU-TEXSpec, we have to verify the safety property about Correspondence between concepts of UML composite components and BIP compound components model Mutex i n c l u d e U s e r . b i p i n c l u d e R e s o u r c e . b i p c o n n e c t o r t y p e r e n d e z v o u s 2 ( P o r t p1 , P o r t p2 ) d e f i n e [ p1 p2 ] end compound t y p e MutexType component R e s o u r c e R1 component U s e r U2 component U s e r U2 c o n n e c t o r r e n d e z v o u s 2 C 1 r e l e a s e ( U1 . P RELEASE , R1 . PR RELEASE ) c o n n e c t o r r e n d e z v o u s 2 C 1 t a k e ( U1 . P TAKE , R1 . PR TAKE ) c o n n e c t o r r e n d e z v o u s 2 C 2 r e l e a s e ( U2 . P RELEASE , R1 . PR RELEASE ) c o n n e c t o r r e n d e z v

Figure 7 :

 7 Figure 7: Mutex BIP model.

Table 1 :

 1 . Correspondence between UML and BIP concepts

	UML Concept	BIP Concept	card.
	Atomic Component	AtomicType	1
	Composite Component	CompoundType	1
	Port	Port	n
	Interface	-	0

Safety analysis of architecturesWe are interested in explicitly modeling safety properties in order to complement incremental techniques. We are looking for a method which takes into account the incremental aspect of modeling in order to be integrated into

Acknowledgement: This research was supported by The National Foundation for Science and Technology Development (NAFOSTED) under Grant 102.03-2013.39: Automated verification and error localization methods for component-based software.