Ghina Dandachi
email: ghina.dandachi@inria.fr

A Frequency-based Intelligent Slicing in LoRaWAN with Admission Control Aspects

Keywords: Slicing, LoRaWAN, Admission Control, Genetic Algorithm

The significant deployment of LoRaWan networks is increasingly questioning its ability to handle massive numbers of IoT devices and its ability to support service differentiation. The few existing attempts to implement service differentiation suffer from a lack of scalability and do not meet the qualitative criteria of the services, since without admission control there is no way to restrain the devices from transmitting. In this paper, we present a scalable probabilistic approach that not only enables an efficient sharing of LoRaWan access networks between different services/slices, but more importantly allows achieving the objectives of the supported services through the integration of an admission control. Since the derivation of devices' repartition probabilities is a very complex problem, we propose an evolutionary algorithm to derive them efficiently. The obtained results clearly show the ability of the proposed solution to efficiently utilize the scarce radio resources, while achieving the qualitative objectives of the prioritized services.

I. INTRODUCTION

Low Power Wide Area Network (LPWAN) is one of the technologies needed to cater for the evolution of the Internetof-Things (IoT). This technology is low cost, energy-efficient and could interconnect thousands of geographically dispersed end devices running on batteries. The interconnection between these devices is made possible by different technologies, such as Long Range Wide Area Network (LoRaWAN), SIGFOX, and NB-IoT. Particularly, LoRaWAN is the most widely adopted due to its simplicity, openness, and cost-effectiveness.

With the emergence of network slicing in 5G/6G networks [START_REF] Kaloxylos | A survey and an analysis of network slicing in 5g networks[END_REF], [START_REF] Zhang | An overview of network slicing for 5g[END_REF], end-to-end slicing of IoT networks, and particularly LoRaWAN networks, is becoming a must. Indeed, the slicing of IoT networks would allow not only to have a support of multiple services within the same infrastructure, but more importantly to have some guarantees, in such best effort networks.

The slicing of LoRaWAN networks mainly consists in partitioning the substrate network into multiple virtual networks. While the virtualization of the core network does not present any particular difficulty, in the age of virtualization and services' cloudification, it is quite different for the access INTELLIGENTSIA is a collaborative research project funded by the French Agence National pour la Recherche (ANR) public funding agency. networks. Indeed, unlike traditional cellular networks where the allocation of resources is based on the assignment of resource blocks, which facilitates the operation of resources' sharing between different services, the access to LoRaWAN networks is completely random (i.e., Aloha-like), which makes it very difficult to virtualize [START_REF] Ta | Lora-mab: Toward an intelligent resource allocation approach for lorawan[END_REF].

Very few works in the literature address the problem of LoRaWAN networks' slicing [?], [START_REF] Dawaliby | Dynamic network slicing for lorawan[END_REF]- [START_REF]Distributed network slicing in large scale iot based on coalitional multi-game theory[END_REF]. These works rely on the assignment of the available frequencies to the IoT devices, which allows improving their distribution. However, allocating an entire frequency to a slice can represent a significant waste of resources in a network where resources are very scarce. Moreover, the number of frequencies being very limited, this restricts the applicability of the approaches. Finally, the fact that no admission control is available means that no qualitative guarantees can be met in such networks.

In LoRaWAN networks, there is obviously no support to enforce service differentiation, except the allocation of frequency to the devices, which suffers from the limitations introduced earlier. There is, also, no straightforward means to control the access attempts of the IoT devices, unlike NB-IoT networks with the Access Class Barring (ACB) mechanism [START_REF] Bouzouita | Estimating the number of contending iot devices in 5g networks: Revealing the invisible[END_REF]. In this respect, we propose in this paper a probabilistic approach for the distribution of the devices between the different available channels, in a way to guarantee the quality of the supported services (i.e., slices), while maximizing the use of the resources compared to a classical solution. In addition, our proposed frequency-based approach incorporates an admission control, which constitutes a precondition for achieving the targeted quality criteria when dealing with massive number of IoT devices. The proposed probabilistic approach is based on the transmission by the LoRaWAN Network Server (LNS) of probabilities of access to frequencies (i.e., channels) as well as a probability of being blocked, which concerns only non-priority devices. The problem of assigning the different probabilities being very complex (i.e., infinite action space), we propose in this work an evolutionary algorithm to solve this problem more efficiently.

The remainder of this paper is organized as follows: Section II provides the background on NB-IoT Access class Barrier strategy, and gives an overview of the literature work on slicing on LoRaWAN. Section IV describes the system model for LoRaWAN, and provides a mathematical formulation of the problem. Section V presents the details of the proposed solution, based on the Genetic algorithm. Section VI presents the simulation environment of the proposed approach and shows its efficiency compared to the existing one. Finally, the paper concludes with a summary of the main advantages and achievements of the proposed system in Section VII.

II. BACKGROUND

LoRaWAN is a Long Range communication protocol [START_REF] Adelantado | Understanding the limits of lorawan[END_REF] often used to create Low Power Wide Area Networks (LPWANs) with an operating range that goes from 300 meters up to 10 kilometers. Among the main LPWANs protocol, LoRaWAN is one of the most known and used, given its open architecture.

LoRa modems modulate symbols into increasing and decreasing frequencies chirps, respectively called up-chirps and down-chirps. LoRa modulation has many parameters, which can partially be modified, depending also on the operating region of the system. These parameters are: carrier frequency, signal bandwidth, coding rate, spreading factor, chirp polarity, and sync word.

More precisely, the spreading factor (SF) defines how many chirps are sent per second. It ranges among SF7 and SF12. In detail, a large SF increases the symbol airtime and the energy consumption, thus improving the communication range, but reducing the available data rate and messages' payload size. In this paper, we consider that all the devices use the Adaptive Data Rate (ADR) mechanism for SF selection [START_REF] Kim | Adaptive data rate control in low power wide area networks for long range iot services[END_REF]. The LoRaWAN ADR is a scheme that allows to optimize the network's data rates, time-on-air (ToA) and energy consumption by controlling the data rate and the transmission power for all the end nodes independently.

As for the LoRaWAN end devices classes, they can be classified into three categories: Class A, B, and C. A Class A device has the lowest energy consumption mode, it can send uplink messages at any time, however downlink messages can be received only during two specific windows of time after an uplink transmission. Class B devices can send uplink messages any time, and have a time-synchronised receiving window for the downlink. Class C devices has the highest power consumption, they keep the receiving window open unless they are transmitting again which is the case of LoRaWAN gateways.

III. RELATED WORK

The need to support personalized services, with their own constraints, has led to the emergence of the concept of network slicing, which has taken shape with 5G cellular networks, and will be generalized in the next 6G to include not only the mobile core network but any other service [START_REF] Guan | Customized slicing for 6g: Enforcing artificial intelligence on resource management[END_REF].

IoT networks are very low cost and best effort networks by definition, but in which there is more and more the need to differentiate services [START_REF] Wijethilaka | Survey on network slicing for internet of things realization in 5g networks[END_REF]. Very few works in the literature tackle this subject, the main attempts concern NB-IoT networks [START_REF] Bouzouita | Multiple access class barring factors algorithm for m2m communications in lte-advanced networks[END_REF].

Integrating slicing in IoT network requires the virtualization of two parts: the core network virtualization and the access network virtualization. With the convergence of the cloud and networking, especially with service virtualization and orchestration technologies, core virtualization has not only become possible, but several solutions already exist. The virtualization of the network access is, however, more challenging.

In M2M networks, which are at the origin of NB-IoT networks, massive access of IoT terminals has been considered very early and several efficient processes have been integrated to address this issue. The Access Class Barring (ACB) strategy is certainly one of the most prominent, as it allows blocking devices before they even have access to the network. This technique consists in assigning an access probability to the various devices, which may enable the support of slicing in this type of access network [START_REF] Aoul | Access control in nb-iot networks: A deep reinforcement learning strategy[END_REF]. In fact, it is simply a matter of finding different access probabilities for each class of service or slice, which allows for a more refined sharing of the network [START_REF] Bouzouita | Dynamic adaptive access barring scheme for heavily congested m2m networks[END_REF].

In the case of LoRaWAN networks, it's a completely different situation. In fact, very few works in the literature address the problem of slicing in LoRaWAN networks [START_REF] Dawaliby | Dynamic network slicing for lorawan[END_REF]. This can be explained by the fact that LoRaWAN networks are unlicensed open networks where there is no technical means to limit congestion [START_REF] Bankov | On the limits of lorawan channel access[END_REF]. Indeed, the only options offered by LoRaWAN are to: limit the transmission of devices through the "duty cycle" mechanism, which indicates the fraction of time a resource is busy, or to assign a terminal to a particular frequency when joining the network. These options are very insufficient to mitigate congestion, and even less to have any guarantee.

