Imen Tounsi
email: imen.tounsi@redcad.org

Mohamed Hadj Kacem
email: mohamed.hadjkacem@redcad.org

Ahmed Hadj Kacem
email: ahmed.hadjkacem@fsegs.rnu.tn

Khalil Drira
email: khalil@laas.fr

A Renement-Based Approach for Building Valid SOA Design Patterns

Although design patterns have become increasingly popular, most of them are proposed in an informal way, which can give rise to ambiguity and may lead to their incorrect usage.

Patterns proposed by the SOA design pattern community are described with informal visual notations. Modeling SOA design patterns with a standard formal notation contributes to avoid misunderstanding by software architects and helps endowing design methods with renement approaches for mastering system architectures complexity. In this paper, we present a formal renement-based approach that aims, rst, to model message-oriented SOA design patterns with the SoaML standard language, and second to formally specify these patterns at a high level of abstraction using the Event-B method. These two steps are performed before undertaking the eective coding of a design pattern providing correct by construction pattern-based software architectures. Our approach is experimented through an example we present in this paper. We implemented our approach under the Rodin platform, which we use to prove model consistency.

Introduction

During its course of nearly ve decades, software engineering has known several main evolutions regarding approaches to software development. Structured programming gave way to the concept of object-orientation. Today's current trend is clearly service orientation. Serviceoriented architecture (SOA), as emerging architectural model, attracts attention worldwide.

Recent advances in SOA, including storage and networking, are providing exciting opportunities to make signicant progress in solving complex real-world challenges.

However these architectures are subject to some quality attribute failures (e.g., reliability, availability, and performance problems). Design patterns, as tested design solutions for common design problems within a context, have been widely used to tackle a spectrum of design problems and solve these weaknesses (Erl, 2009).

Patterns, proposed by the SOA design pattern community, are described with informal visual notations that can raise ambiguity and may lead to their incorrect usage (Erl, 2009).

Modeling these patterns with a standard formal notation contributes to avoid misunderstanding by software architects and helps endowing design methods with renement approaches for mastering system architectures complexity. The intent of our approach is to model and formalize (Tounsi et al., 2013c,b) message-oriented SOA design patterns. These two steps are performed before undertaking the eective coding of a design pattern, so that the pattern in question will be correct by construction. Our approach allows to reuse correct SOA design patterns, hence we can save eort on proving pattern correctness.

Our approach is based principally on three contributions. The rst contribution consists in modeling SOA design patterns with a semi-formal language. We propose an SoaML-based (Service oriented architecture Modeling Language) approach for this modeling step. We introduce a metamodel, using extended UML 2.0 notations. This modeling step is proposed in order to attribute a visual standard notation to SOA design patterns. This part of our approach provides several advantages. First, the modeling process is dened in a high level of abstraction providing a generic and reusable model. Second, our approach seeks to take advantage of the expressive power of standard visual notations provided by the semi-formal SoaML 2.0 language that makes easy the understanding of design patterns. Third, a software environment supporting the dierent features of this approach, has been implemented and integrated as a plug-in in the open source Eclipse framework.

The second contribution consists in proposing a generic formalization of these patterns using the Event-B method. This step is enhanced with the automatic transformation of SoaML pattern diagrams to Event-B pattern specications with respect to transformation rules (Tounsi et al., 2013a). We implement a rule-based generator which automatically translates the design pattern models that can be modeled using our tool into Event-B specications [START_REF] Tounsi | Using SoaML Models and Event-B Specications for Modeling SOA Design Patterns[END_REF].

Finally, the third contribution is based on formal methods. Using the Rodin theorem prover tool supporting Event-B, we check the syntax of the generated Event-B SOA design pattern models as well as their correctness (i.e. no deadlocks...) An other advantage of our approach is the use of renement techniques that make the understanding of pattern models easy. At the rst level of the modeling step an abstract model is specied which is further rened in the next levels to add more details. The graphical models in SoaML are automatically translated into Event-B specications at each renement level.

The remainder of the paper is organized as follows. In section 2, we provide some background information on the SoaML language and the Event-B notation. In section 3, we give a short overview of our approach. In section 4, we present our approach for modeling and rening SOA design patterns, then we show how we can prove their correctness. In section 5, we illustrate our approach through a case study. In section 6, we present the Eclipse plug-in that implements our approach. In section 7, we discuss the related works. We examine several research done on the modeling and the formalisation of design patterns in general. Ultimately, in section 8, we present conclusions and future work.

Basic concepts and notations

In this section, we provide some background information on the SoaML modeling language and the Event-B method.

SoaML

SoaML 1 (Service oriented architecture Modeling Language) (OMG, 2012) is a specication developed by the OMG that provides a standard way to architect and model SOA solutions.

It consists of a UML prole and a metamodel that extends the UML 2.0 (Unied Modeling Language).

To model SOA design patterns, we can represent many description levels. The highest level is described as Services Architectures where participants are working together using services.

A =B ∧ B =C ∧ C =A.
3 Our approach in a nutshell

Our contribution is a formal architecture-centric design approach. It supports the graphical modeling of message-oriented SOA design patterns with the semi-formal SoaML standard language (OMG, 2012), the automatic transformation of pattern diagrams to Event-B specications [START_REF] Abrial | Rodin: An Open Toolset for Modelling and Reasoning in Event-B[END_REF] and the formal verication of their correctness. We provide both structural and behavioral features of SOA design patterns in the modeling step as well as in the formalization step. As presented in Figure 1 All the specications are implemented under the Rodin [START_REF] Abrial | Rodin: An Open Toolset for Modelling and Reasoning in Event-B[END_REF] platform in order to be checked. The specication of a pattern P will be too complicated and error prone if it is done in one shot. In order to handle this complexity, we dene specication levels by using a step-wise development approach. Models are developed in a stepwise manner which are then automatically translated into Event-B specications. Here is our strategy, it is explained in Figure 1:

