Yoann Blein
email: yoann.blein@imag.fr

Yves Ledru
email: yves.ledru@imag.fr

Lydie Du-Bousquet
email: lydie.du-bousquet@imag.fr

Roland Groz
email: roland.groz@imag.fr

Extending Specification Patterns for Verification of Parametric Traces

Keywords: Software and its engineering → Specification languages, Formal software verification, Runtime Verification, Parametric Events, Temporal Specification, Trace Analysis

This article proposes a temporal and parametric specification language (ParTraP) developed for the verification of execution traces. The language extends specification patterns with nested scopes, real-time and first-order quantification over the data inside a JSON trace, while remaining pragmatic. Its design was directed by a case study in the medical field (computer aided surgery). The paper briefly presents the case study and details the design rationale, syntax and semantics of the language. The language has been implemented and several properties have been successfully evaluated over a corpus of 100 surgery traces.

INTRODUCTION

Numerous industrial fields (air and space, transportation, energy, . . . ) have made significant progress in the last decades in order to improve the quality of their systems and software. Although formal methods appear as a way to achieve high quality, their adoption is limited to critical applications. Daniel Jackson and Jeannette Wing have advocated the adoption of lightweight formal methods [START_REF] Jackson | Lightweight Formal Methods[END_REF]. Runtime Verification of execution traces appears as one way to achieve such a transition. In this paper, we report on the design of a trace specification language in the context of the design of Medical Devices, which provide support for complex medical surgeries. Fortunately, these systems can easily be instrumented to provide execution traces enabling us to observe their usage in the field.

In this work, we consider traces of surgical operations. They record the surgery workflow, the inputs captured from sensors and the interactions with the surgeon. The verification of execution traces will serve the following purposes: verify the correctness and the robustness of an implementation when used in real conditions, validate the hypotheses made on the environment and the conditions of use of a device, and understand the device usage in a perspective of product improvement.

One of the main challenges is to make trace properties writable by software engineers with no training in formal methods and readable by domain experts. For this purpose, we are developing ParTraP, a language dedicated to property specification for finite traces. The language extends the specification patterns originally proposed by Dwyer et al. [START_REF] Matthew | Patterns in Property Specifications for Finite-State Verification[END_REF] with parametrized constructs, nested scopes, real-time and first-order quantification over the data inside a JSON trace. A prototype interpreter has been implemented and experimented on traces provided by our industrial partner.

Section 2 motivates the need for a parametric language for property specification by presenting our industrial case study. We introduce the ParTraP language by giving an overview of its major features and some real-world examples in section 3. Section 4 formally describes the semantics of ParTraP and section 5 discusses a prototype implementation of the language. Finally, we discuss related work in section 6 and draw conclusions in section 7.

CONTEXT AND MOTIVATION

This work originates from an industrial collaboration aimed at pushing runtime verification techniques into the Medical Devices industry. After briefly presenting the case study, we describe the trace format in use and illustrate the nature of the requirements.

Case Study Presentation

The case study focuses on a computer assisted guidance system for total knee arthroplasty: TKA, designed by the BlueOrtho company for Exactech implant manufacturer. Total knee arthroplasty is a surgical procedure that involves replacing parts of the knee with a prosthesis. To install the prosthesis, it is necessary to cut off parts of the tibia and the femur. TKA helps the surgeon achieve these cuts with the required precision, through the supervised installation of cutting guides at the "right" position. The position of cutting guides is automatically computed on the basis of several measurements performed by the surgeon using the sensors of TKA, and of additional parameters chosen by the surgeon. This system is currently used worldwide and thousands of surgeries have been conducted with it. TKA consists of several components: a computer able to communicate with the surgeon via a touch screen, a stereoscopic camera, a set of sensors, named trackers, that can be localized in 3D by the stereoscopic camera, and a set of mechanical instruments to attach trackers and cutting guides to the bones of the patient. Fig. 1 shows several trackers, during a tutorial session, using a fake skeleton. The "trackers" have a diamond shape with four blinking LEDs. The stereoscopic camera is synchronized with the LEDs and is able to capture the 3D position, and the orientation of the tracker. The "pointer" is a hand-held tracker whose length has been calibrated. The surgeon uses the pointer to acquire the position of anatomic points of the patient. The other trackers are mechanically attached to the bones, so that they provide a reference when placing the cutting guides.

The surgery process involves a sequence of steps to be performed by the surgeon. The nature of these steps and the order in which they are performed are, to some extent, configurable. In every case, the sequence of steps takes the following macroscopic form: sensor calibration, acquisition of anatomical points using the pointer, check of acquisitions, adjustment of target parameters, positioning of the cutting guides, bones cut, and finally, digitization of the performed cut.

Traces

BlueOrtho systematically collects the logs of performed surgeries. Each log is composed of a sequence of about 3000 parametric events. The nature of these events is very diverse and includes hardware events (communication with the sensors), user input or complex computation results. They carry values of various types: numeric values, lists, 3D points. . . To this day, the company has collected a corpus of about 10 000 traces of surgeries that took place in real conditions.

At the conceptual level, a trace is viewed as a timed sequence of events. Each event is characterized by a name and a set of named parameters. Those parameters can be simple literals such as strings, or compounds values such as records. The original traces are mainly textual and poorly structured. Therefore, original traces are transformed into JSON files, where the top-level element is an array of objects, representing events. Each object must include the "time" and "name" keys, and may have other parameters.

Fig. 2 shows a simplified example of such a trace. The first event registers a tracker of type F (attached to the Femur), whose id is 0. This event took place at time 5. The second event declares that the current surgery needs trackers P and F. The third event corresponds to the registration of the P tracker (P stands for Pointer). The fourth event records the beginning of the acquisition phase. During this phase, the coordinates of the medial and the lateral malleolus are recorded (at times 9 and 20). Also, from 14 to 16, the pointer is replaced by another pointer which is registered and then activated.

[ ... {" time ": 5 , " name ": " RegisterTracker " , " type ": " F " , " id ": 0 } , {" time ": 6 , " name ": " SearchTrackers " , " types ":

[" P " , " F "]} , {" time ": 7 , " name ": " RegisterTracker " , " type ": " P " , " id ": 1 } , {" time ": 8 , " name ": " StartAcquisitions "} , {" time ": 9 , " name ": " MedialMalleolus " , " point ":

[0.5 , 1.0 , 0.8] } , ... {" time ": 14 , " name ": " ReplaceTracker " , " id ": 1 } , {" time ": 15 , " name ": " RegisterTracker " , " id ": 2 , " type ": " P " } , {" time ": 16 , " name ": " ActivateTracker " , " id ": 2 } , ... {" time ": 20 , " name ": " LateralMalleolus " , " point ": [0.6 , 0.9 , 0.9] } ... ]

Requirements for a Trace Property Language

To design a property specification language accessible to engineers with no training in formal methods, we gathered a corpus of properties that BlueOrtho developers would like to verify on the traces produced by TKA. These properties come from three sources: interviews with BlueOrtho developers, reviews of the technical specification documents of TKA, and reviews of some usual and unusual existing traces. Usual traces correspond to surgeries which followed the expected process, and where no problem was reported.

Unusual traces were mainly identified after a report of the surgeon, signalling that something went wrong during the surgery. These reports and the associated traces are analysed by the Blue Ortho engineers. Traces help understand what went wrong during the surgery, and what was the cause of the problem. For example, this analysis may reveal that the camera was positioned on the same side of the patient than the knee being cured (see property 1). The resulting corpus is composed of about 50 properties. They include constraints on event ordering, invariant checking on 3D points and soft real-time constraints. The following examples illustrate some types of properties found in this corpus.

Runtime Property 1. If the medial malleolus is further away from the camera than the lateral malleolus, a warning is issued within 100 milliseconds.

The inversion of malleolus distances could reveal that the 3D camera was installed on the wrong side of the patient (the one of the leg being cured). This property requires the occurrence of a warning event in response to the observation of a set of events that fulfills a predicate. Also, this response is bounded in time and the two malleolus events may happen in any order. Note that geometric computation is out of scope of the language, and we assume that functions such as 3D euclidean distance are defined externally. Runtime Property 2. A replaced tracker is no longer used until it is registered again.

