Marc Aiguier
email: aiguier@lami.univ-evry.fr

Karim Berkani
email: kberkani@hds.utc.fr

Pascale Le Gall
email: legall@lami.univ-evry.fr

Feature specification and static analysis for interaction resolution

Keywords: pre-post formalism, specification consistency, static analysis, feature integration, feature interaction resolution

Introduction

The work presented in this paper was performed within the French project ValiServ 3in collaboration with the French telecommunication company FranceTelecom and the LSR team of the university J. Fourier of Grenoble [START_REF] Bousquet | Feature Interaction Detection using Synchronous Approach and Testing[END_REF]. This project was devoted to service (feature) design for telecommunication purposes. The aim of this project was to better answer both feature system specification and the underlying problems: feature integration and feature interactions. Indeed, software telecommunication systems are composed of a kernel providing the basic expected functionalities and a set of satellite entities, called features 4 . Each of them aims to modify the set of functionalities characterising the rest of the system (possibly including other already existing features). This project also aimed to develop an assistant tool for integrating new phone services. The interest was to provide support for rapid service-oriented development which is an important issue, especially for telecommunication operators. Indeed, the primary motivation to offer numerous features to users is that the set of offered features differentiates providers, and then becomes a significant source of income. However, if some ✝ this work was partially supported by the RNRT French project VALISERV and by the European Commission under WGs Fireworks (23531) behaviours of a telecommunication system do not conform to some feature descriptions offered to customers, this may have calamitous effects on the public image of the concerned provider.

The paper is the continuation of the works developed in [START_REF] Berkani | An Environment for Interaction Service Specification[END_REF][START_REF] Berkani | An Incremental Method for the Design of Featureoriented Systems[END_REF] by giving the theoretical basis of the methodology and the tool presented respectively in [START_REF] Berkani | An Incremental Method for the Design of Featureoriented Systems[END_REF] and in [START_REF] Berkani | An Environment for Interaction Service Specification[END_REF]. This will be briefly recalled in Section 4. Our purpose is then to formally define an integration methodology allowing to solve interactions resulting from an inconsistent integration of a feature in a system specification, according to expert's point of view. The theoretical foundations will be based on algorithms the correctness of which will be proved (see Theorem 2 and Theorem 3). These algorithms deal with specification consistency. More precisely, interactions are properties which are violated. They may be qualified as desirable or not by an expert who can modify both the considered property, and integration choices to make service integration conform to its judgement. Thus, interaction resolution takes care of interactions which may be introduced during the integration process. To ease the service design, we define an axiomatic formalism (i.e. system behaviour is specified by logical properties) which will be used for detection and resolution. This formalism aims to specify telecommunication systems viewed along phone services at which customers can subscribe. Now, both formalism and methodology can be obviously extended and applied to specify and automatically analyse interaction in systems viewed along services (not necessarily phone services) at which objects can subscribe (e.g. lifts equipped with different services such as the basic service and the service which indicates a priority floor).

The methodology presented in this paper will then take advantage of designer's expertise with an interactive integration activity assisted by static analysis of specification consistency. This static analysis will be based on symbolic techniques dealing with phone variables to deduce the appropriate subscription configuration. Hence, the formalism defined in this paper will manipulate state transition rules (str), invariants and inequations between phone variables. The formalism developed in the paper is then a simple restriction of classic pre -post logical language. The interest of such a language is twofold:

1. it allows to automatically detect inconsistencies after integrating a new feature in a system specification. This is precisely the main goal of the present paper. 2. its syntax is very simple up to some syntactical sugar 5 . Hence, specifications are made readable for the expert what will ease his(her) choices to circumvent inconsistencies. Besides, this has been experimented in the ValiServ project with some experts of our partner France Telecom.

The paper is structured as follows. Section 2 presents the formalism and the notion of specification consistency on which our interactions are based on. Specifications are provided in the form of invariant properties and state transition rules, very much as in [START_REF] Nakamura | Design and Evaluation of Efficient Algorithms for Feature Interaction Detection in Telecommunication Services[END_REF]. Examples are also provided. For lack of space, we present a simple and pedagogical example which only integrates three features on a basic system. More generally, our method can deal with all services which can be expressed within our specification formalism and integrated on the intelligent network (see [START_REF] Berkani | Un cadre méthodologique pour l'intégration de services par évitement des interactions[END_REF] and [START_REF] Jouve | Caractérisation et détection automatique d'interactions de services à partir de spécifications graphiques[END_REF] for more than 20 examples of such service specifications). Section 3 details the algorithms used to check specification consistency in the integration process. Section 4 presents the methodology and our results on usual services using the tool [START_REF] Berkani | An Environment for Interaction Service Specification[END_REF] developed in the ValiServ project. Finally, related works are addressed in Section 5.

By lack of space, most of the proofs of propositions and theorems are not given in this paper. However, they can be found in the preliminary version of this paper [START_REF] Aiguier | Feature specification and static analysis for interaction resolution[END_REF]. Only the proof of Theorem 1 is given because the algorithms described in this paper are based on it.

Service specification

Here, we define a formalism dedicated to service (so-called feature) telecommunication systems. Services will be specified along two types of predicates, subscription and status. By the former, we will specify what and how customers subscribe to a service. For instance 6 , ✂✁ ☎✄ ✝✆ ✟✞ ✡✠ ☞☛ ✍✌ will mean that ✞ has subscribed to ✂✁ ☎✄ and any call from ☛ to ✞ is forbidden. By the latter, we will specify communication situations such as to be busy, idle, etc... Moreover, telecommunication systems are dynamic systems. Therefore, in order to automatically analyse interactions, the formalism under definition will manipulate sentences of the form ✆ ✏✎ ✒✑ ✔✓ ✕✠ ✖✓ ✘✗ ✙✓ ✛✚ ✢✜ ✣✠ ✟✎ ✥✤ ✧✦ ★✜ ☞✌ where ✎ ✒✑ ✩✓ and ✎ ✒✤ ✧✦ ✘✜ will be finite sets of atoms denoting respectively pre and post-conditions and ✓ ✛✗ ✕✓ ✛✚ ✢✜ will be an event triggering side-effect. Moreover, some invariants roughly defined by free-quantifier first-order formulas (i.e. state-evolution independent) will be stated.

Syntax

The formalism is devoted to specify features in telecommunication systems. Its syntax is closely related to the one developed in [START_REF] Gammelgaard | Interaction Detection, a Logical Approach[END_REF]. Vocabularies (so-called signatures) over which pre and post-conditions and invariants will be built on, will then contain two types of predicates: status and subscription predicates. Note, by the definition of signatures, that variables are the only allowed arguments for the predicates and the events. Hence, variables will necessarily denote terminals.