• In the rst level (Level0), we start with creating a very abstract model (a context P C0 and a machine P M 0). • In the next levels, we use the horizontal renement techniques (dened in [START_REF] Abrial | Rodin: An Open Toolset for Modelling and Reasoning in Event-B[END_REF] to gradually introduce detail and complexity into our model until obtaining the nal pattern specication. By applying a horizontal renement, we extend the state of a pattern model by adding new variables. We can strengthen the guards of an event or add new guards. We also add new actions in an event. Finally, it is possible to add new events [START_REF] Abrial | Rodin: An Open Toolset for Modelling and Reasoning in Event-B[END_REF]. When we move from Level(i) to Level(i+1), we add a new entity and its connections to the model. In Level(i+1), the context P Ci is extended with the context P C(i + 1) and the machine P M i is rened with the machine P M (i + 1). The

Proposed approach

The upcoming sections provide descriptions of our proposed approach.

Modeling SOA design patterns

We provide a modeling solution for describing SOA design patterns using a visual notation based on the graphical SoaML language (OMG, 2012). Three main reasons lead to use SoaML.

First, it is a standard modeling language dened by OMG. Second, it is used to describe SOA.

Third, diagrams used in SoaML, allow to represent structural features as well as behavioral features of design patterns.

The SoaML metamodel extends the UML2.0 metamodel to support an explicit service modeling in distributed environments. This extension is perfectly applied to SOA design pat- • Entities, that make up the architecture of an SOA design pattern, can be either Participants or Agents. A Participant represents a subclass of Component that provides and/or consumes services. Agents extend Participants with the ability to be active (their needs and capabilities may change over time).

• Entities can have Ports that constitute interaction points with their environment. These Ports are related to one or more provided or required Interf aces and their types can be either Service or Request.

• The communication path between Services and Requests within an architecture is called ServiceChannel, it extends the metaclass Connector. • A Capability is the ability to act and produce an outcome that achieves a result, it extends the metaclass Class. A Participant can realize zero or several capabilities with the link CapabilityRealization.

• ServiceInterfaces are used to describe provided and required operations to complete services functionality, they can be used as protocols for a service port or a request port.

• The MessageType is used to specify information exchanged between services, it extends the metaclass DataT ype. An Attachment is a part of a message that is attached to it, it extends the metaclass P roperty. The stereotype Property extends the metaclass P roperty with the ability to be distinguished as an identifying property (primary key" for messages). In some SOA design patterns entities are organized in various ways across many orthogonal dimensions, for example they can be organized by service layers or by physical boundaries.

Catalogs provide a means of classifying and organizing elements by Categories for any purpose, they extends the metaclass P ackage and specializes the stereotype NodeDescriptor.

Categories are related to Catalogs with the relation Belongs_to. A collection of related entities are characterized by a Category. Applying a Category to an entity by using a

Categorization places that entity in the Catalog.

Formalizing SOA design patterns

In this section, we present an overview of the generic formalization of SOA design patterns with the Event-B method [START_REF] Abrial | Rodin: An Open Toolset for Modelling and Reasoning in Event-B[END_REF]. We use the Rodin Platform [START_REF] Abrial | Rodin: An Open Toolset for Modelling and Reasoning in Event-B[END_REF] in order to prove the correctness of the pattern specication.

Three main reasons lead to use Event-B method. First, it allows the specication of structural and behavioral features of design patterns. Second, renement techniques proposed by this method allow to represent patterns at dierent abstraction levels. Third, mathematical proofs allow to verify model consistency and consistency between renement levels.

A pattern P is described with structural and behavioral features. Structural features are specied with one or several contexts P Ci and behavioral features are specied with one or several machines P M i.

Structural Features

Structural features are generally specied by assertions on the existence of types of entities in the pattern. The conguration of the entities is also described in terms of the static relationships between them [START_REF] Zhu | Laws of pattern composition[END_REF].

Entities, that compose the architecture of an SOA design pattern, can be either P articipants or Agents. Using Event-B, we specify in a context P Ci the two entities as constants. The set Entity is composed of the set of all P articipants and the set of all Agents (Entity = P articipant∪Agent ∧ P articipant∩Agent = ∅). This is specied by using a partition in the AXIOMS clause (Entity_partition).

SETS

Entity

CONSTANTS

P articipant Agent

AXIOMS

Entity_partition : partition(Entity, P articipant, Agent) Agents name A i are also specied as constants. The set of agents is specied using a partition in the AXIOMS clause (Agent_partition), that is

Agent = {A 1 ,...,A n } ∧ A 1 =A 2 ∧...∧ A n-1 =A n . CONSTANTS A1 .
.. An AXIOMS Agent_partition : partition(Agent, {A1}, ..., {An})

In the SoaML modeling a ServiceChannel PushE i E j is a connection between two entities. It can be between two participants (PushP i P j ), two agents (PushA i A j ) and between a participant and an agent. When the direction of the connection is from a participant to an agent, it is named PushP i A j and if it is from an agent to a participant, it is named PushA i P j . Formally, ServiceChannels are specied with an Event-B relation between two entities. ServiceChannel's name PushE i E j are specied with constants in the CONSTANTS clause. The set of ServiceChannels is composed of all ServiceChannel's name. This is specied formally with a partition (ServiceC hannel_partition).

CONSTANTS

Behavioral features

Behavioral features of a design pattern are generally dened by assertions on the temporal orders of the messages exchanged between the dierent pattern entities [START_REF] Zhu | Laws of pattern composition[END_REF].

A machine of a pattern specication P M i has a state dened by means of a number of variables and invariants. Some of variables can be general as the variable Send, which denotes the sent message and the variable P rocess, which denotes the message process.

The variable Send is dened with the invariant Send_Relation which specify that Send is a relation between a ServiceChannel and a M essageT ype so we know the sender, the receiver and the sent message. The variable P rocess is dened with the invariant Process_Function which specify that P rocess is a function between a P articipant and a M essageT ype so we know which participant is processing which message.

VARIABLES

Send P rocess

INVARIANTS

Send_Relation : Send ∈ ServiceChannel ↔ M essageT ype Process_Function : P rocess ∈ P articipant → M essageT ype

Each pattern has its own behavior but some events can be general like the event of sending a message Sending_M i and the event of processing a message P rocessing_M i .

Event

Formal verication

SoaML as a semi-formal language provides many advantages to dening SOA design patterns, such as standard visual notation. However, the fact that SoaML lacks a precise semantics is a serious drawback because it does not allow proofs and in consequence,

with SoaML, we can not verify required properties like liveness (no deadlocks), and reachability property.

During our development, we use a systematic approach that consists in developing a series of more and more accurate models of the pattern we want to build. This technique is called renement [START_REF] Abrial | Rodin: An Open Toolset for Modelling and Reasoning in Event-B[END_REF]. Each pattern model is analyzed and proved, thus enabling us to establish that it is correct relative to a number of criteria. As a result, when the last model is nished, we will be able to say that this model is correct by construction [START_REF] Abrial | Rodin: An Open Toolset for Modelling and Reasoning in Event-B[END_REF].

Four formal verication techniques have been used for checking design patterns;

type checking, model checking, animation and theorem proving.

INVARIANTS Can_Send_INV

: ∀z, x, y•z ∈ Entity ∧ {x → y} ∈ ServiceChannel ↔M essageT ype ∧ dom({x}) = {z} ∧ x → y ∈ Send ⇒ z → y ∈ Can_Send
When we enrich the pattern model by using renement techniques, we make sure that rened models are not contradictory. These proofs are automatically generated by the Rodin Platform. Our approach allows developers to reuse correct SOA design patterns, hence we can save eort on proving pattern correctness.

Case study: Asynchronous Queuing pattern

Asynchronous Queuing pattern2 is an SOA design pattern for inter-service message exchange (Erl, 2009). It belongs to the category "Service Messaging Patterns". It establishes an intermediate queuing mechanism that enables asynchronous message exchanges and increases the reliability of message transmissions when service availability is uncertain. The problem addressed by this pattern is that when services interact synchronously, it can inhibit performance and compromise reliability when one of services cannot guarantee its availability to receive the message. Synchronous message exchanges can impose processing overhead, because the service consumer needs to wait until it receives a response from its original request before proceeding to its next action.

Responses can introduce latency by temporally locking both consumer and service. The proposed solution by this pattern is to introduce an intermediate queuing technology into the architecture. The behavior of this pattern is described in detail section 5.1.2.

Modeling step

Structural features

In the structural modeling step, we specify entities of the pattern and their dependencies (connections) in the Participant diagram (Figure 3) and we specify their interfaces and exchanged messages in the ServiceInterface and MessageType diagrams respectively (Figure 4).

ServiceA, ServiceB and the Queue are dened as participants because they provide and use services. As shown in Figure 3, ServiceB provides a ServiceX used by ServiceA and the Queue provides a storage service. We did not represent the storage service provided by the Queue in order to concentrate principally on the communication between ServiceA and ServiceB and to not complicate the presented diagrams. Participants provide capabilities through service ports. Both ServiceA and ServiceB have a port typed with ServiceX". ServiceB is the provider of the service and has a Service port. ServiceA is a consumer of the service and uses a Request port. We note that ServiceB's port provides the ProviderServiceX" interface and requires the OrderServiceX" interface. Since ServiceA uses a Request port preceded with a tilde (∼), the conjugate interfaces are used. So, ServiceA's port provides the OrderServiceX" interface and uses the ProviderServiceX" interface. In this diagram, ServiceChannels are explicitly represented, they enables communication between the dierent participants.

IJCC IJCC

Figure 4 shows a couple of MessageType that are used to dene the information exchanged between ServiceA and ServiceB. These messages are RequestMessage" and ResponseMessage", they are used as types for operation parameters of the service interfaces. The type of the ServiceB's port is the UML interface ProviderServiceX" that has the operation processServiceXProvider". This operation has a message style parameter where the type of the parameter is the MessageType ResponseMessage".

ServiceA expresses its request for the ServiceX" using its request port. The type of this request port is the UML interface OrderServiceX". This interface has an operation ProcessServiceXOrder" and the type of parameter of this operation is the MessageType RequestMessage". This message is intercepted and stored by an intermediary queue. ServiceB receives the message forwarded by the Queue and ServiceA releases its resources and memory. While ServiceB is processing the message, ServiceA consumes no resources. After completing its processing, ServiceB issues a response message back to ServiceA (this response is also received and stored by the intermediary Queue). ServiceA receives the response and completes the processing of the response while ServiceB is deactivated.

Formalization Step

To illustrate the formalization step of our approach, we apply it on the same pattern example used in the modeling step (Asynchronous Queuing pattern). The model of this pattern is composed of two contexts AQC0 and AQC1 and two machines AQM 0 and AQM 1 (AQC denotes Asynchronous Queuing Context and AQM denotes Asynchronous Queuing Machine). In the rst level of specication, we specify the pattern at a high level of abstraction, i.e. we suppose that the communication is only between

ServiceA and ServiceB. In the second level, we add the Queue and all its behavior to the model. Machines and contexts relationships are illustrated in Figure 6.

Structural features

In the Asynchronous Queuing pattern, we have three Participants: ServiceA, ServiceB and the Queue. In the context AQC0, we specify only two participants ServiceA and ServiceB.

CONSTANTS

ServiceA ServiceB

AXIOMS

Participant_partition : partition(P articipant, {ServiceA}, {ServiceB})

ServiceA and ServiceB are connected together through the ServiceChannels P ushAB and P ushBA. The second context AQC1 is an extension of the context AQC0. In this context we add a new constant Queue and we redene the P articipant_partition by adding the Queue. Also we add four constants P ushAQ, P ushQB, P ushBQ and P ushQA to dene the new ServiceChannels. Axioms that restrict the domain and the range of these ServiceChannels are also added to the context. This part of specication belongs to the Participant diagram (Figure 3) and MessageType diagram (Figure 4).

CONSTANTS

Behavioral features

To specify behavioral features, we have two steps. First, we specify the pattern with a machine at a high level of abstraction. Second, we add all necessary details to the rst machine by using the renement technique.

In the rst machine AQM 0, we only specify the communication between ServiceA and ServiceB, i.e. the queue is completely transparent, meaning that neither ServiceA nor ServiceB may know that a queue was involved in the data exchange. So, the behavior is described as follows: ServiceA sends a RequestM essage to ServiceB and then remains released from resources and memory (unavailable). When ServiceB becomes available, it receives the Request M essage, process it and sends the Response M essage. When ServiceA becomes available, it receives the Response M essage, process it and then becomes deactivated.

Formally, we can use three variables to represent the state of the pattern; Dispo to denote the state of the participant either available or not, Send to indicate who sends what message and P rocess to indicate which participant is processing what message. The rst invariant Dispo_F unction species the availability feature of participants. This feature is specied with a partial function which is a special kind of relation (each domain element has at most one range element associated with it) i.e. the function Dispo relates P articipants to a Boolean value in order to specify their availability. We use the partial function because a participant cannot be available and not available at the same time. The second invariant, i.e. Send_Relation, species what is the sent message, who is the sender and the receiver. The third invariant, i.e. P rocess_F unction, species the message process with a partial function that relates a P articipant to a M essageT ype.

INVARIANTS

Dispo_Function : Dispo ∈ P articipant → BOOL Send_Relation : Send ∈ ServiceChannel ↔ M essageT ype Process_Function : P rocess ∈ P articipant → M essageT ype

As presented in the pattern, initially ServiceA is available and ServiceB is not available. Also, there are no messages sent and no message is processed. Hence, both

Send relation and P rocess function are initialized to the empty set.

INITIALISATION begin init1 : Dispo := {ServiceA → T RU E, ServiceB → F ALSE} init2 : Send := ∅ init3 : P rocess := ∅ end

The dynamic system can be seen in Figure 5. It is formalized by the following events; Sending_Req, Processing_Req, Sending_Resp and Processing_Resp (Req denotes Request and Resp denotes Response). Sending the request message starts when there is no messages sent and ServiceA is available. This is formally specied with the event Sending_Req. This is illustrated in Figure 7. The event of processing the request is triggered when the message is sent, not yet processed and ServiceB is available. In the action part, we add, to the process function, the pair (ServiceB → RequestM essage) to denote that ServiceB is processing the request.

Event Processing_Req when grd1 The second machine AQM 1 renes the cited above AQM 0 machine and uses the AQC1 context. In the AQM 1 machine, we introduce the behavior of the Queue, so as to complete all the behavior of the pattern. We add two new variables named Store and T ransmit. Store is specied with a relation that relates a P articipant to a M essageT ype. We add an invariant that restricts the domain of this relation to only the Queue. Consequently, Store reveals what message the queue is storing. T ransmit is specied with a partial function that relates a P articipant to a M essageT ype. We add an invariant that restricts the domain of this function to only the Queue. The AQM 1 machine events are dened in Figure 8. We keep the Sending_Req and the Sending_Resp events. We add four new events namely Storing_Req, Trans-mitting_Req, Storing_Resp and Transmitting_Resp. These events are related to the Queue behavior. We add more details to the abstract events Processing_Req and Processing_Resp. The two events of processing the messages are rened by adding in the guards clause the condition of transmitting the message. If a participant (ServiceA or ServiceB) receives a message, the storage of this message in the Queue becomes unnecessary, so in the processing event we empty the Queue. The plug-in transforms the generated XML le, according to transformation rules (described in (Tounsi et al., 2013a)) expressed with the XSLT language [START_REF] Tounsi | Using SoaML Models and Event-B Specications for Modeling SOA Design Patterns[END_REF], into Event-B specications. These specications can be imported under the Rodin platform to verify their correctness.

Tool

By applying transformations rules on the generated XML specications, we obtain Event-B specications presented in Figure 10. Among research related to design patterns for Object-Oriented Architectures, we present the work of Gamma et al [START_REF] Gamma | Design Patterns: Elements of Reusable Object-Oriented Software[END_REF]. They have proposed a set of design patterns in the eld of object-oriented software design. These patterns are described with graphical notations based on the OMT (Object Modeling Technique) notation. There is no formal semantics associated with these patterns, hence their meanings can be imprecise. Several research have proposed the formalization of these patterns [START_REF] Gamma | Design Patterns: Elements of Reusable Object-Oriented Software[END_REF] (hereafter referred to as GoF) using dierent formal notations. We quote: Zhu et al. [START_REF] Zhu | Laws of pattern composition[END_REF] [START_REF] Blazy | Reuse of specication patterns with the B method[END_REF] propose an approach for specifying design patterns and how to reuse them formally. They use B-method to specify structural features of design patterns but they do not consider the specication of their behavioral In the branch of SOA design patterns, we nd out the work of Erl. Erl has proposed a set of design patterns for SOA (Erl, 2009). Each pattern is presented with a proprietary informal notation presented in a symbol legend. These patterns are modeled without any formal specication. In order to understand them, the rst step is to form a knowledge on the pattern-related terminology and notation. In addition, Erl proposes a set of specic pattern symbols used to represent a design pattern.

All cited research work are dealing with object oriented design patterns, in our research work we are interested in SOA design patterns dened by Erl (Erl, 2009). For these patterns, there are no work that model or formally specify them. Erl presents his patterns with an informal proprietary notation because there is no standard modeling notation for SOA, but now OMG announces the publication of the SoaML language (OMG, 2012), it is a specication for the UML prole and a metamodel for services.

So, in our work (Tounsi et al., 2013c,b), we propose to model SOA design patterns with the SoaML standard language. After the modeling step, we propose to specify these patterns formally. Similar to [START_REF] Zhu | Laws of pattern composition[END_REF][START_REF] Kim | A formalism to describe design patterns based on role concepts[END_REF] we dene both structural and behavioral features of design patterns using FOL, but we use a dierent formal method which is Event-B.

In conclusion, most proposed patterns are described with a combination of textual description and a graphical presentation [START_REF] Gamma | Design Patterns: Elements of Reusable Object-Oriented Software[END_REF], some times using proprietary notations [START_REF] Hohpe | Enterprise Integration Patterns: Designing, Building, and Deploying Messaging Solutions[END_REF], (Erl, 2009), in order to make them easy Erl (Erl, 2009) Our appr [START_REF] Tounsi | An Approach for Modeling and Formalizing SOA Design Patterns[END_REF] Pattern modeling to read and understand. However, using these descriptions makes patterns ambiguous and may lack details. There have been many research that specify patterns using formal techniques [START_REF] Zhu | Laws of pattern composition[END_REF][START_REF] Blazy | Reuse of specication patterns with the B method[END_REF] but research that model design patterns with semi-formal languages are few [START_REF] Mapelsden | Design pattern modelling and instantiation using DPML[END_REF]. We nd a number of approaches that formally specify dierent sorts of features of patterns: structural, behavioral, or both. Table 1 is a recapitulation of related works that contains a comparison between the above-mentioned approaches and our approach.

Conclusions

In this paper, we presented a formal renement-based design approach supporting the modeling and the formalization of message-oriented SOA design patterns. The modeling phase allows to represent SOA design patterns with a graphical standard notation using the SoaML language. The formalization phase allows to formally specify both structural and behavioral features of these patterns at a high level of abstraction using Event-B method. We implemented the elaborated specications under the Rodin platform.

We illustrated our approach through a pattern example within the "Service messaging patterns" category. In order to reach the generality and the validity of our approach, we have applied it to more pattern examples within the "Service messaging patterns" category and "Transformation patterns" category.

In real applications, problems are complex and their solutions can be represented by compound patterns that require the combination and reuse of other design patterns.

So, as future work, we are working on formally specifying pattern composition and verifying some related properties.

  , in the modeling step, structural features are described with the Participant diagram, the ServiceInterface diagram and the Mes-sageType diagram. These diagrams are modeled with an Eclipse plug-in that we propose and transformed to one or several CONTEXTS in the Event-B specications. Behavioral features, are described with the UML2.0 Sequence diagram that provides a graphical notation to describe dynamic aspects of design patterns. This diagram is modeled with an Eclipse plug-in that we propose and transformed to one or several MACHINES in the Event-B specications.

Figure 1 :

 1 Figure 1: Approach overview (see online version for colours)

  terns modeling. We model structural features of design patterns with Participant diagram, ServiceInterface diagram and MessageType diagram. We model behavioral features with the UML2.0 sequence diagram. To model these diagrams, we use the part of the SoaML metamodel presented in Figure 2. Gray classes represent abstract metaclasses and white classes represent stereotypes. In follows, we only present the base concepts that we use in the pattern modeling.

Figure

  Figure 2: SOA design patterns Metamodel

Figure 3 :

 3 Figure 3: Participant diagram (see online version for colours)

Figure

  Figure 4: ServiceInterface and MessageType diagrams

Figure 5 :

 5 Figure 5: Sequence diagram (see online version for colours)

Figure

  Figure 6: Contexts and machines relationships

Figure:

  Figure 7: AQM 0 Events

  Consequently, Transmit reveals what message the Queue is transmitting. Initially Store relation and T ransmit function are both initialized to the empty set. INVARIANTS Store_Relation : Store ∈ P articipant ↔ M essageT ype Store_Dom_Rest : dom(Store) = {Queue} ∨ Store = ∅ Transmit_Function : T ransmit ∈ P articipant → M essageT ype Transmit_Dom_Rest : dom(T ransmit) = {Queue} ∨ T ransmit = ∅

Figure 8 :

 8 Figure 8: AQM 1 events (see online version for colours)

  Our approach is enhanced by an Eclipse plug-in 3 . It is a graphical modeling tool that makes the modeling of SOA design patterns easier. It ensures an easy and ecient modeling way of SOA design patterns. For the development of the plug-in, we have used several Eclipse frameworks, i.e., GMF (Graphical M odeling F ramework) (Eclipse, 2010a), EMF (Eclipse M odeling F ramework) (Steinberg et al., 2009) and GEF (Graphical Editing F ramework) (Eclipse, 2010b). Several diagrams are available in the plug-in; we can model Participant diagram, Service Interface diagram, Message Type diagram and UML2.0 Sequence diagram. The SOA design patterns diagram editor is a tool where diagrams can be created to model patterns. Graphical elements can be picked up from a tool palette and created in the Diagram editor pane in a drag-and-drop" way. Elements of the palette are listed under N odes and Links elements. The Property Editor" can be used for changing properties of the object selected in the diagram editor pane. Property elements vary depending on the type of the chosen object. Figure 9 shows the diagram editor of the SOA design patterns with an illustration of the pattern example Asynchronous Queueing". After modeling a design pattern, the plug-in generates an XML le describing it.

7

  Figure 9: SOA design patterns plug-in (see online version for colours)

  specify 23 GoF patterns formally. They use the First-Order Logic (FOL) induced from the abstract syntax of UML dened in the Graphic Extension of BNF (GEBNF) to dene both structural and behavioral features of design patterns. Taibi et al.[START_REF] Taibi | Formalising design patterns composition[END_REF][START_REF] Taibi | Formal specication of design pattern combination using BPSL[END_REF] develop the Balanced Pattern Specication Language (BPSL) to formally specify patterns, pattern composition and instances of patterns. This language is used as a formal basis to specify structural features of design patterns in the FOL and behavioral features in the Temporal Logic of Action (TLA). Taibi et al. use as a case study a pattern composition proposed by GoF. Dong et al. (Dong et al., 2007) focus on the specication of design pattern component. They use the FOL to specify structural features of patterns with Object-Z and TLA to specify their behavioral features. As examples, they use GoF patterns. Kim et al. (Kim and Carrington, 2009) present an approach to describe design patterns based on role concepts. First, they develop an initial role meta-model using Eclipse Modeling Framework (EMF), then they transform the meta-model to Object-Z in order to specify structural features. Behavioral features of patterns are also specied using Object-Z. Kim et al. also use GoF patterns as examples. Blazy et al.

Figure 10 :

 10 Figure 10: Excerpt of Event-B specication results (see online version for colours)

  It is modeled using UML collaborations diagram stereotyped ServicesArchitecture. The next level is described as P articipants using UML class diagram stereotyped Participant. The Service Contract is at the middle of the SoaML set of SOA architecture constructs, it describes services mentioned above and it is modeled using UML collaboration diagram stereotyped ServiceContract. In the next level, we nd the specication of Interf aces and M essage T ypes using UML class diagrams stereotyped respectively ServiceInterface and MessageType. For both the service contract and the interface levels we can specify Abrial, 2010) is a formal method for developing systems via stepwise renement, based on rst-order logic. The method is enhanced by its supporting Rodin Platform[START_REF] Abrial | Rodin: An Open Toolset for Modelling and Reasoning in Event-B[END_REF] for analyzing and reasoning rigorously about Event-B models. The basic concept in the Event-B development is the model which is made of two types of components: contexts and machines. A context describes the static part of a model, whereas a machine describes the dynamic behavior of a model. Machines and contexts can be inter-related: a machine can be ref ined by another one, a context can be extended by another one and a machine can see one or several contexts. Each context has a name and other clauses like "Extends", "Constants", "Sets" to declare a new data type and "Axioms" that denotes the type of the constants and the various predicates which the constants obey. It is a predicate that is assumed to be true in the rest of the model. Like a context, a machine has an identication name, variables that constitute the state of the machine (their values are determined by an initialization and can be changed by events), invariants and events.A relation is used to describe ways in which elements of two distinct sets are related. IfA and B are two distinct sets, then R ∈ A ↔ B denotes a relation between A and B. The domain of R is the set of elements in A related to something in B: dom(R). The range of R is the set of elements of B to which some element of A is related: ran(R). We also say that A and B are the source and target sets of R, respectively. Given two elements a and b belonging

	2.2	Event-B method
	Event-B (

behavioral features of patterns using any UML behavior (e.g sequence or activity diagrams). 1 http ://www.omg.org/spec/SoaML/ to A and B respectively, we call ordered pair a to b, the pair having the rst element a (start element) and the last element b (arrival element). We denote that by a → b or (a,b). A partial function is a relation where each element of the domain is uniquely related to one element of the range. If A and B are two sets, then A → B denotes the set of partial functions from A to B. Partitions are used in two dierent manners. The rst one is partition(S, A,B). It means that A and B partition the set S, i.e. S=A∪B ∧ A∩B = ∅. The second one is partition(S, {A},{B},{C }) which is a specialized use for enumerated sets. It means that S={A,B,C} ∧

  In the SoaML modeling Catalogs provide a means of classifying and organizing elements by Categories. A collection of related entities are characterized by a Category. Applying a Category to an entity by using a Categorization places that entity in the Catalog.Formally, Catalogs are specied with an Event-B catalog type and catalogs name C i are specied with constants in the CONSTANTS clause. The set of Catalogs is composed of all Catalogs name. This is specied formally with a partition (C atalog_partition). Catalogs, Categories are specied with an Event-B category type and categories name C i are specied with constants in the CONSTANTS clause. The set of Categories is composed of all Categories name. This is specied formally with a partition (C ategory_partition). The containment relation of a Catalog with Categories is specied with the relation Belongs_to and the link of Categorization is specied with a relation between a Category and an Entity.

	SETS
	M essageT ype
	CONSTANTS
	M1, ..., Mn
	AXIOMS
	Message_partition : partition(M essageT ype, {M1}, ..., {Mn})
	Like SETS
	Catalog
	Category
	CONSTANTS
	C1, ..., Cn
	Ca1, ..., Can
	Belongs_to
	Categorization
	The ServiceInterface diagram models entity interfaces and their relations with
	messages. We don't do the formalisation of all the elements of this diagram to the
	event-B specications, but we do it to know only what entity can send what message.
	ServiceChannel
	P ushEiEj, ..., P ushEnEm

AXIOMS

ServiceChannel_Relation : ServiceChannel ∈ Entity ↔ Entity ServiceChannel_partition : partition(ServiceChannel, {P ushEiEj}, ...,

{P ushEnEm})

To dene the source and the target of a service channel, two axioms must be added, namely the domain and the range. PushEiEj_Domain : dom({P ushEiEj}) = {Ei} PushEiEj_Range : ran({P ushEiEj}) = {Ej} AXIOMS Catalog_partition : partition(Catalog, {C1}, ..., {Cn}) Category_partition : partition(Category, {Ca1}, ..., {Can}) Belongs_to_Relation : Belongs_to ∈ Catalog ↔ Category Categorization : Categorization ∈ Category ↔ Entity Belongs_to_init : Belongs_to = {Cn → Ca1, ..., Cn → Can} Categorization_init : Categorization = {Ca1 → Pi, ..., Can → Aj} A Capability is the ability to produce an outcome that achieves a result. Each Participant is comprised of a set of capabilities. Capabilities are formally specied as follows. SETS Capability CONSTANTS Cp1, ..., Cpn P rovide AXIOMS Capability_partition : partition(Capability, {Cp1}, ..., {Cpn}) Provide_Relation : P rovide ∈ P articipant ↔ Capability Provide_init : P rovide = {Pi → Cp k , ..., Pj → Cpm} CONSTANTS Can_Send AXIOMS Can_Send_Relation : Can_Send ∈ entity ↔ M essageT ype Can_Send_init : Can_Send = {Ei → M k , ..., Ej → Mm} MessageType is the type of messages exchanged between dierent entities, it is declared in the SETS clause. Messages name M i are specied in the CONSTANTS clause. They are attributed with their type with a partition in the AXIOMS clause (M essage_partition).

  Modelchecking and animation are two techniques used to show the dynamic behavior of a model and they allow to systematically explore all its reachable states. We use them to check the behavior of the pattern if it is correct or not. Some temporal/behavioral properties are veried like liveness (no deadlocks present in the model) and reachability (prove that an event whose guard is not necessarily true now will nevertheless certainly occur within a certain nite time) properties. This is done by the model checker ProB[START_REF] Leuschel | ProB: A Model Checker for B[END_REF]. Theorem proving technique allows to check properties which can be experimented either as predicates (INVARIANTS, AXIOMS, THEOREMS) or with guards in the events. It is also ensured by proof obligations. They dene what is to be proved to ensure the consistency of an Event-B pattern model. As example of consistency constraint, we check that each entity can't send a message only if it is authorised. This is controlled by the invariant Can_Send_INV. For sequence diagrams, we require that every message must start an activation.

Type checking is a technique controlling low level properties of variables in a program. We use it to check the syntax of the generated Event-B pattern specications and to detect modeling errors (ex. modeling incomplete ServiceChannel). It is done within the compiler.

  For each service channel, we add two axioms in order to dene the domain and the range. For example, for P ushAB relation we add the following two axioms to denote that its source is ServiceA and its target is ServiceB.We did not specify ports and interfaces because they are ne details.Whereas, we specify messages to know what message is being exchanged. So, we dene the M essageT ype set, two constants RequestM essage and ResponseM essage and then

	ServiceChannel
	P ushAB
	P ushBA
	AXIOMS
	ServiceChannel_Relation : ServiceChannel ∈ Entity ↔ Entity
	ServiceChannel_partition : partition(ServiceChannel, {P ushAB}, {P ushBA})
	PushAB_Domain : dom(P ushAB) = {ServiceA}
	PushAB_Range : ran(P ushAB) = {ServiceB}
	the message partition.
	SETS
	M essageT ype
	CONSTANTS
	RequestM essage
	ResponseM essage

AXIOMS

Message_partition : partition(M essageT ype, {RequestM essage}, {ResponseM essage})

  ServiceB sends the ResponseM essage when the request message is processed and when ServiceB is available. After that ServiceB becomes unavailable.

	Event Sending_Resp
	when
	grd1 : ServiceB ∈ dom(Dispo) ∧ Dispo(ServiceB) = T RU E
	grd2 : RequestM essage ∈ ran(P rocess)
	grd3 : ResponseM essage / ∈ ran(Send)
	then
	act1 : Send := Send ∪ {P ushBA → ResponseM essage}
	act2 : Dispo(ServiceB) := F ALSE
	end
	After sending the response, ServiceA process the received message and becomes
	unavailable.
	Event Processing_Resp
	when
	grd1 : RequestM essage ∈ ran(Send)
	grd2 : ServiceA ∈ dom(Dispo) ∧ Dispo(ServiceA) = T RU E
	then
	act1 : P rocess := P rocess -{ServiceA → ResponseM essage}
	act2 : Dispo(ServiceA) := F ALSE
	end
	: RequestM essage ∈ ran(Send)
	grd2 : RequestM essage / ∈ ran(P rocess)

grd3 : ServiceB ∈ dom(Dispo) ∧ Dispo(ServiceB) = T RU E then act1 : P rocess := P rocess -{ServiceB → RequestM essage} end

Table 1 :

 1 Summary table of related works

		OMT	GoF	GoF	GoF	GoF	GoF	Prop	Prop	SoaML
	Structural formal specica-tion Behavioral formal tion specica-	_ _	(OMT) GEBNF (FOL) GEBNF (FOL)	(OMT) BPSL (FOL) BPSL (TLA)	(OMT) Object Z (FOL) TLA	(OMT) Object Z (FOL) Object (FOL) Z	(OMT) B Method _	Nota _ _	Nota _ _	Event-B Event-B

http://soapatterns.org/design_patterns/asynchronous_queuing

9 Acknowledgment This paper is done with the support of the Ministry of Higher Education and Scientic Research of Tunisia within the Tunisian-French scientic cooperation (DGRS/CNRS). References J.-R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York, NY, USA, 1st edition, 2010. ISBN 0521895561, 9780521895569.


Michaël Bulois
email: michael.bulois@univ-st-etienne.fr

Pascal Hivert
email: pascal.hivert@math.uvsq.fr

Sheets in symmetric Lie algebras and slice induction

Keywords: 17B70, 17B25 semisimple symmetric Lie algebras, adjoint orbits, sheets, induction of nilpotent orbits, Slodowy slice, G

published or not. The documents may come

Sheets of symmetric Lie algebras and slice induction

Michael Bulois, Pascal

Introduction

Let g be a reductive Lie algebra defined over an algebraically closed field of characteristic zero. Assume that g is Z/2Z-graded g = k ⊕ p, with even part k and odd part p. We may refer to such a symmetric Lie algebra as the symmetric pair (g, k).

The algebraic adjoint group G of g acts on g and the closed connected subgroup K ⊂ G with Lie algebra k acts on p. A sheet of p (resp. g) is an irreducible component of a locally closed set of the form p (m) := {x ∈ p | dim K.x = m}, (resp. g (m) := {x ∈ g | dim G.x = m}).

Sheets of g have been extensively studied in several papers in the past decades.

On one hand, the key papers of Borho and Kraft [BK, Bo] describe sheets as disjoint union of so-called decomposition classes (also known as Jordan classes).

1

The decomposition classes form a finite partition of g, each class being irreducible, locally closed and of constant orbit dimension. In particular, there is a dense class in each given sheet. An important notion used in [BK, Bo] is the parabolic induction of orbits introduced in [LS] which gives rise to a notion of induction of decomposition classes. It is shown in [Bo] that a sheet S with dense decomposition class J is precisely the union of the decomposition classes induced from J. Two consequences of this are the following. Firstly, each sheet contains a unique nilpotent orbit. Secondly, there is a parameterization of sheets coming with induction [START_REF] Borho | Über Bahnen und deren Deformationen bei linear Aktionen reduktiver Gruppen[END_REF]§5]. Later, Broer developed methods for a deeper study of decomposition classes, their closures, regular closures, quotients and normalizations in [START_REF] Broer | Decomposition varieties in semisimple Lie algebras[END_REF][START_REF] Broer | Lectures on decomposition classes[END_REF].

On the other hand, making use of the previous parameterization, it is shown in [Kat] that sheets are parameterized by their Slodowy slices. More explicitly, let e be a representative of the nilpotent orbit of a sheet S of g and embed e in an sl 2 -triple S = (e, h, f ). The Slodowy slice of S (with respect to e) is e + X(S, S ) := S ∩ (e + g f ),

where g f stands for the centraliser of f in g. Katsylo proves that S = G.(e + X(S, S )) and that a geometric quotient of S can be expressed as a finite quotient of e+X(S, S ). In [IH], Im Hof shows that the morphism G×(e+X(S, S )) → S is smooth. This relates smoothness of S to smoothness of e + X(S, S ) and eventually leads to a proof of smoothness of sheets in classical Lie algebras.

To our knowledge, the only known case of a singular sheet lies in a simple Lie algebra of type G 2 [Pe, BK]. In this case, the two non-trivial sheets (i.e. non-regular and with more than one orbit) are the two irreducible components of the set of subregular elements. One of these subregular sheets S g 2 is smooth while the other S g 1 is singular. More precisely, we can see that three analytical germs of S g 1 intersect in the neighborhood of elements of the subregular nilpotent orbit. In [START_REF] Hivert | Nappes sous-régulières et équations de certaines compactifications magnifiques[END_REF]§2], an explicit desingularization of S g 1 is constructed in terms of the well-known projection so 7 ։ g.