The existing works are almost all from the same author [?], [4]- [START_REF]Distributed network slicing in large scale iot based on coalitional multi-game theory[END_REF]. There main aspect is that the end devices are grouped based on their requirements by a 4 steps strategy: 1) a clustering step to determine the number of slices, 2) a throughput estimation step based on the average throughput of each device, 3) a resource allocation step by dynamically allocating the channels to gateways and 4) a final step for devices parameters' optimization by choosing either the spreading factor using a utility function [START_REF] Dawaliby | Dynamic network slicing for lorawan[END_REF], [START_REF] Dawaliby | Adaptive dynamic network slicing in lora networks[END_REF] or both the spreading factor and the transmission power using TOPSIS [?], [START_REF]Network slicing optimization in large scale lora wide area networks[END_REF]. The main drawbacks of these works is that it is based on assigning frequencies to the gateways, which is far from reality. Moreover, given the limited number of channels, assigning a whole channel to a slice does not seem very realistic. Finally, there is no guarantee to be provided in the constrained scenarios since there is no admission control.

In this work, we propose a far more efficient approach, avoiding the wastage of the radio resource. Beyond the algorithmic aspects, we propose here an approach that is simple to implement and compatible with current LoRaWAN networks, unlike existing approaches.

IV. SYSTEM MODEL

As shown in Figure 1, LoRaWAN deploys a simple starof-stars network topology and is composed of: end devices, centralized gateways, and a remote network server, more commonly known as the LNS which stands for LoRa Network Server. In particular, LoRaWAN end devices are energyefficient sensors and actuators featuring low data rates ranging from 0.3 kbps to 50 kbps [START_REF] Adelantado | Understanding the limits of lorawan[END_REF] with long-life batteries lasting up to 10 years [START_REF] Alliance | Lorawan what is it?-a technical overview of lora and lorawan lora alliance[END_REF]. Although our approach can be easily generalized to multiple gateways, for the sake of simplicity, we assume in the following a network with a single gateway. Besides, the same assumptions as in [START_REF] Zorbas | Optimal data collection time in lora networks-a time-slotted approach[END_REF] are adopted: (1) a uniform distribution of the devices, (2) devices transmitting packets of the same duration T f for a spreading factor (SF) f , (3) packets transmission following a Poisson process, and (4) no inter-SF collisions. In such a situation, the probability of a successful delivery called Packet Data Rate (PDR), can be given by [START_REF] Zorbas | Optimal data collection time in lora networks-a time-slotted approach[END_REF]:

P f (x) = exp -2T f θN f (min(xR,d)) 2 d 2 , ( 1
)
where x is the distance of the end device to the gateway, θ is the intensity of packets transmission in packets/sec, N f is the number of nodes with SF f ∈ {1, • • • , N SF }, and d is the range of deployment for the given SF. xR represents the range of devices that may interfere with the current communication, where R = 10 P thld 10γ > 1, with γ the path loss exponent and P thld the minimum threshold of the received energy. d being the maximum distance of a device using a given SF when applying ADR technique for SFs selection. Thus, the smaller the distance x to the gateway, the higher the probability P f (x) of successful delivery due to the reduced number of interferers.

A. PDR evaluation

We consider, in the following, the case of two slices/classes of services, a priority class and a best effort (BE) class, with a probability p for a device to belong to the BE class. We also consider the general case of K frequencies, which is for example equal to three (i.e., 383.1, 383.3, and 383.5 MHz) in the European standards.

We define the probability for a best effort device, respectively priority device, to select a frequency i on which it transmits as p i BE , respectively p i Prio , with i ∈ {1, • • • , K}. Thus, the number of end devices using the SF f at the frequency i is:

N i f = N f ((1 -p) p i Prio + p p i BE ) (2)
We assume that the devices are choosing the SF based on their geographical location or using the Adaptive Data Rate (ADR) mechanism. For example, the devices that are located at a distance where the SF 7 is used, will be using the SF 7 regardless of their service class. In order to evaluate the PDR for both priority and BE classes, we start by evaluating for each device the eventual PDR when the IoT device m connects using a frequency i. For this aim, we define the PDR per device/per frequency as follows:

PDR i m = exp -2T f θN i f (min(xR,d)) 2 d 2 (3)
Then, the average PDR per frequency, P DR i is the same for priority and BE classes, and is calculated as the average of the PDR of all devices connected to this frequency:

PDR i = 1 N i f N i f m=1 PDR i m (4)
Finally, the PDR for priority and BE end devices are evaluated as follows:

PDR Prio = K i=1 p i Prio PDR i (5)
PDR BE = K i=1 p i BE PDR i (6)

B. Model with admission control

In this section, we introduce the admission control probability for BE end devices. For this reason, we redefine the number of devices per SF, per frequency as follows:

N i f = N f ((1 -p) p f Prio + p p i BE p i ac ) (7)
with p i ac being the probability of blocking BE devices at the frequency i.

Thus, the PDR for BE end devices is evaluated as follows:

P DR BE = K i=1 p i BE p i ac PDR i (8)
In practice, this admission control parameter will be applied at the end device side before transmitting a packet. The devices select a random number between 0 and 1, and only transmits if the number is higher than the admission control probability for the frequency to be used.

C. Parameters' communication

Our proposal consists of a centralized estimation of the frequency selection probabilities. The network server, will learn, based on the PDR achieved by different end devices from different classes of priority, the optimal values that will maximize the target PDR.

The optimal values need to be actively requested by the end device. This request/response process involves a two-messages protocol, described below, between the end device and the network server.

1) Access parameters' update request: Initially, an end device sets up an over the air activation (OTAA) before transmitting, with assigning equal probabilities for frequency selection, and admission control probabilities equal to 1. This means that all the devices have equal chances to transmit on any frequency, and all low priority devices will be allowed to transmit their packets without any constraints on any selected frequency. The update request mechanism is randomly triggered by an end device with a probability p u , which is equal to 0.1 in our solution. Thus, in average, an update request will be triggered every 10 packets. The network server will gather information about other end devices' performance, and optimize the value of the frequency selection and admission control probabilities as a function of the service level agreements of the supported services/classes.

End device

The communication between an end device and the network server is illustrated in Fig. 2.

2) Access parameters' update response: The implementation of the update request/response is defined by two MAC commands, following the LoRaWAN specifications. The proposed commands are smaller than 15 Bytes in order to be piggybacked with the application data. The transmission of the update request is done by the end device by taking 2 bytes. The update response is transmitted by the network server using 7Bytes, the frequency probabilities of the end device class and their admission control probabilities.

This proposition is easily generalized, since each device will receive the information related to the priority class to which it belongs, meaning that it is possible to have a large number of classes and management strategies to communicate without having to increase the size of the update response.

The Update Request message command syntax can be seen in Table I. The command will trigger the parameters' optimization at the network server side.

The update Response message command syntax is presented in Table II.

The probability values are coded on 1 bytes, i.e. 8 bits, using a Mini-float representation technique, no sign bit required, and with a bias of -7 which will allow to have a wide range of numbers between 0 and 1. An exponent of 3 bits is considered,

Payload

Size (Bytes) CID (0xAA ) and a significand of 5 bits.

1 P f 1 1 P f 2 1 P f 3 1 P ac1 1 P ac2 1 P ac3 1

V. ML-BASED PROBABILITIES CALCULATION

The Genetic algorithm (GA) [START_REF] Katoch | A review on genetic algorithm: past, present, and future[END_REF] is a population based search algorithm. GA is a well-known meta-heuristic algorithm inspired from biological evolution process, which utilizes the concept of survival of the fittest. It consists on using genetic operators on individuals present in the population in order to produce new populations. These elements/operators are:

• Chromosome representation • Chromosome selection • Chromosome crossover • Chromosome mutation • Fitness function
In this paper, we consider that the population consists of N chromosomes, and is defined as

C = {c 1 , c 2 , • • • , c N } with a chromosome c n = [p 1 P rio , • • • , p K P rio , p 1 BE , • • • , p K BE , p 1 ac , • • • , p K ac ]. We consider that p k P rio ∈ [0, 1], p k BE ∈ [0, 1]
, and p k ac ∈ [0, 1] in order to obtain optimal solutions for the probability between 0 and 1.