The system should no longer try to use a tracker that is not currently registered. Trackers registration, replacement and usage can be observed through the events RegisterTracker, Replace-Tracker and ActivateTracker, respectively. Each tracker has a unique identifier that appears as parameter in all those events. Runtime Property 3. All the necessary trackers are detected before starting the acquisitions.

To proceed, the system requires a set of trackers which depends on the profile in use. This set is logged in the parameters of the SearchTrackers event. Each of these trackers should be detected at least once before starting the acquisitions. The set of required trackers may be modified during the surgery (according to the selected profile) and, upon search for the new set, any tracker already detected should not be detected again.

As said previously, we identified about 50 such properties during the requirements analysis. Considering this corpus, we conclude that the specification language should have at least the following properties:

Parametric From the example properties, one can notice that using event parameters is necessary. For instance, Runtime Property 3 relies on a list of values given as parameter of events SearchTrackers. Moreover, it should be possible to access the values of structured parameters such as list and records. Temporal The three example properties constrain the occurrence and ordering of events. Most of the properties from the collected corpus also have this trait. Timed A few properties from the corpus, such as Runtime Property 1, refer to physical time. Although time can be treated as regular data, a first class support for it can help write properties that are easier to understand and more efficient to process.

LANGUAGE FEATURES

ParTraP (Parametric Trace Property language) is a new property specification language for finite parametric traces, designed to meet the properties stated in the previous section. Although it was mostly influenced by the specification patterns proposed by Dywer et al. [START_REF] Matthew | Patterns in Property Specifications for Finite-State Verification[END_REF], it differs from them by being event-based, featuring parametric events, allowing nested scopes and providing timed properties.

In spite of the inspiration from specification patterns, the language does not restrict properties to pairs composed of a scope and a pattern. Instead, most of the property expressions are built on top of other properties, and can be freely nested. The inner property and the outer part are always separated by commas. Nested properties are evaluated from the outermost property towards the innermost. This is important since each one may modify the evaluation environment that will be used to evaluate any inner property. This mechanism allows relating different events, possibly according to their parameters.

Events Descriptors

Event descriptors allow matching events from a trace. At the simplest, events are designated by their name, such as in absence_of A where A is the name of the event. Additionally, an event can be bound to a variable x as in A x. In this case, it is also possible to add a condition on the event thanks to the where construct: A x where c. This expression describes the set of events having the name A and fulfilling the condition c when bound to the variable x.

It is also possible to designate an unordered collection of events with the set construct: set(E1 x1, ..., En xn) where c. This event set will be triggered after seeing all of the events E1. . . En in any order, provided that they respect the guard c when E1. . . En are bound to x1. . . xn, respectively.

Temporal Properties

3.2.1 Scopes. The range of a trace where a property should hold can be restricted through scopes. In the absence of such construct, a property must hold on the whole trace. Scopes are delimited by events and, as properties themselves, can be nested. If the event delimiting a scope never occurs, the scope does not exist and the whole property is considered satisfied. Scopes can be classified according to their arity, i.e. the number of events they involve. Unary scopes, illustrated in Fig. 3, are the building blocks of the language.

All scopes are strict, i.e., delimiter events are not included in the interval they define. The "each" variants may describe several intervals and happen to be useful combinators. For instance, we can express that the property P should be true for all the segments of a trace between an event A and an event B by nesting two scope expressions: after each A, before first B, P. For convenience, we included this scope in the language as between A and B, as well as its weak variant since A until B. Those two binary scopes are illustrated in Fig. 3 being defined on top of nested scopes, the event delimiting the end of a binary scope may depend on the one starting it. Scopes implicitly extend the evaluation environment for the inner property with all the events that are associated to a variable name. For instance, the property after first A v where v . x != 0 , P will evaluate P on the scope starting after the first event A with a non-zero x parameter, and in an environment where the value of the variable v is this first event. This is especially useful with the each variants of after and before as the sub-property to verify may depend on the events delimiting each scope. For instance, the following ParTraP property encodes the fact that each entered state should be exited eventually:

after each EnterState e , occurrence_of ExitState x where e . state == x . state By delimiting the range of a trace where a property should hold, and providing access to the parameters of a delimiter event at the same time, scopes allow to concisely express temporal properties.

Patterns.

The only mandatory components of properties are patterns. They rule the occurrences of events in a trace. There are two unary patterns: occurrence_of n A, where n is optional, and its dual absence_of A. The first one requires the occurrence of at least n events A in the current range of the trace. If n is omitted, it defaults to 1. The second one simply prevents an event from occurring. As usual, the event descriptor A may be bound to a variable and filtered with the where construct.

Following Dwyer's specification patterns, the language also includes the response pattern A followed_by B and the precedence pattern A precedes B. The first one requires an occurrence of the event 𝐵 after each occurrence of an event 𝐴, while the second one prevents the event 𝐵 from occurring until the event 𝐴 occurs (but 𝐴 may occur without 𝐵). The language also features another convenient pattern: A prevents B, which prevents any occurrence of the event 𝐵 after an occurrence of the event 𝐴. Note that the three binary patterns are later defined as combinations of scopes and unary patterns. A direct consequence is that the event descriptor on the right-hand side may depend on the event matched on the left-hand side.

Timed Variants.

Unary scopes and binary patterns may be additionally constrained by a duration expressed in common time units.

Unary scopes can be prefixed with the within keyword and a duration expression, like in the property within 2 ms before each A , absence_of B

The inner property only has to hold for the given duration starting immediately at the delimiter event for the after scope, or ending exactly at the delimiter event in the before case. In the previous example, the event 𝐵 should not occur during the two milliseconds preceding any occurrence of an event 𝐴.

Binary patterns may also be extended with a suffix and a duration expression. For instance, the response pattern becomes bounded in time: A followed_by B within 2s.

Non-Temporal Properties

3.3.1 Quantifiers. The trace format allows compound values in event parameters. In particular, they can be lists of values. The language allows exploiting them through quantified properties.

The universal quantifier takes the following form: forall a in L, P, where a is an identifier and L is a list. For each value in L, P must be satisfied in an environment where a is bound to that value. The existential quantifier exists is also defined as usual.

Since quantified properties are themselves properties, they can be arbitrarily nested. In particular, it is convenient to use a quantifier inside a scope property: if a parameter of the event delimiting the scope is a list, it can be used as a quantification domain.

Event

Selection. The only way to extract the parameters of an event so far is to bind the event in a scope. However, the associated restriction of the trace range might not be wanted.

The given expression takes the same syntactic form as scopes, i.e. suffixed with an occurrence specifier (first, last or each) and an event descriptor. It wraps another property that will be evaluated in an environment extended with the selected event. In the each case, the property must be true for all events matching the event descriptor. Like scopes, a property constructed with given will be true if no event matches the descriptor.

Examples

Let us illustrate the language features by formalizing the examples introduced in subsection 2.3. Runtime Property 1 can be expressed as follows:

set ( LateralMalleolus l , MedialMalleolus m )
where norm ( m . point ) > norm ( l . point ) followed_by WarningMalleolusInverted within 100 ms This expression states that any unordered pair of misplaced malleolus events should result in a warning.

Runtime Property 2 simply combines a since/until scope delimiting the range of a trace where a specific tracker is replaced, with an absence pattern preventing the activation of this tracker: This expression captures the property concisely by combining four constructs: a past scope, an event selector, an universal quantifier and a pattern.

LANGUAGE SEMANTICS

This section formalizes the semantics of ParTraP. It is defined in terms of inference rules over traces instead of translating it into an existing formalism because there is no well-established formalism for parametric specification.

For space reasons, we describe the semantics of all ParTraP constructs except events sets. This construct adds a layer of complexity but does not change the global shape of the semantic rules. The simpler and shorter version presented here is close to the complete rules, which can be found in the language reference [START_REF] Blein | MODMED WP1/D1: Preliminary Definition of a Domain Specific Specification Language[END_REF]. The additional complexity mainly comes from the two following points:

(1) Contrary to single events, events sets last in time; scopes must be updated accordingly. (2) The first and last events sets matching a set description must be defined carefully. Some elements of the language such as the where clause rely on predicate expressions. Since the language producing those expressions is orthogonal to the definition of ParTraP, we will not specify it here. Instead, we will assume that any well-typed expression 𝑒 can be evaluated in the environment 𝜂 to the value 𝑣 with the judgement form 𝜂 ⊢ 𝑒 ↓ 𝑣.