We now look at the symmetric case and sheets of p. Most of the ground results the authors are aware of in this setting are gathered in [START_REF] Tauvel | Lie algebras and algebraic groups[END_REF]]. An important feature is that there exists a notion of K-decomposition class in p and these classes share several good properties with the usual decomposition classes of g. In particular, there is still a unique dense K-decomposition class in each sheet of p. In addition, each sheet of p contains at least one nilpotent orbit. However the uniqueness statement no longer holds in general.

One of the obstacles rising in the study of the sheets of p is the lack of a well behaved notion of parabolic induction as one can check in the (sl 2 , so 2 )-case. For instance the induction theory developed in [START_REF] Ohta | Induction of nilpotent orbits for real reductive groups and associated varieties of standard representations[END_REF] does not preserve orbit codimension, hence is of little help for our purpose. The main philosophy of [Bu] consists in noting that, at least in the case g = gl n , the Slodowy slices of a sheet S of p still seem to encode significant geometric information of S. One of the aim of the present work is to justify this assertion in a more systematic manner. For instance, we show in Section 2 that several properties of sheets, such as dimension, smoothness and orbits involved, are fully reflected in the corresponding Slodowy slices. We state these results for wider classes of subvarieties of p in Proposition 2.4, Theorem 2.6 and Proposition 2.8.