The procedure of GA is described in Algorithm 1. First, a population C 0 of size N chromosomes is randomly initialized. The fitness of each chromosome is calculated using the fitness function defined in Eq. 9. The first two chromosomes of highest fitness values are selected as the parents c 0 j and c 0 l for generating the next population. The genes of the parents are crossed-over using a single point crossover strategy. Using these parents a new generation is created by applying a mutation on the offspring calculated for the parents. The new population will replace the old population. This process is repeated until the best solution is found or the maximum number of generations is reached.

The fitness function fitness we use for this problem is defined as follows:

fitness = 1 1 + |PDR Prio -PDR target Prio | (9)
This fitness function ensures a good fitness if the priority class devices reach their target PDR, and a low fitness if it is not reached (< 1). Moreover, this fitness function has also lower value if the PDR of priority class devices is higher than the target PDR. This ensures an optimal PDR for the priority class devices and avoids the PDR degradation of BE class devices once the target PDR of priority class is reached.

Algorithm 1: Genetic Algorithm (GA).

Data: Population C size, N; Maximum number of iterations, MAX.

Result: Global best solution, c best .

Begin:

Generate initial population of N chromosomes

C 0 = {c 0 1 , c 0 2 , • • • , c 0 N } (i = 1, 2, • • • , n); Set iteration counter it = 0;
Compute the fitness value of each chromosomes; while it < M AX do Select a pair of chromosomes, c it j and c it l , from initial population C it based on their fitness; Apply crossover operation on selected pair with crossover probability; Apply mutation offspring with mutation probability; Replace old population with newly generated population; Increment the current iteration it by 1; end Return the best solution c best ;

The main advantage of using the genetic algorithm to solve this problem is that it allows to explore a very large set of solutions while providing a solution that is globally optimal.

VI. EVALUATION

In this section, we evaluate the proposed slicing strategy in LoRaWAN using the genetic algorithm. The evaluation consists of comparing the PDR of both priority classes for different PDR targets for the high priority class.

A. Simulation setup

Our proposal is evaluated in a simulator written in Python. The model parameters are as follows:

• Total number of devices: {200, 400, 600, 800, 1000} As for the genetic algorithm, we consider 200 generations of 20 individuals/chromosomes per population. A chromosome is composed of 9 genes. Two parents are selected from each generation using a tournament parent selection, and a single point crossover. A random mutation is used with 20% for genes mutation. We use the PyGAD Python library for building the genetic algorithm and optimizing its results [START_REF] Gad | Pygad: An intuitive genetic algorithm python library[END_REF].

B. General performance of the genetic algorithm

In this section, we present the simulation performance of the genetic algorithm for a target PDR of 0.7 for the priority class of end devices. We compare the best fitness value as a function of the generations for a population of 10, 20, and 40 chromosomes. Fig. 3 shows that it is possible to reach an optimal solution for 20 chromosomes with a comparable performance with 40 chromosomes. The GA starts to find an optimal solution almost around the 15 th generation.

C. Comparison of different desired PDR output

In Fig. 4, we evaluate the PDR of BE and priority devices as a function of the number of devices in the system, for different targets of PDR (70%, 80%, 90%).

We observe in Fig. 4a that the priority class achieves the target PDR of 90%. The BE class presents a very low PDR, starts with 45% for 200 IoT devices and decreases to 9% for 1000IoT devices. This is explained by an increase in the number of BE blocked by the admission controller, see Fig. 4b.

We show in Figs. 4c and4d the PDR and the number of blocked BE devices for a priority devices target PDR of 80%. We observe that the proposed genetic algorithm ensures that the priority devices achieve their target PDR, while trying to maximize the BE class PDR. The number of blocked devices has been reduced from 630/700 to 400/700, where 700 is the total number of BE devices (70% of total devices).

Finally, for a target priority class PDR of 70%, the performance of BE devices improves for a number of devices lower than 600, see Figs. 4e and4f. As for higher than 600 devices, the obtained performance of BE devices is similar to that obtained with a target of 80%. The reason behind this performance could be the blockage probability for BE devices.

D. Comparison of performance under different problem settings

In this section, we perform a comparison of the packet delivery rate as well as the number of blocked devices under different problem settings: the case of low charged, medium charged and highly charged systems. For this aim, we modify in this case the intensity of packets transmission θ as follows:

• Low charged: θ = 1/1800 [packets/sec] • Medium charged: θ = 1/1200 [packets/sec] • Highly charged: θ = 1/600 [packets/sec] For the following, we consider a target PDR for priority class of 80%.

We first start with the results of a highly charged system for a packets intensity of 1/600 [packets/sec]. In Fig. 5a, we observe that the priority class devices achieve their target PDR, while the BE class devices get their PDR reduced as the number of devices increase, with a percentage of blocked BE devices over the total number of BE devices varying 10/140 to 570/700 (Fig. 5b).

As the packets intensity decreases, we observe that the PDR of BE increases. The system is less saturated and allows for a better service for BE devices while maintaining the target PDR for priority devices. The number of blocked BE devices also drops from a maximum of 570/700 for θ = 1/600, to 400/700 for θ = 1/1200, to 340/700 for θ = 1/2400.

VII. CONCLUSION

In this paper, we consider the problem of slicing in Lo-RaWAN for 5G/6G networks. We introduce an empirical formulation for the problem of network slicing, which ensures the access slicing by using a probabilistic model for the frequencies selection. An admission control probability is also introduced in order to control the back-off time for the lowest priority class. An evolutionary algorithm was used to find the optimal values for the frequency selection probabilities as well as the admission control probabilities. We show that it is possible, using the optimized probabilities for frequency selection and admission control, to achieve a target PDR for a given class of devices. It is possible to generalize this problem to the case of a higher number of classes of priority with different admission control strategies for different classes.

Fig. 1 :

 1 Fig. 1: LoRaWAN architecture.

Fig. 3 :

 3 Fig. 3: Fitness function variation as a function of the generation number.

Fig. 4 :

 4 Fig. 4: Variation of PDR and Number of blocked devices as a function of the target PDR for priority slice.

Fig. 5 :

 5 Fig. 5: Variation of PDR and Number of blocked devices as a function of the packets intensity, for a target PDR of 80% for priority slices.

TABLE I :

 I MAC Command: Update Request

TABLE II :

 II MAC Command: Update Response (case of three frequencies)

  Packets transmission intensity: θ = 1/1200 [packets/sec]. • Path loss Exponent: γ = 2.08 • Power threshold: p thld = 6 • Probability of BE devices: p = 0.7

	• The SFs maximum distance from a gateway following
	ADR strategy for SF selection:
	d = {2200, 2500, 3000, 3700, 4100, 6400} [m]
	sponding to SFs {7, 8, 9, 10, 11, 12}, respectively.
	• Time on Air for each SF:
	{79.1, 147.97, 275.46, 509.95, 1101.82, 2039.81} [ms]
	starting from SF7 and ending with SF12.

• • Number of frequencies: K = 3


Simon Bliudze
email: simon.bliudze@inria.fr

Petra Van Den Bos
email: p.vandenbos@utwente.nl

Marieke Huisman
email: m.huisman@utwente.nl

Robert Rubbens
email: r.b.rubbens@utwente.nl

Larisa Safina
email: larisa.safina@inria.fr

JavaBIP meets VerCors: Towards the Safety of Concurrent Software Systems in Java

We present "Verified JavaBIP", a tool set for the verification of JavaBIP models. A JavaBIP model is a Java program where classes are considered as components, their behaviour described by finite state machine and synchronization annotations. While JavaBIP guarantees execution progresses according to the indicated state machine, it does not guarantee properties of the data exchanged between components. It also does not provide verification support to check whether the behaviour of the resulting concurrent program is as (safe as) expected. This paper addresses this by extending the JavaBIP engine with run-time verification support, and by extending the program verifier VerCors to verify JavaBIP models deductively. These two techniques complement each other: feedback from run-time verification allows quicker prototyping of contracts, and deductive verification can reduce the overhead of run-time verification. We demonstrate our approach on the "Solidity Casino" case study, known from the VerifyThis Collaborative Long Term Challenge.

Introduction

Modern software systems are inherently concurrent: they consist of multiple components that run simultaneously and share access to resources. Component interaction leads to resource contention, and if not coordinated properly, can compromise safety-critical operations. The concurrent nature of such interactions is the root cause of the sheer complexity of the resulting software [START_REF] Bliudze | On methods and tools for rigorous system design[END_REF]. Modelbased coordination frameworks such as Reo [START_REF] Arbab | Reo: A channel-based coordination model for component composition[END_REF] and BIP [START_REF] Basu | Modeling heterogeneous real-time components in BIP[END_REF] address this issue by providing models with a formally defined behaviour and verification tools.