Additionally, we require this language to provide at least an infix "." operator allowing to access the fields of a record, as in record.field. Such a construct is necessary to inspect the parameters of an event.

Preliminary Definitions

We use 𝑋 → 𝑌 and 𝑋 ⇁ 𝑌 to denote sets of total and partial functions from 𝑋 to 𝑌 , respectively. We write maps (partial functions) as [𝑥 0 ↦ → 𝑣 0 , . . . , 𝑥 𝑖 ↦ → 𝑣 𝑖 ] and the empty map as [ ]. We note 𝑚[𝑦 ↦ → 𝑣] the map which is the same as 𝑚 except that the mapping for 𝑦 is updated to refer to 𝑣:

𝑚[𝑦 ↦ → 𝑣] (𝑥) = 𝑣 if 𝑥 = 𝑦 𝑚(𝑥) otherwise.
If 𝑍 is a set, let 𝑍 * be the set of finite sequences of elements of 𝑍 .

Equipped with these notations, we may now formalize the traces content and format. The set of values is the smallest set Val such that:

(

↦ → 𝑣 1 , . . . , 𝑓 𝑖 ↦ → 𝑣 𝑖 ] is a value.
An environment is a map from variable names to values:

Env = Var ⇁ Val,
where Var is a set of variable names. An event is characterized by a name, an occurrence time and a set of named parameters. Formally an event is defined as a triplet:

Event = Σ × N × (𝑃 ⇁ Val),
where Σ and 𝑃 are finite sets of event names and parameter names, respectively. Note that this definition permits events to have the same name and yet different parameters. This provides more flexibility with the input traces and allows, for instance, to have optional parameters. For convenience, we define the three following projections on an event 𝑒 = ⟨𝜎, 𝑡, 𝑝⟩: name(𝑒) = 𝜎, time(𝑒) = 𝑡 and param(𝑒) = 𝑝.

Finally, a trace is a sequence of events (𝑒 𝑖 ) 𝑛 𝑖=1 with non-decreasing occurrence times. We can formally define the set of possible traces as follows:

Trace = { (𝑒 𝑖 ) 𝑛 1=𝑖 ∈ Event * | ∀𝑖 ∈ 1 . . 𝑛-1, time(𝑒 𝑖 ) ≤ time(𝑒 𝑖+1 ) }.
In the following, traces are also denoted as 𝜏 when the indices are irrelevant.

Events Extraction and Time Slicing

Finding events that satisfy some constraints expressed in ParTraP properties is a basic necessity to define the semantics of the language. We first introduce a dedicated function that handles that matter. The semantic rules of ParTraP are built upon that function and focus on the temporal aspect.

The function 𝑀 computes the events of a trace that match an event description with a name and a condition on the event, and respect an occurrence specifier, i.e. an element of {first, last, each}. More precisely, given a trace (𝑒 𝑖 ) 𝑚 𝑖=1 , 𝑀 ((𝑒 𝑖 ) 𝑚 𝑖=1 , 𝜎, 𝑥, 𝑐, 𝜂, 𝑜) is the set of indices 𝑖 of the trace such that:

• 𝑒 𝑖 has the name 𝜎,

• the condition 𝑐 evaluates to true in the environment 𝜂 extended with 𝑥 associated to 𝑒 𝑖 , and • 𝑒 𝑖 respects the occurrence specifier 𝑜. This set can be computed in two steps: finding 𝑀 desc , the set of all the indices that match the event description, and then selecting the ones that respect the occurrence specifier. The definition of the function 𝑀 is based on that idea:

𝑀 ((𝑒 𝑖 ) 𝑚 𝑖=1 , 𝜎, 𝑥, 𝑐, 𝜂, 𝑜) =              𝑀 desc if 𝑜 = each {min 𝑀 desc } if 𝑜 = first and 𝑀 desc ≠ ∅ {max 𝑀 desc } if 𝑜 = last and 𝑀 desc ≠ ∅ ∅ otherwise
where

𝑀 desc = { 𝑗 ∈ 1 . . 𝑛 | name(𝑒 𝑗 ) = 𝜎∧𝜂 [𝑥 ↦ → param(𝑒 𝑗 )] ⊢ 𝑐 ↓ true}.
𝑀 desc is the result of the first step, i.e. it is the set of indices that match the event description given by the name 𝜎 and the condition 𝑐.

The subset of 𝑀 desc that is actually returned is computed according to the occurrence specifier 𝑜. For instance, if 𝑜 = first, only the minimal index in 𝑀 desc is returned, which indeed corresponds to the first event of the trace that matches the description.

We also need the ability to slice a trace according to a time limit. If (𝑒 𝑖 ) 𝑚 𝑖=1 is a trace and 𝑙 a natural, the function upto((𝑒 𝑖 ) 𝑚 𝑖=1 , 𝑙) = (𝑒 𝑖 )

max( { 𝑗 ∈ [1..𝑚] | time(𝑒 𝑗 ) < 𝑙 } ∪ {0}) 𝑖=1
slices the trace (𝑒 𝑖 ) 𝑚 𝑖=1 from its beginning and up to the time limit 𝑙. The union with the singleton {0} in the upper bound ensures that an empty sequence is returned if there are no events occurring before the time limit.

Semantic Rules

Properties are evaluated over finite traces and in a specific environment. The satisfaction relation between a trace 𝜏, an environment 𝜂 and a property 𝑝 is the smallest relation 𝜏 𝜂 𝑝 satisfying the 8 rules given in Fig. 4. We say that a trace 𝜏 satisfies a property 𝑃 when 𝜏 [ ] 𝑃.

The semantics of the original pattern system proposed by Dwyer et al. was given through translation rules manually defined for each pair of pattern and scope. Because of the number of combinations, there are numerous rules and they have been shown to be inconsistent by Taha et al. [START_REF] Taha | A compositional automata-based semantics and preserving transformation rules for testing property patterns[END_REF]. Since ParTraP scopes can be arbitrarily nested, the number of combinations is infinite and defining an exhaustive set of rules is impossible. Instead, the satisfaction relation is defined through recursive rules derived from its informal meaning, and where each rule only handle a single construct.

The first three rules are straightforward. The next one, Forall, handles universally quantified properties by first evaluating the expression that represents the quantification domain, and then evaluating the subsequent property for all values in that domain. The rule Occ asserts the occurrence of a particular event description by measuring the size of 𝑀, i.e. counting the number of events that match this description in the current trace, and checking that is is greater than the computed value of 𝑛 𝑒 . The rules for the after scope are Aft and AftT for its timed variant. They rely on the results of the 𝑀 function to slice the trace after the end of each event set matching the description and to update the evaluation environment. Additionally, AftT evaluates a duration expression and slices the trace so that it lasts at most for this duration. The rule for the given expression is the same as Aft without slicing the trace. The rules Bef and BefT for the before scope are not given here for space reasons. They are symmetrical to Aft and AftT, respectively.

The previous rules allow defining the additional logical expressions with the usual identities:

• (between 𝐴 and 𝐵, 𝑃) and (after last 𝐵, after first 𝐴, 𝑃) When events that are not explicitly associated to a variable name, they are bound to the empty variable name. Finally, omitted where conditions on events default to true.

IMPLEMENTATION AND VALIDATION

We implemented a trace verification tool based on the proposed language. It is written in Haskell and freely available online 1 . It checks the conformance of JSON-formatted traces to property expressions. All the proposed features have been implemented. However, the expressions allowed in where clauses are currently limited to simple boolean and arithmetic expressions along with access to event parameters. We plan to complete them with a foreign function interface to call routines written in Python, which is well suited for data manipulation and numeric computations.