Then we introduce in Section 3 the notion of slice induction. It turns out to be precise enough to rebuilt important parts of the theory resulting from parabolic induction in the Lie algebra case. This includes (see Theorem 3.5 and Corollary 3.7):

• Construction of one parameter deformations of orbits.

• Stratification properties for decomposition classes.

• Characterization of a sheet with dense K-decomposition class J as the union of induced classes from J.

In the Lie algebra case, this also provides a new insight on these results.

In [Bu], the connection between sheets of g and sheets of p was studied. In particular it was shown that, whenever sheets of g are smooth, sheets of p are also smooth. The last goal of this paper is the description of sheets of p in the non-trivial symmetric Lie algebra of type G 2 . We make use of two approaches for this study. In Section 4.1, we study the subregular sheets through their Slodowy slices. This provides the set-theoretical description of the sheets and describes the behavior of the singularities of S g 1 through the intersection with p. In Section 4.2, we exploit the symmetry of g making use of 4-ality as described in [LM]. This allows us to construct a nice desingularization in so 7 of the singular sheet (Proposition 4.5), following the guidelines of [Hi].

It is plausible that most of what is stated in Section 2 and 3 remains true in the more general setting of θ-representation. However, the authors are unaware of references for a general theory of decomposition classes in this setting. exists a symmetric Lie algebra ĝ = k ⊕ p such that the k-module p is isomorphic to the g-module g1 . As a consequence, all the statements enounced below in the symmetric setting hold for Lie algebras replacing both k and p by g, and K by G. A large part of the Lie theory have a symmetric counterpart. We refer to [KR] for the ground results on symmetric Lie algebra.

Let G be the adjoint group of g and K be the closed connected subgroup of

G with Lie algebra k ∩ g ′ . The group K acts on p. For x ∈ p, it follows from [KR, Proposition 5] that dim K.x = 1 2 dim G.x, dim k -dim k x = dim p -dim p x .
(2.1)

For A ⊂ g, we set A • := {a ∈ A| ∀a ′ ∈ A, dim G.a dim G.a ′ }.
Note that we can replace G by K in the previous definition when A ⊂ p thanks to (2.1). For A, B ⊂ g, the centralizer in

B of A is denoted by c B (A) := {b ∈ B| ∀a ∈ A, [a, b] = 0}. If m is a Z/2Z-subspace of g we write k m := k ∩ m, p m := p ∩ m and we have m = k m ⊕ p m .
We say that a Levi subalgebra l ⊂ g arises from p if there exists a semisimple element v ∈ p such that l = g v (it corresponds to the notion of subsymmetric pair in [PY]). In this case, l and l ′ are reductive and semisimple Z/2Z-graded Lie subalgebras of g. In addition, we can decompose g in l-modules in the following way

g = l ⊕ l ⊥
where l ⊥ is the orthogonal complement of l in g ′ with respect to the Killing form. More concretely, if l = g v we can write

l ⊥ = [g, v].
It is well-known that c g (l) is the center of l. In particular, p l = c p (l) ⊕ p l ′ . Moreover, we have [START_REF] Tauvel | Lie algebras and algebraic groups[END_REF]38.8.4]

c p (l) = c g (l) ∩ p = c p (p l ),
(2.2)

c p (l) • = c g (l) • ∩ p = {u ∈ c p (l)| g u = l}. (2.3) We denote by K l (resp. K l ′ ) the closed connected subgroup of K with Lie algebra k l ∩g ′ (resp. k l ′ ). Then, K l = (K v )
• and the K l -orbits of p l are precisely the orbits associated to the reductive symmetric Lie algebra l = k l ⊕ p l . The same holds for K l ′ -orbits (=K l -orbits) of p l ′ . Define

U l := {y ∈ p l | g y ⊂ l}.
(2.4)

The next lemma shows that K-orbits and K l -orbits of elements of U l are closely related.

Lemma 2.1. Let l be a Levi subalgebra arising from p. Then, the following conditions are equivalent for any y ∈ p l .

(i) y ∈ U l , (ii) g s ⊂ l, where s is the semisimple component of y,

(iii) codim p K.y = codim p l K l .y, (iv) [k, y] = p l ⊥ ⊕ [k l , y].
Moreover, U l is an open subset of p l .