JavaBIP [START_REF] Bliudze | Exogenous coordination of concurrent software components with JavaBIP[END_REF] is an open-source Java implementation of the BIP coordination mechanism. It separates the application model into component behaviour, modelled as Finite State Machines (FSMs), and glue, which defines the possible stateless interactions among components in terms of synchronisation constraints. The overall behaviour of an application is to be enforced at run time by the framework's engine. Unlike BIP, JavaBIP does not provide automatic code generation from the provided model; instead it realises the coordination of existing software components in an exogenous manner, relying on component annotations that provide an abstract view of the software under development.

To model component behaviour, functions of a JavaBIP program are annotated as FSM transitions. These annotated functions model the actions of the program components. The computations are assumed to be terminating and non-blocking. Furthermore, any side-effect is assumed to be either taken into account by the change of the FSM state, or to be irrelevant for the system behaviour. Any correctness argument for the system depends on these assumptions. A limitation of the JavaBIP approach is that it does not guarantee that these assumptions hold. This paper proposes a joint extension of JavaBIP and VerCors [START_REF] Blom | The VerCors tool set: Verification of parallel and concurrent software[END_REF] providing such guarantees about the implementation statically and at run time.

VerCors [START_REF] Blom | The VerCors tool set: Verification of parallel and concurrent software[END_REF] is a state-of-the-art deductive program verification tool for concurrent programs. It verifies programs, written in e.g. Java, using permissionbased separation logic [START_REF] Amighi | Permission-based separation logic for multithreaded Java programs[END_REF]. This logic is an extension of Hoare logic that allows one to specify properties using contract annotations. These contract annotations include permissions, pre-and postconditions and loop invariants. VerCors automatically verifies programs with contract annotations. To verify JavaBIP models, we (i) extend JavaBIP annotations to include verification annotations, and (ii) adapt VerCors to support JavaBIP annotations. VerCors transforms the verification annotations and JavaBIP models into contract annotations, leveraging their structure as specified by the FSM annotations and the glue.

For some programs VerCors requires extra contract annotations, e.g. when complicated loops are involved. To enable properties to be analysed when not all necessary annotations are added yet, we extend the JavaBIP engine with support for run-time verification. During a run of the program, the verification annotations are checked for that specific program execution. The run-time verification support is set up in such a way that it ignores any verification annotations that were already statically verified, reducing the overhead of run-time verification.

This paper presents the use of deductive and run-time verification in Verified JavaBIP to prove assumptions made on the JavaBIP models. Specifically, we make the following contributions:

-We extend regular JavaBIP annotations with verification annotations on preand postconditions for transitions, and invariants for components and states. -We extend VerCors to deductively verify a JavaBIP model, taking into account its FSM and glue structure. -We add support for run-time verification to the JavaBIP engine.

-We link VerCors and the JavaBIP engine such that deductively proven annotations need not be monitored at run-time.

-Finally, we demonstrate our approach on a variant of the Casino case study from the VerifyThis Collaborative Long Term Challenge.

Related Work

There are several approaches to verify and validate behaviours of abstract models in the literature.

JavaBIP and Verification Annotations

JavaBIP annotations capture the FSM specification and describe the behaviour of a component. They are attached to classes, methods or method parameters, and were first introduced by Bliudze et al [START_REF] Bliudze | Exogenous coordination of concurrent software components with JavaBIP[END_REF]. Listing 1 shows an example of JavaBIP annotations. The class annotation @ComponentType indicates that this class is a JavaBIP component and specifies its initial state. In the example, this is the WAITING state. @Port declares the list of possible transition labels. Method annotations include @Transition, @Guard and @Data. An @Transition annotation consists of the name of a port, a start and end state, and optionally a guard. The transition in the example goes from WAITING to PINGED whenever the PING port is triggered. As no guard is specified, the transition may always be taken. @Guard declares a named boolean function, whose result indicates if a transition is enabled. @Data either declares outgoing data of a getter method, or, incoming data via a method parameter. Note that the example does not specify when ports are activated. This is specified as glue, separately from the JavaBIP component [START_REF] Bliudze | Exogenous coordination of concurrent software components with JavaBIP[END_REF]. We added component invariants and state predicates to Verified JavaBIP. These are declared using the following annotations: @Invariant(expr) for a property that must hold after construction of the component and before and after executing a transition, and @StatePredicate(state, expr) for property that must hold when entering the state, and is assumed to hold when departing from the state. Furthermore, Verified JavaBIP includes pre-and postconditions as part of the @Transition annotation. These have to hold before and after execution of the corresponding function, respectively. Lastly, @Pure indicates that a method is side-effect-free, and is used only in conjunction with @Guard.

Expressions within annotations should follow the grammar of Java expressions with some limitations: we do not support lambda expressions and method references, switch expressions, expressions containing new or instanceOf, and wildcard arguments. These are limitations of the current implementation. In the future they might be lifted.

Architecture of Verified JavaBIP

The architecture of Verified JavaBIP is shown in Figure 1. The user starts with a JavaBIP model, optionally with verification annotations. The user then has two choices: verify the model with VerCors, or execute it with the JavaBIP Engine. We extended VerCors to automatically transform a JavaBIP model to the internal representation of VerCors, Common Object Language (COL), which is roughly equal to the union of the input languages of VerCors. This representation is then verified. An example of this transformation is given in Listings 2 and 3. If verification succeeds, the JavaBIP model is memory safe, has no data races, and all its components respect the specified properties. In this case no extra run-time verification is needed.

If verification fails, there are either memory safety issues, or components violate properties. In the first case, the user needs to update the verification annotations, and retry verification with VerCors, since memory safety properties cannot be checked by the JavaBIP engine. In the second case, VerCors outputs and stores a verification report with the JavaBIP model, indicating which properties were verified and which were not.

We extended the JavaBIP engine with run-time verification support. If a verification report is included with the JavaBIP model, the JavaBIP engine uses it to only verify at run time the verification annotations that were not verified deductively. If no verification report is included, the JavaBIP engine verifies all verification annotations at run time.

Implementation of Verified JavaBIP

This section briefly discusses relevant implementation details for Verified JavaBIP.

Run-time verification in the JavaBIP engine is performed by checking the relevant properties at points of interest. For example, before the execution of a transition, the pre-condition of the transition as well as the component invariant is checked. Furthermore, the user can configure what should happen if run-time verification fails: print a warning and continue execution, or terminate execution. Deductive verification is done by encoding the JavaBIP semantics into COL. We describe this encoding with an example. Listing 2 shows the ping method, where the @Transition annotation indicates a transition from state PING to PING. The guard indicates that the transition may only be taken if it is not the last ping. The name HAS_PING refers to the @Guard annotation of the corresponding method hasPing, which returns pingsLeft >= 1.

Listing 3 shows the COL representation of the ping method after encoding the JavaBIP semantics. Line 1 states the precondition of the ping method, and line 2 the postcondition. PING_state_predicate() refers to the state predicate of state PING. It may restrict the values of the fields in the class. If not defined by the user, it is true. Since the predicate is both a pre-and a postcondition, it is assumed at the start of the method, and needs to be proven to hold at the end of the method. hasPing() is the method with the @Guard annotation for the HAS_PING label. The method is used directly in the COL representation. For each JavaBIP construct, we have implemented such a transformation of JavaBIP to COL. As these transformations are all similar, the rest of them are not discussed.

To prove memory safety of JavaBIP models, we extended VerCors to automatically generate permission annotations. Currently, a naive policy is used, where each component owns the data of all its fields. This works well for JavaBIP models where each component has full ownership over its data, and none of it is shared. If this is not the case, the naive approach will not suffice, and a different approach will be needed, e.g. by VerCors taking into account user written permissions. For more info about permissions, we refer the reader to [START_REF] Amighi | Permission-based separation logic for multithreaded Java programs[END_REF].

VerifyThis Casino and Verified JavaBIP

Finally, we illustrate Verified JavaBIP with the Casino case study adapted from [START_REF]VerifyThis collaborative long-term verification challenge: The Casino example[END_REF]. We discuss the case study, the JavaBIP transformation, and its verification.

The Casino consists of three component types: a player, an operator, and the casino. The model supports multiple players and casinos; each casino has only one operator. The players can place bets on a coin flip. The casino pays out twice for a correct guess, and keeps the money otherwise. The operator can choose to add or withdraw money to the pot of the casino. To decide how much money to add or withdraw, the operator maintains locally the balance of the casino pot.