Since we are performing offline verification only, we consider complete execution traces and not a prefix of them as in online monitoring. Having access to a full trace allows exploring it back and forth and not just sequentially. A direct consequence is that it is possible to interpret properties naively, in the sense that an interpreter may follow their syntactic structure. For instance, to check the property before first A, P, the interpreter may simply process the input trace forward, looking for an event A, and then process the trace until A again to check for P. This approach avoids the typical bookkeeping overhead of parametric monitoring and performs well in our context. For instance, verifying the moderately complex Runtime Property 3 on a trace of 11 120 events takes 202.63 µs on a first generation mobile Intel Core i5 (M520). This result does not include trace parsing, which account for about 6 ms. We used the ParTraP interpreter to verify a dozen properties over the same corpus. Those properties encode requirements for TKA, hypotheses made on the device usage or usage queries. No errors were found in TKA software, but we discovered abnormal events and suspicious behaviors in the usage of the system. For instance, the periodically reported temperature of the 3D camera occasionally reaches the extreme value of -273. It is the result of a failure when querying the temperature sensor. Although not critical, this error illustrates an issue between the software and its execution environment.

Using a temporal usage query we also noticed that for 11 % of the traces in the corpus, the user performs an action within less than 100 ms after a new screen is displayed. Even experienced users could miss information in such a short time. After further investigation, the manufacturer attributed this issue to a defect in the pointer device or a poor handling of that same device. This defect is not critical because the surgeon may always go back to the missed screen.

RELATED WORK

We first present several specification formalisms classified by style and then offer some elements of comparison with ParTraP.

Overview

6.1.1 Pattern Systems. An important challenge in the design of ParTraP was to make temporal specification accessible. A famous technique to assist users with finite-state verification is to provide high-level temporal patterns with a verbose syntax. Dwyer et al.

proposed a major step in that direction with a pattern system covering the temporal requirements of a very large study [START_REF] Matthew | Patterns in Property Specifications for Finite-State Verification[END_REF]. Those patterns are domain agnostic and relatively simple to use. Propel refines them with additional mandatory clauses which help to remove ambiguities due to the english-like syntax [START_REF] Smith | PROPEL: an approach supporting property elucidation[END_REF]. The Requirement Specification Language (RSL) is another pattern system with limited temporal relations but a high emphasis on real-time [START_REF] Damm | Using contract-based component specifications for virtual integration testing and architecture design[END_REF].

While being relatively easy to use, pattern systems have a severely limited expressiveness. The Salt language [START_REF] Bauer | SALT -Structured Assertion Language for Temporal Logic[END_REF] addresses that issue with composable patterns and common temporal operators behind a natural syntax. It features many constructs, ranging from timed temporal operators to star-free regular expressions. All those systems share a common limitation as a consequence of supporting finite-state verification: they do not support parametric events. 6.1.2 Temporal Logics. The Linear Temporal Logic (LTL) is a widely accepted temporal logic with a precise semantics [START_REF] Pnueli | The Temporal Logic of Programs[END_REF]. However, it targets infinite traces and its semantics is not adapted to runtime verification. Bauer et al. offer a formal treatment on adapting LTL for runtime verification, LTL 𝑓 , as well as its timed variant, TLTL 𝑓 , and discuss different trade-offs and their implications [START_REF] Bauer | Comparing LTL Semantics for Runtime Verification[END_REF][START_REF] Bauer | Runtime Verification for LTL and TLTL[END_REF]. The Counting Fluent Temporal Logic (CFLTL) is another interesting adaptation of LTL to event-based traces [START_REF] Regis | Specifying Event-Based Systems with a Counting Fluent Temporal Logic[END_REF]. It features a simple and powerful mean of counting event occurrences and comparing them. However, none of those adaptations support parametric traces.

To deal with parametric traces, many first order temporal logics have been proposed, most of them also deriving from LTL. Stolz introduced free variables and quantification in next-free LTL with parametrized propositions [START_REF] Volker | Temporal Assertions with Parametrised Propositions[END_REF]. FO-LTL + [START_REF] Hallé | Runtime Monitoring of Message-Based Workflows with Data[END_REF] is another approach adding quantification to LTL. It targets data-rich XML traces and events parameters may exhibit a hierarchical structure, similarly to ParTraP. Parameters can be accessed through quantifiers over a domain described with XPath queries. In spite of the additional capabilities, FO-LTL + retains the simplicity and conciseness of LTL.

However, we argue that the resulting elegance impairs pragmatism: the only way to access events is through quantification over their parameters. In consequence, single-valued parameters must also be quantified, which makes formulas harder to understand. Basin et al. proposed a semantics and algorithm for the Metric First Order Temporal Logic (MFOTL) [START_REF] Basin | Monitoring Metric First-Order Temporal Properties[END_REF] and implemented it with the MONPOLY tool [START_REF] Bversiooasin | MONPOLY: Monitoring Usage-Control Policies[END_REF]. They further extended MFOTL with SQL-like aggregation operators [START_REF] Basin | Monitoring of temporal first-order properties with aggregations[END_REF]. Eagle [START_REF] Barringer | Rule-Based Runtime Verification[END_REF] is a radically different and powerful temporal logic as it does not derive from LTL, but still encompasses it. This very succint logic also features parametric events and data quantifiers. Transitions are labelled with event descriptions and taken whenever a matching event is observed. Whereas pattern systems and temporal logics are declarative, FSM encode specifications in an operational style.

FSM are especially popular in the parametric trace slicing framework [START_REF] Chen | Parametric Trace Slicing and Monitoring[END_REF], where events are composed a name and a tuple of parameters. For instance, FSM constitute the core of the expressive Quantified Event Automata [START_REF] Barringer | Quantified Event Automata: Towards Expressive and Efficient Runtime Monitors[END_REF] and its efficient implementation MarQ [START_REF] Reger | MarQ: Monitoring at Runtime with QEA[END_REF]. Mufin [START_REF] Decker | Runtime Monitoring with Union-Find Structures[END_REF] also uses parametric trace slicing and relies exclusively on FSM. It is faster but less expressive than QEA/MarQ. 6.1.4 Rule-Based Systems. The use of rule-based systems for runtime verification has also received some interest. This model seems well suited for processing data rich events, as exemplified by the RuleR system [START_REF] Barringer | Rule Systems for Run-time Monitoring: from Eagle to RuleR[END_REF] or the more efficient Logfire [START_REF] Havelund | Rule-based runtime verification revisited[END_REF]. Rules take the form condition 1 , . . . , condition 𝑛 =⇒ action, where the conditions depend on a memory of facts and the action can add or remove facts, or yield a verdict. Constantly managing a database of facts through action rules makes rule-based system highly operational.

6.1.5 Hybrid. Some formalisms or monitoring tools support several specification styles.

LogScope [START_REF] Barringer | Formal Analysis of Log Files[END_REF] is a solution proposed in a context similar to the one of ParTraP. It targets offline verification for data-rich traces. LogScope is composed of a higher-level pattern language that compiles down to FSM, which can also be used to encode more complex properties. Despite some common characteristics with ParTraP, the higher-level language is different in many ways: its scoping mechanism is much more limited as there is a single scope (equivalent to our before first scope), quantification is completely implicit, time is not handled at language-level and specification of event sequences is much easier. This kind of two-levels systems have the advantage of providing a very simple high-level language. However, they also force the user to learn two formalisms, including a low-level one, often with different paradigms (e.g. declarative and operational for LogScope).

JavaMOP [START_REF] Jin | JavaMOP: Efficient parametric runtime monitoring framework[END_REF] also supports several formalisms, called "logics". It is another incarnation of parametric trace slicing, being famous for making it efficient. Contrary to the two-level hierarchy found in LogScope, logics in JavaMOP are not cleary ordered and complement each other.

6.1.6 Stream Computation. All the solutions presented so far check properties on the execution of a system by observing events or state changes of the system. Lola is a runtime monitor for synchronous systems which takes a radically different approach: specification are written as computations over the stream of values manipulated by a synchronous system. This unique approach allows specification to resemble a synchronous program. Besides checking logical properties, Lola also supports numeric queries over streams. Lola was specifically designed for synchronous systems and adapting it for event traces is not obvious. For this reason, we omit Lola in the rest of this section.

Comparison and Discussion

Comparing the expressiveness of various temporal specification formalisms is difficult. For instance, Reger and Rydeheard showed that the relationship betwen First-Order Linear Temporal Logic for finite traces and parametric trace slicing is not trivial [START_REF] Reger | From First-order Temporal Logic to Parametric Trace Slicing[END_REF]. Instead of establishing a formal relation between ParTraP and the aforementioned formalisms, we propose to compare several aspects that are important when writing specifications.