Proof. We have On the other hand, we see that (iv) is just (iv') intersected with p. Let v ∈ p such that l = g v . With the help of (2.1), we have

y ∈ l . Hence [g, y] = [l ⊥ , y] ⊕ [l, y] ⊂ l ⊥ ⊕ [l,
dim(p l ⊥ ⊕ [k l , y]) -dim[k, y] = dim[k, v] + dim[k l , y] -dim[k, y] = 1 2 (dim[g, v] + dim[l, y] -dim[g, y]) = 1 2 (dim(l ⊥ ⊕ [l, y]) -dim[g, y])
Since we have the inclusion [k, y] ⊂ p l ⊥ ⊕ [k l , y], we get the equivalence between (iv') and (iv). Through tangeant spaces, we also see that (iii) is equivalent to (iv).

There remains to show that (i) is equivalent to (ii). Denote the nilpotent part of y by n. We have g y = g s ∩ g n so (ii) implies (i). Let us now assume that g s is not included in l. Since s, n ∈ l, the endomorphism ad n stabilizes the non-trivial subspace g s ∩ l ⊥ . Since ad n is nilpotent, there exists a non-zero element in g n ∩ g s ∩ l ⊥ . Hence, g y ⊂ l. By contraposition, (i) implies (ii) . Definition 2.2. Given a Levi subalgebra l of g arising from p, a nilpotent element e ∈ p l embedded in a normal sl 2 -triple S := (e, h, f ) ⊂ l (here normal means e, f ∈ p, h ∈ k and we allow (0, 0, 0) as sl 2 -triple) and a subset J ⊂ p, we define

X l (J, S ) ⊂ p f l via e + X l (J, S ) := (e + p f l ) ∩ U l ∩ J,
where U l is as in (2.4). We say that e + X l (J, S ) is the Slodowy slice of J with respect to (l, S ). This is a generalization of the notion appearing in [Sl, Kat, Bu]. In fact, in the case l = g, we have U l = g and e + X(J, S ) := e + X g (J, S ) = (e + p f ) ∩ J is the natural analogue in the symmetric setting of the ordinary Slodowy slice in Lie algebras, see [Bu].

In what follows, a cone of p means a subset of p stable under multiplication by k * . The next lemma is well-known (see e.g. [START_REF] Katsylo | Sections of sheets in a reductive algebraic Lie algebra[END_REF]§4]).

Lemma 2.3. Let J be a K-stable cone of p and S = (e, h, f ) a normal sl 2triple such that X(J, S ) = ∅. Then e belongs to each irreducible component of e + X(J, S ). In particular, e ∈ J.

Proof. A standard proof of this lemma is based on the construction of a oneparameter subgroup of K × k * Id which contracts e + X(J, S ) to e. Define the characteristic grading g := i∈Z g(i, h) by g(i, h)

:= {x ∈ g | [h, x] = ix}. For t ∈ k * , let F t ∈ GL(g) be such that (F t ) |g(i,h) = t -i+2 Id.
We have F t .e = e and F t .(e + p f ) = e + p f since p f is compatible with the characteristic grading. On the other hand, it is easy to show [START_REF] Tauvel | Lie algebras and algebraic groups[END_REF]38.6.2] that

t -2 F t ∈ K, hence F t ∈ K × k * Id.
As a consequence, F t normalizes the cone J and hence (e + X(J, S )). Since e + p f ⊂ e + i 0 g(i, h), we have lim t→0

F t .(e + x) = e
(2.5) for any x ∈ p f . Since (F t ) t∈k * is a one parameter subgroup of GL(g), each irreducible component of e + X(J, S ) is stable under the F t -action and the lemma follows.

Next, we wish to enlight the strong connection linking J and X(J, S ). This was lacking in [Bu] in the general case and the following Proposition renders some definitions and techniques of this paper obsolete. For example, it can easily be used together with [START_REF] Tauvel | Lie algebras and algebraic groups[END_REF]38.6.9(i)] to show that condition (♣) of [START_REF] Bulois | Sheets of symmetric Lie algebras and Slodowy slices[END_REF]§9] is automatically satisfied.

Proposition 2.4. Let l be a Levi subalgebra of g arising from p and S = (e, h, f ) a normal sl 2 -triple of l ′ . Let J be an irreducible locally closed K-stable

subset of p such that X l (J, S ) = ∅ and Y be a locally closed subset in X l (p, S ). Set c(J) := codim p J, c(Y ) := codim X l (p,S ) Y and r := codim p X l (p, S ). (i) The action of K on p yields a smooth morphism ψ : K ×(e+X l (p, S )) → p of relative dimension dim K -r. (ii) codim p K.(e + Y ) c(Y ).
(iii) X l (J, S ) is a pure locally closed variety of codimension c(J) in X l (p, S ).

(iv) Let X 0 be an irreducible component of X l (J, S ). Then K.(e+X 0 ) is dense in J.

(v) ψ restricts to a smooth dominant morphism

ψ J : K × (e + X l (J, S )) → J.
Proof. First of all, ψ is K-equivariant with respect to the K-action on the domain of ψ given by k ′ .(k, y) = (k ′ k, y). Hence it is sufficient to check that ψ is smooth at points of the form (1 K , y). Moreover, since the domain and codomain of ψ are smooth (recall from Lemma 2.1 that e + X l (p, S ) is open in the affine space e + p f l ), it is sufficient to check that the induced map on the tangeant spaces is surjective

[AK, VII Remark 1.2]. At the point (1 K , y), it is given by (d ψ ) (1,y) : k × p f l → p (k, x) → [k, y] + x . Hence, thanks to Lemma 2.1, we have (d ψ ) (1,y) (k × p f l )) = [k, y] ⊕ p f l = p l ⊥ ⊕ [k l , y] ⊕ p f l . This implies that d ψ is smooth at (1, y) if and only if d ψ ′ is, where ψ ′ : K l × (e + p f l ) → p l
is the morphism yielded by the action of K l on p l . In other words, we can restrict ourselves to the case g = l.

In this case, we follow [START_REF] Slodowy | Simple singularities and simple algebraic groups[END_REF]7.4 Corollary 1]. We easily see from graded sl 2 -

theory that p = [k, e] ⊕ p f so ψ is smooth at (1, e). Consider the (F t ) t∈k * -action on K × (e + p f ), given by F t .(k, x) = (F t kF t -1 , F t (x)).
Then ψ is equivariant with respect to this action. Hence the open set of smooth points of ψ is stable under F t . Therefore, it follows from (2.5) that ψ is smooth on 1 K × (e + p f ) and hence on the whole domain K × (e + p f ). (ii) We have K.(e + Y ) = ψ(K × (e + Y )). Assertion (i) implies that ψ has constant fiber dimension. Hence, the dimension of any fiber of ψ |K×(e+Y ) is less or equal to dim K-r and we have dim [START_REF] Hartshorne | Algebraic geometry[END_REF]I Proposition 7.1] (which also holds for locally closed subsets of an affine space) states that codim p X 0 c(J)+ r for any irreducible component X 0 of X l (J, S ). On the other hand, since J is K-stable, we have K.(e + X 0 ) ⊂ J and we deduce codim X l (p,S ) X 0 c(J) from (ii). Since J is irreducible, this proves (iii) and (iv). (v) It follows from (iv) that ψ J is dominant. In order to obtain smoothness, we apply the argument of base extension by J ֒→ p as in [START_REF] Im | The sheets of classical Lie algebra[END_REF]2.8 and above]. More details can also be found in [START_REF] Bulois | Sheets of symmetric Lie algebras and Slodowy slices[END_REF]Proposition 3.9]. Proposition 2.5. Let l, J, S be as in Proposition 2.4, omitting the assumption

K.(e+Y ) dim K+dim Y -(dim K-r) = dim Y + r = dim p -c(Y ). (iii-iv)
X l (J, S ) = ∅. Then (i) X l (J, S ) is a dense open subset of X l (J , S ), (ii) K.(e + X l (J, S )) is an open subset of J. Proof. (i) If X l (J, S ) = ∅,
there is nothing to prove. From now on, we assume that it is non-empty. Since J is open in J, the subset X l (J, S ) is open in X l (J, S ). Let X 0 be an irreducible component of X l (J, S ). Then K.(e + X 0 ) is a dense constructible subset of J by Propostion 2.4(iv). Hence it meets J and, since J is K-stable, we have J ∩ X 0 = ∅. In other words, the open subset X l (J, S ) ⊂ X l (J, S ) meets each irreducible components of X l (J, S ). (ii) Since smooth morphisms are open [AK, V Theorem 5.1 and VII Theorem 1.8], the result is a consequence of (i) and Proposition 2.4(v).

The equivalent statements (i), (ii) and (iii) of the following Theorem are inspired by similar properties in the Lie algebra case, which can be deduced from parabolic induction theory when J is a decomposition class (see e.g. [START_REF] Borho | Über Schichten halbeinfacher Lie-Algebren[END_REF]§2]).

Theorem 2.6. Let e ∈ p be a nilpotent element embedded in a normal sl 2triple S := (e, h, f ) and let J be a locally closed K-stable cone. The following conditions are equivalent: (iv) X(J, S ) = ∅.

(i) e ∈ J.
(v) X(J, S ) = ∅.

Proof. The implications (ii)⇒(iii)⇒(i)⇒(v) are obvious and (v)⇒(iv) is a consequence of Proposition 2.5(i) applied to an irreducible component of J meeting e + p f . Let us now prove (iv)⇒(ii). Take U = K.(e + X(J, S )). It is open in J by Proposition 2.5(ii) and, for any z ∈ U , we have X(K.(k * z), S ) = ∅. Then, our implication is a consequence of Lemma 2.3 applied to the K-stable cone

K.(k * z).
From the computational point of view, the previous theorem may be of key importance. Indeed, the existence of a degeneration from J to e reduces to the existence of an element in the intersection of J with the affine space e + p f , which might be much easier to check.

On the other hand, we have the following proposition derived from [START_REF] Tauvel | Lie algebras and algebraic groups[END_REF]Theorem 38.6.9 (i)].

Proposition 2.7. If J is a K-stable cone of p (r) = {x ∈ p| dim K.x = r}, then there exists a nilpotent element e ⊂ p such that (i) e ∈ J,

(ii) dim K.e = r.
Proposition 2.8. Let J ⊂ p (r) be a locally closed K-stable cone and (e i ) i∈I a set of representatives of the nilpotent K-orbits satisfying (i) and (ii) of Proposition 2.7 embedded in normal sl 2 -triples

(S i ) i∈I . Let U i := K.(e i + X(J, S i )). Then, (U i ) i∈I is an open cover of J.
Proof. The sets U i are open thanks to Proposition 2.5(ii). Pick z ∈ J, then it follows from Proposition 2.7 that there exists i ∈ I such that e

i ∈ K.(k * z). Applying Theorem 2.6 to K.(k * z), we get X(K.(k * z), S i ) = ∅, so U i ∩K.(k * z) = ∅. Since U i is stable under the action of K × k * Id, we get z ∈ U i .
Remarks 2.9. -A major consequence of this Proposition is that the whole geometry of J is closely related to the geometry of its different Slodowy slices. Indeed, locally, we can assume that J = K.(e i + X(J, S i )) for some i ∈ I and it follows from Proposition 2.4(v) that this variety is smoothly equivalent to

X(J, S i ).
-This also provides a more solid ground to the philosophy of [START_REF] Bulois | Sheets of symmetric Lie algebras and Slodowy slices[END_REF]§9], where it is proven in some particular cases that the Slodowy slices contains enough information to describe the whole variety.

-The main drawback of this approach is that it does not yield |I| = 1 when J is irreducible in the Lie algebra case, contrary to other parameterization such as [START_REF] Borho | Über Bahnen und deren Deformationen bei linear Aktionen reduktiver Gruppen[END_REF]§5]. However, this drawback is somehow necessary since the property |I| = 1 may fail in the symmetric case (see e.g. [START_REF] Tauvel | Lie algebras and algebraic groups[END_REF]39.6.3] for the description of the regular sheet when (g, k) = (sl 2 , so 2 )).

We have several examples in mind of such locally closed K-stable cone included in some p (r) . We have already seen that K.(k * z) plays a role in the previous proofs. We can also consider a K-decomposition class J 1 , or its regular closure J 1