We have added several invariants to this model. The purse of every player, the casino pot and its operator copy, the wallet of the operator, and a placed bet, must all be non-negative, as the model does not support debts. If no bet is placed, it must be zero. These properties are defined as @Invariant or @StatePredicate verification annotations on the corresponding components and states in the JavaBIP model (see Appendix A).

There are two problems with this model. However, because their root cause, detection and solutions are very similar, we only discuss one of them. Specifically, the problem is that the player can win more than the casino pot contains. This is possible because there are no restrictions on how much the player can bet.

This problem is detected by both deductive and run-time verification. Concretely, VerCors cannot prove that the casino pot is non-negative, which is part of the casino invariant, after the PLAYER_WIN transition. The JavaBIP run-time engine can also detect this problem, but it is not guaranteed to. This is because the model contains some non-determinism. For example, if no player ever wins, this problem does not occur, and run-time verification does not detect it.

There are several possible solutions. First, the user can choose to only run the model with run-time verification enabled, such that the execution can be stopped upon violation. Depending on the model, combined with the performance penalty of run-time verification, this might be an acceptable solution. Second, extra JavaBIP guards can be added to the transitions, restricting model behaviour at run time. For example, a guard could be added to PLACE_BET that requires bet <= pot. However, in the general case, adding guards might introduce deadlocks, and it slows down run-time verification. Third, a solution is to change the model in such a way that this problem cannot occur. For example, the casino could offer choices of how much the player can bet. This solution introduces no extra run-time checks. However, refactoring a model takes effort, and in the general case the behaviour of the model will change. Depending on the situation, the user may opt for each of these three solutions.

Conclusions and Future Work

We presented Verified JavaBIP, a tool set for verifying the assumptions of JavaBIP models and their implementations. The tool set extends the original JavaBIP annotations with annotations intended for verification of functional properties. Verified JavaBIP offers both deductive verification of models using VerCors, and run-time verification of the model using the JavaBIP engine. Any properties not verified deductively can be checked at run-time, while any properties verified deductively are skipped for checking at run time. In the demonstration, we used Verified JavaBIP on the Casino case study, automatically detecting a problem.

There are several directions for future work. Support for automatically checking memory safety could be further extended by also supporting data-sharing between components. We would also like to support run-time verification of memory safety. Additionally we would like to do more experimental evaluation on the capabilities and performance of Verified JavaBIP. Finally, we are planning to investigate run-time verification of safety properties of the JavaBIP model beyond invariants. Figure 2 visualizes the structure of the casino as a state machine. The operator can add to and remove money from the pot of the casino at any time. Except after a bet is placed, then the operator can only add money to the pot, because placing a bet is only allowed if there is enough money in the pot. If it were possible to remove money from the pot after placing a bet, the casino could end up with a negative balance. For more details, we refer the reader to the VerifyThis website explaining the challenge [START_REF]VerifyThis collaborative long-term verification challenge: The Casino example[END_REF].

Idle Game available

Bet placed

A.2 Solidity Casino: JavaBIP Encoding

The JavaBIP encoding of the Casino diverges from the original casino example to generalize the original case study. Concretely, the concept of "operator" and "player" were factored out and made independent. This allows instantiation of the model with any number of casinos, players, and operators. There are several reasons for the generalization. First, a model that can be instantiated for different parameter values makes doing performance evaluations easier. Unfortunately, because of time constraints, this is still future work. Second, the generalized model also allows use of an advanced feature of the JavaBIP framework that was not relevant before, which is that of a three-way synchronization.

We will now discuss the actual JavaBIP encoding. In this encoding, there are three component types: Player, Operator, and Casino. Changes in the state take place as synchronizations between components. For example, when money is added to the pot of the casino, Operator and Casino synchronize, transferring the amount to be added from the Operator to the Casino. Similarly, when Player bets, Player and Casino synchronize, communicating the amount to be betted. Finally, when a bet is decided, a ternary synchronization takes place to establish in all three components that the bet was decided. For Operator, this means the amount of money in the Casino has either increased or decreased. For Player, it either receives twice the bet, or nothing. For the Casino, it either needs to pay out, or transfer the bet to the pot. The components and their transitions are visualized in Figure 3.

Consider the code in Listing 4, which shows part the Casino component. The component starts in state IDLE. As indicated by the @Transition annotation, the ADD_TO_POT transition can be activated in the BET_PLACED state. A requirement of the transition is that only the operator can trigger it, which is fulfilled by the guard part of the transition annotation. Besides that, it is always safe to add money to the pot, so it has no pre-and postconditions. In the full JavaBIP model, the method can also be activated in other states, but these annotations have been omitted from the paper for brevity. In the next subsection we will discuss parts of the model that might not be safe, and how these limitations can be expressed in contracts.

The After receiving the bets, the Casino is checking the guesses and concludes that player 2 wins! However, this makes the pot to be negative, which triggers an alert from the invariant violation.

A.5 Fixing the problem

As discussed in Section 6, there are several ways to fix a broken model: (i) always execute the model with run-time verification, (ii) add extra guards, or (iii) refactor the model. For the sake of illustrating the tool set, we will show an example of applying option (ii). Concretely, we add the guard ENOUGH_FUNDS to the transition annotation of REMOVE_FROM_POT. The updated annotated method is shown in Listing 6. This will restrict the transition to only be enabled when there is enough money in the casino pot, ensuring that the casino pot cannot become negative because of withdrawals from the operator. For deductive verification, the change in the model causes VerCors to succesfully verify the model: it prints "Verification completed successfully." upon termination, which indicates that the model is memory safe, data race free, and respects the verification annotations. Furthermore, a verification report is produced, which states that the invariant of the Casino component has been verified. For run-time verification, the change will cause the model to no longer crash at run-time when run-time verification is enabled, as the invariants are no longer violated. Additionally, when the previously produced verification report is included when executing the model, the run-time verifier skips checking the component invariant of Casino while running the model. For a small model such as this one, the difference between doing the run-time checks and not doing them is negligible. However, we speculate that for models with more components, the overhead could be noticeable.

Fig. 1 .

 1 Fig. 1. Verified JavaBIP architecture. Ellipse boxes represent analysis or execution.

@Listing 2 .

 2 Transition ( name = PING , source = PING , target = PING , guard = HAS_PING ) public void ping () { pingsLeft --; } Example of a transition in JavaBIP. requires PING_state_predicate () && hasPing (); ensures PING_state_predicate (); public void ping () { pingsLeft --; } Listing 3. COL representation of Listing 2 after encoding JavaBIP semantics.

Fig. 2 .

 2 Fig. 2. Finite state machine representation of the Solidity Casino smart contract. Note that this figure does not visualize the structure of the JavaBIP encoding.