Parametric Events. Supporting parametric events was a critical requirement for ParTraP. Although pattern systems and adaptations of LTL for finite traces do not support parametric events, most temporal specification formalisms designed for runtime verification do.

Compound Values. Parametric events may carry compound values such as lists and records. To the best of our knowledge, only a few of the formalism presented previously, including ParTraP, support further inspection of compound values.

Local vs. Global Quantification. We can distinguish two types of quantification in formalisms for parametric monitoring. In global quantification the domain value of a quantified variable is defined as the values taken by this variable in a whole trace. On the contrary, in local the quantification domain of a variable may only depend on the current state. Local quantification is mostly useful in combination with support for compound values as it allows quantifying over lists that are carried as event parameters. While ParTraP and a few others uses local quantification, all approaches based on parametric trace slicing use global quantification.

Reference to Past Data. It is well-known that adding past operators to LTL does not increase its expressiveness [START_REF] Gabbay | On the Temporal Basis of Fairness[END_REF]. However, this result no longer holds when LTL is extended with quantifiers. To see why, consider the following informal specification: "for each value 𝑥 in the parameter 𝑝 1 of an event 𝑒 1 , there must be an occurrence of an event 𝑒 2 before 𝑒 1 and with a parameter 𝑝 2 equal to 𝑥" (this specification constitutes the core of Runtime Property 3). Because the occurrences of the event 𝑒 2 are constrained by the parameters of another event that is yet to occur, this property cannot be captured in a future-only LTL extended to first order. Monitoring such a property is expensive and many specification formalisms do not include past operators for efficiency and simplicity reasons. A possible approach -as taken in QEA [START_REF] Barringer | Quantified Event Automata: Towards Expressive and Efficient Runtime Monitors[END_REF] -is to explicitly store the data for future use, e.g. the set of values taken by the parameter 𝑝 2 . In ParTraP, there is no notion of past or future because properties

✓ ✓ local ✗ ✓ declarative MFOTL/MONPOLY ✓ ✗ global ✓ ✓ declarative JavaMOP ✓ ✗ global ✓ ✗ mixed QEA/MarQ ✓ ✗ global ✓ ✗ operational Mufin ✓ ✗ global ✓ ✗ operational Ruler ✓ ✗ n/a ✓ ✗ operational Logfire ✓ ✗ n/a ✓ ✗ operational LogScope ✓ ✓ global ✗ ✗ mixed ParTraP ✓ ✓ local ✓ ✓ declarative
are evaluated over whole slices of trace. In consequence, events and their data never belong to the past and always remain accessible.

The aforementioned specification can be formalised with ParTraP as demonstrated in the encoding of Runtime Property 3.

Language Support for Real-Time. Real-time support can be classified according to three levels: unsupported, supported as regular data, supported at language-level. We argue that supporting time at language-level is critical since it allows much clearer specifications and more efficient implementation thanks to the monotonicity of time. For instance, one can stop checking a bounded safety property once the time bound has passed.

Paradigm. Specification formalisms may be classified according to their paradigm: declarative or operational. Even if they both have their strengths, as exemplified by Havelund and Reger [START_REF] Havelund | Specification of Parametric Monitors[END_REF], we argue that an operational style introduces additional complexity for the user. For instance, in rule-based system each rule may impact the behavior of the others by adding or removing shared facts, which requires careful attention. This problem is similar to imperative code routines where side-effects interplay is often critical. ParTraP uses a declarative style to operate at a higher level.

Summary. Table 1 summarises the comparison between Par-TraP and the other specification languages mentioned previously. It appears from this table that ParTraP has a unique combination of features.

CONCLUSION

ParTraP is a specification language for parametric execution traces that is designed to be simple to use by software engineers thanks to a declarative style and a verbose syntax. Its development originated from an industrial cooperation with Medical Devices manufacturers. A large majority of the requirements of the studied system involves temporal constraints and data values. ParTraP allows formalising these requirements concisely, yet remaining readable. It was inspired by specification patterns and extends them with nested scopes, real-time and first-order quantification. Event parameters have a centric role and all ParTraP constructs may extract or exploit them.

A prototype implementation for verification of JSON traces is available online. This implementation has been used to verify several representative requirements for a medical device over a hundred surgery traces. It also showed promising results in spotting unusual behaviors of the system or the user.

Although ParTraP was developed in the context of offline runtime verification, we believe it could be adapted for online monitoring. This will require to rework the language semantics or remove some operators from the language. For example, constructs such as last may refer to different events while the trace is produced. Also, an absence_of property will only have a definitive verdict when the trace is completed (unless the events appears in the trace, falsifying the property). Moreover, intuitiveness and flexibility had higher priority than efficiency in the development of the language. While this is fine for offline verification, it may induce a significant overhead over the monitored system in the online case.

Although the design of ParTraP was driven by logs and requirements from the medical field, it is not specific to that particular field. The generation and gathering of execution traces is already a standard practice in many industries, but their systematic and automatic exploitation is not generalized. ParTraP should be transposable to any of them, and would be particularly useful for traces with complex structured data. We are currently working on a case study in the field of home automation, where traces include parametric information from sensors, and actions performed by the inhabitants and by the control system. At longer term, we have contacts with another medical devices manufacturer, and also envision log analysis of access control systems.

Finally, temporal specification in a flexible language remains delicate regardless of the efforts put into its ease of use. To help with this issue, we believe that the language should be complemented with tools to help writing and understanding properties. We are working on providing the means to analyze the verdict of ParTraP properties and to evaluate their coverage over a set of traces. In particular, we are studying the transformation of properties into disjunctive normal form, in order to measure the coverage of the sub-properties and get a finer understanding of the property.

Figure 1 :

 1 Figure 1: Pointer and trackers

Figure 2 :

 2 Figure 2: Example of JSON trace

Figure 3 :

 3 Figure 3: Graphical representation of scopes

Figure 4 :

 4 Figure 4: Operational semantics for property satisfaction