• . Sheets are particular examples of the last type.

K-decomposition classes and induction

Recall from the beginning of Section 2 that a Levi subalgebra l is said to arise from p if it is the centralizer of a semisimple element s ∈ p. Recall also that, in this case, the orbits in p l associated to the symmetric Lie algebra structure

l = k l ⊕ p l coincide with the K l = (K s ) • -orbits. Definition 3.1. A datum of (g, k) is a pair (l, O)
where l is a Levi subalgebra of g arising from p and O is a nilpotent K l -orbit in p l .

The K-decomposition class defined by a datum (l, O) is

J(l, O) := J (g,k) (l, O) := K.(c p (l) • + O).
Remarks 3.2. -These definitions make sense with (g, k) replaced by any other reductive other reductive symmetric pair. For instance, if l 2 ⊂ g is a Levi subalgebra arising from p and (l 1 , O 1 ) is a datum of (l 2 , k l2 ), we have

J (l2,k l 2 ) (l 1 , O 1 ) = K l2 .(c p l 2 (l 1 ) reg + O 1 ) = K l2 .(c p (l 1 ) reg + O 1 )
where

A reg := {a ∈ A|∀a ′ ∈ A, dim K l2 .a dim K l2
.a ′ } is a regularity condition taken with respect to the action of K l2 .

-The classes we have defined are the symmetric analogue of decomposition classes studied in [START_REF] Borho | Über Bahnen und deren Deformationen bei linear Aktionen reduktiver Gruppen[END_REF][START_REF] Borho | Über Schichten halbeinfacher Lie-Algebren[END_REF][START_REF] Broer | Decomposition varieties in semisimple Lie algebras[END_REF][START_REF] Broer | Lectures on decomposition classes[END_REF] -The K-orbits of Levi-factors arising from p are in one to one correspondance with their G-orbits which are, in turn, easily characterized through the Satake diagram of (g, k), cf. [START_REF] Bulois | Sheets of symmetric Lie algebras and Slodowy slices[END_REF]§7]. Hence, in order to have a convenient classification of K-decomposition classes, it would be enough to understand in which cases (l, O 1 ) is N K (l)/K l -conjugate to (l, O 2 ). This plays an important role in the classification of sheets when O i , i = 1, 2 are rigid orbits as shown in [START_REF] Borho | Über Schichten halbeinfacher Lie-Algebren[END_REF]3.9,3.10,4.5,4.6]. However, for our purposes, we will not need such a classification.

The K-decomposition classes are equivalence classes of elements sharing a similar Jordan decomposition in the following sense:

J(l, O) = K.{x = s + n ∈ p | g s = l, K l .n = O} (3.1)
and we refer to [START_REF] Tauvel | Lie algebras and algebraic groups[END_REF]§39.5] for most of the known properties of these classes (called K-Jordan classes in loc. cit.) in the symmetric Lie algebra case. In particular, we note that K-decomposition classes form a finite partition of p. These classes are also irreducible, locally closed and of constant orbit dimension. As a consequence, in each sheet S there exists a dense open K-decomposition class J 0 and we have

S = J 0 • .
In the Lie algebra case, such regular closures of G-decomposition classes have been studied in [BK], where an important parameterization is given in Theorem 5.4 (see [START_REF] Katsylo | Sections of sheets in a reductive algebraic Lie algebra[END_REF]Lemma 3.2] for a refinement). In [Bo], this understanding has been deepened thanks to the parabolic induction theory of nilpotent orbits. Let us recall the definition. Take two Levi subalgebras l 1 ⊆ l 2 ⊆ g, with corresponding subgroups L i ⊆ G, i ∈ {1, 2}. One can choose a parabolic subalgebra q of l 2 with Levi-factor l 1 . Denote by n q the nilpotent radical of q. Given a nilpotent

L 1 -orbit O 1 ⊂ l 1 , the parabolically induced orbit from l 1 to l 2 is the dense nilpotent L 2 -orbit O 2 of L 2 .(O 1 + n q ) ⊂ l 2 .
For the purpose of our exposition, we will say in such case that the pair (l

1 , O 1 ) (resp. the G-decomposition class J g (l 1 , O 1 )) parabolically induces (l 2 , O 2 ) (resp. J g (l 2 , O 2 )).
The aim of this section is to extend a significant number of the known properties of G-decomposition classes of [BK, Bo] to K-decomposition classes. However, as mentioned in the introduction, the parabolic subalgebras behave badly in general for a symmetric Lie algebra. This is why we introduce a new notion of induction, using the tools developed in Section 2. This notion turns out to coincide with the parabolic induction in the Lie algebra case, see Corollary 3.7.

Definition 3.3. 1. Given two data (l i , O i ) (i = 1, 2) of (g, k), we say that (l 1 , O 1 ) weakly slice induces (l 2 , O 2 ) if l 1 ⊆ l 2 and J (l2,k l 2 ) (l 1 , O 1 ) ∩ (n 2 + p m2 l2 ) = ∅ (3.2)
where n 2 is an element of O 2 embedded in a normal sl 2 -triple S 2 = (n 2 , h 2 , m 2 ) of l 2 .

2. We say that (l 1 , O 1 ) slice induces (l 2 , O 2 ) if, moreover, dim

K l2 .x = dim O 2 for some x ∈ J (l2,k l 2 ) (l 1 , O 1 ).
3. Given two K-decomposition classes J i (i = 1, 2), we say that J 1 (weakly) slice induces J 2 if there exist data (l i , O i ) with

J i = J(l i , O i ), (i = 1, 2) such that (l 1 , O 1 ) (weakly) slice induces (l 2 , O 2 ).
When, there is no context of parabolic induction, the term induction will always refer to slice induction.

When J 1 and J 2 are K-decomposition classes, we write

J 1 ↑ J 2 if J 1 weakly slice induces J 2 , J 1 ↑↑ J 2 if J 1 slice induces J 2 .
Remarks 3.4. -The definitions do not depend on the choices of n 2 or S 2 since all of these are K l2 -conjugate. Also, all the elements of J (l2,k l 2 ) (l 1 , O 1 ) share the same K l2 -orbit dimension. Finally, it is worth noting that the notions of induction and weak induction of data do only depend on the involved data and not on the ambient Lie algebra g.

-If l 2 = g, condition 3.2 can be written in the nicer form:

X(J(l 1 , O 1 ), S 2 ) = ∅. (3.3) -Assume that l 1 ⊆ l 2 . The data (l 1 , O 1 ) (weakly) induces (l 2 , O 2 ) if and only if (l 1 ∩ l ′ 2 , O 1 ) (weakly) induces (l ′ 2 , O 2 ). Indeed, n 2 + p m2 l2 = c p (l 2 ) + (n 2 + p m2 l ′ 2 ) and J (l2,k l 2 ) (l 1 , O 1 ) = c p (l 2 )+J (l ′ 2 ,k l ′ 2 ) (l 1 ∩l ′ 2 , O 1 ).
In particular, when studying induction, one can always assume that the ambient Lie algebra g is semisimple.

Assume that g is semisimple. In view of Theorem 2.6 and (3.3), a Kdecomposition class J 1 weakly induces a nilpotent orbit O (i.e. the K-decomposition class J(g, O)) if and only if O ⊂ J 1 .

The purpose of the following theorem is to extend this property to induction of arbitrary K-decomposition classes. Recall that X l (J, S ) is introduced in Definition 2.2. Theorem 3.5. Let J 1 , J 2 be K-decomposition classes. The following conditions are equivalent.

(i) J 1 ↑ J 2 , (ii) X l2 (J 1 , S 2 ) = ∅ where (l 2 , O 2 ) is some (any) datum defining J 2 and S 2 is a normal sl 2 -triple in l 2 whose nilpositive element belongs to O 2 . (iii) J 2 ∩ J 1 = ∅, (iv) J 2 ⊂ J 1 ,
Proof. (iv)⇒ (iii) is obvious.

(iii)⇒ (ii): Choose n 2 ∈ O 2 and embed it in a normal sl 2 -triple S 2 of l 2 . Since J 2 ∩ J 1 is K-stable we can choose an element y 2 in this intersection such that the Jordan decomposition of y 2 is s 2 + n 2 with s 2 ∈ c p (l 2 ) • and

n 2 ∈ O 2 . Therefore g s2 = l 2 (2.3) so y 2 ∈ U l2 and X l2 (J 1 , S 2 ) = ∅. Then Proposition 2.5(i) yields X l2 (J 1 , S 2 ) = ∅.
(ii)⇒(i): Choose an element y 1 ∈ X l2 (J 1 , S 2 ) and consider its Jordan decomposition s 1 +n 1 . Since y 1 ∈ U l2 , the centralizer l 1 := g s1 is a Levi subalgebra of l 2 (Lemma 2.1). Hence it makes sense to speak of the K l2 -decomposition class

J (l2,k l 2 ) (l 1 , O 1 ) with O 1 := (K s1 ) • .n 1 . Since l 1 = l s1
2 , we derive from (3.1) that y 1 belongs to this class. Since y 1 ∈ n 2 + p m2 l2 , the datum (l 1 , O 1 ) weakly induces (l 2 , O 2 ).

(i)⇒(iv): Choose a datum (l 1 , K l1 .n 1 ) defining J 1 , which weakly induces a datum (l 2 , K l2 .n 2 ) defining J 2 . Since l 1 ⊂ l 2 , we have c p (l 1 ) ⊃ c p (l 2 ) and

J 1 = K.(c p (l 1 ) • + n 1 ) ⊃ K l2 .(c p (l 2 ) + c p l ′ 2 (l 1 ) + n 1 ) = c p (l 2 ) + J ′ 1 where J ′ 1 is the K l ′ 2 -decomposition class J (l ′ 2 ,k l ′ 2
) (l 1 , K l1 .n 1 ). On the other hand, we have seen in Remark 3.4 that our hypothesis implies that J ′ 1 weakly induces 12

K l2 .n 2 in l ′ 2 .
Then it follows from Theorem 2.6, applied to the symmetric pair (l ′ 2 , k l ′ 2 ), that n 2 ∈ J ′ 1 . Hence J 1 ⊃ c p (l 2 ) + n 2 and we get J 2 ⊂ J 1 by K-stability of J 1 .

A key point in the proof of (iii)⇒(iv) is that whenever we have x ∈ J 2 ∩ J 1 with Jordan decomposition x = s+n, we can manage to realize the degeneration through a one parameter family (x t ) t∈k * ∈ J 1 , lim t→0 x t = x with the x t lying in a Slodowy slice centered on x and included in g s . Hence the whole degeneration takes place in the Levi g s and thus yields a degeneration toward any element with Jordan decomposition similar to x. Lemma 3.6. Let J 1 , J 2 be K-decomposition classes such that J 1 ↑ J 2 . Then J 1 ↑↑ J 2 if and only if the dimension of K-orbits in J 1 and J 2 coincide.

Proof. Choose a datum (l 2 , O 2 ) defining J 2 . We can argue as in Theorem 3.5 (ii)⇒(i) to find a data (l 1 , O 1 ) defining J 1 and an element

y 1 ∈ J 1 ∩ U l2 ∩ J (l2,k l 2 ) (l 1 , O 1 ). On the other hand, any element y 2 ∈ c p (l 2 ) • + n 2 , n 2 ∈ O 2 satisfies y 2 ∈ J 2 ∩ U l2 .
Then, it follows from Lemma 2.1(iii) that y 1 and y 2 share the same K-orbit codimension in p if and only if they share the same K l2 -orbit codimension in p l2 . Since dim K l2 .y 2 = dim O 2 , the result follows.

As a consequence of Theorem 3.5 and Lemma 3.6, we are now able to prove the following.

Corollary 3.7. (i) If J 0 is a K-decomposition class, then

J 0 = J↑J0 J, J 0 • = J↑↑J0 J.
(ii) If J 1 and J 2 are K-decomposition classes, J 1 ∩J 2 is a union of K-decomposition classes.

(iii) Sheets are union of K-decomposition classes.

(iv) Induction (resp. weak induction) of data and of K-decomposition classes are transitive. That is, for classes,