Definition 1 (Signature

Systems will be specified by means of two kinds of formulas: State transition rules ( ✦ ✘✜ ✽✑

) and Invariants. Moreover, as we are interested by automatically analysing interactions (which will be defined by properties), manipulated formulas will be constrained on their form. In the sequel, quantifier-free first-order formulas will be simply called formulas. We will note ❆ ❈❇ ✑ ✆ ✟✞ ✥✌ the set of variables occurring in ✞ ✵ ✟ ❉★ ✜ ✽✑ ✩✠ ✭✦ ☛✫ ✼✮ ✦ ✠ ✫✎ ✑ ✩✓ ✕✠ ✟✎ ✒✤ ✧✦ ✘✜ ✣✠ ❊❄ ✘✙ .

We have chosen to separate in str-formulas, subscription atoms from pre and postconditions because events do not modify subscriptions. Hence, subscriptions are necessarily preserved along transitions.

Definition 4 (Service specification).

A service specification ❋ is a • -tuple ✆ ✪ ✠ ✄ ✞ ✼✌ where ✪ is a signature and ✄ ✞ is a set of str-formulas and invariants over ✪ .

❋ is said finite if both ✪ and ✄ ✞ are a finite signature and finite set of axioms, respectively. In the sequel ✄ ✞ will be also noted ✄ ✬ ■❍ ✿❏ ❅❑ . ✄ ✬ ▲❍ and ❑

will then contain all the str-formulas and invariants, respectively, of ✄ ✞ .

Examples

We now provide examples: the specifications of the basic telecommunication system, classically called POTS, and of three common services destined to be plugged on it. The different components of the specifications will be indexed by the specification name. Moreover, elements of the underlying system POTS are implicitly present for the specification of the three services.

example 1: POTS, the Plain Old Telephone Service

✄ ✬✜ ❁▼ ❖◆ ◗ ❙| contains ✖ ❯❚ ❲❱ ✫✓ ✙✆ ✞ ✥✌ (" ✞ is idle"), ❚ ❲✖ ❇ ❱ ✞❳ ❇ ✖ ✜ ✆ ✞ ✥✌ (" ✞ is in dial
☎ ❏❱ ✆ ✟✞ ✵✓ ✷✶ ✸ ✺✹ ✠ ❉ ✏ ❅✭ ✁❊ ❋☛ ✍• ■❍ ❏✒ ✔✓ ❲✽ ✹ ✕ ✾✽ ▲❊ ❳☛ ✔• ■❍ ✁☛ ✔• ■❍ ❏✒ ✹ ✽ ✿✓ ✼✕ offhook ✤ ◆❇ ❈✧ ✩ ✫✪ ( ✭ ✮✎ ❀✎ ❀✏ ❅❊ ✮✒ ✔✓ ❑✽ ✹ ✕ ✾✽ ( ✭ )✎ ✑✎ ❀✏ ✛✏ ✁✒ ✹ ✽ ✢✓ ✖✕ ✴✳ ☎ ★❬ ✆ ✟✞ ✵✓ ✷✶ ✸ ✺✹ ✠ ( ✭ )✎ ✑✎ ❀✏ ❅❊ )✒ ✔✓ ❲✽ ✹ ✕ ✾✽ ( ✭ ✮✎ ❀✎ ❀✏ ✛✏ ✬✒ ✹ ✽ ✢✓ ✼✕ ✗ (❭ )✜ ☞✗ ✢✗ ✾✣ ❋✤ ✦✥ ★✧ ✩ ✫✪ ☛ ✔✌ ✁✎ ❀✏ ✬✒ ✔✓ ✼✕ ✾✽ ◗ ✚| ❏❙ ☞❚ ✱ ✿❯ ❋• ★✏ ✁✒ ✹ ✕ ✴✳ ☎ ❏❴ ✆ ✟✞ ✵✓ ✷✶ ✸ ✺✹ ✠ ( ✭ )✎ ✑✎ ❀✏ ❅❊ )✒ ✔✓ ❲✽ ✹ ✕ ✾✽ ( ✭ ✮✎ ❀✎ ❀✏ ✛✏ ✬✒ ✹ ✽ ✢✓ ✼✕ ✗ (❭ )✜ ☞✗ ✢✗ ✾✣ ❋✤ ◆❇ ❈✧ ✩ ■✪ ☛ ✍✌ ✁✎ ✑✏ ✁✒ ✹ ✕ ✾✽ ◗ ✾| ❏❙ ☞❚ ✱ ❵❯ ❳• ★✏ ✬✒ ✔✓ ✼✕ ✴✳ ☎ ★❛ ✆ ✟✞ ✵✓ ✷✶ ✸ ✺✹ ✠ ❉ ✏ ❅✭ ✁❊ ❋☛ ✍• ■❍ ❏✒ ✔✓ ❲✽ ✹ ✕ ✾✽ ▲❊ ❳☛ ✔• ■❍ ✁☛ ✔• ■❍ ❏✒ ✹ ✽ ✿✓ ✼✕ ✘✗ (❭ )✜ ☞✗ ✢✗ ✚✣ ✛✤ ✦✥ ★✧ ✩ ■✪ ☛ ✔✌ ✁✎ ❀✏ ✬✒ ✔✓ ✼✕ ✾✽ ▲☛ ✔✌ ✁✎ ❀✏ ✬✒ ✹ ✕ ✴✳ ☎ ❏❜ ✆ ✟✞ ✡✠ ◗ ✚| ❏❙ ☞❚ ✱ ✿❯ ❋• ★✏ ✁✒ ✔✓ ✖✕ ✗ (❭ )✜ ☞✗ ✢✗ ✾✣ ❋✤ ✦✥ ★✧ ✩ ✫✪ ☛ ✔✌ ✁✎ ❀✏ ✬✒ ✔✓ ✼✕ ❝✳ ☎ ❏❞ ✆ ✟✞ ✡✠ ☞✌ ✬☛ ✍✭ ✮✎ ✑✯ ✻✭ ✁☛ ✲✱ ☞✒ ✔✓ ✼✕ ✗ ✾❭ ❡✜ ☞✗ (✗ ✾✣ ❋✤ ❖✥ ❈✧ ✩ ■✪ ☛ ✍✌ ✁✎ ✑✏ ✁✒ ✔✓ ✖✕ ❝✳ ❑ ✣▼ ❖◆ ◗ ❙|
contains several invariants expressing that status predicates are mutually exclusive when they concern the same variables. For example, it contains:

✧ ❣❢ ✾ ✁ ❅✌ ✛ ✆ ✜ ❇ ❱ ❤✄ )✖ ✚ ❙( ✢✆ ✄ ✠ ❢ ✌ ✂✐ ✺✜ ❇ ❱ ❤✄ ❃✖ ✚ ❙( ✢✆ ✄ ✠ ✖✁ ☎✌ ✌ ✓✽ ✧ ✌ ✛ ✆ ✝✖ ❯❚ ❱ ✟✓ ✙✆ ✄ ✌ •✐ ✺✜ ❇ ❱ ❤✄ )✖ ✚ ❙( ✢✆ ✄ ✠ ❢ ✌ ✌ ✘✽
For lack of space, we do not give all such invariants. However, they can be found in [START_REF] Berkani | Un cadre méthodologique pour l'intégration de services par évitement des interactions[END_REF].

POTS characterises the behaviour of a terminal which has just subscribed to the basic telephone service, when communicating with another terminal with the same subscription. For example, ❦ ✘• says that if the call initiator hangs up during a communication, then his party gets a busy tone. example 2: TCS, Terminating Call Screening (this service screens out incoming calls from terminals belonging to the TCS subscriber's black list).

✄ ✯✮ ♠ |

contains Tcs ✆ ☛ ✼✠ ☞✞ ✼✌ : calls from ✞ to ☛ are forbidden by ☛

. ❑ ♠ | contains ♥ ☎ ✆ ♦✞ ✵✓ ✷✶ ✸ ✺✹ ✠ Tcs ✒ ✔✓ ❑✽ ✹ ✕ •♣ rq ❉ ✏ ❅✭ ✁❊ ❋☛ ✍• ■❍ ❏✒ ✹ ✽ ✢✓ ✼✕ ❝✳ while ✄ ✲ ■❍ ❈♠ | contains ♥ ✆ ✆ ♦✞ s✠ Tcs ✒ ✹ ✽ ✢✓ ✼✕ ✾✽ ▲✌ ✬☛ ✔✭ ✮✎ ✑✯ ✻✭ ✁☛ ✔✱ ✚✒ ✔✓ ✼✕ ✾✽ ❵☛ ✍✌ ✁✎ ✑✏ ✁✒ ✹ ✕ ❁ ✚❂ ✦❃ ❅❄ ✑✤ ✦✥ ✘❆ ❇ ❈✧ ✩ ✫✪ ◗ ✚| ❏❙ ☞❚ ✱ ✿❯ ❋• ★✏ ✬✒ ✔✓ ✼✕ ✴✳
example 3: CFB, Call Forward on Busy (this service allows a subscriber to forward all incoming calls to a designated terminal, when the subscriber's terminal is busy).

✄ ✯✮ ❅♠ ✉t ✉✈ contains Cfb ✆ ✞ ✠ ☞☛ ✍✌ : when ✞ is not idle, forward incoming calls to ☛ . ❑ ❡♠ ✉t ✉✈ contains ✇ ☎ ✝✆ ❣✞ s✠ ✛q Cfb ✒ ✔✓ ❲✽ ✢✓ ✼✕ ❝✳ ✇ ✆ ✖✆ ❣✞ ✹ ✶ ✸ ✿ ✠ Cfb ✒ ✔✓ ❑✽ ✹ ✕ •♣ rq Cfb ✒ ✔✓ ❲✽ ✿ ✕ ❝✳ and ✄ ✬ ■❍ ♠ ✉t •✈ contains ✇ ▼ ✆ ❣✞ ✹ ✶ ✸ ✿ ✠ Cfb ✒ ✹ ✽ ✿ ✕ ✾✽ ✢✌ ✬☛ ✍✭ ✮✎ ✑✯ ✻✭ ✁☛ ✲✱ ☞✒ ✔✓ ✼✕ ✾✽ ☛ ✔✌ ✁✎ ❀✏ ✬✒ ✹ ✕ (✽ ✿☛ ✍✌ ✁✎ ✑✏ ✁✒ ✿ ✕ ❁ ✾❂ ◆❃ ☞❄ ✑✤ ✦✥ ✘❆ ❇ ✧ ✩ ■✪ ❉ ✏ ❅✭ ✁❊ ❳☛ ✔• ■❍ ❏✒ ✔✓ ❑✽ ✿ ✕ ✾✽ ▲❊ ❳☛ ✔• ■❍ ✁☛ ✔• ■❍ ❏✒ ✿ ✽ ✿✓ ✼✕ ❝✳ ✇ ❱ ✆ ❣✞ ✹ ✶ ✸ ✿ ✠ Cfb ✒ ✹ ✽ ✿ ✕ ✾✽ ✢✌ ✬☛ ✍✭ ✮✎ ✑✯ ✻✭ ✁☛ ✲✱ ☞✒ ✔✓ ✼✕ ✾✽ ☛ ✔✌ ✁✎ ❀✏ ✬✒ ✹ ✕ (✽ ☛ ✍✌ ✁✎ ✑✏ ✁✒ ✿ ✕ ❁ ✾❂ ◆❃ ☞❄ ✑✤ ✦✥ ✘❆ ❇ ✧ ✩ ■✪ ◗ ✚| ■❙ ❅❚ ✱ ❵❯ ❳• ★✏

✰ ✄✂ ✆☎

contains two new events related to the pin dialling:

❚ ❲✖ ❇ ❱ ✝( ✙✤ ✩✤ ✜❚ ✘✎ ✖ ✚ ✯✆ ✞ ✼✌ for " ✞
is dialling the expected correct pin", and

❚ ❲✖ ❇ ❱ ✫✮ ❇ ❚ ✘✎ ✖ ✚ ✯✆ ✞ ✼✌ for " ✞
is dialling a wrong pin".

✄ ✬ ■❍ ✠ ✡✂ ✆☎

contains:

☛ ☎ ✻✆ ♦✞ ✡✠ Intl ✒ ✔✓ ✖✕ ✾✽ ✿✱ ✿☛ ✌☞ ✏ ✬✒ ✔✓ ✖✕ ✾✽ ✿☛ ✔✌ ✁✎ ❀✏ ✬✒ ✔✓ ✼✕ ✗ ✾✙ ✛✙ ✛✜ ❅✗ ✢✗ ✾✣ ❋✤ ✦✥ ★✧ ✩ ■✪ ✯ ✰✭ ✁☛ ✲✱ ✎✍ ✫☛ ✔• •✒ ✔✓ ✼✕ ✾✽ ❵✱ ✿☛ ✌☞ ✏ ✬✒ ✔✓ ✼✕ ✴✳ ☛ ✆ ✼✆ ♦✞ ✡✠ ☞✯ ✰✭ ✁☛ ✲✱ ✎✍ ☛ ✍• •✒ ✔✓ ✖✕ ❁ ✚❂ ✦❃ ❅❄ ✏ (✗ (✗ ✢❁ ✒✑ ❅❂ ◆❭ ✮✤ ❖✥ ❈✧ ✩ ✫✪ ✌ ✬☛ ✔✭ ✮✎ ✑✯ ✻✭ ✁☛ ✔✱ ✚✒ ✔✓ ✼✕ ✴✳ ☛ ▼ ✆ ♦✞ ✡✠ ☞✯ ✰✭ ✁☛ ✲✱ ✎✍ ☛ ✍• •✒ ✔✓ ✖✕ ❁ ✚❂ ✦❃ ❅❄ ✔✓ ✔❃ ☞❁ ✕✑ ☞❂ ◆❭ ✮✤ ✦✥ ★✧ ✩ ✫✪ ☛ ✔• ✗✖ ✬✭ ✮✎ ✑☛ ✔✌ ■✒ ✔✓ ✖✕ ✳ ☛ ❱ ✆ ♦✞ ✡✠ ☞☛ ✔• ✗✖ ✬✭ ✮✎ ✑☛ ✔✌ ■✒ ✔✓ ✖✕ ✂✗ (❭ ❡✜ ❅✗ ✢✗ ✾✣ ❋✤ ✦✥ ★✧ ✩ ✫✪ ☛ ✔✌ ✁✎ ❀✏ ✬✒ ✔✓ ✖✕ ✳ ☛ ❬ ✆ ♦✞ ✡✠ ☞✯ ✰✭ ✁☛ ✲✱ ✎✍ ☛ ✍• •✒ ✔✓ ✖✕ ✗ ✾❭ ❡✜ ☞✗ (✗ ✾✣ ❋✤ ❖✥ ❈✧ ✩ ■✪ ☛ ✍✌ ✁✎ ✑✏ ✁✒ ✔✓ ✖✕ ❝✳
Specifications are restricted to service specificities. They implicitly refer to the underlying system. For example, the TCS specification contains a service invariant characterising a newly prohibited situation (the subscriber terminal cannot be put in communication with a terminal from its screening list) and a limited behavioural description (what happens when a forbidden terminal attempts to call the subscribing terminal).

Semantics Definition 5 (Models

). Let ✪ ✆ ✄ ✬✜ ✣✠ ✖✄ ✯✮ ✩✠ ✰ ✱✌ be a signature. A ✪ -model ✘ ✆ ✚✙ ✝✠ ✖✄ ✬✠ ✛✆ ✟✓ ✜✛ ❀✌ ✮ ✡✢ ✤✣ ✌ is a set ✙ (terminals)
-✆ ✲ ✠ ✖✦ ✔✌ ✌ ✎ ✆ ✟✞ ✠ ☞✡ ☞✡ ☛✡ ✠ ☞✞ ✻ ✌ ✴✳ ✶✵ ✎ ✆ ✲ ✆ ✞ ✌ ✠ ☞✡ ☞✡ ☛✡ ★✠ ✲ ✆ ✟✞ ✻ ✌ ✌ ✵ ✦ -propositional connectives are handled as usual. ✘ satisfies a formula ❄ , noted ✘ ✌ ❄
, if and only if for every ✦ ✵ ✄

and every ✲ ✬ ✂ ✻ ✙ , ✆ ✲ ✠ ✭✦ ✛✌ ■✌ ❄ . Definition 7 (Transition satisfaction). A ✪ -model ✘ satisfies for ✦ ✵ ✄ and ✲ ✬ ✂ ✻ ✙ a str-formula ❄ of the form ✧ ★ ✜ ✽✑ ✪✌ ✦ ☛✫ ✼✮ ✦ ✬ ✔✎ ✒✑ ✔✓ ✮ ✰✯ ✲✱ ✳ ✵ ✷✶ ✷✶ ✷✶ ✵ ✱ ✸ ✹ ✺ ✼✻ ✎ ✒✤ ✧✦ ✘✜ ✽ , noted ✘ ✌ ✸✷ ✵ ✹ ❄ , if
and only if, if for every ✞ ✿✾ ☛ ✺✵ ★ ✜ ✽✑ , ✲ ✆ ✟✞ ✥✌ ✕✾ ✺✲ ✆ ☛ ✍✌ then: ✘ which satisfies it and such that the cardinality of its set ✙ of terminals satisfies:

7 We note ❙ ✏ ✼✻ ✻✒ | ☎ ✽ ✄✽ ✄✽ ✡✽ ☞✽ | ❭ ✕ ❙ ✄✾ to mean that ✒ ❙ ✽ ❙ ✱✾ ✕ ❀✿ ✏ ✮✻ ✰✒ | ☎ ✽ ✡✽ ✄✽ ✄✽ ☞✽ | ❭ ✕ . if ✆ ✲ ✠ ✖✦ ✔✌ ✌ ✁ ✢ ✹ ✄✂ ✆☎ ✞✹ ✞✝ ✠✟ ☛✡ ✰✮ ☞ then ✌ ✦ ✎✍ ✢✵ ✄ ✲✠ ✖✦ ✓ ✜✛ ✆ ✲ ✆ ✟✞ ✌ ✣✠ ☛✡ ☞✡ ☛✡ ✠ ✲ ✆ ✞ ✻ ✌ ✌ ✦ ✎✍ ✟✵ ✆ ✲ ✠ ✖✦ ✎✍ ✌ ✌ ✁ ✢ ✏✟ ☛✑ ✡✹ ✓✒ ☞ ✌ Definition 8 (Invariant satisfaction). A ✪ -model ✘ satisfies for ✦ ✵ ✄ and ✲ ✬ ✂ ✻ ✙ an invariant ✧ ✠★ ✜ ✽✑ ✪✌ ❄ ✽ , noted ✘ ✌ ✷ ✵ ✹ ✧ ✠★ ✜ ✽✑ ✪✌ ❄ ✽ , if and only if, if for every ✞ ✾ ☛ ✶✵ ★ ✜ ✽✑ ✩✠ ✲ ✆ ✞ ✼✌ ✾ ✲ ✆ ✟☛ ✍✌ then ✆ ✲ ✠ ✖✦ ✔✌ ✌ ❄
✌ ✙ ✌ ✕✔ ✝ ❇ ✞ ✟ ✴❆ ❈❇ ✑ ✆ ★ ✜ ✽✑ ✧✌ ☞✌ ✖ ✧ ★ ✜ ✽✑ ❃✌ ✦ ☛✫ ✼✮ ★✦ ✕✬ ✎ ✑ ✩✓ ✮ ✻ ✎ ✒✤ ✧✦ ✘✜ ✓✽ ☎✵ ✄ ✲ ■❍ ✘✗ ✙✖ ✧ ✗★ ✜ ✽✑ ✪✌ ❄ ✽ ☎✵ ❑ ✪✙
The last condition on the carrier cardinality of ✪ -models prevents trivial ✪ -models. A trivial ✪ -model is such that the number of terminals in ✙ is not sufficient to satisfy each inequation occurring in the ★ ✜ ✽✑ part of each formula in ✄ ✬ ■❍ and ❑ .

Fundamental results

We first define a ✪ -model which will be useful to us in the next section. Let ✪ ✁ ✆ ✫✄ ✬✜ ✣✠ ✭✄ ✯✮ ✔✠ ✰ ✌ be a signature. Let ✙ and ✄ ❀ ✥ ✆ ✫✄ ✲✜ ✥☎ ✆ ✚✙ ☎✌ ✌ be two sets of terminals and states, respectively. Let ✄ ✬ ■❍ be a set of str-formulas over ✪ . Therefore, define the

✪ -model ✚ ✆ ✞✙ ✠ ✖✄ ✴✌ ✆ ✚✙ ✝✠ ✖✄ ✛✍ ✟✠ ✛✆ ✟✓ ✆✜ ✯ ✣✢ ✪✵ | ✹ ✌ ✮ ✡✢ ✤✣ ✌
as follows:

-✄ ✍ is the set inductively defined by ✄ ✍ ✥✤ ✎ ✧✦ ✩★ ✄ ✎ with: such that for every

✪ ✄ ✬✫ ✄ ✪ ✦ ✎✍ ✵ ✄ ✻ ✳ ✵ ✭ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✯ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✰ ✖ ✧ ★ ✜ ✽✑ ✪✌ ✦ ☛✫ ✼✮ ✦ ✭✬ ★✎ ✑ ✩✓ ✮ ❊✯ ✲✱ ✳ ✵ ✷ ✶ ✷ ✶ ✷ ✶ ✵ ✱ ✸ ✹ ✺ ✼✻ ✎ ✥✤ ✧✦ ★✜ ✓✽ ☎✵ ✄ ✬ ■❍ ✠ ✱✖ ✲ ✬ ✂ ✻ ✙ ✠ ✖ ✍✦ ☎✵ ✄ ✻ ✳✲ ✠ ✛✆ ✌ ✞ ✿✾ ☛ ✵ ★ ✜ ✽✑ ✩✠ ✲ ✆ ✞ ✥✌ ✕✾ ✺✲ ✆ ☛ ✍✌ ✌ (✐ ✆ ✲ ✠ ✖✦ ✔✌ ✌ ✁ ✢ ✹ ✞✂ ✏☎ ✞✹ ✞✝ ✠✟ ☛✡ ✰✮ ☞ ✐ ✦ ✎✍ ✆ ✫✦ ✵✴ ✟ ✎ ✆ ✲ ✆ ☛ ✌ ✣✠ ☞✡ ☛✡ ☞✡ ✘✠ ✲ ✆ ☛ ✠✶ ✌ ☞✌ ☛✌ ✛ ✎ ✆ ☛ ✠ ☞✡ ☛✡ ☞✡ ✘✠ ☞☛ ✠✶ ✌ ❀✵ ✎ ✥✤ ✧✦ ✘✜ ✰✙ ✔✌ ✳ ✟ ✎ ✆ ✲ ✆ ✟☛ ✌ ✠ ☞✡ ☛✡ ☞✡ ★✠ ✲ ✆ ☛ ✠✶ ✌ ☞✌ ☛✌ ✎ ✆ ☛ ✠ ☞✡ ☛✡ ☞✡ ★✠ ☛ ✠✶ ✂✌ ✝✵ ✎ ✥✤ ✧✦ ★✜ ✰✙ -For every ✓ ✔✻ ✵ ✹✰ and every ✆ ✞✫ ✠ ☛✡ ☞✡ ☛✡ ✠ ✆✫ ✻ ✌ ✵ ✦✙ ✧ ✡ ☞✡ ☛✡ ✩✧ ✪✙ ✫ ✬ ✮✭ ✯ ✻ times , ✓ ✏✜ ✯ ✣✢ ✪✵ | ✹ ✆ ✝✫ ✠ ☛✡ ☞✡ ☛✡ ✠ ✆✫ ✻ ✌ is defined: ✦ ✓ ✆✜ ✯ ✣✢ ✪✵ | ✹ ✆ ✝✫ ✠ ☞✡ ☛✡ ☞✡ ✘✠ ✆✫ ✻ ✌ ✦ ✎✍ ✆✳ ✶✵ ✭ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✯ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✰ ✖ ✧ ★ ✜ ✽✑ ✪✌ ✦ ☛✫ ✼✮ ✦ ✬ ✎ ✑ ✩✓ ✮ ❊✯ ✲✱ ✳ ✵ ✷ ✶ ✷ ✶ ✷ ✶ ✵ ✱ ✸ ✹ ✺ ✏✻ ✎ ✥✤ ✧✦ ✘✜ ✍✽ ☎✵ ✄ ✬ ■❍ ✠ ✱✖ ✲ ✬ ✂ ✻ ✙ ✠ ✆ ✌ ✒ ✔ ✸✷ ✔ ✚ ✲✠ ✲ ✆ ✟✞ ✺✹ ✛✌ ✫ ✻✹ ✛✌ ✾✐ ✆ ✌ ✞ ✿✾ ☛ ✺✵ ★ ✜ ✽✑ ✩✠ ✲ ✆ ✞ ✼✌ ✾ ✺✲ ✆ ✟☛ ✌ ✌ (✐ ✆ ✲ ✠ ✖✦ ✔✌ ✌ ✁ ✢ ✹ ✞✂ ✏☎ ✞✹ ✞✝ ✠✟ ☛✡ ✰✮ ☞ ✐ ✦ ✎✍ ✆ ✫✦ ✼✴ ✟ ✎ ✆ ✲ ✆ ☛ ✌ ✣✠ ☛✡ ☞✡ ☞✡ ★✠ ✲ ✆ ☛ ✠✶ ☎✌ ✌ ☞✌ ✛ ✎ ✆ ☛ ✠ ☛✡ ☞✡ ☞✡ ★✠ ☞☛ ✠✶ ✌ ❀✵ ✎ ✒✤ ✧✦ ✘✜ ✰✙ ✳ ✟ ✎ ✆ ✲ ✆ ☛ ✌
✰ ☎ ✆ ✝✂ ✶✌ ✠✟ ✦ ✕❀ ✄ ✜ ☎ ✆ ✝✂ ✌ ☛✌ ✌ ✲ ✬ ✂ ✻ ✂ ✠ ✌ ✧ ★ ✜ ✽✑ ✪✌ ❄ ✗✽ ☎✵ ✢❑ ✒✠ ✆ ✌ ✞ ✿✾ ☛ ✺✵ ★ ✜ ✽✑ ✩✠ ✲ ✆ ✞ ✥✌ ✕✾ ✺✲ ✆ ☛ ✍✌ ✌ ✵ ✆ ✫✦ ✠ ✲ ✌ ■✌ ❄ ✲✌ ✰✙ then define ❑ ☎ ✆ ✞✂ ✌ ✟ ✦ ☎✵ ✰ ☎ ✆ ✝✂ ✌ ☛✌ ✾ ✖ ✍✦ ✍ ✵ ✰ ☎ ✆ ✝✂ ✌ ✠ ✖✦ ✍ ❀ ✦ ✙ . Proposition 1.
✞ ✩✍ ✾ ☛ ✺✍ ❀✵ ★ ✜ ✽✑ ✏✍ , ✲ ✍ ✆ ✞ ✍ ✌ ✾ ✲ ✍ ✆ ☛ ✺✍ ✌ , ✆ ✦ ✠ ✲ ✍ ✌ ✌ ✁ ✢ ✹ ✄✂ ✆☎ ✞✹ ☎✞ ✝ ✠✟ ✡ ✰✮ ☎✞ ☞ , ✛ ✎ ✆ ✝❳ ✠ ☞✡ ☛✡ ☞✡ ✠ ✥❳ ✵✶ ☎✌ ✱✵ ✎ ✥✤ ✧✦ ★✜ ✞✍ and ✲ ✆ ☛ ✎ ✌ ✲ ✍ ✫✆ ✞❳ ✎ ✌ ( ✒ ✔ ✖ ✔ ✝ ). As ❋ is consistent, there exists a ✪ -model ✘ which satisfies it. Let ✲ ✍ ✍ ✬ ✂ ✻ ✙
be an interpretation in ✘ such that for ev-

ery ✞ ❂✾ ☛ ✵ ★ ✜ ✽✑ and ✞ ✍ ✾ ☛ ✍ ✵ ★ ✜ ✽✑ ✍ , ✲ ✍ ✍ ✆ ✞ ✼✌ ✾ ✲ ✍ ✍ ✆ ✟☛ ✌ and ✲ ✍ ✍ ✆ ✟✞ ✍ ✌ ✾ ✲ ✍ ✍ ✆ ☛ ✍ ✌
, and

✲ ✍ ✍ ✆ ✟✞ ✎ ✌ ✲ ✍ ✍ ✫✆ ✞❳ ✎ ✌ ❈✒ ✩✔ ✖ ✔ ✚
. By the property on the carrier cardinality of ✪ - models, ✲ ✍ ✍ exists.

By construction of

✚ ✆ ✝✂ ✠ ✥❑ ☛☎ ✆ ✞✂ ✌ ☞✌ , there exists a state ✦ ✎✍ ✍ in ✘ such that ✲ ✍ ✍ ✆ ✫✦ ✔✌ ✓❀ ✦ ✍ ✍ .
We then have for every

☞ ✵ ✦ ☞✫ ✢✮ ✦ ✼✳ ☎✦ ☛✫ ✼✮ ★✦ ✏✍ ✳ ❀✎ ✑ ✩✓ ✢✳ ❀✎ ✑ ✩✓ ✏✍ that ✆ ✫✦ ✎✍ ✍ ✫✠ ✲ ✍ ✍ ✌ ✌ ☞ . Therefore, there exists ✦ ✠✟ in ✘ such that ✦ ✎✍ ✍ ✓ ✆✜ ✯ ✆✁ ✓✵ ✡✄ ✯ ✆✁ ✹ ✝✹ ✆ ✲ ✍ ✍ ✆ ✞ ✌ ✠ ☞✡ ☛✡ ☞✡ ★✠ ✲ ✍ ✍ ✆ ✞ ✻ ✌ ☞✌ ✦ ✠✟ . But, we have both ✎ ✆ ✲ ✍ ✍ ✆ ☛ ✌ ✣✠ ☛✡ ☞✡ ☞✡ ✲ ✍ ✍ ✆ ☛ ✶ ✌ ✌ ✵ ✦ ✠✟ and ✎ ✆ ✲ ✍ ✍ ✆ ✟☛ ✌ ✠ ☞✡ ☞✡ ☛✡ ✲ ✍ ✍ ✆ ☛ ✶ ✌ ☞✌ ✜✾ ✵ ✦ ✠✟
what is impossible.

8 ❁ ✾ is the set of state of ☛ ✒ ✌☞ ✽ ☎✍ ✏✎ ✰✒ ✌☞ ✕ ▲✕ 9 Without any loss of generality, we only consider the case of a positive literal ✍ ✘✒ ❚ ☎ ✽ ✄✽ ✄✽ ✄✽ ❅✽ ❚ ✠✑ ✕ in ✍ ✫❯ ❙ ✱ . The case of a negative literal q ✍ ✘✒ ❚ ☎ ✽ ✄✽ ✄✽ ✡✽ ☞✽ ❚ ☞ ✕ can be handled in a similar way.

✎ ✑ ✩✓ ✎ ✮ ✁ ❁✯ ✲✱ ✳ ✵ ✷✶ ✷✶ ✷✶ ✵ ✱ ✸ ✺ ✏✻ ✎ ✒✤ ✧✦ ✘✜ ✎ ✽ in STR, ✚ interpretations ✲ ✎ ✬ ✂ ✻ ✂
and ✚ ✄✂ ✒ states ✦ ✎ with ✦ ✦ and ✦ ✻ ✆☎ ✦ ✎✍

, such that for every

✒ ❈✔ ✖ ✓✔ ✚ and every ✞ ✾ ☛ ✺✵ ★ ✜ ✽✑ ✎ ✲ ✎ ✆ ✟✞ ✥✌ ✿✾ ✲ ✎ ✆ ✟☛ ✍✌ , ✆ ✦ ✎ ✠ ✲ ✎ ✌ ✌ ✁ ✢ ✹ ✄✂ ✆☎ ✞✹ ✝ ✠✟ ☛✡ ✰✮ ☞ , ✦ ✎ ✓ ✜ ✯ ✂✁ ✓✵ ✄ ✯ ✆✁ ✹ ✝✹ ✎ ✆ ✲ ✎ ✆ ✞ ✎ ✌ ✣✠ ☛✡ ☞✡ ☛✡ ★✠ ✲ ✎ ✆ ✞ ✎ ✻ ✌ ✌ ✦ ✎ ☎ and ✆ ✫✦ ✎ ☎ ✠ ✲ ✎ ✌ ✌ ✁ ✢ ✏✟ ✑ ✹ ✄✒ ☞ . By construction of ✚ ✆ ✞✂ ✠ ✥❑ ☎ ✆ ✝✂ ✌ ✌
, this then means there exists for every

✒ ✢✔ ✖ ✭✔ ✚ , ✎ ✼✎ ✖✆ ☛ ✎ ✠ ☞✡ ☛✡ ☞✡ ★✠ ☛ ✎ ✶ ✌ ✵ ✄ ✜ ✆☎ ✆ ✝✂ ✌ such that ✲ ✆ ☛ ✎ ✹ ✌ ✲ ✎ ✖✆ ☛ ✎ ✹ ✌
for every

✒ ✭✔ ✷ ✔ ✝ ✎
, and

✎ ✼✎ ☞✆ ✲ ✆ ✟☛ ✎ ✌ ✣✠ ☞✡ ☛✡ ☞✡ ✘✠ ✲ ✆ ☛ ✎ ✶ ✌ ✌ ❀✵ ✦ but ✎ ✼✎ ✆ ✲ ✆ ☛ ✎ ✌ ✣✠ ☛✡ ☞✡ ☞✡ ★✠ ✲ ✆ ☛ ✎ ✶ ✌ ✌ ✴✾ ✵ ✦ ✎✍ .
As ❋ is consistent, there exists a ✪ -model ✘ which satisfies it. Let ✲ ✍ ✬ ✂ ✻ ✙ be an interpretation in ✘ such that for every

✞ ✾ ☛ ✸✵ ★ ✜ ✽✑ ✳ ✤ ✞✝ ✎ ✝ ✻ ★ ✜ ✽✑ ☛✎ , ✲ ✍ ✆ ✞ ✥✌ ✭✾ ✲ ✍ ✆
✆ ✦ ✎✍ ✎ ☎ ✠ ✲ ✍ ✌ ✌ ✁ ✢ ✏✟ ✑ ✹ ✄✒ ✠
☞ . Whence we deduce that for every

✒ ✔ ✖ ✔ ✚ , ✎ ✏✎ ✖✆ ✲ ✍ ✆ ☛ ✎ ✌ ✣✠ ☛✡ ☞✡ ☞✡ ✘✠ ✲ ✍ ✆ ☛ ✎ ✶ ✌ ✌ ❀✵ ✦ ✎✍ ✻ ✆☎ and ✎ ✼✎ ☞✆ ✲ ✍ ✆ ☛ ✎ ✌ ✣✠ ☛✡ ☞✡ ☛✡ ★✠ ✲ ✍ ✆ ☛ ✎ ✶ ✌ ✌ ✴✾ ✵ ✦ ✎✍ ✻ ✆☎ what is impossi- ble.
Let us note that the proof of Theorem 1 highlights the 3 questions to solve in order to show specification consistency. They have been noted InvCons, NonDet and Vio-lInv. The two last ones will be solved by the two algorithms given in Section 3. The first question will be tackled in Section 4.2. Let us remark that str-formula determinism is sufficient to ensure specification consistency but in no case it is necessary.

Service integration

The key question now is how to define service integration provided with an adequate semantic counterpart. A first answer might be to consider the union of axioms issued from different service specifications. However, this is not a good solution. Indeed, recall that a service is defined as possibly modifying the behaviour of the existing system on which it will be plugged on. Hence, any system obtained by the union of axioms of its different services would be lucky enough to be inconsistent. Therefore, in order to avoid to introduce inconsistencies during integration steps, choices are needed about which axioms are preserved, lost, modified and added. Hence, the integration of two services will be parameterised by choices. In this paper, we propose an interactive methodology based on algorithms introduced in Section 3 to determine these choices. These algorithms will automatically check consistency of service specifications. When inconsistencies (i.e. interactions) are detected, they are presented to an expert who makes integration choices (see Section 4 for more explanations on how this methodology is worked up).

Interactions

We have seen in the proof of Theorem 1 that the inconsistency of a service specification may be the result of: the inconsistency of invariants InvCons, or the non-determinism of some events such as specified in the service specification NonDet, or because some str-formulas question some invariants ViolInv.

The first step, that is the question of invariant consistency InvCons, boils down to a classical boolean satisfiability problem 11 . The way we reduce InvCons to the boolean satisfiability problem will be handled in Section 4.2. Below, we detail the algorithms which solve the two last questions NonDet and ViolInv.

Non-determinism

Input A finite specification ❋ ✆ ✪ ✠ ✥❑ ❏ ✄ ✬ ■❍ ☎✌ such that ❑ is consistent. A finite set of variables ✂ . Two str-formulas in ✄ ✬ ■❍ , ✧ ★ ✜ ✽✑ ✌ ✦ ☞✫ ✢✮ ✦ ✬ ✎ ✑ ✩✓ ✮ ❊✯ ✱ ✳ ✵ ✷✶ ✷✶ ✷✶ ✵ ✱ ✸ ✹ ✺ ✼✻ ✎ ✒✤ ✧✦ ✘✜ ✽ and ✧ ✗★ ✜ ✽✑ ✁ ✌ ✦ ☛✫ ✢✮ ✦ ✁ ✬ ✘✎ ✑ ✩✓ ✁ ✮ ❊✯ ✁ ✳ ✵ ✷✶ ✷✶ ✷✶ ✵ ✸ ✹ ✺ ✼✻ ✎ ✒✤ ✧✦ ✘✜ ✁ ✽ Initialisation Compute ❑ ☛☎ ✆ ✝✂ ✌ and ✚ ✆ ✞✂ ✠ ✥❑ ☛☎ ✆ ✝✂ ✌ ✌ . Note ✄ ✍ the set of states of ✚ ✆ ✝✂ ✠ ✥❑ ☛☎ ✆ ✝✂ ✌ ✌ and ✂ ✁
the whole set of endofunctions from

✂ to ✂ . ✝ ✎ ✢✬ ✄ ✍ and ❇ ✚ ✡✦ ☛❳ ✓ ✛✑ ❈✬ ✜ ✽✑ ✴✫ ✥✓ . Loop while ✝ ✎ ✾ ✂ and ❇ ✚ ✡✦ ☞❳ ✂✓ ✘✑ ❇ ❱ ✦ ✛✓ do: 1) choose ✦ in ✝ ✎ and ✝ ✎ ✬ ✝ ✎ ✴ ✟ ✦ ✙ ; 2) ✝ ✎ ✩✍ ❙✬ ✂ ✁ ; 3) Loop while ✝ ✎ ✍ ✾ ✂ and ❇ ✚ ✡✦ ☛❳ ✓ ✛✑ ❇ ❱ ✫✦ ✛✓ do: 3.1) choose ✲ in ✝ ✎ ✍ s.t. ✲ ✆ ✞ ✼✎ ✽✌ ✲ ✆ ✟☛ ✎ ✌ ( ✒ ✔ ✖ ✔ ✚
), and

✝ ✎ ✍ ✚✬ ✝ ✎ ✩✍ ✳✴ ✟ ✲ ✙ ; 3.2) if ✌ ✞ ✾ ☛ ✺✵ ✤ ✹ ☎✄ ✵ ✁ ★ ✜ ✽✑ ✹ ✠ ✲ ✆ ✞ ✼✌ ✲ ✆ ✟☛ ✍✌ then if ✌ ☞ ✵ ✤ ✹ ☎✄ ✵ ✁ ✦ ☛✫ ✢✮ ✦ ✹ ✳ ✎ ✑ ✩✓ ✹ ✠ ✘✆ ✲ ✠ ✭✦ ✔✌ ✌ ☞ then ❇ ✚
✄ ✲ ■❍ , ✧ ★ ✜ ✽✑ ✌ ✦ ☞✫ ✢✮ ✦ ✬ ✎ ✒✑ ✩✓ ✮ ❊✯ ✲✱ ✳ ✵ ✷✶ ✷✶ ✷✶ ✵ ✱ ✸ ✹ ✺ ✼✻ ✎ ✥✤ ✧✦ ✘✜ ✽ and ✧ ★ ✜ ✽✑ ✁ ✌ ✦ ☛✫ ✼✮ ✦ ✁ ✬ ✧✎ ✒✑ ✔✓ ✁ ✮ ❊✯ ✆ ✳ ✵ ✷✶ ✷✶ ✷✶ ✵ ✸ ✹ ✺ ✼✻ ✎ ✥✤ ✧✦ ★✜ ✁ ✽
, the above algorithm terminates and answers false.

Invariant preserving

Let ❋ ✆ ✪ ✠ ✭✄ ✬ ■❍ ❏ ❑ ✙✌ be a specification. Let ✂ be a set of variables which contains all variables occurring in ❋ . By definition, we have:

✌ ✁ ✵ ❑ ✠ ✌ ✦ ✵ ❑ ☞☎ ✆ ✞✂ ✌ ✣✠ ✌ ✲ ✬ ✂ ✻ ✂ ✠ ✚ ✆ ✝✂ ✠ ❊❑ ☞☎ ✆ ✝✂ ✌ ✌ ✌ ✸✷ ✵ ✹
The question ViolInv is equivalent to the following one: are invariants preserved for states in ✄ ✛✍ ✕✴ ✓❑ ☞☎ ✆ ✞✂ ✌ ? where ✄ ✛✍ is the set of states of ✚ ✆ ✝✂ ✠ ❊❑ ☛☎ ✂✆ ✞✂ ✌ ☞✌ .

When ✄ ✲ ■❍ , ❑ and ✂ are finite sets, the above problem is computable as expressed by the following algorithm:

Input A finite specification ❋ ✆ ✪ ✠ ✥❑ ❏ ✄ ✬ ■❍ ☎✌ . A finite set of variables ✂ which contains all the variables that occur in axioms of ❋ . An invariant ✧ ★ ✜ ✽✑ ❃✌ ❄ ✗✽ in ❑ . Initialisation Compute ❑ ☛☎ ✆ ✝✂ ✌ and ✚ ✆ ✞✂ ✠ ✥❑ ☛☎ ✆ ✝✂ ✌ ✌ . Note ✄ ✍ the set of states of ✚ ✆ ✝✂ ✠ ✥❑ ☛☎ ✆ ✝✂ ✌ ✌ and ✂ ✁
the whole set of endofunction from

✂ to ✂ . ✝ ✎ ✬ ✄ ✍ ✴ ❑ ☞☎ ✆ ✝✂ ✌ and ❇ ✚ ✡✦ ☞❳ ✂✓ ✘✑ ✬ ❇ ❱ ✫✦ ✛✓ . Loop while ✝ ✎ ✾ ✂ and ❇ ✚ ✡✦ ☞❳ ✂✓ ✘✑ ❇ ❱ ✦ ✛✓ do: 1) choose ✦ in ✝ ✎ and ✝ ✎ ✬ ✝ ✎ ✴ ✟ ✦ ✙ ; 2) ✝ ✎ ✩✍ ❙✬ ✂ ✁ ; 3) Loop while ✝ ✎ ✍ ✾ ✂ and ❇ ✚ ✡✦ ☛❳ ✓ ✛✑ ❇ ❱ ✫✦ ✛✓ do: 3.1) choose ✲ in ✝ ✎ ✍ and ✝ ✎ ✍ ✬ ✝ ✎ ✩✍ ✕✴ ✟ ✲ ✙ ; 3.2) if ✌ ✞ ✾ ☛ ✺✵ ★ ✜ ✽✑ , ✲ ✆ ✟✞ ✥✌ ✭✾ ✺✲ ✆ ☛ ✍✌ then ❇ ✚ ✡✦ ☛❳ ✓ ✛✑ ❈✬ ✚ ✤ ✔✜ ✆ ☞✆ ✲ ✠ ✭✦ ✛✌ ■✌ ❄ ✲✌ end of loop end of loop Output ✑ ✔✓ ✛✜ ❯✫ ✥✑ ✔✚ ✯✆ ❇ ✚ ✡✦ ☛❳ ✓ ✛✑ ✩✌ Theorem 3. ✚ ✆ ✝✂ ✠ ✥❑ ☎ ✆ ✝✂ ✌ ✌ satisfies ❑
if and only if for every invariant in ❑ , the above algorithm terminates and answers false.

Methodology and experiments

When integrating a new feature, we enter upon the problem of how to apply the algorithms and in which order, to ensure the consistency of the resulting specification.

The Design Phase Process

We have seen in Section 2.5 that to avoid introducing inconsistency during integration, choices are needed about which formulas are preserved, lost, modified or added. We propose an interactive approach based on the algorithms introduced before. Interactions are detected and presented to an expert who makes integration choices.

A service specification ❋ provides modifications with respect to an implicit system. From a formal point of view, the integration of ❋ on a system ✂ ☛ ✍✦ is a composition which is parameterised by the required choices, i.e., it is abstractly denoted by ✂ ☛ ✍✦ ✂ ☎✄ ✝✆ ✑ ✎ ✞✄ ✮ ✕✹ ❋ . It generally leads to some modifications of ✂ ☛ ✍✦ ; thus, we do not easily get the addition of two services together to a system (✂ ☛ ✍✦ ✂ ✄

✟ ☛❋ ✠ ❋ ✁ ✙
) from the addition of each of them, ✄ ✂✁ ✄ ✂ ✄ ❋ and ✄ ✂✁ ✱✄ ✄✂ ☎✄ ✁ ❋ ✁ . Indeed, it would suppose not only to confront the specifications ❋ and ❋ ✁ , but also to re-examine ★ and ★ ✁ because ★ was thought on ✂ ☛ ✍✦ and not on ✂ ☛ ✍✦ modified by ★ ✁ , and conversely. Thus our approach is to integrate services one by one. Therefore, given POTS and services ❋ ✠ ☞✡ ☛✡ ☞✡ ★✠ ❋ ✻ , we build an integration ✆ ✆✡ ☞✡ ☛✡ ✘✆

POTS ✂ ✄ ✳ ❋ ✎ ✳ ✌ ✂ ✄ ☎✄ ✝✆ ✞✆ ✟✆ ✂ ✄ ✸ ❋ ✎ ✸ ✌
, where the order

✖ ✠ ✆ ✞✆ ✟✆ ✠ ✆✖ ✻ is significant with respect to the choices ★ ✠ ✆ ✞✆ ✞✆ ✠ ★ ✻ . Note ✄ ✬☛ ✍✦ ✹ ✲ ✆ ✪ ✹ ✲ ✠ ✭✄ ✬ ■❍ ✹ ✲ ❏ ❑ ✹ ✲ ✌
the system specification resulting from

✆ ❁✡ ☞✡ ☛✡ ✘✆ ✡✠ ☞☛ ✂✄ ✟✂ ☎✄ ✳ ❋ ✎ ✳ ✌ ✂ ☎✄ ✄ ✡ ☞✡ ☛✡ ✂ ☎✄ ✍✌ ✳ ❋ ✎ ✎✌ ✑✏ ✳ ✌ and ❋ ✎ ✒✌ ✆ ✪ ✎ ✎✌ ✠ ✖✄ ✬ ■❍ ✎ ✒✌ ❏ ❑ ✣✎ ✎✌ ✛✌
. In order to determine the next choice ✂ ✄ ✌ for integrating ❋ ✎ ✒✌

, the following process is applied: . Otherwise, the process is terminating.

To ensure termination of the above process, a strategy is to impose that:

1. for every pair ✆ ✠ ✁ ✌ where and ✁ are two str-formulas satisfying conditions of Point • ✡ ❇ , if all non-determinism conflicts for with all str-formulas of ✄ ✬ ■❍ ✹ ✲ have been already handled (i.e. ✁ is a str-formula which has been added

or modified during some previous steps of the first algorithm) then the choice of the expert to solve the non-determinism conflict between and ✁ (when it exists) necessarily rests on ✁ . 2. when a consistency conflict occurs on invariants by the algorithm ViolInv, the choice of the expert necessarily rests on invariants (i.e. str-formulas of ✄ ✬ ■❍ are preserved).

Implementation

In the Valiserv project framework, the process presented in the previous section has been implemented. We have then defined a prototype to help the expert for specifying and validating service-oriented telecommunication systems. To produce more efficient implementations of algorithms, a first step of the above process has been to restrict the cardinality of the set of variables ✂ occurring in axioms of the specification under consideration. This has allowed to reduce the invariant consistency InvCons to a propositional satisfiability problem of reasonable size and to decrease the complexity of the step 3) in both algorithms NonDet and ViolInv in Section 3. The point is to translate a set of invariants into an equivalent single invariant. To achieve this purpose we first transform any axiom into its Skolem form. To simplify, let us consider an invariant of the form

✌ ✲ ✆ ✝✂ ✌ ✳ ✂ ✁ ✠ ✱ ☎ ✄ ✢ ✷ ✯ ✄ ✒ ✡ ✳ ✹ ✧✝ ✄ ✒ ✡ ✄ ✞ ✎ ✾ ☛ ✎ ✵ ❦
. The computation of an optimal substitution is done by means of systematic study of all substitutions compatible with the inequality constraints. By iterating such a variable factorisation between all invariants, we can control the whole number of variables to be considered. The boolean satisfiability problem corresponding to a formula

✌ ✂ ✠ ✱ ✆ ✄ ✢ ✄ ✒ ✡ ✞ ✼✎ ✾ ☛ ✎ ✵ ❦
is then simply given by the propositional formula

✝ ✞ ✠✟ ✁ ☛✡ ✁ ✓✵ ☞ ✴✱ ✄ ✚✢ ✄ ✒ ✡ ✥✵ ✞ ✯ ✲✱ ✝✹ ✄ ✞ ✯ ✆ ✹ ✌ ✆ ❦ ✌
where the atoms

✎ ✆ ✞ ✠ ☛✡ ☞✡ ☞✡ ★✠ ☞✞ ✻ ✌ occurring in ✌ ✆ ❦ ✌
are viewed as simple propositional variables.

Case study

The above methodology has been applied on many telecommunication examples. Among other, it has been applied on the example presented in Section 2. Here, we give the report of this case study. Its interest is it is significant enough but short enough to be presented in this paper. We incrementally integrate several services yielding the system (((POTS

✂ ☎✄ ✳ TCS) ✂ ✄ ✄ CFB) ✂ ✄ ✎✍ INTL).
The main steps have been the following:

✪ POTS ✂ ☎✄
✳ TCS: a non-determinism has been detected between ❦ ✁ and . We have modified ❦ ✁ , intuitively giving the priority to TCS on POTS. During the integration process, we have modified four of them and introduced a new one. The ValiServ tool automatically detects current interactions, presents the detected interactions to the expert under a detailed form and allows the expert to modify the related specification part so that the considered interaction is suppressed according to its judgment. Such an approach allows to manage the intrinsic complexity of serviceoriented systems since the expert only intervenes to solve interactions according to their subjective status. Thus, our service integration method may be viewed as a sequence of expert choices in a set of resolution options, each of these expert choices coming from an automatic feature interaction detection.

Related Work

Several previous works have been interested by feature integration and interaction detection issues from a high level of abstraction. In particular, new architectures have been designed for telecommunications systems in order to facilitate the addition of a new service. [START_REF] Bredereke | Maintening telephone switching software requirements[END_REF] or [START_REF] Jackson | Distributed feature composition: A virtual architecture for telecommunications services[END_REF] present such approaches, useful for designing and implementing new services but not to found rigorous interaction detection methods. [START_REF] Schätz | Service-based systems engineering : Consistent combination of services[END_REF] gives a general framework to systematically combine services together. Only consistent combinations of services are considered. When an inconsistency is detected for a given combination of services, this means that there exists an interaction between combined features. However, the paper is not concerned by the need of providing theoretical and methodological help in order to combine service in presence of interactions. Some other works, like [START_REF] Felty | Feature specification and automated conflict detection[END_REF], are also based on the use of model-checking tools in order to detect interactions. This allows to consider general temporal properties. The main drawback of all these approaches is that they require to instantiate a priori different configurations to build all the interesting subscription patterns among a small number of fixed phones.

We claim that the use of symbolic techniques for dealing with phone variables is the key to deduce interactions built over an appropriate number of phones equipped with their subscriptions. Some other works manipulate generic variables to represent phones, without restricting the number of phones to be considered. In particular, several approaches rely on STR-like specifications. [START_REF] Gammelgaard | Interaction Detection, a Logical Approach[END_REF] precisely explains the interest of using STR formulas, invariants and inequality preconditions. The authors were already concerned with providing guidelines to integrate a service on the basic call system and hints on how to perform non-determinism checks. Unfortunately, the described detections are mainly guided by hand-waving and thus, there was no study of how to systematically support this process. Our framework which is largely inspired by their process, addresses this weakness. [START_REF] Nakamura | Design and Evaluation of Efficient Algorithms for Feature Interaction Detection in Telecommunication Services[END_REF][START_REF] Tatekuwa | Automatic deleting specification errors which cause miss-detection of feature interactions[END_REF] have proposed specialised techniques for interaction detection based on STR-like specifications. From a given initial state, they analyse properties of reachability graphs in terms of non-determinism or deadlock or contradictions raised by the simultaneous application of two STR sentences . . . Works introduced in [START_REF] Yoneda | A Formal Approach for Definition and Detection of Feature Interaction[END_REF][START_REF] Yoneda | Formal approaches for detecting feature interactions, their experimental results, and application to voip[END_REF] discuss the advantage of dealing with static methods, without building any intermediate graph. They introduce techniques for finding interactions from nondeterminism criteria or from elicitation knowledge between two services. They compute a lot of interactions, but as they do not look for service integration, they do not exploit their presence to compose services in an adequate way. Moreover, as they do not use invariants, they cannot help the specifier in designing STR specifications. Let us remark that we handle the preservation of invariants as in [START_REF] Cansell | Abstraction and Refinement of Features[END_REF]. However, the underlying proofbased techniques require too much expertise to our point of view. [START_REF] Samborski | Stack Service Model[END_REF][START_REF] Guelev | Feature Integration as Substitution[END_REF][START_REF] Gaston | Algebraic Treatment of Feature-oriented Systems[END_REF] introduce systematic mechanisms of service composition avoiding a lot of interactions. Roughly speaking, all of these works are based on some precedence relations between services: the last integrated feature seems to have the highest priority level. However, if undesirable interactions subsist, then it is not possible to review the integrated system, except if a new design process is managed from the beginning.

Conclusion and perspectives

We presented a methodology for service-oriented development that takes interaction and integration issues into account. We introduced a dedicated formalism taking into account subscriptions. and manipulating two kinds of formulas, state invariants and state transition rules. We gave algorithms allowing the specifier to check the consistency of the specification under consideration. The service integration results from the incremental insertion of formulas preserving at each step the consistency of the target specification. Each detected consistency problem represents an interaction and requires an expert decision to modify, and to replace the formula(s) causing inconsistency. The whole methodology has been validating by the industrial partner France Telecom of the project ValiServ.

This work can be pursued in several ways. We want to study state reachability issues to ensure that each detected non-determinism case corresponds to a real interaction case. We also want to study how it is possible to introduce different types on variables to capture different rôles (users, phone numbers or IP addresses) in order to apply our algorithms and methodology to application domains such as voice over IP [START_REF] Jouve | An Automatic Off-Line Feature Interaction Detection Method by Static Analysis of Specifications[END_REF]. From a methodological point of view, we aim to strengthen expert assistance by minimising choices and backtrack at design step. Such improvement should rely not only on theoretical consideration but also on expertise about the telecommunication domain.

  . and are also mutually exclusive.

1 .

 1 (a) Checking the invariant consistency of ❑ ✹ ✲ ✳ ✢❑ ✣✎ ✒✌ using the algorithm ConsInv by considering one by one the invariants of ❑ ❉✎ ✎✌ (b) Solving inconsistency as soon as it occurs by modifying one of the involved invariants and starting again Point 1.a after each encountered inconsistency. This first step generates a consistent set ❑ ❉☎ ✓✌ ✑✏ ✳ ✝ ☎ ✌ , or more simply ❑ , of invariants which will be used in the reference specification for the next two following points. 2. (a) Performing the algorithm NonDet on every pair ✆ ✠ ✁ ✌ where ✵ ✄ ✬ ▲❍ ✹ ✲ and ✁ ✵ ✄ ✬ ▲❍ ▲✎ ✒✌ such that and ✁ satisfy the condition of the input part of the algorithm (i.e. the event which occurs in and ✁ is the same). (b) Solving non-determinism conflicts as soon as they occur, and starting again Point • ✡ ❇ after each one of them. This gives rise to a new set of str-formulas ✄ ✬ ■❍ . 3. (a) Performing the algorithm ViolInv on every invariant in ❑ with respect to the ✪ ✹ ✲ ✳ ✪ ✎ ✒✌ -model ✚ ✆ ✝✂ ✠ ❊❑ ☞☎ ✔✌ ✑✏ Solving inconsistency conflicts as soon as they occur. 4. Point ✕ ✡ possibly modifies both sets ✄ ✬ ■❍ and ❑ , and then gives rise to two new sets ✄ ✬ ■❍ ✍ and ❑ ✕✍ . If this is the case, then starting again the above process for ❑ ✺✍ and ✄ ✬ ■❍ ✍

  of variables occurring in ★ ✜ ✽✑ and ❦ . Obviously, such a formula can be written under its equivalent Skolem form:

.

  a non-determinism has been detected between ❦ ✟ and ✏ ✟ We have modified ❦ ✟ . We have then detected that ✏ ✟ violates the TCS invariant . We have corrected it by adding ✛ ★ ✦ ✆ ✁ ✠ ✄ ✌ to the subscription set of ✏ ✟ . Then, we add the following str-formula for the case we have ★ ✦ ✕✆ ✫✁ ✠ ✄ ✌ : ✇ ✾ ▼ ✆ ♦✞ ✹ ✶ ✸ ✿ ✠ Cfb ✒ ✹ ✽ ✿ ✕ ✾✽ ✾ ( ☞❙ ✒ ✿ ✽ ✿✓ ✼✕ ✾✽ ▲✌ ✬☛ ✔✭ ✮✎ ✑✯ ✻✭ ✮☛ ✲✱ ✚✒ ✔✓ ✼✕ ✾✽ ☛ ✔✌ ✁✎ ❀✏ ✬✒ ✹ ✕ (✽ ▲☛ ✔✌ ✁✎ ❀✏ ✬✒ ✿ ✕ ✘❁ ✚❂ ✦❃ ❅❄ ✑✤ ✦✥ ✘❆ ❇ ❈✧ ✩ ✫✪ ◗ ✾| ❏❙ ☞❚ ✱ ❵❯ ❳• ★✏ ✬✒ ✿ ✕ ✾✽ ✿☛ ✔✌ ✁✎ ❀✏ ✬✒ ✿ ✕ ❝✳ Thus, TCS has the priority on CFB and CFB has the priority on POTS. a non-determinism has been detected between ❦ and . We have modified ❦ , intuitively giving the priority to INTL on POTS, TCS and CFB. The specification of POTS, TCS, CFB and INTL together contains twenty formulas.

Notation 2

 2 Let ✪ ✁ ✆ ✄ ✬✜ ✣✠ ✖✄ ✴✮ ✔✠ ✰ ✱✌ be a signature. Let ✂

	be a set of variables. Note 1. ✄ ✜ ✆☎ ✆ ✝✂ ✶✌ ✠✟ ✎ ✆ ✞ ✠ ☛✡ ☞✡ ☞✡ ✘✠ ☞✞ ✻ ✌ ✍✌ ✎ ✒✻ ✺✵ ✄ ✬✜ ✢✳ ✺✄ ✯✮ ✩✠ ☞✞ ✏✎ ✯✵ ✑✂ ✠ ✓✒ ✕✔ ✗✖ ✘✔ ✚ ✚✙ ✄ ✜ ✆☎ ✆ ✝✂ ✌ and ✄ ✜ ✆☎ ✆ ✞✂ ✌ the two sets defined by: 2. ✄ ✜ ☎ ✆ ✝✂ ✶✌ ✠✟ ✜✛ ✎ ✆ ✞ ✠ ☛✡ ☞✡ ☞✡ ✘✠ ☞✞ ✻ ✌ ✍✌ ☞✎ ✒✻ ✺✵ ✄ ✬✜ ✢✳ ✸✄ ✴✮ ✔✠ ☞✞ ✎ ✵ ✢✂ ✠ ✘✒ ✕✔ ✗✖ ✍✔ ✚ ✚✙ Note ✄ ✯✮ ✣☎ ✆ ✝✂ ✶✌ and ✄ ✴✮ ✤☎ ✆ ✝✂ ✌ (resp. ✄ ✬✜ ✆☎ ✆ ✝✂ ✶✌ and ✄ ✲✜ ✆☎ ✆ ✝✂ ✌ ) the two subsets of ✄ ✜ ✥☎ ✆ ✝✂ ✶✌ and ✄ ✜ ✥☎ ✂✆ ✝✂ ✌ restricted to predicates in ✄ ✯✮ (resp. in ✄ ✬✜ ). be a signature. Let ✂ be a set of vari-Definition 3 (Formulas). Let ✪ ✦ ✆ ✫✄ ✲✜ ✣✠ ✖✄ ✯✮ ✔✠ ✖✰ ✱✌ ables. 1. A str-formula over ✪ is a sentence of the form ✧ ✩★ ✜ ✽✑ ✪✌ ✦ ☛✫ ✢✮ ✦ ✭✬ ✘✎ ✑ ✩✓ ✭✮ ✰✯ ✲✱ ✴✳ ✰✵ ✷ ✶ ✷ ✶ ✷ ✶ ✵ ✱ ☛✸ ✜✹ ✺ ✼✻ ✎ ✥✤ ✧✦ ★✜ ✓✽ where: -★ ✜ ✽✑ is a set of inequations ✞ ✿✾ ☛ with ✞ ✠ ☞☛ ✺✵ ✢✂ , -✦ ☛✫ ✼✮ ★✦ ✕❀ ✄ ✴✮ ✣☎ ✆ ✞✂ ✌ ✢✳ ✄ ✯✮ ✣☎ ✂✆ ✝✂ ✌ , -✎ ✑ ✩✓ ✕✠ ✟✎ ✥✤ ✧✦ ✘✜ ✍❀ ✄ ✬✜ ✆☎ ✆ ✝✂ ✌ ✢✳ ✄ ✬✜ ❁☎ ✆ ✝✂ ✶✌ are two finite sets, and -✓ ✔✻ ✵ ✰ and ✞ ✼✎ ✲✵ ✢✂ for ✒ ✭✔ ✗✖ ✘✔ ✚ . 2. An invariant over ✪ is a sentence of the form ✧ ❂★ ✜ ✽✑ ❃✌ ❄ ❅✽ where ★ ✜ ✽✑ is defined as above, and ❄ is a quantifier-free first-order formula over ✄ ✲✜ ✼✳ ✄ ✯✮

.

  and a set ✄ ✗❀ ✦✥ ✆ ✄ ✜ ☎ ✆ ✞✙ ☎✌ ☞✌ (states) equipped for every ✓ ✧✻ ✵ ✰ and every ✆ ✞✫ ✠ ☛✡ ☞✡ ☞✡ ★✠ ✆✫ ✻ ✌ ☎✵ ✦✙ ★✧ ✡ ☛✡ ☞✡ ✩✧ ✪✙

	✫ nary relation 7 ✓ ✫ ✬ ✮✭ ✯ ✻ times ✓ ✛ ✆ ✝✫ ✠ ☛✡ ☞✡ ☞✡ ✘✠ ✆✫ ✻ ✌	with a bi-✬ ✱✭ ✯ ✻ times	,
	and an interpretation ✲ ✬ ✏✂ ✻ ✙ satisfy a formula

✛ ✆ ✞✫ ✠ ☞✡ ☞✡ ☛✡ ★✠ ✥✫ ✻ ✌ ❀ ✄ ✦✧ ✄ . ✘ is deterministic if and only if for every ✓ ✧✻ ✵ ✰ and every ✆ ✝✫ ✠ ☞✡ ☛✡ ☞✡ ★✠ ✥✫ ✻ ✌ ✵ ✪✙ ★✧ ✡ ☛✡ ☞✡ ✟✧ ✰✙ is a partial function. Definition 6 (Formula satisfaction). Let ✪ ✆ ✄ ✬✜ ✣✠ ✖✄ ✯✮ ✩✠ ✰ ✱✌ be a signature. Let ✘ be a ✪ -model. A state ✦ ✵ ✄ ❄ , noted ✆ ✲ ✠ ✖✦ ✔✌ ✌ ❄ , if and only if:

  ✣✠ ☛✡ ☞✡ ☛✡ ★✠ ✲ ✆ ✟☛ ✠✶ ☎✌ ☞✌ ☞✌ ✎ ✆ ✟☛ ✠ ☛✡ ☞✡ ☛✡ ★✠ ☞☛ ✽✶ ✂✌ ✵ ✎ ✒✤ ✧✦ ✘✜ ✰✙ ✔✌ and STR are finite sets, then ✚ ✆ ✞✙ ✠ ✭✄ ✯✌ is computable. Let us consider ✪ a signature, ✂ a set of variables over ✪ and ❑

	Let us point out that when
	a set of
	invariants. Define

✂ , ✙ , ✄

  When ✪ is a finite signature and ✂ a service specification. ❋ is consistent if and only if ✚ ✆ ✞✂ ✠ ✥❑ ☛☎ ✆ ✝✂ ✌ ✌ satisfies all the axioms of ❋ . Proof. The if part is obvious. The only if part. Suppose that ❋ is consistent but ✚ ✆ ✝✂ ✠ ❊❑ ❉☎ ✆ ✝✂ ✌ ✌ does not satisfy it. Obviously, the consistency of ❋ means the consistency of ✄ ✲ ■❍ Therefore, if ✚ ✆ ✞✂ ✠ ✥❑ ☛☎ ✆ ✝✂ ✶✌ ☞✌ does not satisfy ❋ then by construction of ✚ ✆ ✞✂ ✠ ✥❑ ✴☎ ✆ ✝✂ ✌ ✌

	and Theorem 1. Let ❋ ❑ ☎ ✆ ✝✂ ✌ are computable. ✆ ✪ ✠ ✭✄ ✬ ■❍ ❏ ❑ ✙✌		and	❑ are finite sets, then ✰ ✕☎ ✆ ✝✂ ✶✌
	struction, the consistency of	❑ implies that	❑ ❉☎ ✆ ✝✂ ✌	and of is not empty. In the following, the ❑ . By con-
	question of (the verification of) the consistency of
	✲ ✬ ❲✂	✻	✂	✺ ✼✻ , ✲ ✆ ✞ ✼✌ ✭✾ ★ ✜ ✽✑ such that for every ✞ ✾ ☛ ✸✵	✎ ✒✤ ✧✦ ✘✜ ✽ ☎✵ ✄ ✬ ▲❍ ✲ ✆ ☛ ✍✌ , ✆ ✫✦ ✠ ✲ ✌ ▲✌	, ✦ ✵ ✄ ✍ ☞ , but and
	✁ ✢ ✹ ✄✂ ✆☎ ✞✹ ✞✝ ✠✟ ☛✡ ✰✮ ✲ ✆ ✞ ✌ ✣✠ ☞✡ ☛✡ ☞✡ ✠ ✲ ✆ ✞ ✻ ✌ ☞✌ ✥✦ ✎✍ ✍ . By definition, this means that there exists and 9 ✎ ✆ ☛ ✠ ☞✡ ☞✡ ☛✡ ★✠ ☛ ✠✶ ✌ ❀✵ ✎ ✒✤ ✧✦ ✘✜ there exists ✦ ✏✍ such that ✦ ✬✓ ✆✜ ✯ ✂✁ ✓✵ ☎✄ ✯ ✆✁ ✹ ✝✹ ✆ and ✎ ✆ ✲ ✆ ✟☛ ✌ ✣✠ ☞✡ ☛✡ ☞✡ ✘✠ ✲ ✆ ☛ ✠✶ ✌ ☞✌ ✜✾ ✵ ✦ ✎✍ ✧ ★ ✜ ✽✑ ✆✍ ❯✌ ✦ ☛✫ ✢✮ ✦ ✎✍ ✍✬ ✙✎ ✒✑ ✔✓ ✏✍ ✮ ❊✯ ✆✝ ✳ ✵ ✷✶ ✷✶ ✷✶ ✵ ✝ ✸ ✹ ✺ ✼✻ ✎ ✒✤ ✧✦ ✘✜ ✞✍ ✓✽ ☎✵ ✄ ✬ ▲❍ and ✲ ✍ ✬ ❙✂ ✻ ✂

be ❑ will be simply denoted by InvCons.

which relies on str-formulas, either two str-formulas with the same event lead to two incompatible states or a str-formula leads to a state violating the invariants. These two cases are denoted by respectively NonDet for non-deterministic str-formulas and Vio-lInv for the non preservation of the invariants by str-formulas. Then, let us prove that both NonDet and ViolInv lead to a contradiction. 1. NonDet there exists 8 ✧ ★ ✜ ✽✑ ❃✌ ✦ ☛✫ ✼✮ ★✦ ✬ ✛✎ ✒✑ ✩✓ ✮ ❊✯ ✲✱ ✜✳ ❊✵ ✷✶ ✷✶ ✷✶ ✵ ✱ ☛✸ ✜✹

2 .

 2 ViolInv there exists ✦ ✎✍ ✡✵ ✄ ✍ ✕✴ ✓❑ ☞☎ ✆ ✞✂ ✌ 10 , an invariant ✧ ✩★ ✜ ✽✑ ✪✌ ❄ ✽

	and an interpreta-but ✆ ✫✦ ✏✍ ✠ ✲ ✌ ✜✾ ✌ ❄ . str-formulas ✧ ★ ✜ ✽✑ ❉✎ ❊✌ ✦ ☛✫ ✼✮ ★✦ ☛✎ ✚✬ ✺✲ ✆ ✟☛ ✌ ✲ ✆ ✞ ✼✌ ✾ By definition, this means that there exists ✦ ☎✵ ❑ ❉☎ ✆ ✝✂ ✌ tion ✲ ✬ ✂ ✻ ✂ such that for every ✞ ✿✾ ☛ ✵ ★ ✜ ✽✑ , ✚

  ✡✦ ☞❳ ✂✓ ✘✑ ✬ ✜ ✽✑ ✴✫ ✥✓

		;
	end of loop
	end of loop Output ✑ ✔✓ ✛✜ ❯✫ ✥✑ ✔✚ ✯✆	❇ ✚ ✡✦ ☛❳ ✓ ✛✑ ✩✌
	Theorem 2. Let ❋ and ❑ and ✄ ✬ ■❍ are finite sets. Let ✆ ✪ ✠ ✥❑ ✓❏ ✄ ✲ ■❍ ☎✌ ✂ be a specification where ✪ is a finite signature, be a finite set of variables which contains all variables occurring in ❑ ❏ ✄ ✬ ■❍ . Then, ✚ ✆ ✝✂ ✠ ❊❑ ☎ ✆ ✞✂ ✌ ☞✌ is deterministic if and only if
	for every pair of str-formulas in

the acronym of which means "Validation de Services".

In the following, we will indifferently use the two words feature and service although we are aware of that services also represent more particularly the notion of components such as web services.

which will not be presented in the paper in order not to make heavy the presentation. The interested readers can find them in[START_REF] Berkani | An Environment for Interaction Service Specification[END_REF][START_REF] Gammelgaard | Interaction Detection, a Logical Approach[END_REF].

✾ ❀✿ ✝❁ is an usual acronym for the Terminating Call Screening.

❁ ✾ is the set of state of ☛ ✒ ✌☞ ✽ ☎✍ ✎ ✒ ✌☞ ✕ ▲✕ .

The boolean satisfiability problem is solved by SAT solvers, e.g. GRASP[START_REF] Marques-Silva | GRASP: A search algorithm for propositional satisfiability[END_REF] and Chaff[START_REF] Moskewicz | Chaff : Engineering an efficient SAT solver[END_REF].


Vladyslav V Lisnyak
email: vladyslavv.lisnyaklisnyak@univ.kiev.ua

Alexander N Zaderk

Ruslan Mariychuk
email: ruslan.mariychuk@unipo.sk

Volodymyr Lysenko
email: vladimir.lysenko@univ-lyon1.fr

Olga Yu Boldyrieva
email: olgayu.boldyrievaob@univ.kiev.ua

Valeriy A Skryshevsky
email: skryshevsky@gmail.com

Gauhar Mussabek
email: gauhar.musabek@kaznu.kzyerzhantaurbayevtaurbayev@taur.kaznu.kz

Yerzhan Taurbayev
email: taurbayev@mail.ru

Nazym Zhylkybayeva

• Oksana

Yu Tananiko
email: otananaiko@gmail.com

Alexander N Zaderko

Oksana Yu Tananiko

Preparation and characterization of F-, O-, and N-containing carbon nanoparticles for pH sensing

Keywords: F-,O-, and N-containing carbon NPs, Solvothermal synthesis, Photoluminescence, pH nanosensors

A novel sensing system was designed for pH measurements based on the enhanced and quenched photoluminescence (PL) and UV-Vis absorption of the diluted water solutions of F-, O-, and N-containing carbon nanoparticles (FON-CNPs). These FON-CNPs were solvothermally synthesized, dissolved, ultra-iltrated, and separated by thin-layer chromatography. The total luorine content in them was found to be 1.2-1.5 mmol per gram. Their TGA showed a total weight loss of 52.7% because of the thermal decomposition and detachment of the surface groups and the partial burning of the functionalized shell on the carbon core at temperatures below 1200 °C. TEM and Raman data conirmed the presence of graphitic structures in the carbon core. From the results of ATR FTIR and UV-Vis spectroscopies, we showed that a carbon shell incorporates diferent functional groups covering the carbon core. The surface groups of the carbon shell include carboxyl, phenolic, and carbonyl groups. Heterocyclic N-containing and amino groups and triluoromethyl groups supporting the hydrophobicity were also found. We suggested the possible reasons for the pH responses obtained with the sensing system considering them dependent on the de-protonation of functional groups with pH change.

U N C O R R E C T E D P R O O F 1 3

Introduction

Carbon nanoparticles (CNPs), including carbon dots (CDs), are of special attention in a broad range of applications because of their tunable optical properties and excellent biocompatibility [START_REF] Xia | Evolution and synthesis of carbon dots: from carbon dots to carbonized polymer dots[END_REF][START_REF] Sun | Ultralong lifetime and eicient room temperature phosphorescent carbon dots through multiconinement structure design[END_REF][START_REF] Nevar | Carbon nanodots with tunable luminescence properties synthesized by electrical discharge in octane[END_REF][START_REF] Tarasenka | Structure and optical properties of carbon nanoparticles generated by laser treatment of graphite in liquids[END_REF][START_REF] Zuo | Fluorine-doped cationic carbon dots for eicient gene delivery[END_REF][START_REF] Pal | Recent advances in crystalline carbon dots for superior application potential[END_REF]). These green and nontoxic carbonic nanomaterials were used as the luorophores and absorbers. In case of an increase in the spectral overlap between absorbing species and luorophore, one can see a decrease in luorescence/photoluminescence intensity of NPs. This decrease is considered as a response and enables quantitative measurement of the adsorbents. Today, numerous publications are devoted to the application of CNPs as selective photoluminescence on-of-on probes [START_REF] De León | Tuning the luminescence of nitrogen-doped graphene quantum dots synthesized by pulsed laser ablation in liquid and their use as a selective photoluminescence on-off-on probe for ascorbic acid detection[END_REF][START_REF] Feng | A novel application of luorine doped carbon dots combining vortex-assisted liquid-liquid microextraction for determination of 4-nitrophenol with spectroluorimetric method[END_REF][START_REF] Zan | One-step synthesis of green emission carbon dots for selective and sensitive detection of nitrite ions and cellular imaging application[END_REF][START_REF] Wang | Synthesis of N-doped carbon dots and application in vanillin detection based on collisional quenching[END_REF]).

On the other hand, many semiconductors showed the photoluminescence (PL) intensity and decay lifetime strongly dependent on the value of pH. This pH dependence, in the case of porous Si, is explained by competition between UV-induced hydrogen efusion, hydrogen adsorption from the bufer solution, and surface oxidation. Within the phenomenon, pH sensors were already proposed [START_REF] Benilov | Inluence of pH solution on photoluminescence of porous silicon[END_REF]). Besides, when diferent luminescent NPs are storage in the porous Si and nanosilicas, they can be used as speciic probe units in multicomponent sensors [START_REF] Serdiuk | Storage of luminescent nanoparticles in porous silicon: toward a solid state "golden fleece[END_REF][START_REF] He | Anchoring carbon nanodots onto nanosilica for phosphorescence enhancement and delayed luorescence nascence in solid and liquid states[END_REF].

Despite a wide variety of CNPs, the luorine and nitrogencontaining CNPs have rarely been used as efective pH sensors [START_REF] Long | Self-protective room-temperature phosphorescence of luorine and nitrogen codoped carbon dots[END_REF][START_REF] Su | Eicient room temperature phosphorescence carbon dots: Information encryption and dual-channel pH sensing[END_REF]) and for other application until nowadays [START_REF] Sim | The synergistic efect of nitrogen and luorine co-doping in graphene quantum dot catalysts for full water splitting and supercapacitor[END_REF][START_REF] Wang | Synthesis of N-doped carbon dots and application in vanillin detection based on collisional quenching[END_REF][START_REF] Liu | Electrochemical sensor based on F, N-doped carbon dots decorated laccase for detection of catechol[END_REF][START_REF] Jiang | Photoactivated luorescence enhancement in F, N-doped carbon dots with piezochromic behavior[END_REF].

In this work, we report on new luorine-, oxygen-, and nitrogen-containing carbon nanoparticles (FON-CNP). They were obtained by a one-stage solvothermal method from citric acid, urea, and 3-(triluoromethyl) aniline. The latter was applied as a source of luorine and nitrogen. Here, citric acid and urea were pyrolyzed to form the carbon matrix. The resulting FON-CNPs have excellent water solubility and bright PL in aqueous solutions. Remarkably, the PL intensity and UV absorption of FON-CNP showed pH-dependent responses. The PL intensity maintains certain stability over a wide pH range of 1.0-11, showing good reversibility. Based on the pH-dependent behavior of FON-CNPs, one can create a sensor system for accurate pH measurements. Pharmaceutical-grade anhydrous citric acid and pro-analysis quality urea were supplied by LLC Himlaborreaktiv (Brovary, Ukraine). LLC Himlaborreaktiv solvents, acids, bases, and reagents in the present study were of analytical purity and were used as received. For dilution, Millipore deionized water was used in the experiments. Phosphate-bufered (PB) solutions of diferent pH levels were prepared by titrating 0.01 mol L -1 phosphoric acid solution with 1 M NaOH solution to the required pH values. The preparation was carried out under control with a pH electrode (InLab Routine Pro, Mettler Toledo).

Experimental

Synthesis of FON-CNPs

The samples of FON-CNPs were synthesized by the solvothermal method [START_REF] Zaderko | The process for obtaining of luoralkylated carbon quantum dots[END_REF]. In a typical synthesis procedure, we had composed a mixture of 10 g of urea (0.167 mol), 16 g of anhydrous citric acid (0.083 mol), and 3.35 g of 3-(triluoromethyl) aniline (0.021 mol). The mixture was placed in a glass reactor and left it open. The reactor with the mixture within was placed in an electric oven, which was heated from 25 to 135 °C for 30 min, and held at this temperature for the next 30 min to get a yellow melt from the stored mixture. After that, the reactor temperature was increased from 135 to 165 °C for 10-13 min. After 2 h of heat treatment at this temperature, the melt was transformed into a dark brown shining solid. 75 ml of an ethanol/ water solution (50/50) was added to the reactor after the synthesis to dissolve the solid. The resulting dark brown solution was then iltered through Whatman ilter paper and acidiied by adding 20 ml of concentrated HCl. When HCl was added, FON-CNP locks began to form in the solution. After holding for an hour, the precipitate was separated by vacuum iltration, and the resulting brownish powder was dried in the air.

Instrumentation

Fourier-transform infrared attenuation total reflectance (FTIR ATR) spectra were collected on a Shimadzu IRPrestige 21 instrument. A MIRacle module (Pike Technology), with a ZnSe crystal plate for the sample contact, was used during FTIR ATR measurements. Transmission electron microscopy (TEM) images were captured on an electronic microscope (Jeol JEM-2100F, 200 kV). Energy-dispersive X-ray (EDX) analysis of TEM imaged samples was carried out on an AZtec X-MAX energy-dispersion spectrometer from Oxford Instruments. Ultraviolet-visible (UV-vis) absorption spectra were recorded by a UV-vis spectrophotometer (Varian Cary 50) at an UV-Vis scan rate of 600 nm min -1 . PL spectra of the solutions of FON-CNPs were measured at 20 °C on the Agilent Cary Eclipse luorescence spectrophotometer (Xe lash lamp). Applied Nanoscience

1 3

Thermogravimetric analysis (TGA) of dried samples was carried out in an argon gas low with a custom instrument reported elsewhere [START_REF] Tsapyuk | Efect of ultrasonic treatment on the thermal oxidation of detonation nanodiamonds[END_REF]. Measurements of the total luoride content (C F ) were done in an aqueous solution prepared by pyrolytic decomposition of samples [START_REF] Zaderko | Fluoroalkylated nanoporous carbons: testing as a supercapacitor electrode[END_REF]. The Mettler Toledo (SevenExcel-lence™) pH meter was used to measure pH levels with maximum measurement accuracy. Raman spectrum of FON-CNPs was collected in backscattered mode with a HORIBA Jobin Yvon-LabRAM ARA-MIS integrated confocal micro-Raman system equipped with a microscope (BX41, Olympus, Japan) and a diode-pumped solid-state laser. A 633 nm laser was focused by an Olympus 100 × objective lens (UPLSAPO, NA = 0.95) on the sample placed in an open-air environment at room temperature. The excited Raman scattering signal was collected by a Labram ARAMIS (Jobin-Yvon) spectrometer.

Results and discussion

EDX analysis conirms the presence of luorine, oxygen, carbon, and nitrogen in the FON-CNPs. According to the chemical analysis, the luorine content C F equals 1.2-1.5 mmol per gram. Figure 1a shows the formation of polydisperse agglomerates of monodisperse primary particles. Although the pseudo-spherical NPs are showed a wide range of size distribution, from 25 to 80 nm, the mean agglomerate diameter is about 55 ± 5 nm. The SAED pattern conirms the amorphous structure of the prepared agglomerated NPs (Fig. 1b).

The alcohol-water solutions of FON-CNPs (3 ml, 46 g of dry FON-CNPs/L in 37 wt/v% alcohol solution diluted with 2 mL of water) were subjected to ultrailtration. Giving a brown solution, the ultra-iltration with 10 kDa membrane centrifugal ilters showed that the FON-CNPs could be completely iltered for 3 h at 5500 g. To prepare the solution of FON-CNPs of the smallest molecular weight range, the prepared ultra-iltrate was diluted three times with water and iltered in sequence with centrifugal ilters from Vivaspin and Microsep Omega, equipped with membranes with molecular weight cut-ofs of 5 and 1 kDa, at 5000 g. The iltrates of 0.03 mass% solutions of FON-CNPs after iltering with a 1 kDa membrane showed yellow and white luminescence under 254 nm and 365 nm excitations, respectively (Fig. 1d). This conirms a bimodal luminescence nature in the alcohol-water solutions of FON-CNPs similar to that observed by [START_REF] Yang | Nitrogen/sulfur Codoping strategy to synthesis green-yellow emitting carbon dots derived from xylose: toward application in pH sensing[END_REF] for green-yellow emitting CDs derived from xylose and applied in the pH sensing.

After ultrailtration, the resulting yellow solution to be used in subsequent experiments was subjected to thin-layer chromatography (TLC) with a silica layer (6 nm silica, 15 mkm). On the TLC plate after chromatographing, one can see two components, which exhibit blue and yellow luminescence under UV light (see insert in Fig. 1c).

FTIR ATR spectrum (Fig. 2a) of FON-CNPs was registered for the sample, which was dried on a Parailm™ M substrate. This spectrum conirmed the formation of diferent functional groups forming a shell on the surface. For all benzene derivatives containing CF 3 groups, an asymmetric C-F stretching vibration at 1330 cm -1 appears with very strong intensity [START_REF] Yadav | Vibrational spectra and normal coordinate analysis for substituted triluoromethyl benzenes[END_REF]. A band at 1553 cm -1 (C=N) and bands at 1611 and 1666 cm -1 (C=C) can be assigned to stretching vibrations in the aromatic rings of the carbon (N) skeleton [START_REF] Rap | Stable isomeric structures of the pyridine cation (C 5 H 5 N• + ) and protonated pyridine (C 5 H 5 NH + ) elucidated by cold ion infrared spectroscopy[END_REF]. According to [START_REF] Singh | Vibrational studies of triluoromethyl benzene derivatives 1: 2-amino, 5-chloro and 2-amino. 5-bromo benzotriluorides[END_REF], three mid-intensity bands peaked at 697 cm -1 , 797 cm -1 , and 890 cm -1 are due to the C-C-C inplane bending mode, the symmetric C-F stretching vibration in the CF 3 group that mixed with the ring-breathing mode vibrations, and the out-of-plane C-H bending vibrations, correspondingly.

A band at 1128 cm -1 could be assigned to the N-H and C-H stretching vibrations. Unless otherwise stated, here and below the group frequencies are assigned according to [START_REF] Socrates | Infrared characteristic group frequencies[END_REF] and [START_REF] Coates | Interpretation of infrared spectra a practical approach[END_REF]. Some spectral features are consistent with the formation of oxygen-containing groups. Two peaks centered at 1708 cm -1 and 1666 cm -1 are from C=O stretching vibrations of carbonyl groups [START_REF] Bellamy | Carbonyl Frequencies[END_REF]. A band at 1449 cm -1 corresponds to the C-N stretching vibrations or the overlapping bands assigned to the CH 2 scissoring and C-O-H bending vibrations. Applied Nanoscience 1 3

The complex of spectral bands observed between 1500 and 1800 cm -1 includes the contribution of the NH 2 and CHN bending vibrations and that of CNH stretching vibrations. According to [START_REF] Larkin | Infrared and Raman spectroscopy principles and spectral interpretation[END_REF], the quadrant ring and semi-circle stretching vibrations in heterocycles absorb in this spectral region. Broadband absorption in the region of 1000-1320 cm -1 covers the whole range of frequencies in which the C-OH, C-C, C-N, and C-O stretching vibrations are registered. A peak at 1071 cm -1 is from C-O stretching vibrations, and it can contain the isopropanol contribution (Coblentz Soc., Inc. 2018). While the broadband at 3200-3600 cm -1 could be assigned to the O-H stretching vibrations overlapped with N-H vibrational frequencies in aromatic and heterocyclic groups, and those of imino groups [START_REF] Lin | Pyridine vs. N-Hydrogenated pyridine moieties: theoretical study of stability and spectroscopy of nitrogen-contained heterocyclic aromatic compounds and graphene nanolakes[END_REF]). The reversed Christiansen peaks at 2916 cm -1 and 2846 cm -1 are attributed to asymmetrical and symmetrical stretching vibrations of -CH 2 . These peaks are from isopropanol solvent [START_REF] Shahravan | Controlled manipulation of wetting characteristics of nanoparticles with dry-based plasma polymerization method[END_REF] and Parailm™ M substrate. According to [START_REF] Kaufman | FT-IR study of CO 2 adsorption in a dynamic copper (II) benzoate-pyrazine host with CO 2 -CO 2 interactions in the adsorbed state[END_REF], three bands at 2312 cm -1 , 2345 cm -1 , and 2376 cm -1 are from adsorbed CO 2 surface species. Broadband with a peak at 3564 cm -1 could also include the contribution from defects forming hydroxyl and from isopropanol conformers (Coblentz Soc., Inc. 2018). In the highest wavenumber region, presumably, a peak at 3730 cm -1 could be assigned to free hydroxyl ions or the hydroxyl coverage of FON-CNPs. Besides, according to [START_REF] Larkin | Infrared and Raman spectroscopy principles and spectral interpretation[END_REF], the combination band deriving from the bands involving the CO 2 in-phase stretching and out-of-phase stretch could be observed as two doublets in the 3730-3500 cm -1 range. Presumably, the reason for increasing the PL eiciency is the constitutional and shell nitrogen-containing groups.

Figure 2b shows the Raman spectrum of the sample, where the D, G, and D′ bands are seen. In the present study, the width of the D band is very wide, relecting the wide distribution of crystallite sizes. One should note that the ratio I D /I G equals 0.98, so by Cancado's general formula (Cancado et al. 2006), which allows the determination of the crystallite size L a by Raman spectroscopy, the L a value of 39.3 nm was calculated. A Raman peak at 1569 cm -1 , which is assigned to the G band of graphitic structures, can overlap with the abundant Raman bands, those vibrations most likely assigned to the bending -OH vibrations, deformation N-H vibrations, ring C=C vibrations, and C=O and C-N stretching vibrations [START_REF] Lin-Vien | The handbook of infrared and Raman characteristic frequencies of organic molecules[END_REF][START_REF] Mochalin | Contribution of functional groups to the Raman spectrum of nanodiamond[END_REF][START_REF] Mermoux | Surface modiications of detonation nanodiamonds probed by multiwavelength Raman spectroscopy[END_REF][START_REF] Tarasenka | Structure and optical properties of carbon nanoparticles generated by laser treatment of graphite in liquids[END_REF]. The resulting broad asymmetric peak showed a low signal-to-noise ratio. In fact, the reason for this observation is rather strong luorescence, which agrees with the results of PL studies on nanocolloids. An analysis of the Raman spectrum shows a typical feature of nanostructured materials, which is the redshift of the D band, by 50 cm -1 , as compared with the literature data [START_REF] Smith | UV and VIS Raman spectra of natural lonsdaleites: towards a recognised standard[END_REF].

According to TGA data (Fig. 2c), the FON-CNPs are stable below 200 °C, and the total weight loss of 52.7% is because of the thermal decomposition and detachment of the surface groups and the partial burning of the carbon shell. The content of physisorbed molecules, which are desorbed below 140 °C, is negligible, only 0.4%. The diferential thermal gravimetric (DTG) curve revealed three main weight loss peaks at 365 °C, 533 °C, and 1096 °C. Here, the efect at 533 °C has a complex nature, and one can see the shoulder on the DTG curve between 650 °C and 800 °C. Actually, the Applied Nanoscience 1 3

irst and second weight loss efects are diicult to separate precisely. If they are separated by the temperature corresponding to the smallest weight change (of about 476 °C), the efect peaked at 365 °C will give 19.6% weight loss, while the efect at 533 °C-23.3% weight loss. The third efect at 1096 °C corresponds to 9.4% weight loss. From the above consideration, the schematic of the synthesis and the suggested products are depicted in Fig. 3. At the irst stage of the synthesis, aniline reacts with urea and citric acid, as a result, thermolysis products are formed and water is split of (Fig. 3a). It is likely that heterocyclic nitrogen-containing compounds are formed due to thermolytic condensation when citric acid reacts with urea (Fig. 3b). At a further stage, thermolysis products can participate in the construction of a growing carbon particle, enriching it with nitrogen atoms and triluoromethyl groups.

**The aqueous solution of the FON-CNPs is yellowish and transparent under sunlight illumination. Figure . 4a shows two speciic absorption peaks at 246 and 350 nm (Fig. 4a), attributed to the π-π* (aromatic C=C) and n-π* (the C=O bond) transitions according to [START_REF] Wang | Excitation wavelength independent visible color emission of carbon dots[END_REF]. Furthermore, according to [START_REF] Shen | The production of pH-sensitive photoluminescent carbon nanoparticles by the carbonization of polyethylenimine and their use for bioimaging[END_REF], [START_REF] Xiang | Synthesis of carbon dots with multiple color emission by controlled graphitization and surface functionalization[END_REF][START_REF] Ding | Full-color light-emitting carbon dots with a surface-state-controlled luminescence mechanism[END_REF], the observed short-and longwavelength absorption bands, at ca. 277 nm and at 435 nm and ca. 511 nm, can be attributed to the π → π* (aromatic C=C) and n → π* (C-N) transitions of nitrogen-containing groups in the FON-CNPs, respectively. To consider the efect of constitutional (structural heterocyclic) nitrogen and the active surface functional groups, we examined the response of FON-CNPs to various pH conditions in the PB bufer with variable pH values (Fig. 4b). At a wavelength of 212 nm, the FON-CNPs have a good response The prepared FON-CNPs in solutions showed high tolerance to possible changes in the ionic strength. In fact, the PL intensity showed good stability in solutions with up to 1.0 mol L -1 NaCl. These solutions have good resistance to photobleaching, and the PL intensity remains constant under continuous irradiation for 2 h. We suggest that FON-CNPs can ind potential applications in bio-labeling/bio-imaging. Moreover, the hydrogen bonds of the shell and steric protection of C-F bonds reduce photoluminescence quenching at room temperature.

On the other hand, the PL features of the prepared FON-CNPs are highly pH-dependent (Fig. 5). This observation indicates that PL species in the FON-CNPs should have basic/acidic sites taking part in reversible protonation and responsible for the PL intensity variation. We assume that the pH level increasing caused the negative surface charging; the de-protonation can dissociate hydrogen bonds. It will be a reason for the dissociation of both amide groups and carboxylic groups, in the background of possible deprotonating of nitrogen-containing groups [START_REF] Long | Self-protective room-temperature phosphorescence of luorine and nitrogen codoped carbon dots[END_REF].

As shown in Fig. 4, as pH increased from 3.0 to 10.0, a gradient increase of the PL intensity of FON-CNPs centered at 510-525 nm can be seen. This increase of the PL intensity remained relatively steady in the 9.0-10.0 pH range (Fig. 5a-e). However, the PL signal peak is slightly redshifted from 510 to 525 nm when the pH values increased from 3.0 to 11.0. The speciic features, the blue shift to 475 nm and the PL signal quenching was registered when pH values in the colloid solutions increased from 10.0 to 12.0 (see Fig. 5e-g). As can be seen from Fig. 5, the prepared FON-CNPs could be sensitive pH indicators due to their pH-dependent PL intensity. Additionally, there is a good linear relationship between the PL intensity and the pH of solutions in the range of 3.0-9.0, the relationship between the PL intensity and pH values was itted as a linear equation of PL(a.u.) = (16.76 ± 2.2)[pH] + 769.0 ± 20 with R 2 = 0.99. But the PL response deviates from linearity in the higher and lower ranges.

An alternative view on the pH-sensing mechanism could be formulated considering the chemistry of FON-CNPs. If judging by the TG data, the prepared FON-CNPs are rich in carboxyl groups and other oxygen functionality (phenolic and carbonyl groups).

With an increase in pH, the carboxyl groups are irst deprotonated. This de-protonation can increase the luminescence with the concentration of ionized particles in the solution. At high basic pH levels, we observe some quenching of luminescence. One can explain this observation by the ionization of the carbonyl functional group. The latter is typical for dyes at such high pH values. Apparently, the ionization of the carbonyl groups leads to the destruction of conjugated systems inside the matrix and, accordingly, results in the quenching of the PL signal.

Conclusion

The core-shell FON-CNPs prepared using triluoromethylated derivatives were found to be excellent PL probes for pH measurements. We consider possible reasons for the pHsensitive PL enhancement and PL subsequent quenching in the solutions of FON-CNPs. It has been demonstrated that the FON-CNPs have a good linearity range in the detection of pH levels. The reported sensing system based on the PL response of FON-CNPs shows many advantages, including rapid detection, high sensitivity, and medium-low production costs of the probe FON-CNPs. Potentially, as high

Materials 3 -

 3 (Triluoromethyl)aniline (> 99%, CAS#98-16-8) provided by Merck was used for the preparation of the FON-CNPs.

Fig. 1 a

 1 Fig. 1 a TEM image and b SEAD pattern of FON-CNPs agglomerated with HCl, c Suggested structure of NPs, d Photographs of FON-CNPs after 10 and 1 kDa iltering under 254 nm and 365 nm UV light (from left to right), Insert in c Completed chromatograms of FON-CNPs dissolved in 2:1 isopropanol-water solution on TLC plates photographed under UV lamp excitation

Fig. 2

 2 Fig. 2 Spectra a FTIR ATR and b Raman, and c TG analysis of FON-CNPs

Fig. 3

 3 Fig. 3 Schematic illustration of FON-CNPs synthesis a thermolysis and b thermolytic condensation

Fig. 4 aFig. 5

 45 Fig. 4 a UV-Vis spectrum of FON-CNPs in water solution (0.03 mass%) and b pH-dependent response of FON-CNPs in diferent pHs (from top to bottom)

  73, and h 12.03

	361 362 363 364 365 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 4 11 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 366 376 432

Author Proof

Acknowledgements G.K. Mussabek, Y.T. Taurbayev, and V.V. Lisnyak acknowledge the support of Grant No AP08856579 of the Ministry of Education and Science of the Republic of Kazakhstan. G.K. Mussabek is grateful to Al-Farabi Kazakh National University for a Scholarship in the Postdoctoral Fellowship program. A.N. Zaderko and V.A. Skryshevsky recognize a support from the Ministry of Education and Science of Ukraine, Grant No 0119U100326. A.N. Zaderko is also thankful for the scholarship of the National Scholarship Programme of the Slovak Republic, Grant No 32492. This work was partially supported by EU Horizon 2020 Research and Innovation Staf Exchange Programme (RISE) under Marie Skłodowska-Curie Action (project 101008159 "UNAT").


Hongxin Ge

Nicolas Bibent

Kavita Kumar

Laetitia Dubau

Frédéric Maillard

Sandrine Berthon-Fabry
email: sandrine.berthon-fabry@mines-paristech.fr

Fe-N-Carbon aerogel catalyst for oxygen reduction reaction

Proton exchange membrane fuel cell (PEMFC)s are an excellent energy conversion device for wide application of hydrogen, especially for portable or transportation applications. To reduce the total cost of these devices, non-precious-metal catalysts (NPMCs) have shown promises in replacing platinum-based catalysts. Among NPMCs, iron-nitrogen-carbon (Fe-N-C) catalysts subclass are the most mature. These catalysts are based on nitrogen (N) coordinated iron (Fe) ions embedded in a carbon (C) matrix acting as catalytically active centers. Numerous studies have focused on promoting their catalytic performance towards the oxygen reduction reaction (ORR). Nevertheless, such materials remain less performant than carbon-supported platinum nanoparticles (Pt/C), leading to ca. 3-10 times thicker cathodes, and associated mass transport limitations.

Carbon aerogels are ideal candidates to synthesize Fe-N-C catalysts with tuneable mass transport properties thanks to their tridimensional open texture, tailored pore size distribution from micro to macropores and their good electrical conductivity. Herein, we show the promises of Fe-N-C aerogels synthesized a "one pot" sol-gel method comprising formation of a Fe-doped resorcinol (R)-formaldehyde (F)-melamine (M) hydrogel, and followed by carbon dioxide (CO2) supercritical drying, and high temperature pyrolysis under N2 and NH3 atmosphere. By introducing ligands in the synthesis mixture, we modified the chemical environment of the Fe precursor. The resulting changes in morphology, ORR activity and mass transport properties are investigated a rotating disk electrode (RDE) set-up and a PEMFC device.

Introduction

Proton exchange membrane fuel cell (PEMFC) is a promising device for wide application of hydrogen, especially for portable and transportation applications. In a PEMFC, hydrogen is oxidized at the anode, and oxygen is reduced into water at the cathode. Due to sluggish oxygen reduction reaction (ORR) kinetics, large quantity of catalyst is necessary at the cathode to enhance the efficiency of the device. Currently, carbon-supported platinum (Pt)based nanoparticles is the most state of art catalyst, but Pt is an expensive and rare element, which constrains the commercialization of PEMFCs. To reduce the cost of these devices, the demand of developing alternative non-precious-metal catalysts (NPMCs) becomes urgent, and investigations to replace Pt-based catalysts are carried out. Among them, ironnitrogen-carbon (Fe-N-C) catalysts subclass is the most promising.

Scientific Approach

Numerous studies have focused on promoting the catalytic performance and exploring the ORR mechanism of Fe-N-C catalysts. [START_REF] Tian | Optimized synthesis of Fe/N/C cathode catalysts for PEM fuel cells: a matter of iron-ligand coordination strength[END_REF]- [START_REF] Jaouen | Average turn-over frequency of O2 electro-reduction for Fe/N/C and Co/N/C catalysts in PEFCs[END_REF] These are usually synthesized through pyrolysis of Fe, N and C precursors at high temperature. Such high-temperature treatment leads to a wide variety of moieties, which can be divided in two main categories: (i) the Fefree moieties and (ii) the Fe-containing moieties. [START_REF] Guo | Active sites of nitrogen-doped carbon materials for oxygen reduction reaction clarified using model catalysts[END_REF]- [START_REF] Yang | Carbon-based metal-free ORR electrocatalysts for fuel cells: past, present, and future[END_REF] Using extended X-ray absorption fine structure and 57 Fe Mӧssbauer spectroscopy, Zitolo et al. revealed that the enhancement of the ORR activity is directly related to the existence of porphyrin-like FeN4C12 moieties. [START_REF] Zitolo | Identification of catalytic sites in cobalt-nitrogen-carbon materials for the oxygen reduction reaction[END_REF] Many attempts have been made to increase the density of these active sites. Pyrolysis under NH3 revealed best adapted, because NH3 etches the most disordered regions of the carbon matrix during pyrolysis, leading to the formation of micropores-hosted Fe-Nx sites. [START_REF] Jaouen | Heat-treated Fe/N/C catalysts for O2 electroreduction: are active sites hosted in micropores?[END_REF] Fe-N-C catalysts with enhanced ORR activities were also prepared by using precursors with preexisting Fe-N coordination (Fe-phthalocyanine or Fe-phenanthroline complexes), instead of separate Fe and N precursors. [START_REF] Li | The challenge of achieving a high density of Fe-based active sites in a highly graphitic carbon matrix[END_REF] Despite these efforts, Fe-N-C catalysts remain still less efficient than Pt/C, and the activity difference must be offset with ca. 3-10 times thicker PEMFC cathodes. [START_REF] Jaouen | Oxygen reduction activities compared in rotating-disk electrode and proton exchange membrane fuel cells for highly active FeNC catalysts[END_REF] Also, mass transport limitations become a concern in PEMFC devices, and need to be optimized. Large mesopore and macropore volumes are required to ensure optimal Fickian diffusion of O2 and ORR product (H2O). [START_REF] Proietti | Iron-based cathode catalyst with enhanced power density in polymer electrolyte membrane fuel cells[END_REF] The ideal texture of Fe-N-C materials should thus combine micropores (hosting the active sites) and mesopores/macropores (allowing Fickian diffusion of O2 and H2O).

Due to their high specific surface area and tuneable pore size distribution (at micro, meso and macro scales), carbon aerogels are ideal candidates to synthesize highly performant Fe-N-C catalysts. Carbon aerogels are commonly prepared by pyrolysing an organic aerogel of resorcinol (R) and formaldehyde (F). [START_REF] Elkhatat | Advances in tailoring resorcinol-formaldehyde organic and carbon gels[END_REF]- [START_REF] Al-Muhtaseb | Preparation and properties of resorcinol-formaldehyde organic and carbon gels[END_REF] As for traditional Fe-N-C catalysts, N can be introduced by adding melamine (M) during the polymerization process. [START_REF] Nagy | Nitrogen doped mesoporous carbon aerogels and implications for electrocatalytic oxygen reduction reactions[END_REF]- [START_REF] Brun | Original design of nitrogendoped carbon aerogels from sustainable precursors: application as metal-free oxygen reduction catalysts[END_REF] The Fe, N-doped carbon aerogel is promising to present both high ORR activity and mass transport properties. Nagy et al. demonstrated that N-doped carbon aerogels without metal could perform high specific surface area, [START_REF] Nagy | Nitrogen doped mesoporous carbon aerogels and implications for electrocatalytic oxygen reduction reactions[END_REF], [START_REF] Nagy | Synergism of nitrogen and reduced graphene in the electrocatalytic behavior of resorcinol -Formaldehyde based carbon aerogels[END_REF] and our previous research found that iron doping could greatly enhance the ORR activity of aerogel. [START_REF] Wang | One-pot synthesis of Fe-N-containing carbon aerogel for oxygen reduction reaction[END_REF] Herein, we synthesized Fe-N-C aerogel catalysts using a "one pot" sol-gel method comprising formation of a Fe-doped resorcinol (R)-formaldehyde (F)-melamine (M) hydrogel, and followed by CO2 supercritical drying and pyrolysis under N2 and NH3 atmosphere. By adding ligands, namely ethylenediaminetetraacetic acid (EDTA) or 1,10-phenanthroline (Phen), we modified the chemical environment of the Fe precursor. The resulting changes on the physicochemical characteristics were investigated using scanning electron microscopy (SEM), nitrogen sorption isotherms, X-ray photoelectron spectroscopy (XPS), inductively coupled plasma mass spectrometry (ICP-MS) and X-ray diffraction (XRD) analysis. The performance of the synthesized Fe-N-C materials was then evaluated using rotating disk electrode (RDE) setup and membrane-electrode-assemblies (MEAs).

Experiments

Sample synthesis

The Fe-N-C catalysts were prepared inspired from the method described by us before, and resorcinol (R), formaldehyde (F), melamine (M), and (NH4)2Fe(SO4)2 as precursors. [START_REF] Wang | One-pot synthesis of Fe-N-containing carbon aerogel for oxygen reduction reaction[END_REF] Sodium carbonate (NaC) was used to promote the polymerization in deionized water (W). Two different ligands (EDTA and Phen) were introduced in the synthesis solution to investigate if Fe-coordination could enhance the ORR activity of the synthesized catalysts. The reactants and solvent were mixed at 70 °C with the molar ratio of 2:7:1:0.033:60: for R:F:M:NaC:W. (NH4)2Fe(SO4)2 was added with a stoichiometry R:Fe of 1:0.015, targeting ca. 1 wt. % Fe in the final catalysts. For ligand-containing catalysts, the EDTA or Phen was firstly mixed with the Fe precursor in deionized water to form the complex with molar ratio of 1:1 or 1:3, respectively and then added into the mixture solution. Subsequently, the pH of solution was adjusted to 8 by adding NaOH solution under continuous stirring until the gel formed. The hydrogel was then aged in a water bath at 70 °C for 120 h. The obtained hydrogels were subjected to a water-acetone exchange and then to CO2 supercritical drying. Subsequently, the aerogels were pyrolysed at 800 °C under N2 flow for 1 h, smashed by ball-milling method and washed with 0.5 M H2SO4 to remove Fe nanoparticles, which were possibly generated during the pyrolysis. In order to increase the density of active sites, a second heat treatment was conducted at 950 °C under NH3 atmosphere.

Physicochemical characterization

The Fe content in the catalysts was determined by ICP-MS. XRD analysis was performed using an X"pert Pro Philips diffractometer using filtered Cu Kα radiation (λ=0.15418 nm) generated at 40 kV and 30 mA. The morphologies of the catalysts were determined by SEM (ZEISS SUPRA TM 40) operated at 3.0 kV. The detailed specific surface areas were measured by nitrogen sorption isotherms at 77 K with a Micromeritics ASAP 2020 instrument, and the pore size distribution was calculated using the 2D-NLDFT-Heterogenerous Surface method based on the adsorption isotherms. XPS was used to identify the elemental composition of the surface of the catalysts. The measurements were performed using Thermo Scientific TM K-Alpha TM spectrometer equipped with an Al Kα1,2 monochromatic source (1486.6 eV).

Electrochemical measurements

Rotating disk electrode (RDE) measurements were performed under atmospheric pressure and room temperature in a three-electrode cell. The reference electrode was a reversible hydrogen electrode (RHE) and the counter electrode was a graphite electrode. The catalyst ink was prepared by ultra-sonicating 10 mg catalyst powder, 95 µL 5 wt. % Nafion, 752 µL ethanol, and 46 µL deionized water for 1 h. 7 µL of this ink was dropped on a 0.196 cm 2 glassy carbon disk, resulting in a catalyst loading of 0.4 mgFe-N-C/cm 2 . The ORR activities were measured in O2-saturated 0.05 M H2SO4 aqueous solution. Linear scan voltammograms were recorded (LSV) at 10 mV/s from 1.1 to 0 V vs. RHE under constant revolution rate (1600 rpm). The same test was repeated in N2-saturated electrolyte to eliminate the pseudo-capacitive current ('background' current). Cyclic voltammograms between 0 and 1.0 V vs. RHE were measured at 10 mV/s in N2-saturated electrolyte. For PEMFC testing, 20 mg of catalyst, 915 µL 5 wt. % Nafion solution, 63 µL of 1-propanol, and 272 µL of deionized water were mixed and subjected to sonication for 1 hour. The ink was deposited on a 4.84 cm 2 gas diffusion layer as the cathode, resulting in a catalyst loading of 4.1 mgFe-N-C/cm 2 . The cathode was then dried at 80 °C, and hot-pressed at 135 °C with a Pt/C anode and a Nafion membrane. The temperature of cell was stabilized at 80 °C during the test and the relative pressure of H2 and O2 was 1 bar.

Results

The synthesized catalysts are listed in Table 1, along with the results of their physicochemical and electrochemical characterizations. (NH4)2Fe(SO4)2 was selected as Fe precursor because of the high solubility of Fe 2+ compared to Fe 3+ in aqueous solution of pH 8 (solubility product constant (Ksp) of 2.79×10 -39 and 4.87×10 -17 for Fe(OH)3 and Fe(OH)2, respectively). [START_REF] Lide | Handbook of Chemistry and Physics[END_REF] The ligands (EDTA or Phen) were introduced to modify the solubility of Fe ions in the precursor solution (resulting to a different dispersion of Fe atom in the carbon aerogel) and coordinate Fe 2+ to form preexisting Fe-N bonds, leading to better ORR activity. [START_REF] Li | The challenge of achieving a high density of Fe-based active sites in a highly graphitic carbon matrix[END_REF] Table 1. Physicochemical and electrochemical characterization of catalysts prepared with different ligands.

The Fe content in the final catalyst was determined using ICP-MS and XPS, and the results are listed in Table 1. Similar values obtained from the two methods suggesting a uniform distribution of Fe atoms both in the bulk and at the surface. The Fe content was close to the targeted value (1 wt. %) for the catalysts synthesized using exclusively the Fe precursor or the Fe precursor + Phen, but it revealed extremely low for the catalyst prepared using Fe + EDTA. We relate this result to the enhanced solubility of Fe ions resulting from EDTA addition. Indeed, during the solvent exchange (between water and acetone for CO2 supercritical drying), the solvent became slightly coloured, suggesting that the complex was more soluble in water than in acetone, and accounting for the Fe content loss.

Morphology and porosity of catalysts

The SEM images displayed in Figure 1 (a)-(c) provide insights into the porosity of the synthesized catalysts. Similar texture was observed for the ligand-free and EDTA-containing catalysts. A more heterogeneous texture was observed for the catalyst prepared with Phen, probably resulting from the agglomeration of large clusters. The XRD patterns shown in Figure 1 (d) indicate that all catalysts were poorly crystallized (confirmed by Raman spectrometry). Three small peaks at 2θ = 26.4°, 34.6°, and 52.4° can be found in the pattern of Fe-Phen catalyst, but could not be attributed to any Fe-containing species (α-Fe, -Fe, Fe3C or oxides). TEM images (not shown here) also confirmed that no Fe-based nanoparticles were detected in the three catalysts. Figure 1 (e) shows the pore size distribution of catalysts derived from N2 adsorption isotherms at 77 K, and the microporous and mesoporous volumes of the catalysts are listed in Table 1. In agreement with SEM images, the ligand-free and Fe-EDTA catalysts exhibit similar mesopore distribution (centered around 6-10 nm), suggesting that EDTA mildly affected the poly-condensation process. In contrast, the catalyst prepared with Phen featured larger mesopores size distribution with size centered around 20 nm: this may result from a different poly-condensation mechanism caused by the presence of Phen. Similar micropore size distributions were observed for the three catalysts. Such result makes sense if one considers that micropores are mainly generated during the thermal treatment (pyrolysis under N2 and then NH3) process, [START_REF] Jaouen | Heat-treated Fe/N/C catalysts for O2 electroreduction: are active sites hosted in micropores?[END_REF], [START_REF] Wang | One-pot synthesis of Fe-N-containing carbon aerogel for oxygen reduction reaction[END_REF] and that identical conditions were used for all catalysts.

Electrochemical characterization

The impact of ligand additives on the ORR activity of the Fe-N-C catalysts were firstly evaluated using rotating disk electrode set-up. The polarization curves of catalysts are shown in Figure 2 (a) and the kinetic currents at E = 0.8 V vs. RHE (corrected from Ohmic drop, pseudocapacitive current and from O2 transport in solution) are listed in Table 1.

Clearly, the ligand-free Fe-N-C catalysts was the more active, with a current density of 1.89 A/gFe-N-C at E = 0.8 V vs RHE. Due to similar Fe content the Fe-Phen featured similar massnormalized ORR activity. The poor ORR activity of Fe-EDTA was attributed to its low Fe content. kJ/mol determined at zero overpotential from MEA data by Osmieri et al. [START_REF] Osmieri | Elucidation of Fe-N-C electrocatalyst active site functionality via in-situ Xray absorption and operando determination of oxygen reduction reaction kinetics in a PEFC[END_REF] These results clearly suggest that, besides pure charge-transfer limitations, other characteristics, such as the accessibility of O2 and H + to the active sites limit the performance in PEMFC configuration. It is important that the polarization curves do not collapse at high current densities (j > 0.5 A/cm 2 geo), demonstrating the excellent mass transport properties of carbon aerogels.

Conclusion

Fe-N-C aerogel catalysts with high porosity and good ORR activity were synthesized using a one-pot sol gel method, based on the polymerization of resorcinol, melamine and formaldehyde in the presence of (NH4)2Fe(SO4)2. Two ligands (EDTA or 1,10phenanthroline) were integrated in the synthesis, and their impact on pore size distribution and ORR activity was investigated. The Fe-EDTA catalyst exhibits similar pore size distribution with the ligand-free Fe-N-C catalyst; however the enhanced solubility of Fe(II)-EDTA complex leads to loss of Fe during the solvent exchange step, and reduces the Fe content and consequently the final ORR activity. The introduction of Phen allows reaching the targeted Fe content due to a stronger interaction between Phen and the organic matrix and larger mesopore size distribution. Its ORR mass activity can also be comparable with the ligand-free Fe-N-C catalysts in RDE set-up. Polarization curves in real PEMFC device were also measured to compare with RDE results. The curves do not collapse at high current densities (j > 0.5 A/cm 2 geo) demonstrating the excellent mass transport properties of the Fe-N-C aerogels. They also present the same trends with electrochemical available areas obtained from CV curves in RDE set-up, showing that the ligand-free catalyst outperforms Fe-EDTA and Fe-Phen.

Figure 1 .

 1 Figure 1. (a)-(c) SEM images, (d) XRD patterns and (e) pore size distribution plots derived from N2 adsorption isotherms at 77 K for the synthesized catalysts.

Figure 2 .

 2 Figure 2. (a) Oxygen reduction reaction polarization curves and (b) cyclic voltammograms recorded in O2-or N2-saturated 0.05 M H2SO4 at 10 mV/s on RDE, respectively; (c) Tafel plots of the O2-transport and background-current corrected kinetic current obtained from the steady-state I-E curves at = 1600 rpm, and (d) iR-free polarization curves recorded in PEMFC devices for the catalysts synthesized in this work (T = 80°C, 100 % RH, PO2 = 1 bar, 150 mL/min).

/g) Vtotal (cm 3 /g) Vmicro (cm 3 /g) Vmeso (cm 3 /g) Current density (A/gFe-N-C) XPS

			ICP
	Iron precursor	Ligand	BET surface (m 2 Fe wt. % Fe at. %				RDE at E = 0.8 V vs. RHE	PEMFC at U = 0.8 V	PEMFC at U = 0.5 V	C at. %	N at. %	O at. %	Fe at. %
		EDTA	0.16 0.03	1274	1.63	0.37	1.21	1.01	2.00	89.7	93.92 3.30 2.72 0.06
	(NH4)2Fe(SO4)2	Phen	0.73 0.16	1455	2.32	0.43	1.83	1.74	1.21	74.7	93.20 2.76 3.85 0.20
		-	0.70 0.15	1665	1.92	0.46	1.34	1.89	9.44	150.1	95.37 3.08 1.38 0.18

Acknowledgements

This work was supported by the French National Research Agency in the frame of the ANIMA project (grant number n°ANR-19-CE05-0039).