6. 1 . 3 Finite

 13 State Machines. Finite State Machines (FSM) form another popular specification formalism in runtime verification.

  Note that the event delimiting the end of the scope depends on the one starting it. If several trackers are replaced, the property will be enforced for all of them because of the since/until semantics (see Fig.3).Finally, Runtime Property 3 is captured by the following expression:

	since ReplaceTracker rep
	until RegisterTracker reg where reg . id == rep . id ,
	absence_of ActivateTracker act
	where act . id == rep . id
	before each StartAcquisitions ,
	given last SearchTrackers st ,
	forall type in st . types ,
	occurrence_of TrackerDetected td
	where td . type == type

  1) literals (booleans, integers, strings and floating-point numbers) are values; (2) if 𝑣 1 , . . . , 𝑣 𝑛 are values, then the sequence (𝑣 𝑘 ) 𝑛 𝑘=1 is a value; (3) if 𝑣 1 , . . . , 𝑣 𝑛 are values and 𝑓 1 , . . . , 𝑓 𝑛 are names, then the map, or record, [𝑓 1

  𝑃 1 and 𝑃 2 ≡ not (not 𝑃 1 or not 𝑃 2 ) • 𝑃 1 implies 𝑃 2 ≡ not 𝑃 1 or 𝑃 2 • 𝑃 1 equiv 𝑃 2 ≡ (𝑃 1 implies 𝑃 2 ) and (𝑃 2 implies 𝑃

1 ) • exists 𝑥 in 𝑒, 𝑃 1 ≡ not (forall 𝑥 in 𝑒, not 𝑃 1 ), and the additional temporal expressions: • absence_of 𝐸 ≡ not (occurrence_of 𝐸) • 𝐴 followed_by 𝐵 within 𝛿 ≡ within 𝛿 after each 𝐴, occurrence_of 𝐵 • 𝐴 precedes 𝐵 within 𝛿 ≡ within 𝛿 before each 𝐵, occurrence_of 𝐴 • 𝐴 prevents 𝐵 within 𝛿 ≡ within 𝛿 after each 𝐴, absence_of 𝐵 • between 𝐴 and 𝐵, 𝑃 ≡ after each 𝐴, before first 𝐵, P • since 𝐴 until 𝐵, 𝑃 ≡

  𝜏 𝜂 𝑃 1 𝜏 𝜂 𝑃 1 or 𝑃 2 DisjL 𝜏 𝜂 𝑃 2 𝜏 𝜂 𝑃 1 or 𝑃 2 DisjR 𝜏 𝜂 𝑃 𝜏 𝜂 not 𝑃 Neg 𝜂 ⊢ expr ↓ 𝐿 ∀𝑣 ∈ 𝐿, 𝜏 𝜂 [𝑥↦ →𝑣 ] 𝑃 𝜏 𝜂 forall 𝑥 in expr, 𝑃 Forall 𝜂 ⊢ 𝑛 𝑒 ↓ 𝑛 𝑛 ≤ |𝑀 (𝜏, 𝜎, 𝑥, 𝑐, 𝜂, each)| 𝜏 𝜂 occurrence_of 𝑛 𝑒 𝜎 𝑥 where 𝑐 Occ ∀𝑗 ∈ 𝑀 (𝜏, 𝜎, 𝑥, 𝑐, 𝜂, 𝑜), (𝜏 𝑖 ) 𝑖> 𝑗 𝜂 [𝑥↦ →param(𝜏 𝑗 ) ] 𝑃 𝜏 𝜂 after 𝑜 𝜎 𝑥 where 𝑐, 𝑃 Aft 𝜂 ⊢ 𝛿 𝑒 ↓ 𝛿 ∀𝑗 ∈ 𝑀 (𝜏, 𝜎, 𝑥, 𝑐, 𝜂, 𝑜), upto((𝜏 𝑖 ) 𝑖> 𝑗 , time(𝜏 𝑗 ) +𝛿) 𝜂 [𝑥↦ →param(𝜏 𝑗 ) ] 𝑃 𝜏 𝜂 within 𝛿 𝑒 after 𝑜 𝜎 𝑥 where 𝑐, 𝑃 AftT ∀𝑗 ∈ 𝑀 (𝜏, 𝜎, 𝑥, 𝑐, 𝜂, 𝑜), 𝜏 𝜂 [𝑥↦ →param(𝜏 𝑗 ) ] 𝑃 𝜏 𝜂 given 𝑜 𝜎 𝑥 where 𝑐, 𝑃 Given

Table 1 :

 1 Comparison of several temporal specification languages

	Language	Parametric Comp. Values Quantification Ref. Past Data Real-Time Paradigm
	Dwyer's Patterns	✗	n/a	n/a	n/a	✗	declarative
	Propel	✗	n/a	n/a	n/a	✗	declarative
	RSL	✗	n/a	n/a	n/a	✓	declarative
	Salt	✗	n/a	n/a	n/a	✓	declarative
	LTL 𝑓	✗	n/a	n/a	n/a	✗	declarative
	TLTL 𝑓	✗	n/a	n/a	n/a	✓	declarative
	CFLTL	✗	n/a	n/a	n/a	✗	declarative
	Eagle	✓	✗	global	✗	✓	declarative
	Stolz's Param. Prop. ✓	✗	local	✗	✗	declarative
	FO-LTL +

https://gricad-gitlab.univ-grenoble-alpes.fr/modmed/partrap

ACKNOWLEDGMENTS

This work is funded by the ANR MODMED project (ANR-15-CE25-0010). We also thanks our partners Arnaud Clère (MinMaxMedical) and Fabrice Bertrand (BlueOrtho) for the fruitful discussions about TKA and the design of software for medical devices.


Jean-Claude Bermond

A Germa

Marie-Claude Heydemann

Dominique Sotteau

Girth in digraphs

la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.


Cecilia Written

Darnault

Titouan Parcollet

Mohamed Morchid

Artificial Intelligence: A Tale of Social Responsibility

Keywords:

whether they are published or not. The documents may come   L'archive ouverte pluridisciplinaire

Introduction

Novel technologies and especially Artificial Intelligence (AI) paradigms induce a massive interest from researchers across different domains, and raise questions and concerns. Indeed, some "worries about the transformations and the possible destruction that could put in danger our world" [START_REF] Ganascia | Le Mythe de la Singularité[END_REF]; Krishnan 2016), while "others, convinced of the inevitability of the upheavals to come, seek to influence the movement to make this future livable" [START_REF] Ganascia | Le Mythe de la Singularité[END_REF]). In fact, AI "might be the most important transition of the next century either ushering in an unprecedented era of wealth and progress or heralding disaster" [START_REF] Wiblin | Positively shaping the development of artificial intelligence[END_REF]. The scientific community does not remain indifferent and warns AI-based systems users against the risks related to AI models and the manner that the models have been learned. For about ten years, experts warned that "if research continues to advance without enough work going into the research problem of controlling such machines, catastrophic accidents are much more likely to occur" [START_REF] Wiblin | Positively shaping the development of artificial intelligence[END_REF]. These concerns are shared by the civil society (UNESCO 2018; [START_REF] Floridi | Ai4people-an ethical framework for a good ai society: opportunities, risks, principles, and recommendations[END_REF]) that has a certain mistrust of AI, but they are also difficult to develop and formalize due to the technical complexity of the technology.

In spite of few recent specialized applicable standards, such as for the protection of personal data [START_REF] Heisenberg | Negotiating privacy: The European Union, the United States, and personal data protection[END_REF][START_REF] Albrecht | How the gdpr will change the world[END_REF]) or in robotics [START_REF] Schlenoff | An ieee standard ontology for robotics and automation[END_REF][START_REF] Johnson | Responsibility practices in robotic warfare[END_REF], a general and global legal system control the AI related risks does not exist. Fortunately nature abhors a vacuum and solutions have been developed. At the edge of lawlessness and mandatory law, a whole range of applicable standards more or less restrictive are emerging to fill possible legal loopholes, often out of necessity, as prior regulatory basis or to overcome political and economical issues at a national or international scale [START_REF] Guzman | International soft law[END_REF]Pellet 2018). These private standards are not meant to replace the necessary traditional legal norms, but reflect a need for regulation. Due to the development of private initiatives, and with non-binding legal tools also known as soft law [START_REF] Dupuy | Soft law and the international law of the environment[END_REF][START_REF] Cazala | Le soft law international entre inspiration et aspiration[END_REF]) that are actively used in other legal domains, such as environmental law, the civil society is mobilizing to guarantee the development of AI for social good. This mobilization reflects a form of empowerment of the society in the prevention of AI-related risks. The term responsibility defines the principle of facing the consequences of our actions. However, the responsibility is expressed in different ways such as a coercive normative constraint, an economic mechanism, a moral imperative or a governance mechanism [START_REF] Dahlsrud | How corporate social responsibility is defined: an analysis of 37 definitions[END_REF][START_REF] Costa | La diffusion des mécanismes de contrôle dans l'union européenne: vers une nouvelle forme de démocratie?[END_REF]. Consequently, a social accountability emerges and leads to the deployment of voluntary standards, coming from the civil society to guarantee a suitable principle of social good in addition or as a precursor to the traditional normative framework. This paper explores and defines how voluntary standards enable the use of AI for social good with the introduction of different tools that have been successfully employed jointly with legal regulations in other legal areas such as the environmental law. Therefore, the major forms of voluntary standards applicable to AI ensuring its positive use according to the social good are gradually introduced, starting with the stakeholder awareness, followed with the voluntary application of private standards, and concluding with the incitement to the development of AI for social good.

The actors empowerment and the integration of social good for AI start with the democratization of the information related to both AI risks for social good, and to the awareness of the concepts of social good for AI.

Risk awareness of AI for social good. The fast development of AI leads to concrete risks to the social good in different aspects of our societies. Different examples are available such as in the economic field, with the strong impact of AI on robotics and the employment market [START_REF] Manyika | A future that works: Ai automation employment and productivity[END_REF], or in the social area with the unfortunate transfer of important human biases to the systems (e.g. racism, sexism,etc.) [START_REF] Bolukbasi | Man is to computer programmer as woman is to homemaker? debiasing word embeddings[END_REF][START_REF] Zhao | Men also like shopping: Reducing gender bias amplification using corpus-level constraints[END_REF]2018), or within the security domain with concerns involving the relations of AI to the concept of democracy [START_REF] Ferrara | The rise of social bots[END_REF], arms monitoring or in a legal aspect, with multiple questions on the protection of personal data and privacy [START_REF] Albrecht | How the gdpr will change the world[END_REF][START_REF] Tankard | What the gdpr means for businesses[END_REF], or on the problem of accountability of AI systems [START_REF] Taddeo | How ai can be a force for good[END_REF][START_REF] Tual | Intelligence artificielle : ce qu'il faut retenir du rapport de cédric villani[END_REF]. Researchers have drawn up a non-exhaustive list that includes "labor displacement, inequality, an overall oligopolistic structure, totalitarianism, shifts and volatility in national power, strategic instability, and an AI race that sacrifice safety and other values" [START_REF] Dafoe | Ai governance: A research agenda[END_REF]. Raising the awareness of AI risks is of crucial interest to ensure its implementation with respect to the standards of social good.