(J 1 ↑↑ J 2 ) ∧ (J 2 ↑↑ J 3 ) ⇒ J 1 ↑↑ J 3 , resp. (J 1 ↑ J 2 ) ∧ (J 2 ↑ J 3 ) ⇒ J 1 ↑ J 3 .
(v) In the Lie algebra case, the parabolic induction coincides with the slice induction.

Proof. Since K-decomposition classes form a partition of p, the first part of (i) is an immediate consequence of the equivalence (i)⇔ (iii)⇔ (iv) in Theorem 3.5. The second part of (i) follows from the first one and Lemma 3.6. Then we deduce from (i) the statement (iv) concerning K-decomposition classes.

Let us now show (iv) on data. Choose three data (l i , O i ), i = 1, 2, 3 such that (l i , O i ) (weakly) induces (l i+1 , O i+1 ), i = 1, 2. Without loss of generality, we can assume that g = l 3 (see Remark 3.4). Then J(l i , O i ) (weakly) induces

J(l i+1 , O i+1 ) for i = 1, 2, so J(l 1 , O 1 ) (weakly) induces J(l 3 , O 3 ). Hence there exist data ( l i , O i ), K-conjugate to (l i , O i ) (i ∈ {1, 3}), and such that ( l 1 , O 1 ) (weakly) induces ( l 3 , O 3 ). Since l 3 = g, we have ( l 3 , O 3 ) = (l 3 , O 3 ) so, up to K-conjugacy, we can assume that ( l 1 , O 1 ) = (l 1 , O 1 ).
In order to show (ii), we only need to note that J 1 ∩ J 2 is the union of Kdecomposition classes induced both by J 1 and J 2 . Statement (iii) follows from the fact that any sheet is the regular closure of a K-decomposition class.

In [START_REF] Borho | Über Schichten halbeinfacher Lie-Algebren[END_REF]] it is shown that, whenever J 0 is a G-decomposition class, J 0

•

is the set of G-decomposition classes parabolically induced by J 0 . Then (v) for G-decomposition classes follows from (i) and the discussion in Remark 3.2. We now prove (v) for data, using arguments similar to the proof of (iv) for data. Without loss of generality, we can restrict to the cases where a datum (l 1 , O 1 ) slice (resp. parabolically) induces a datum of the form (g, O 2 ). Since (g, O 2 ) is the only datum defining J(g, O 2 ), such a slice (resp. parabolic) induction is equivalent to the corresponding induction from J(l 1 , O 1 ) to J(g, O 2 ). The result on data then follows from the result on decomposition classes.

An important consequence of Corollary 3.7 (v) is that the slice induction can be seen as a generalization of the parabolic induction, fitting to the symmetric Lie algebra setting needs. Note in particular that (i), (ii), (iv) and (iii) are respective analogues of [START_REF] Borho | Über Schichten halbeinfacher Lie-Algebren[END_REF]3.5,3.8,2.3] and [START_REF] Borho | Über Bahnen und deren Deformationen bei linear Aktionen reduktiver Gruppen[END_REF]5.8.d].

The fact that a closure of a decomposition class is a union of K-decomposition classes has also been shown in [Le] when the ground field is precisely C. Example 3.8. Using the results of Section 2 and of this section, we can reconsider the example given in [START_REF] Bulois | Sheets of symmetric Lie algebras and Slodowy slices[END_REF]§14(5)] (where there is a mistake in the definition of l). Here (g, k) = (sp 6 , gl 3 ), the sheet S G of g is defined by S G = J g (l, 0)

• ⊂ g (16) with l arising from p of type A 1 (long root). We know that 16) embedded in a normal sl 2 -triple S 0 satisfies e 0 ∈ J 0

J g (l, 0) ∩ p is the single K-decomposition class J 0 := J (g,k) (l, 0) [Bu, Theo- rem 7.8]. In particular, S G ∩ p has only one irreducible component of maximal dimension 8 + dim c p (l) = 10, namely J 0 • [Bu, Lemma 8.2]. Any nilpotent el- ement e 0 ∈ p (8) ⊂ g (
• if and only if dim X(J 0 • , S 0 ) = dim J 0 -8 = 2 (see Theorem 2.6 and Proposition 2.4). We choose the two nilpotent elements e, e ′ ∈ p (8) as in [START_REF] Bulois | Sheets of symmetric Lie algebras and Slodowy slices[END_REF]§14(5)] and embed them in sl 2 -triples S , S ′ . It turns out that the Slodowy slices X(S G ∩ p, S ) and X(S G ∩ p, S ′ ) are irreducible varieties of respective dimension 1 and 2. In particular J 0 ↑↑ K.e while J 0 ↑↑ K.e ′ . An other consequence is that S G ∩ p has at least two irreducible components, J 0 • of dimension 10 and K.(e + X(S G ∩ p, S ))

• of dimension 1 + 8 = 9, see Proposition 2.8. This is a counterexample to the equidimensionality of S ∩ p for S a sheet of g, this property being observed when g = gl n [START_REF] Bulois | Sheets of symmetric Lie algebras and Slodowy slices[END_REF]Theorem 13.2] 4 Sheets of g in type G 2

In this section, we assume that g is a simple Lie algebra of type G 2 . We are interested in studying non-trivial (i.e. non-regular and not restricted to one nilpotent orbit) sheets in this case. We adopt conventions and notations of [FH]. In particular, we fix a Cartan subalgebra h of g. In the corresponding root system, we fix a basis {α 1 , α 2 }, with α 1 a short root, and label the associated positive roots as pictured

α1 α2 α3 α4 α5 α6
We choose, as a Chevalley basis, the one given in [START_REF] Fulton | Representation theory[END_REF]p.346] and denote it by

h 1 , h 2 , x i (i ∈ [[1, 6]]), y i (i ∈ [[1, 6]]), with x i ∈ g αi , y i ∈ g -αi and (x i , h i , y i ) an sl 2 -triple for i = 1, 2.
The nilpotent cone of g consists of five nilpotent conjugacy classes. We denote the orbit of dimension 2i (i ∈ {0, 3, 4, 5, 6}) by Ω 2i . Moreover, we choose some particular representatives n i (two of them when i = 5) of these orbits as given in column 2 of Table 1.

G-orbit Ω Representative K-orbit O Ω 0 0 O 0 Ω 6 n 3 := x 5 O 3 Ω 8 n 4 := x 4 O 4 Ω 10 n 5a := x 5 + y 3 O 5a n 5b := x 2 + x 5 O 5b Ω 12 n 6 := x 3 + y 2 O 6
Table 1: Representatives for Ω i and O i Since g is of rank two, the only non-regular non-nilpotent elements of g are semisimple subregular elements. This gives rise to two subregular sheets of g which can be described as union of G-decomposition classes as follows.

S g 1 := G.(k * h 1 ) ⊔ Ω 10 , S g 2 := G.(k * h 2 ) ⊔ Ω 10
. This follows from the fact that G.(k * h 1 ) and G.(k * h 2 ) are of the same dimension (here, 11) and that both must contain a nilpotent orbit in their regular closure (Proposition 2.7). A practical criterion to distinguish generic elements of S g 1 from those of S g 2 is that elements of the former lie in a Levi of type A 1 (short root) while their centraliser is a Levi of type A 1 (long root).

It is known [Sl, Pe, BK, Hi] that S g 1 is smooth at points of G.(k * h 1 ) and is singular at points of Ω 10 , undergoing a threefold covering in a resolution of singularities, see e.g. Proposition 4.4. On the other hand, S g 2 is a smooth variety.

Letting

k := h ⊕ i∈{1,6} g ±αi , p := i∈{2,3,4,5} g ±αi ,
we construct a symmetric Lie algebra of type G 2(2) . It corresponds to the single non-compact form for an algebra of type G 2 and we have k ∼ = sl 2 ⊕ sl 2 . Let us describe the K-orbits of interest in this setting. First, the symmetric Lie algebra is of maximal rank, hence any G-orbit intersects p [An]. Since semisimple orbits intersect p into single orbits (see e.g. [START_REF] Bulois | Sheets of symmetric Lie algebras and Slodowy slices[END_REF]Proposition 6.6]), there are exactly two subregular semisimple K-decomposition classes: J i := K.(k * h i ), with hi an element of G.h i ∩ p, i = 1, 2. It turns out [START_REF] Djokovic | Classification of nilpotent elements in simple exceptional real Lie algebras of inner type and description of their centralizers[END_REF] that Ω 2i ∩ p is a single K-orbit O i for i ∈ {0, 3, 4, 6} and is the union of two K-orbits O 5a and O 5b in the subregular case i = 5 (respectively numbered by 3 and 4 in [START_REF] Djokovic | Classification of nilpotent elements in simple exceptional real Lie algebras of inner type and description of their centralizers[END_REF]). We refer to Table 1 for representatives of these different K-orbits.

Note that, since sheets of p are union of K-decomposition classes, there are two 6-dimensional sheets of subregular elements. These are S 1 := J 1

• and S 2 := J 2 • . Even if each of these sheets must contain at least a nilpotent orbit among O 5a and O 5b (Proposition 2.7), it is a non-trivial problem to decide which orbits belong to a given sheet. At this point, we may even not rule out the existence of a possible 5-dimensional subregular sheet consisting of a single orbit O 5a or O 5b .

Applications of the Slodowy slice theory

We now apply partly the general theory of Sections 2 and 3 to our special case.

The main result of this subsection is the following (ii) The decomposition of each sheet S i (i = 1, 2) as union of K-decomposition classes is

S i = J i ⊔ O 5a ⊔ O 5b (= S g i ∩ p).
(iii) The sheet S 1 is smooth on J 1 and O 5a . At points of O 5b , the singularities of S 1 are smoothly equivalent to the intersection of three lines.

(iv) The sheet S 2 is smooth.

Recall that the only decomposition classes of subregular elements are J 1 , J 2 , O 5a and O 5b . So, since sheets are regular closures of decomposition classes, (ii) implies (i).

The statements (ii), (iii) and (iv) rely on computations on the Slodowy slices. In fact, embedding n 5a and n 5b into respective normal sl 2 -triple, S 5a and S 5b , we claim that Lemma 4.2. (i) X(p (5) , S 5a ) is the union of two lines kt i (i = 1, 2), with n 5a + t 1 ∈ J 1 and n 5a + t 2 ∈ J 2 .

(ii) X(p (5) , S 5b ) is the union of four lines kt i (i = 3, 4, 5, 6), with n 5b + t i ∈ J 1 for i ∈ {3, 4, 5} and n 5b + t 6 ∈ J 2 .

In particular, X(J i , S 5x ) = ∅ so J i slice induces O 5x for i ∈ {1, 2} and

x ∈ {a, b}. Hence Proposition 4.1 (ii) follows from Corollary 3.7 (or, in a more simple way, from Lemma 2.3). The other consequence of Lemma 4.2 is that J i ⊔ O 5a (i = 1, 2) (resp.

J 2 ⊔ O 5b
) is smoothly equivalent to the (smooth) affine line X(S i , S 5a ) (resp. X(S 2 , S 5b )), see Remark 2.9. On the other hand J 1 ⊔ O 5b is smoothly equivalement to a union of three lines meeting at a point. This explains (iii) and (iv) of Proposition 4.1.

To sum up, the picture is the following. Only one branch in the neighborhood of the singularities of S g 1 at points of O 5a is preserved under the intersection with p. On the contrary, the singularities at points of O 5b are "intact" when intersected with p.

The idea of the proof of Lemma 4.2 is the following. Due to Lemma 2.5, an element in the Slodowy slice is subregular if and only if it is not regular. In particular, we get explicit equations of the subregular locus in the Slodowy slice via minors of some matrices. Then, these equations are simple enough to solve. Most of the computations have been made by hand and then checked by [GAP] using W. de Graaf's package [SLA] 2 . We give the explicit outcome of the computation in terms of our Chevalley basis. Set m 5a := x 3 + y 5 and m 5b := -4 3 y 2 + 2 3 y 3 + 2 3 y 4 + 4 3 y 5 . Then S 5a := (n 5a , -2h 2 , m 5a ) and S 5b := (n 5b , 2h 1 + 4h 2 , m 5b ) are normal sl 2 -triples and the elements t i of the lemma can be chosen as follows.