Fig. 3 .

 3 Fig. 3. Finite state machines of components in JavaBIP Casino case study @ComponentType ( initial = IDLE , name = CASINO_SPEC ) @Invariant ( " bet >= 0 && pot >= bet " ) @StatePredicate ( state = IDLE , expr = " bet == 0 " ) public class Casino { int pot ; Coin guess ; int bet ; // Other variables omitted ... @Transition ( name = ADD_TO_POT , source = BET_PLACED , target = BET_PLACED , guard = IS_OPERATOR ) public void addToPot ( @Data ( name = OPERATOR ) Integer sender , @Data ( name = INCOMING_FUNDS ) int funds ) { pot = pot + funds ;

/}Listing 6 .

 6 / Remove money from pot @Transition ( name = REMOVE_FROM_POT , source = IDLE , target = IDLE , guard = " IS_OPERATOR && ENOUGH_FUNDS" ) public void removeFromPot ( @Data ( name = OPERATOR ) Integer sender , @Data ( name = INCOMING_FUNDS ) int funds ) { pot = pot -funds ;System . out . println ( " CASINO " + id + " : " + funds + " removed by operator " + sender + " , pot : " + pot ) ; REMOVE_FROM_POT transition with the new guard underlined.

  @Invariant and @StatePredicate annotations in Listing 4 indicate the component invariant and state invariant, respectively. The component invariant indicates that bet and pot should both contain non-negative integers. The state predicate indicates that in the IDLE state, the bet variable should be equal to zero. The full JavaBIP model contains more annotations, but they are omitted for brevity.

	add_to_pot [is_operator] remove_from_pot	add_to_pot [is_operator] remove_from_pot		add_to_pot
		create_game		receive_bet
	IDLE	[is_operator]	GAME_AVAILABLE	[is_operator]	BET_PLACED
		casino_win [is_operator && !guessed]
	Casino	player_win [is_operator && guessed && is_player]
	create_game			create_game		create_game
	decide_bet			decide_bet		decide_bet
		add_to_pot		remove_from_pot
	PUT_FUNDS			WORKING		WITHDRAW_FUNDS
		prepare_to_add [enough_funds]	prepare_to_remove
	Operator
	receive_money
	GAME_AVAILABLE	prepare_bet	BET_PREPARED
	Player			place_bet

Appendix A Demonstration

This appendix demonstrates the Verified JavaBIP tool set by applying it to the VerifyThis Casino case study. This case study was chosen because it strikes a good balance between being non-trivial, and easy to understand. Additionally, it also contains a problem, detectable with both deductive and run-time verification.

We first discuss the case study and its origin in Appendix A.1, followed by an explanation of how the case study was encoded in JavaBIP, in Appendix A.2. We show how to detect the problem in Appendices A.3 and A.4, and how to fix the problem in Appendix A. [START_REF] Arbab | Reo: A channel-based coordination model for component composition[END_REF].

Before the artefact deadline, we will provide an artefact containing the following:

-Instructions on the structure and usage of the artefact; -The source and binary of VerCors with JavaBIP support; -The JavaBIP Engine with run-time verification support; -Examples to test the tool set; -Various versions of the Casino example to illustrate problems with the model and how they can be fixed; -Scripts to run the tool set on the provided examples; and -Sources of the tools.

A.1 Solidity Casino: Case Study

The VerifyThis Collaborative Long Term Challenge considers a casino implemented in Solidity, a language for defining smart contracts [START_REF]Solidity programming language[END_REF]. This particular implementation of a casino allows players to bet on the outcome of a coin flip. If they guess the correct outcome, they win, and the casino pays out twice the bet. If they guess incorrectly, no money is received, and the casino keeps the money. -------------------------------------In this transition the invariant of the component is not maintained , since ... --------------------------------------[ ----------2 @Invariant (" bet >= 0 && pot >= bet ") - ---------] ------------------------------------- Even though the model was carefully designed, it contains a problem: the operator can withdraw more money than is available in the Casino pot. We will now show how this problem can be detected with both deductive and run-time verification.

A.3 Deductive Verification

To deductively verify the Casino model with VerCors, the source code of the model is given to VerCors: $ vercors Casino . java Constants . java Operator . java Player .

java Main . java

After several seconds of analysis, VerCors reports that the invariant of the Casino component does not hold after removing money from the pot, as shown in Listing 5.

Note how both the transition that violates the invariant is shown, as well as which part of the invariant is violated. As bet is supposed to be non-negative, and pot should be greater or equal to bet, it follows that VerCors cannot prove that pot remains non-negative.

A.4 Run-time Verification

The JavaBIP engine with run-time verification now checks the contract that, according to the VerCors output, it was not able to verify: pot >= bet.

In the following we see that the execution starts with creating the casino, and initializing the operator and players with the predefined amount of money in their wallets. After that players make their first bet.


C.-E Notredame

R Jorioz

M Wathelet

C Mannoni

P Grandgenèvre

C Debien

N Pauwels

F Ducrocq

E Leaune

M Morgiève

C.-E Notredame

C-E Notredame

P Thomas

G Vaiva

Dr Charles- Edouard Notredame
email: charles-edouard.notredame@chru-lille.fr.

Les dispositifs d'aide à distance : lignes de force de la prévention du suicide en France

teaching and research institutions in France or abroad, or from public or private research centers.

Introduction

Presque aussi anciens que la téléphonie elle-même, les dispositifs d'aide à distance figurent parmi les modalités de prévention du suicide les plus anciens [START_REF] Shneidman | Clues to suicide[END_REF]. Du fait de leur très grande hétérogénéité et des difficultés méthodologiques qu'il y a à les étudier, la littérature internationale peine encore à dégager un corpus de preuves convergent pour étayer leur efficacité sur les taux de conduites suicidaires [START_REF] Hoffberg | Suicidal Self-Directed Violence Among Homeless US Veterans: A Systematic Review[END_REF]. En revanche, leur intérêt individuel en termes de lutte contre l'isolement, d'apaisement, de réduction des idées suicidaires et d'orientation vers les soins est davantage étayé [START_REF] Hoffberg | Suicidal Self-Directed Violence Among Homeless US Veterans: A Systematic Review[END_REF][START_REF] Gould | Impact of Applied Suicide Intervention Skills Training on the National Suicide Prevention Lifeline[END_REF]. Aussi, les dispositifs d'aide à distance sont recommandés comme l'une des pierres angulaires des stratégies nationales de prévention [START_REF]Haut Conseil de la santé publique. Évaluation du programme national d'actions contre le suicide[END_REF][START_REF]Preventing suicide: a global imperative[END_REF], notamment afin de potentialiser les actions de communication et de promotion de l'accès à l'aide.

Or, depuis deux ans, l'aide à distance a justement pris une place de premier rang dans le champ de la santé mentale en général et plus particulièrement de la prévention du suicide.

Deux événements permettent de l'expliquer. D'une part, l'épidémie de Covid-19 et son sillage de détresse psychique ont vu se mobiliser de nombreux acteurs associatifs et sanitaires, donnant lieu à une multiplication de dispositifs téléphoniques locaux, départementaux et régionaux. En parallèle, le ministère des Solidarité et de la Santé a confié aux cellules d'urgence médicopsychologiques le pilotage d'une ligne nationale animée par un regroupement d'associations [START_REF] Gillaizeau | Le dispositif national d'écoute téléphonique dans le cadre de l'épidémie de COVID-19[END_REF]. D'autre part, la France a franchi depuis le 1 er octobre 2021 une étape décisive en se dotant pour la première fois d'un numéro national professionnel de prévention du suicide. Du point de vue de la santé publique, le lancement du 3114 donne lieu à une évolution du paysage de l'aide psychologique et sociale à distance. Afin de mieux penser les articulations et les complémentarités, il invite notamment à un travail de revalorisation et de clarification des rôles, positions et objectifs des dispositifs déjà en place, en même temps que d'opérationnalisation des coopérations entre ces dispositifs et le 3114.

À l'appui de cette perspective, nous proposons dans cet article un rapide panorama du champ de la prévention du suicide par l'aide à distance en France, en en retraçant les lignes de force historiques, en tâchant d'en délinéer une typologie et en ouvrant sur les perspectives de devenir de ce champ.

Les services de prévention et d'aide à distance en santé

Quelques repères historiques

Pour l'aide à distance européenne et française, la prévention du suicide représente un primum movens. En 1953, le révérend Edward Chad Varah, prêtre anglican ému par le suicide d'une adolescente dont il avait organisé les funérailles, fonde en Grande-Bretagne les Samaritans, le tout premier service bénévole d'écoute dédié à la souffrance psychique et à la lutte contre la solitude [START_REF] Chareyre | De la téléphonie santé aux forums sur le Net : cinquante ans d'évolution de l'aide à distance en santé[END_REF]. Quelques années plus tard, en France, l'association SOS Amitié lui emboîte le pas, amorçant le développement massif des services dits de « téléphonie sociale ».

Initialement nourri de militantisme solidaire, ce mouvement a d'abord été exclusivement porté par le monde associatif avant d'être investi par les services de l'État [START_REF]Suicide. Connaître pour prévenir : dimensions nationales, locales et associatives[END_REF]. Il s'est alors accompagné d'une large diversification de nature et d'objet aboutissant à ce que le champ de l'aide à distance conquiert de nombreux territoires de la santé publique, bien au-delà de la seule prévention du suicide.

Structuration de l'aide à distance en France

À ce jour plusieurs plus de nombreux service d'aide à distance existent aux échelons local et national. Leur typologie est complexe, mouvante et s'appuie sur des critères multiples tels que [START_REF] Chareyre | De la téléphonie santé aux forums sur le Net : cinquante ans d'évolution de l'aide à distance en santé[END_REF][START_REF]Suicide. Connaître pour prévenir : dimensions nationales, locales et associatives[END_REF][START_REF]La téléphonie sociale entre information et écoute du public[END_REF] :

• l'objet exact du dispositif, souvent traité selon un abord populationnel (ex. jeunes, femmes victimes de violence, etc.) ou thématique (solitude, prévention du suicide, postvention, etc.)

• le profil des personnes qui assurent la réponse au public : bénévoles, professionnels ou équipes mixtes

• le statut juridique du dispositif : le plus souvent, association ou groupement d'intérêt public • les modalités de financement : financements d'État ou organisme indépendant

• le type d'actions menés : accompagnement, prévention, postvention, soins, formations, etc.

• le périmètre géographique : infra-départemental, départemental, régional ou national Depuis le début des années 2000 des initiatives successives ont été entreprise afin de structurer ce foisonnement de dispositifs, en particulier dans le champ de la prévention du suicide. Structuration par l'auto-organisation d'abord, lorsque plusieurs associations se sont fédérées en 1996 en une Union Nationale de Prévention du Suicide (UNPS) afin de renforcer le maillage territorial et de porter une voix commune auprès des pouvoirs publics. À ce jour, l'UNPS compte près d'une quarantaine de membres [START_REF]Les membres adhérents[END_REF], dont trois lignes nationales oeuvrant directement pour la prévention du suicide : SOS Amitiés, Suicide Écoute et SOS Suicide Phénix.

Structuration par la régulation d'État ensuite, lorsque la

Valeurs et principes d'action

D'une façon générale, les PADS oeuvrant pour la prévention du suicide proposent un accueil, une écoute et un accompagnement pour les personnes en souffrance et leurs proches.

Leur particularité tient à ce qu'ils s'appuient sur un référentiel valoriel et éthique fort pour mener à bien leurs missions [START_REF] Huët | Les devenirs politiques de l'épuisement quotidien[END_REF]. Héritage de leurs racines socio-historiques et infléchi par le large recours au bénévolat, ce référentiel constitue une véritable colonne vertébrale identitaire (il participe à définir les PADS en tant que PADS) et pragmatique (il guide leur pratique et leurs actions). Souvent formalisées par de chartes que les bénévoles ont à signer au moment de s'engager (ex. [START_REF] Sos Amitié | [END_REF]), il s'articule autour de principes-pivot :

• l'anonymat, qui porte autant sur l'appelant que le bénévole, et qui n'est levé que pour porter assistance en cas de danger imminent ;

• la non-directivité, conçue comme la condition de la juste position de l'écoutant et le moyen de respecter voire de restituer son autonomie à l'appelant. Ce principe de nondirectivité se concrétise par l'adoption de la pratique de « l'écoute active » ;

• l'absence de jugement, et la résistance à toute influence confessionnelle, philosophique, morale ou politique. 1

SOS Amitié, SOS Suicide Phénix, PHARE Enfants-Parents, Suicide Écoute, Fil Santé Jeunes et la ligne Azur

Bien que recommandant un renforcement de l'évaluation des pratiques d'écoute et des meilleurs liens avec les circuits de prise en charge, le Haut Conseil de Santé Publique a souligné l'intérêt social des PADS et leur rôle de levier pour l'orientation des personnes en détresse [START_REF]Haut Conseil de la santé publique. Évaluation du programme national d'actions contre le suicide[END_REF]. De fait, les écoutants des 16 dispositifs pilotés par SPF a reçu près d'un million d'appels en 2017 [START_REF]Aide à distance en santé : l'offre de service[END_REF].

En 2014, SOS Amitié avait quant à elle répondu à plus de 681 600 appels, dont 2,2 % avaient directement trait au suicide [START_REF]Suicide. Connaître pour prévenir : dimensions nationales, locales et associatives[END_REF].

Les dispositifs professionnels de prévention du suicide à distance

VigilanS

Maturée à la faveur de plusieurs protocoles de recherche-action successifs [START_REF] Vaiva | ALGOS: the development of a randomized controlled trial testing a case management algorithm designed to reduce suicide risk among suicide attempters[END_REF], la mise en place du dispositif VigilanS en 2014 a marqué, en France, l'entrée de la prévention du suicide à distance dans le champ professionnel. Inspiré d'expériences pionnières marquantes [START_REF] Motto | A randomized controlled trial of postcrisis suicide prevention[END_REF][START_REF] Carter | Postcards from the EDge project: randomised controlled trial of an intervention using postcards to reduce repetition of hospital treated deliberate self poisoning[END_REF] et appuyé sur un corpus empirique fort [START_REF] Milner | Letters, green cards, telephone calls and postcards: systematic and meta-analytic review of brief contact interventions for reducing self-harm, suicide attempts and suicide[END_REF][START_REF] Inagaki | Interventions to prevent repeat suicidal behavior in patients admitted to an emergency department for a suicide attempt: A meta-analysis[END_REF], VigilanS s'inscrit dans la lignée des dispositifs de recontact bref qu'il double d'une dimension de veille. Comme d'autres dispositifs locorégionaux (voir, par ex. [START_REF] Notredame | Pertinence et expérience des dispositifs de veille et de recontact dans la prévention suicidaire auprès des enfants et des adolescents[END_REF]), il vise à prévenir la réitération suicidaire (prévention dite « ciblée ») en combinant de façon algorithmique différentes modalités d'action [START_REF] Duhem | Combining brief contact interventions (BCI) into a decision-making algorithm to reduce suicide reattempt: the VigilanS study protocol[END_REF]. Depuis son ouverture le 1 er octobre 2021, le nombre d'appels quotidiens au 3114 a connu une croissance quasi-constante (voir Figure 1). Au jour de la soumission du présent article, ce sont près de 85.000 personnes qui ont appelé le 3114, avec un taux de décroché de plus de 70%.

Valeurs et principes d'action

Contrairement aux PADS, les dispositifs professionnels de prévention du suicide à distance français sont encore jeunes. Si leur assise scientifique empirique et théorique est solide, leur identité, leur cadre éthique et déontologique et leurs principes d'action sont en cours de maturation. Des lignes de force, qui traversent à la fois VigilanS et le 3114, se dégagent néanmoins :

• La confidentialité des échanges plutôt que l'anonymat. Dans le cadre de VigilanS, ce dernier est rendu impossible par le processus d'inclusion. Dans le cadre du 3114, les répondants s'efforcent de le lever afin de gagner en efficacité d'évaluation et en latitude d'intervention au bénéfice de la prévention. Dans un cas comme dans l'autre, le principe de confidentialité s'inscrit dans le cadre déontologique plus large du secret médical auquel sont rompus les soignants.

• La proactivité, conçue comme une réponse aux difficultés de demande d'aide des personnes en détresse psychique. Mise en balance par le principe de non-intrusion, cette proactivité se traduit par une propension à aller au-devant des personnes, à intervenir auprès d'elle de façon d'autant plus directive qu'elles sont en danger et à leur porter assistance.

• L'attention à la qualité relationnelle et du lien avec l'appelant. Le substrat éthique est celui de l'inquiétude comme une aiguillon à ne pas rester indifférent ou inerte face à la détresse, dans une dynamique de souci de l'autre [START_REF] Walter | Les racines philosophiques du « rester en lien » : la clinique du souci[END_REF].

Évolution des dispositifs d'aide et de prévention à distance : l'aire du numérique

En France, 77% de la population sont équipés d'un smartphone [START_REF]Économiques. 94 % des 15-29 ans ont un smartphone en 2021[END_REF], 93% sont usagers réguliers d'internet et 80,3% disposent d'un compte sur les réseaux sociaux [START_REF]We are social, Hootsuit. Digital 2022: another year of bumper growth[END_REF]. La transformation numérique de la société et la reconfiguration des interactions sociale qui l'accompagne ont entraîné dans leur mouvement une évolution des modalités d'aide à distance.

En effet, si les espaces sociaux digitaux viennent avec leur cortège de risques nouveaux ou augmentés, ils offrent également des leviers inédits pour surmonter les barrières traditionnelles de la recherche d'aide : omniaccessibilité spatiale et temporelle, gratuité, anonymat, immatérialité ou encore impression de contrôle des interactions [START_REF] Notredame | Leveraging the Web and Social Media to Promote Access to Care Among Suicidal Individuals[END_REF][START_REF] Lille | Prendre soin des jeunes suicidaires jusque sur les réseaux sociaux : le projet Elios[END_REF].

Capitalisant sur ces leviers, plusieurs PADS ont développé un espace tchat où les bénévoles et intervenants peuvent interagir en ligne avec les personnes qui les sollicitent. D'autres ont opté pour immersion encore plus complète dans l'écosystème numérique de leur public. C'est par exemple le cas de Fil Santé Jeunes qui a noué un partenariat avec le jeu vidéo Habbo pour proposer un espace d'échange de proximité sous la forme d'un bus virtuel [START_REF] Santé | Fil Santé Jeunes sur Habbo[END_REF].

Dans la même perspective, mais davantage dans le champ de la prévention professionnelle à distance, le CHU de Lille porte un projet de mise à disposition d'une équipe de web-cliniciens (infirmiers et psychologues) joignable directement depuis les réseaux sociaux par les adolescents et jeunes adultes en détresse. Baptisé Elios, ce projet est fondé sur le postulat selon lequel il est aujourd'hui plus facile pour les jeunes en souffrance d'établir un premier contact avec des ressources d'aide en passant par les réseaux sociaux que par téléphone ou en prenant un rendez-vous en personne [START_REF] Lille | Prendre soin des jeunes suicidaires jusque sur les réseaux sociaux : le projet Elios[END_REF]. En s'appuyant sur un système numérique spécialement développé, le dispositif aura vocation à fonctionner comme un portail digital dynamique vers les soins de santé mentale. Initialement implémenté dans le cadre d'un essai contrôlé randomisé, Elios pourrait être généralisé, en cas d'efficacité prouvée, comme un dispositif de prévention universelle.

Conclusions

  Direction Générale de la Santé (DGS) a confié à Santé Publique France (SPF) le financement et le pilotage de 16 associations d'aide à distance, dont 5 participent directement ou significativement à la prévention du suicide 1 . Ce pilotage a donné lieu à une réorganisation collaborative des dispositifs d'aide à distance passant notamment par l'homogénéisation et la généralisation des modalités d'évaluation, l'harmonisation d'une partie des formations, la mise en place d'un processus de labellisation et la modernisation des outils de recueil de données et d'orientation [8]. Par ailleurs cette consolidation méthodologique s'est accompagnée d'une évolution conceptuelle, les lignes de « téléphonie sociale » devenant successivement « ligne de téléphonie en santé » puis « dispositifs de prévention et d'aide à distance en santé » (PADS) afin de prendre en compte leur adossement quasi-systématique à un site internet d'information et de ressources [8].

  De façon schématique, tout patient sortant d'un centre d'inclusion VigilanS (urgences hospitalières ou service de soins) se voit remettre une carte-ressource sur laquelle figure un numéro de téléphone joignable en journée les jours de semaine. Il reçoit par ailleurs une fiche d'information lui rappelant le déroulement de la veille ainsi que ses droits. En cas de difficulté, il peut alors trouver assistance auprès d'une équipe de professionnels, infirmiers et psychologues sous supervision médicale, formée à l'intervention de crise téléphonique. Dans le cas où la tentative de suicide ayant motivé l'inclusion n'était pas la première, un appel proactif systématique est organisé entre J10 et J20 afin de prendre des nouvelles du patient. Si ce dernier reste injoignable, ou si un surcroit de sollicitude est jugé nécessaire, une carte postale personnalisée lui est envoyée chaque mois pendant quatre mois. En parallèle, l'équipe VigilanS assure un travail de mobilisation de l'entourage personnel et professionnel de la personne afin de tisser autour d'elle un réseau de veille actif.Placée sous la coordination d'une mission d'appui basée au CHU de Lille, la généralisation de VigilanS sur l'ensemble du territoire national a été inscrite dans la feuille de route de la Santé Mentale et de la Psychiatrie 2021 du ministère des Solidarités et de la Santé[21], puis réaffirmée à l'occasion du Ségur de la Santé. Elle devrait être effective d'ici la fin 2022. Depuis son lancement, près de 110 000 personnes ont d'ores et déjà bénéficié du dispositif, avec des premiers résultats concluants. Une étude de cohorte historique comparant 3 068 suicidants inclus dans VigilanS à 3 694 suicidants contrôles retrouvait ainsi un risque de réitération suicidaire divisé par presque 5 dans le premier groupe[START_REF] Plancke | Effectiveness of a French Program to Prevent Suicide Reattempt (VigilanS)[END_REF]. De façon concordante, dans le Nord -Pas-de-Calais, les trois années qui ont suivi la mise en place de VigilanS ont également connu une baisse de mortalité par suicide de près de 10% en comparaison des trois années antérieures[START_REF] Duhem | Premières analyses de mortalité par suicide en Nord-Pas-de-Calais depuis l'implantation de VigilanS[END_REF]. Le 3114, numéro national de prévention du suicide En 2016, le Haut Conseil de Santé Publique, dans son évaluation du plan d'action contre le suicide 2011-2014, faisait écho aux aspirations de plusieurs experts et acteurs de la prévention en recommandant la mise en place d'une ligne téléphonique professionnelle dédiée, aux côtés des PADS [4]. Préfigurée dans une instruction de 2019 de la DGS relative à la stratégie multimodale de prévention du suicide, cette mise en place a finalement été accélérée à la faveur de l'épidémie de Covid-19. Après appel à projet sur cahier des charges, elle a été confiée en février 2022 au CHU de Lille, qui s'est associé à plusieurs partenaires pour se constituer en « Pôle national ». Le déploiement du « Numéro national de prévention du suicide » (2NPS), rapidement devenu « 3114 », a été conçu selon un modèle décentralisé à travers l'implantation de centres régionaux (CR) sur l'ensemble du territoire, outre-mer compris. Sa structuration a d'emblée été organisée autour d'une double valence : 1. Un service de recours à distance destiné aux personnes en détresse, inquiètes pour un proche, et aux professionnels. L'objectif est de couvrir l'ensemble du spectre du processus suicidaire, depuis l'émergence des premières idées jusqu'au risque imminent de passage à l'acte en passant par la postvention individuelle. Comme pour VigilanS, ce service est assuré par des infirmiers et psychologues spécialement formés, alors qualifiés de « répondants ». Gratuitement accessible 24h/24, 7j/7 en tout point du territoire, le 3114 vise à offrir à tout appelant un accueil soucieux de la qualité du lien relationnel, une évaluation stratégique articulée autour de l'urgence suicidaire, une intervention proportionnée (conseil, information, désescalade émotionnelle, envoi de secours) et une orientation adaptée aux besoins vers les services sanitaires, médicosociaux, sociaux ou associatifs pertinents. 2. Un acteur territorial au service de la prévention du suicide. Incarnée par le médecin responsable, un chargé de réseau et un assistant de service social, chaque CR dispose d'une mission propre d'ancrage à l'écosystème loco-régional de la prévention du suicide, d'articulation aux actions et dispositifs déjà déployés, de stimulation et d'intégration dans le cadre des stratégies régionales pilotées par les ARS. Une attention particulière est portée à l'accessibilité du 3114, notamment aux personnes porteuses d'un handicap, ainsi qu'à la réduction des inégalités sociales et territoriales de santé.

Figure 1 .

 1 Figure 1. Évolution du nombre moyen d'appels reçus au 3114 depuis son ouverture, le 1 er octobre 2021. La ligne jaune représente un lissage de la courbe par régression polynomiale locale. Elle est accompagnée de son erreur-type (ombre jaune).

  Ancrée de longue date dans la prévention du suicide française, l'aide à distance connaît depuis moinsde 10 ans une accélération de son développement et de sa diversification. Depuis la mise en place de VigilanS et du 3114, c'est une structuration autour de deux modalités de cette aide qui s'organise, l'une associative, l'autre professionnelle. Si chacune de ces modalités dispose de caractéristiques, de valeurs et de principe d'action qui font leur identité et guide leur action (voir Tableau I), il reste à dégager les conditions de leur mise en synergie et de leur articulation. La multiplicité des déterminants des conduites suicidaires et la variété des expressions et besoins en lien avec la souffrance psychique plaide pour la préservation de la richesse de l'écosystème de l'aide à distance. Cette richesse pose néanmoins des défis d'ampleur pour soutenir une prévention du suicide stratégique, opérante et coordonnée : comment offrir à la population une lisibilité suffisante du panel des offres disponibles ? Comment se saisir pleinement et de façon collaborative des possibilités nouvelles qu'offrent le numérique ? Quelles articulations avec les soins et les associations n'agissant pas directement dans le champ de la prévention du suicide ? Enfin, et surtout, comme l'aide à distance peut-elle se mettre au service d'un perspective globale de prévention du suicide en soutenant l'ensemble des autres actions et dispositifs qui la constituent ? Tableau I. Comparaison des principales caractéristiques des dispositifs de prévention du suicide et d'aide à distance en santé et des dispositifs professionnels de prévention du suicide à distance. prévalents -Anonymat -Non-directivité -Non-jugement et neutralité -Confidentialité -Pro-activité -Inquiétude et souci de l'autre