Without a normative framework, and in the same manner as the recent mobilization of numerous employees against a partnership involving their AI products and the army [START_REF] Harwell | Google to drop Pentagon AI contract[END_REF], some researchers become aware of these risks, and take responsibility and fight to establish safeguards for a responsible development of AI (Montréal 2018;[START_REF] Harwell | Google to drop Pentagon AI contract[END_REF]. A growing awareness expressed in the economic sphere by the recent creation of ethical committees from private companies, such as the advanced technology external advisory council [START_REF] Levin | Google AI ethics council[END_REF] or the foundation of an ethical institute [START_REF] Shead | Facebook AI ethics institute[END_REF]) aiming at conducting independent research increasing awareness by providing advice on the subject of AI for social good. Moreover, and at the country level, some governments realize the lack of standards and the increasing risk of AI, and start to build national study committees. As an example, France and Canada have recently announced the joint creation of the international panel on artificial intelligence (IPAI 2018). These mechanisms are expected to promote a respectful and ethical approach of AI with the principles of sustainable development. Unfortunately, some of them already suffer from internal biases on the subject [START_REF] Levin | Google AI ethics council[END_REF] highlighting the complexity of the task. Concurrently to these private initiatives, numerous open events promoting a risk awareness on AI for social good emerge, including well-known international conferences and workshops broadening the debate of stakeholders on this topic (e.g. NeurIPS AISG Workshop, Conference on AI, Ethics, and Society, International Conference on Artificial Intelligence and Law). All of these tools are essential to raise awareness of the risks of artificial intelligence. Despite reflecting a beginning of interest, additional efforts must be made to improve their impact.

Raising the AI actors awareness to the social good. Well-known researchers on social sciences and on the management theory I. Nonaka and H. Takeuchi have proposed an interesting approach particularly suited for these issues called the rugby metaphor. The latter idea highlights the richness of the information that can be cultural, moral, emotional or technical as well as the importance of the selection and transfer processes of the information by the actors of a specific situation [START_REF] Bellon | Quelques fondements de l'intelligence économique[END_REF]. This work demonstrates the importance of the information and of its circulation among the various stakeholders, but most importantly, it shows the need to mobilize relevant and meaningful information at the right moment. Based on these hypothesis, the use of AI for social good necessarily involves both formal and informal education and training to allow a transfer of the relevant information to raise the awareness of the different actors.

In the same manner as computer science students are often introduced to the economics and management sciences, AI actors could and have to be initiated to fundamentals of social good (e.g. basic rights, social sciences, risk management,...) to integrate them whether consciously or unconsciously to their research or processes of production. Conversely, a dissemination of non-scientific or basic knowledge on methods related to AI to the civil society is crucial and must be encouraged to simplify the integration of the AI-related concepts and their impact on our societies. As an example, it is feasible to apply existing tools, including advertising campaigns or public seminars, to leverage a minimal but global knowledge on AI. Then and as a result of Corporate Social Responsibility (CSR), some organizations have set up an entire legal culture that could be transferred to AI to develop a collective intelligence of their teams regarding AI. A very simple, but powerful tool, is to create and broadcast informative e-learning videos. Indeed, it represents a training tool among others that raises awareness by focusing on the actions and reflexes to adopt, especially on the identification of a potential risk.

Awareness of artificial intelligence actors allows them to become conscious of the impact of their actions and their decisions in the development of risks related to new technologies. Once aware, they can act to limit these risks facilitating the advancement of an artificial intelligence for social good. Despite the fact that this paper proposes to study soft law techniques related to AI for social good, an effective and complete awareness of all actors in this field requires that our leaders and representatives are also interested. In fact, soft law techniques must be complementary to the adoption of public policies for the supervision of AI. Therefore, it is necessary to bring the attention of politicians to the many risks of AI and the crucial interest of its management.

Private standardization of social good for AI

Once the different AI actors are well-aware of the concept of social good, various instruments must be proposed to formalize its integration and induce behaviors that are respectful of the idea of social good within the use of AI, such as the development of voluntary standards from private initiatives.

Ethical standards for social good in AI. As stated by the Nobel Prize for Economics Joseph Stiglitz, " we are a global community, and like all communities, we must follow rules to live together. They must be clearly seen as fair and just. They must pay due attention to the poor as well as the powerful, and demonstrate a deep sense of honesty and social justice " [START_REF] Ferry-Maccario | Gestion juridique de l'entreprise[END_REF]) and regardless of the considered domain. In this extent, AI constitutes a major scientific and technological breakthrough that brings important social benefits, but also rises critical ethical and social risks (Montréal 2018). Ethical challenges that the community, and in the absence of a legal framework in this area, has took off. Indeed, among the tools of voluntary standardization to enhance the concept of social good within the AI domain, some ethical standards have recently emerged while others are still in development.

As an example, the Montréal declaration for a responsible development of artificial intelligence (Montréal 2018) is advocating for a positive development and use of AI based on specifics social good principles. Following the latter declaration, others institutions such as the Council of Europe are interested in extending these principles to a general ethical framework for a responsible and ethical use of AI with respect to the Human Rights, rule of law, and democracy. More precisely, the Council of Europe investigates the impact of AI in specific domains, including the medical field (Bioethics Committee) [START_REF] Yuste | Four ethical priorities for neurotechnologies and ai[END_REF], with a strategic action plan on the interactions of technologies and Human Rights in the biomedical context, or gender equality (Gender Equality Committee), with a funded project to prevent and reduce the risk of sexism induced by AI algorithms [START_REF] Zhao | Gender bias in coreference resolution:evaluation and debiasing methods[END_REF]2017;[START_REF] Bolukbasi | Man is to computer programmer as woman is to homemaker? debiasing word embeddings[END_REF]. In fact, numerous areas with an emphasize on AI are investigated, including education, discrimination, cyber-security,..., Despite various ongoing projects on ethical standards that constitute a significant progress toward the supervision of AI for social good, coordination and the practical application of these standards remain an open and crucial problem. Indeed, all these institutions could benefit from coordinating their ethical standards. More precisely, a global coordination would enable an international ethical framework for AI, and would make the effectiveness of its application easier. Furthermore, and due to the abstract concepts driven by the idea of an ethical AI, an effective implementation of these texts implies to improve them with more global actions. As an example, we propose to conceive specific ethical "codes of conduct " for professionals, to deploy in private companies or in public institutions. Ethics is of particular interest to the artificial intelligence community.

Nevertheless, the research in this field mainly comes from western-based societies. Thus, AI for international social good must envision common values and its principles must come from around the world.