Remarks 4.3. -Note that, thanks to (2.5), our method also provides explicit one-parameter degenerations lim γ→0 n 5x + γt i = n 5x . (x ∈ {a, b}) t 1 x 3 + 9y 5 t 2 x 3 + y 5 t 3 y 3 + y 4 t 4 6y 2 -3y 3 + y 4 t 5 y 3 -3y 4 -6y 5 t 6 2y 2y 3y 4 -2y 5 -In the real case, we have no reason to think that decomposition classes closure inclusions always leaves footprints on the Slodowy slice level (see proof of the crucial statement Proposition 2.4(iii)). However, it is an interesting feature to note that our method may still provide real degeneration in some cases. Indeed, here, all the t i belong to the obvious real form of g.

-The computations presented in this section can be improved in order to get similar results in higher rank. For example, in a work in progress, the first author has found two singular sheets in the (ordinary) Lie algebra of type F 4 , the others being smooth. The singular sheets are those appearing in line 9 and 10 in the last table of [START_REF] Broer | Decomposition varieties in semisimple Lie algebras[END_REF].

4-ality and projections

We now provide an explicit desingularization of S 1 through the well-known projection so 7 ։ g. We first note that it would be hard to follow Broer's approach [START_REF] Broer | Decomposition varieties in semisimple Lie algebras[END_REF][START_REF] Broer | Lectures on decomposition classes[END_REF] in the Lie algebra case for normalization and desingularization since it uses fiber bundles of the form G × P Y with P a parabolic subgroup of G.

In order to achieve our goal, we use an other description of our algebra g of type G 2 using 4-ality as defined in [START_REF] Landsberg | Representation theory and projective geometry[END_REF]§3.4]. Namely, we choose four copies C 1 , C 2 , C 3 , D of a 2-dimensional space equipped with a non-degenerate bilinear skew-symmetric form ω. Then

g 0 := sl(C 1 ) × sl(C 2 ) × sl(C 3 ) × sl(D) ⊕ (C 1 ⊗ C 2 ⊗ C 3 ⊗ D)
can be equipped with a Lie bracket in such a way that g 0 ∼ = so 8 , see (4.2) for an identification. In this model, k 0 := sl(C 1 ) × sl(C 2 ) × sl(C 3 ) × sl(D) is a Lie subalgebra of g 0 and acts on p 0 := C 1 ⊗ C 2 ⊗ C 3 ⊗ D in the usual way. We refer to [LM] for the definition of the bracket of two elements of p 0 using ω which, for instance, identifies C 1 with its dual and hence sl 2 (C 1 ) with S 2 C 1 .

This presentation of so 8 relies on the S4-symmetry of so 8 as can be seen on the extended Dynkin diagram of type D 4 . We are interested in the S2 (resp. S3)-action on g 0 induced by permutations on the 2 spaces C 1 and C 2 (resp. on the 3 spaces C i ). Its fixed point space g 1 ⊂ g 0 (resp. g 2 ⊂ g 1 ) is isomorphic to so 7 (resp. g) and can be described as

g i = k i ⊕ p i with k 1 := sl(C ′ ) × sl(C 3 ) × sl(D) p 1 := S 2 C ′ ⊗ C 3 ⊗ D k 2 := sl(C) × sl(D) p 2 := S 3 C ⊗ D ,
where C and C ′ are again copies of our two-dimensional space. Choosing a Cartan subalgebra of g 2 in sl(C) × sl(D) and weight vectors c -, c + (resp. d -, d + ) in C (resp. D), we rediscover the combinatorics of the root spaces in g 2 as pictured below.

sl(C)

c 3 -⊗ d + c 2 -c + ⊗ d + c -c 2 + ⊗ d + c 3 + ⊗ d + sl(D) c 3 + ⊗ d - c -c 2 + ⊗ d - c 2 -c + ⊗ d - c 3 -⊗ d -
Moreover, we have a natural projection π : g 1 ։ g 2 , given for instance on

p 1 via π(xy ⊗ z ⊗ t) = xyz ⊗ t. Its kernel is a k 2 = sl(C) × sl(D)-module so π is SL(C) × SL(D)-equivariant.
We also introduce faithful representations that allow us to manipulate more easily these algebras. Let V

8 := C 1 ⊗ C 2 ⊕ C 3 ⊗ D with action of p 0 given by (c 1 ⊗c 2 ⊗c 3 ⊗d).(c ′ 1 ⊗c ′ 2 +c ′ 3 ⊗d) = ω(c 1 , c ′ 1 )ω(c 2 , c ′ 2 )c 3 ⊗d+ω(c 3 , c ′ 3 )ω(d, d ′ )c 1 ⊗c 2
and standard action of k 0 . It is one of the three inequivalent fundamental representations of g 0 ∼ = so 8 of dimension 8 and g 0 ⊆ gl(V 8 ) is the subalgebra preserving the symmetric form

ω(c 1 ⊗ c 2 + c 3 ⊗ d, c ′ 1 ⊗ c ′ 2 + c ′ 3 ⊗ d ′ ) = ω(c 1 , c ′ 1 )ω(c 2 , c ′ 2 ) -ω(c 3 , c ′ 3 )ω(d, d ′ ). As an sl(C) × sl(D)-module, V 8 decomposes as V 1 ⊥ ⊕ V a ⊥ ⊕ V b where V 1 = Λ 2 C ′ , V a = S 2 C ′ and V b = C 3 ⊗ D. Setting V 7 := V a ⊕ V b ,
one gets that g 1 is the subalgebra of so 8 stabilizing both subspaces V 1 and V 7 while k 1 is the subalgebra of g 1 stabilizing both subspaces V a and V b . In particular, we recover that g 1 ∼ = so 7 ⊕so 1 ∼ = so 7 and that (g 1 , k 1 ) is a symmetric pair isomorphic to (so 7 , so 4 ⊕so 3 ) [PT].

We denote by Ω ′ 10 the SO 7 -orbit of dimension 10 in g 1 . Its Young diagram is . Moreover, we let T be the set elements of g 1 of rank at most 2 with respect to the representation on V 7 . The closed set T is nothing but the union SO 7 .(k * t) ⊔ Ω ′ 10 where t is any semisimple element whose centraliser is a Levi of type B 2 . In particular T • is a sheet in g 1 .

One can then extract the following information from [LSm, Kr, Hi]. (ii) The cardinality of fibers is given by the following table:

y ∈ G 2 .(k * h 1 ) Ω 10 Ω 8 Ω 6 0 # π -1 (y) ∩ T = 1 3 2 1 1
We refer to [START_REF] Ohta | Induction of nilpotent orbits for real reductive groups and associated varieties of standard representations[END_REF] for the classification of nilpotent orbits in p 1 . In g 1 , the . We also define T p1 := T ∩ p 1 . We can then state the following result Proposition 4.5. (i) π induces finite surjective maps O ′ 5x → O 5x (x ∈ {a, b}), T p1 → S 1 and a desingularization T p1 \ {0} → S 1 \ {0} (ii) The cardinality of fibers is given by:

y ∈ J 1 O 5a O 5b O 4 O 3 0 #π -1 (y) ∩ T p1 = 1 1 3 2 1 1
Proof. (ii) An element of p 1 acts on V 8 in the following way:

   0 0 0 0 0 p 0 p ∨ 0    V 1 V a V b
where p ∈ Hom(V b , V a ) and p ∨ is the dual of p with respect to ω |Va⊕V b . We are interested into rank 2 elements of this form and these are exactly elements for which p is of rank 1. We make use of the After computation, one gets Table 2 where the column I presents the Kdecomposition class of S 1 under consideration. Up to easy SL(C) × SL(D)conjugation, one can turn our representatives of Table 1 to the element y ∈ p 2 in column II. Finally, column III present all elements in the fiber π -1 (y) ∩ T p1 .

(i) The desingularization property follows from #π -1 (y) = 1 for y ∈ J 1 and the fact that T p1 \{0} is a smooth variety. Let us check this last point. Under the natural isomorphism g 1 ∼ = Λ 2 V 7 , we have

p 1 = V a ∧ V b and T p1 = {v a ∧ v b |v a ∈ V a , v b ∈ V b }.
The smoothness is then a consequence of the transitivity of the action of GL(V a ) × GL(V b ) on T p1 \ {0}.

In view of Proposition 4.4, there only remains to see that π(O ′ 5x ) = O 5x for x ∈ {a, b}. For instance, since c + , c -, d + , d -are isotropic vectors with respect to ω, we can check that the pre-image z := c 2 + ⊗ (c and z ∈ O ′ 5a .

+ ⊗ d + + c -⊗ d -) of n 5a I II III J 1 = K.(k * (x 4 + y 4 )) c 2 + c -⊗ d + + c + c 2 -⊗ d -c + c -⊗ (c + ⊗ d + + c -⊗ d -) O 5a c 3 + ⊗ d + + c 2 + c -⊗ d - c 2 + ⊗ (c + ⊗ d + + c -⊗ d -) O 5b c 2 + c -⊗ d + + c + c 2 -⊗ d + c + c -⊗ (c + + c -) ⊗ d + c + (c + + c -) ⊗ c -⊗ d + (c + + c -)c -⊗ c + ⊗ d + O 4 c 2 + c -⊗ d + c 2 + ⊗ c -⊗ d + c + c -⊗ c + ⊗ d + O 3 c 3 + ⊗ d + c 2 + ⊗ c + ⊗ d + 0 0 0 Table 2:

  (ii) There exists a non-empty open set U ⊂ J such that e ∈ K.(k * z) for any z ∈ U .(iii) There exists z ∈ J such that e ∈ K.(k * z).

  in the Lie algebra case. We call these last classes G-decomposition classes and they are of the form J g (l, O) := G.(c g (l) • + O) with l ⊆ g any Levi subalgebra and O a nilpotent L-orbit in l. In fact, using notation of Section 2, the G-decomposition classes are exactly the images of the K-decomposition classes under the natural isomorphism p ∼ = g. These are of the form J (ĝ, k) ( l, Ô) with l = {(x, y)|x ∈ l, y ∈ l} and Ô = {(x, -x)|x ∈ O}. The connection between a K-decomposition class J and the G-decomposition class containing J is studied in[START_REF] Bulois | Sheets of symmetric Lie algebras and Slodowy slices[END_REF] §8].

Proposition 4. 1 .

 1 (i) The only sheets of subregular elements in p are S 1 and S 2 .

Proposition 4. 4 .

 4 (i) π induces finite surjective maps Ω ′ 10 → Ω 10 , T → S g 1 and a desingularization T \ {0} → S g 1 \ {0}.

SO 7

 7 -orbit Ω ′ 10 splits into two SO 3 × SO 4 -orbits O ′ 5a and O ′

  4-ality setting to describe such elements. An element of p 1 = (S 2 C ′ ) ⊗ (C 3 ⊗ D) induces a rank one element of Hom(S 2 C ′ , C 3 ⊗ D) (and, equivalently, of Hom(C 3 ⊗ D, S 2 C ′ )) if and only if it is a pure tensor of the form (αc 2 ++ βc + c -+ γc 2 -) ⊗ (c + ⊗ d 1 + c -⊗ d 2 ) with α, β, γ ∈ k and d 1 , d 2 ∈ D.

  fibers of the form π -1 (y) ∩ T p1 sends c 2 -∈ V a on a non-zero multiple of c + ⊗ d + + c -⊗ d -∈ V band this last one is sent on a non-zero multiple of c 2 + ∈ V a . Hence the ab-diagram of z is

  y], with equality if and only if g y ∩l ⊥ = {0} if and only if g y ⊂ l. As a consequence, (i) is equivalent to (iv'): [g, y] = l ⊥ ⊕ [l, y]. By the way, we also note that g y ∩ l ⊥ = {0} is an open condition on y.

Namely ĝ = g × g, k = {(x, x)|x ∈ g} and p = {(x, -x)|x ∈ g}.

These GAP computations are available at https://hal.archives-ouvertes.fr/ hal-01017691v2/file/gap_g2_v6.txt.

Acknowledgments. We are grateful to the referees for the fast and careful reading of the paper. In particular, Section 3 has benefited from their remarks.