Technical standards for social good in AI. In the last decades, the concept of social responsibility, that relies on the voluntary initiative, has been highly investigated in the field of corporate social responsibility for the environmental protection and Human rights (Hay, Stavins, and Vietor 2005;[START_REF] Idowu | Encyclopedia of corporate social responsibility[END_REF][START_REF] Darnault | Les PME face au contentieux économique: essai de guide pratique[END_REF]. The social responsibility answers a global need for references (e.g. standards, laws), enabling an institution or a company (e.g. AI-related products) to fully integrates its economical, social and legal environments alongside with its different stakeholders, within the management of the institution or company. The standardization is a crucial element of the soft law, that represents common standards to illustrate and standardize the practices of the social responsibility, and ensures a certain efficacy by proposing a collective solution to technical or organizational issues [START_REF] Castka | Integrating corporate social responsibility (csr) into iso management systems-in search of a feasible csr management system framework[END_REF][START_REF] Helfrich | La régulation des pratiques de rse par les normes: le cas de la norme iso 26000 sur la responsabilité sociale. 5e Congrès de l'ADERSE[END_REF]). The private standardization based on soft law techniques offers the advantage of tailored voluntary commitments but does not replace legal regulations.

Various national, regional or international organizations are at the origin of these voluntary standards designed specifically for the audiences they target to build a common frame of reference for AI. In fact, and in the same manner as W3C that has standardized the compatibility of certain web-based technologies, few organizations start to embrace the concept of AI and its supervision for social good. As an example, the International Standardization Organization (ISO) is currently working toward new strong standards for AI in collaboration with the United Nations (UN) Sustainable Development Goals (SDG). Despite the fact that recently published standards mostly consider information technologies (IT) and the reference data architectures, numerous ongoing or upcoming projects focuse on the use of AI, such as the standard ISO/IEC AWI 38507 that relates to the governance of IT and the governance impacts of the use of AI technologies (ISO 2019). In the same context, a French standardization association, named AFNOR, actively works on important aspects of the use of AI including ethical and social concerns, reliability and the integration of the risks induced by systems relying on machine learning based solutions (AFNOR 2019). These voluntary standards are based on consensus among all actors and in this sense they all agree: economic actors and consumers, professionals and users, to clarify and harmonize practices and define the quality level, security, compatibility, impact of products, services and practices. While they contribute to the establishment of minimum quality thresholds, the achievement of compatibility between organizations and the reduction of organizational variability, these standards are usually purely functional and must complement legal regulations that protect the common good.

Incitement to social good for AI

Based on the previous introduction to social behaviors of social good standards for the use of AI, it is now feasible and important to actively promote their development toward the community and to induce a generalization of social good in AI.

Contractual commitment to social good for AI. While most of the contractual relations are limited to the principal intentions of the parties and solely consider their main duties (Nurit-Pontier and Rousseau 2012), it is worth emphasizing that a contract not only establishes a commercial relationship but also enables to anticipate foreseeable risks [START_REF] Deharo | ingenierie contractuelle et performance de l'entreprise: perspective économique et dynamique de droit des contrats[END_REF][START_REF] Posner | Economic analysis of contract law after three decades: Success or failure[END_REF]. More precisely, it represents a legal instrument that defines a powerful communication tool, that can be used to determine contractual partners engaged in responsible processes or to incite them to develop this aspect. It is therefore of crucial interest to integrate informational components in the contracting process of the formation of the contract, to motivate and lead to the partners agreement to the concept of social good for the use of AI, as it has already been demonstrated for climate change (Hautereau-Boutonnet and Porchy-Simon 2019).

For example, voluntary environmental standards have gradually shaped international trade rules by infiltrating the contractual practice [START_REF] Howard | Standard or smokescreen? implementation of a voluntary environmental code[END_REF][START_REF] Delmas | A framework for analyzing environmental voluntary agreements[END_REF][START_REF] Johansson | Can voluntary standards regulate forestry?-assessing the environmental impacts of forest certification in sweden[END_REF]. Thus, the use of the contractual tool, in particular the environmental clauses mentioned in the ethical charters or stipulated in the international contracts, formalizes the commitment of certain companies in the fight against the environmental risks. A method used in environmental matters that can be transposed, combined with the deployment of voluntary standards, to fight against the risks of AI. Then, and with both public and private institutions, it is feasible to internally integrate the observance of ethical standards in employment contracts. In fact, among the sources of applicable labor law, it is necessary to distinguish external sources (e.g. international rules, laws, collective agreements) from internal sources (e.g. collective agreements of companies, regulations, uses ...). Thus, the employer can develop rules, standards of ethical behavior that are imposed on workers [START_REF] James | Reinforcing ethical decision making through organizational structure[END_REF]. Externally, ones can consider to obtain the adherence of institutional, commercial or financial partners to the defined ethical standards, to ensure the integration of technical standards enabling a responsible development of AI within the partner organization. In fact, in the same manner that employers can induce the ethical behavior of its employees by contract, an organization can influence the behavior of its partners by their contractual commercial relations. The freedom that frames the contractual tools makes it possible to consider adding contractual clauses regulating the use of a research object, or a product, to limit restrictively the utilization and the resale of an AI technology compliantly to social good principles.

Ensure the use of AI for social good. Despite the fact that the integration of a standardization constitutes an important step toward a responsible use of AI for social good, standards are non-binding and their is no guarantee of their correct application within private or institutional organizations. As a consequence, it is essential to propose tools to ensure the conformity of the acts of an organization that specifically showcases its compliance with a responsible AI program, or to at least inform the public and the stakeholders of the organizations that commit or not. In fact, the principle of certification is to give citizens (i.e. customers, users, administrators) an insurance on the quality of a service or a product. The certification brings the evidence, testifies, establishes the respect of a reference frame. In this extent, new control centers must be developed.

In particular, it is important to dissociate the standardization, that defines the process of conception and production of reference materials (e.g standards) from the certification that denotes the conformity assessment obtained by an entity from a third-party body with respect to specific standards [START_REF] Grenard | Normalisation, certification: quelques éléments de définition[END_REF][START_REF] Krzan | Standardization and certification in the area of environmentally degradable plastics[END_REF]. In fact, the latter certification bodies are part of the voluntary standard-setting instruments due to the fact that organizations choose to comply without any legal obligation. As an example, environmental protection often involves to demonstrate on the packaging of a product its attachment in the fight against climate change, through a label, or by highlighting the efforts made to limit the CO 2 consumption, or even by showcasing its involvement to a sustainable development program aiming at promoting the recourse to local producers (Hautereau-Boutonnet and Porchy-Simon 2019). Thereby, it is possible to follow the same approach, but with AI products and toward the use of social good for AI [START_REF] Rolnick | Tackling climate change with machine learning[END_REF]). However, it is necessary to recall that most of the certifications provide the compliance guarantee with certain standards, including private standards. Thus, one must pay attention to the standards whose certification ensures compliance. In addition, the major certification centers are also voluntary standardization centers. Therefore, they ensure compliance with the rules and standards they have established, in accordance with the regulations in force, but do not guarantee behaviors established and controlled by the public authorities. The source of certified standards and the defended interests being distinct, differentiation is more than necessary. While certifications must be used with cautions, they represent an interesting tool to encourage those involved in AI to guide its development toward social good.

Finally, it is admitted and well-known that voluntary standards and soft law techniques do not replace legal regulations. Nevertheless, they enable the civil society to opt for an important and effective virtuous circle driving the development of AI toward social good as illustrated in Figure 1.

Conclusion

In this paper, it has been shown that the lack of a legal system, despite the crucial need for frameworks and standards regarding AI, leads to the rise of a private standardization. The latter voluntary standardization enables, through the numerous and various tools introduced in this work (summarized in Figure 1), to gradually build foundations for the future legal edifice. The awareness raising of the civil society and the actors of the field to the AI-related risks allows the establishment of voluntary ethical and technical standards. These standards lead to a change in the behavior of the actors that adhere to them but also impact the behavior of their employees and partners. A virtuous circle illustrating the role that everyone can play in the development and use of artificial intelligence for social good. These soft law techniques can boost the international normative activity by extending its scope, particularly in the context of emerging legal areas such as AI. Indeed, these tools have various advantages including flexibility and adaptation that facilitate their development and application. Based on soft law techniques, the different AI actors can directly act on their own behaviors, but also on their collaborators actions to encourage an AI for the social good. An important interest for soft law that is easily explained by its lightened nature on the procedural level and its faculty of extension. Nevertheless, the gap between the flexibility of this process and the power of action it provides represents a risk of legal protection for the civil society. It is therefore crucial to keep in mind that voluntary standards, despite their multiple benefits, must remain a temporary alternative or an accompaniment to the adoption of legally binding standards. Indeed, if they guarantee a form of social good to artificial intelligence, they do not guarantee the respect for the common good, which is protected by government standards. Further research is thus needed on the AI governance issue: the problem of devising global norms, policies, and institutions to better ensure the beneficial development and use of AI advances [START_REF] Dafoe | Ai governance: A research agenda[END_REF].

Figure 1 :

 1 Figure 1: Illustration of the virtuous model based on soft law techniques for the development of an AI for social good.