Safety Contracts for Timed Reactive Components in SysML

Iulia Dragomir, Iulian Ober, and Christian Percebois Université de Toulouse -IRIT 118 Route de Narbonne, 31062 Toulouse, France {iulia.dragomir,iulian.ober,christian.percebois}@irit.fr Abstract. A variety of system design and architecture description languages, such as SysML, UML or AADL, allows the decomposition of complex system designs into communicating timed components. In this paper we consider the contract-based specification of such components. A contract is a pair formed of an assumption, which is an abstraction of the component's environment, and a guarantee, which is an abstraction of the component's behavior given that the environment behaves according to the assumption. Thus, a contract concentrates on a specific aspect of the component's functionality and on a subset of its interface, which makes it relatively simpler to specify. Contracts may be used as an aid for hierarchical decomposition during design or for verification of properties of composites. This paper defines contracts for components formalized as a variant of timed input/output automata, introduces compositional results allowing to reason with contracts and shows how contracts can be used in a high-level modeling language (SysML) for specification and verification, based on an example extracted from a real-life system.

Motivation and Approach

The development of safety critical real-time embedded systems is a complex and costly process, and the early validation of design models is of paramount importance for satisfying qualification requirements, reducing overall costs and increasing quality. Design models are validated using a variety of techniques, including design reviews [START_REF] Parnas | Active Design Reviews: Principles and Practices[END_REF], simulation and model-checking [START_REF] Emerson | Characterizing Correctness Properties of Parallel Programs Using Fixpoints[END_REF][START_REF] Queille | Specification and verification of concurrent systems in CESAR[END_REF]. In all these activities system requirements play a central role; for this reason processes-oriented standards such as the DO-178C [START_REF]Software Considerations in Airborne Systems and Equipment Certification[END_REF] emphasize the necessity to model requirements at various levels of abstraction and ensure their traceability from high-level down to detailed design and coding.

Since the vast majority of systems are designed with a component-based approach, the mapping of requirements is often difficult: a requirement is in general satisfied by the collaboration of a set of components and each component is involved in satisfying several requirements. A way to tackle this problem is to have partial and abstract component specifications which concentrate on specifying how a particular component collaborates in realizing a particular requirement; such a specification is called a contract. A contract is defined as a pair formed of an assumption, which is an abstraction of the component's environment, and a guarantee, which is an abstraction of the component's behavior given that the environment behaves according to the assumption.

The justification for using contracts is therefore manyfold: support for requirement specification and decomposition, mapping and tracing requirements to components and even for model reviews. Last but not least, contracts can support formal verification of properties through model-checking. Given the right composability properties, they can be used to restructure the verification of a property by splitting it in two steps: [START_REF] Alur | A Theory of Timed Automata[END_REF] verify that each component satisfies its contract and (2) verify that the network of contracts correctly assembles and satisfies the property. Thus, one only needs to reason on abstractions when verifying a property, which potentially induces an important reduction of the combinatorial explosion problem.

Our interest in contracts is driven by potential applications in system engineering using SysML [START_REF] Omg | Object Management Group -Systems Modeling Language (SysML)[END_REF], in particular in the verification of complex industrialscale designs for which we have reached the limits of our tools [START_REF] Dragomir | A case study in formal system engineering with SysML[END_REF]. In SysML one can describe various types of communicating timed reactive components; for most of these, their semantics can be given in a variant of Timed Input/Output Automata (TIOA) [START_REF] Kaynar | The Theory of Timed I/O Automata -Second Edition[END_REF]. For this reason, in this paper we concentrate on defining a contract theory for TIOA. This contract theory is applied on a SysML case study extracted from real-life.

A Meta-Theory for Contract-based Reasoning

Our contract theory is an instance of the meta-theory proposed in [START_REF] Quinton | Contract-Based Verification of Hierarchical Systems of Components[END_REF] and later detailed in [START_REF] Quinton | Design, vérification et implémentation de systèmes à composants[END_REF], which formalizes the relations that come into play in a contract theory and the properties that these relations have to satisfy in order to support reasoning with contracts. The term meta-theory refers to the fact that the formalism used for component specification is not fixed, nor the exact nature of certain relations defined on specifications (conformance, refinement under context). In order to obtain a concrete contract theory for a particular specification formalism one has to define these relations such that certain properties, prerequired by the meta-theory, are satisfied. In return, this meta-theory provides a ready-to-use contract-based methodology.

The purpose of this methodology is to support reasoning with contracts in a system obtained by hierarchical composition of components. At any level of the hierarchy, n components K 1 , ..., K n are combined to form a composite component K 1 ... K n , where denotes the parallel composition operator. Then verifying that the composite satisfies a global property ϕ runs down to checking that the contracts implemented by K 1 , ..., K n combine together correctly to ensure ϕ. This avoids the need to directly model-check the composite to establish ϕ and, so, alleviates the combinatorial explosion of the state space. The contracts being specified by more abstract automata, one can assume that their composition will be reduced.

The reasoning proceeds as follows: for each component K i , a contract C i is given which consists of an abstraction A i of the behavior of K i 's environment, and an abstraction G i that describes the expected behavior of K i given that the environment acts as A i . Fig. 1 presents three components K 1 , K 2 and K 3 and a corresponding set of contracts C 1 , respectively C 2 and C 3 . Step 1 of the reasoning consists in verifying that each component is a correct implementation of the contract, i.e. the component satisfies its contract. The satisfaction relation is directly derived from a more general one named refinement under context. The purpose of the latter is to model that a component K i is a correct refinement of the specification K j in the given environment E k . Thus, a component implements ! " # Fig. 1: Contract-based reasoning for a three-component subsystem ( [START_REF] Quinton | Design, vérification et implémentation de systèmes à composants[END_REF]). a contract if and only if refinement under context holds between the component K i and the guarantee G i in the environment A i .

Step 2 of the reasoning consists in defining a contract C = (A, G) for the composition K 1 ... K n and proving that the set of contracts {C 1 , C 2 , ..., C n } implies C. To do so, the meta-theory introduces a hierarchy relation between contracts, called dominance: a set of contracts {C 1 , C 2 , ..., C n } dominates a contract C if and only if the composition of any valid implementations of C 1 , C 2 , ..., C n is an implementation of C. In a multi-level hierarchy, the second step can be applied recursively up to a top-level contract, i.e. a contract for the whole (sub)system.

Finally, in the third step one has to prove that the top contract C = (A, G) implies the specification ϕ. This is done by verifying that A G ϕ, where is a conformance relation. This step is sufficient for proving that the whole system satisfies ϕ if and only if either the assumption A is empty as it is the case when the property is defined for the entire closed modeled system or A is a correct abstraction of the environment E with which S communicates given that S behaves like G, i.e. E satisfies the "mirror" contract C -1 = (G, A).

The reasoning strategy presented here assumes that the system designer defines all the contracts necessary for verifying a particular requirement ϕ. How these contracts are produced is an interesting question but it is outside the scope of this paper.

The theoretical contribution of this paper is the instantiation of this metatheory for a variant of Timed Input/Output Automata [START_REF] Kaynar | The Theory of Timed I/O Automata -Second Edition[END_REF], by choosing the appropriate refinement relations and proving that they satisfy certain properties needed for the meta-theory to be applied. Concretely, the difficulties of the theoretical work consisted in defining the conformance and refinement under context relations such that one can reason in a contract framework only by handling assumptions and guarantees once satisfaction has been proven. The refinement relation has to satisfy the compositionality property and the soundness of circular reasoning, detailed in §4. Compositionality allows for incremental design by incorporating parts of the environment into the component under study while refinement under context holds at every step. Circular reasoning allows for independent implementability by breaking the dependency between the component and the environment.

The practical contribution of this paper is the application of the contract framework to a case study modeled in SysML, which can be found in §5. Due to space limitations we skip the syntactic details of how contracts are expressed in SysML and we concentrate on describing the example, the property of interest and the contracts involved in proving it. The relatively complex SysML language aspects are detailed in [START_REF] Dragomir | Integrating verifiable Assume/Guarantee contracts in UML/SysML[END_REF].

3 Timed Input/Output Automata Many mathematical formalisms have been proposed in the literature for modeling communicating timed reactive components. We choose to build our framework on a variant of Timed Input/Output Automata of [START_REF] Kaynar | The Theory of Timed I/O Automata -Second Edition[END_REF] since it is one of the most general formalisms, thoroughly defined and for which several interesting compositional results are already available.

A timed input/output automaton (or component) defines a set of internal variables of arbitrary types and clocks and a set of input actions I, output actions O, visible actions V and internal actions H. We denote by E = I ∪ O ∪ V the set of external actions that also gives the interface of the component and by A = E ∪ H the set of actions. The state space of an automaton is described by the set of possible valuations of the set of variables. The state evolves either by discrete transitions or by trajectories. A discrete transition instantly changes the state and is labeled with an action from the mentioned sets. Trajectories change the state continuously during a time interval.

The behavior of a TIOA is described by an execution fragment which is a finite or infinite sequence alternating trajectories and discrete transitions. The visible behavior of a TIOA is given by a trace, which is a projection of an execution fragment on external actions and in which, from trajectories, only the information about the elapsed time is kept, while information about the variable valuations is abstracted away. For full definitions of all these notions, the reader is referred to the long version of this paper [START_REF] Dragomir | Safety Contracts for Timed Reactive Components in SysML[END_REF] and to [START_REF] Kaynar | The Theory of Timed I/O Automata -Second Edition[END_REF].

The difference between the TIOA of [START_REF] Kaynar | The Theory of Timed I/O Automata -Second Edition[END_REF] and our variant is that in addition to inputs and outputs, we allow for another type of visible actions; this is because, in [START_REF] Kaynar | The Theory of Timed I/O Automata -Second Edition[END_REF], when composing two automata, an output of one matched by an input of the other becomes an output of the composite, which does not correspond to our needs when using TIOA for defining the semantics of usual modeling languages like SysML. Indeed, the matching between an input and an output results in a visible action in SysML that is not further involved in any synchronizations.

Moreover, in the following we will limit our attention to trajectories that are constant functions for discrete variables, and linear functions with derivative equal to 1 for clocks, while [START_REF] Kaynar | The Theory of Timed I/O Automata -Second Edition[END_REF] allows more general functions to be used as trajectories. This restriction makes the model expressiveness equivalent to that of Alur-Dill timed automata [START_REF] Alur | A Theory of Timed Automata[END_REF], and will be important later on as it opens the possibility to automatically verify simulation relations between automata (simulation is undecidable for the TIOA of [START_REF] Kaynar | The Theory of Timed I/O Automata -Second Edition[END_REF]). However, this hypothesis is not needed for proving the compositional results in §4.

The parallel composition operator for TIOA is based on binary synchronization of corresponding inputs and outputs and on the interleaved execution of other actions, like in [START_REF] Kaynar | The Theory of Timed I/O Automata -Second Edition[END_REF]. The only difference is related to the interface of the composite timed input/output automata: the input and output sets of the composite are given by those actions not matched between components, while all matched input-output pairs become visible actions. Two automata can be composed if and only if they do not share variables and internal and visible actions. Two automata that can be composed are called compatible components. As in [START_REF] Kaynar | The Theory of Timed I/O Automata -Second Edition[END_REF], we use timed trace inclusion as the refinement relation between components.

Definition 1 (Comparable components). Two components K 1 and K 2 are comparable if they have the same external interface, i.e. E K1 = E K2 .

Definition 2 (Conformance). Let K 1 and K 2 be two comparable components.

K 1 conforms to K 2 , denoted K 1 K 2 , if traces K1 ⊆ traces K2 .
The conformance relation is used in the third step for verifying the satisfaction of the system's properties by the top contract: A G ϕ, where A G and ϕ have the same interface. It can be easily shown that conformance is a preorder. The following useful compositional result (theorem 8.5 of [START_REF] Kaynar | The Theory of Timed I/O Automata -Second Edition[END_REF]) can be easily extended to our variant of TIOA:

Theorem 1. Let K 1 and K 2 be two comparable components with K 1 K 2 and E a component compatible with both K 1 and K 2 . Then K 1 E K 2 E.

Contracts for Timed Input/Output Automata

In this section we formalize contracts for TIOA and the relations described in §2 and we list the properties that we proved upon these and that make contractbased reasoning possible. Definition 3 (Environment). Let K be a component. An environment E for the component K is a timed input/output automaton compatible with K for which the following hold:

I E ⊆ O K and O E ⊆ I K . Definition 4 (Closed/open component). A component K is closed if I K = O K = ∅. A component is open if it not closed.
Closed components result from the composition of components with complementary interfaces. Definition 5 (Contract). A contract for a component K is a pair (A, G) of TIOA such that

I A = O G and I G = O A (i.

e. the composition pair A G defines a closed component) and

I G ⊆ I K and O G ⊆ O K (i.e. the interface of G is a subset of that of K).
A is called the assumption over the environment of the component and G is called the guarantee. The interface of a contract is that of its guarantee.

The first step of the verification, as presented in §2, is to prove that the modeled components are an implementation of the given contracts. For this, we firstly define the refinement under context preorder relation which, in our framework, is further based on conformance. The complete formal definition of refinement under context can be found in [START_REF] Dragomir | Safety Contracts for Timed Reactive Components in SysML[END_REF]. Definition 6 (Refinement under context). Let K 1 and K 2 be two components such that

I K2 ⊆ I K1 ∪ V K1 , O K2 ⊆ O K1 ∪ V K1 and V K2 ⊆ V K1
. Let E be an environment for K 1 compatible with both K 1 and K 2 . We say that

K 1 refines K 2 in the context of E, denoted K 1 ⊑ E K 2 , if K 1 E E ′ K 2 E K ′ E ′
where

-E ′ is a TIOA defined such that the composition K 1 E E ′ is closed. E ′
consumes all outputs of K 1 not matched by E and may emit all inputs of K 1 not appearing as outputs of E.

-K ′ is a TIOA defined similarly to E ′ such that the composition of K 2 E K ′ E ′ is closed and comparable to K 1 E E ′ .
Since we want to take into account interface refinement between components and conformance imposes comparability, we have to compose each member of the conformance relation obtained from refinement under context with an additional timed input/output automaton E ′ , respectively K ′ , such that they both define closed comparable systems. Both automata are uniquely defined by their interfaces and can be automatically computed.

Furthermore, the particular inclusion relations between the interfaces of K 1 and K 2 in the previous definition are due to the fact that both K 1 and K 2 can be components obtained from compositions, e.g.,

K 1 = K ′ 1 K 3 and K 2 = K ′ 2 K 3 , where I K ′ 2 ⊆ I K ′ 1 , O K ′ 2 ⊆ O K ′ 1 and V K ′ 2 ⊆ V K ′ 1 .
This happens in particular when K ′ 2 is a contract guarantee for K ′ 1 . Then, by composition, actions of K 3 may be matched by actions of K ′ 1 but have no input/output correspondent in K ′ 2 .

Theorem 2. Given a set K of comparable components and a fixed environment E for their interface, refinement under context ⊑ E is a preorder over K.

We derive the satisfaction relation from refinement under context.

Definition 7 (Contract satisfaction). A component K satisfies (implements)

a contract C = (A, G), denoted K |= C, if and only if K ⊑ A G.
We have introduced the notions and relations in order to verify that a component is a correct implementation of a contract. The second step of the contractbased verification methodology relies on the notion of dominance, introduced informally in §2, which is formally defined in [START_REF] Quinton | Design, vérification et implémentation de systèmes à composants[END_REF]

i } n i=1 such that ∀i, K i |= C i , we have (K 1 K 2 • • • K n ) |= C.
In order to ease dominance verification by discarding components from now on and to be able to apply the meta-theory, we prove that the following compositional results hold in our framework.

Theorem 3 (Compositionality). Let K 1 and K 2 be two components and E an environment compatible with both K 1 and

K 2 such that E = E 1 E 2 . Then K 1 ⊑ E1 E2 K 2 ⇔ K 1 E 1 ⊑ E2 K 2 E 1 .
Theorem 4 (Soundness of circular reasoning). Let K be a component, E its environment and C = (A, G) the contract for K such that K and G are compatible with each of E and A. If [START_REF] Alur | A Theory of Timed Automata[END_REF]

traces G is closed under limits, (2) traces G is closed under time-extension, (3) K ⊑ A G and (4) E ⊑ G A then K ⊑ E G.
The definitions of closure under limits and closure under time-extension for a set of traces are those given in [START_REF] Kaynar | The Theory of Timed I/O Automata -Second Edition[END_REF]. Closure under limits informally means that any infinite sequence whose finite prefixes are traces of G is also a trace of G, while closure under time-extension denotes that any finite trace can be extended with time passage to infinity. By making these hypotheses on G, G can only express safety properties on K and cannot impose stronger constraints on time passage than K. The proofs of all theorems presented here can be found in [START_REF] Dragomir | Safety Contracts for Timed Reactive Components in SysML[END_REF].

Then based on theorems 2, 3 and 4, the following theorem also proved in [START_REF] Dragomir | Safety Contracts for Timed Reactive Components in SysML[END_REF] which is a variant of theorem 2.3.5 from [START_REF] Quinton | Design, vérification et implémentation de systèmes à composants[END_REF] holds: Theorem 5 (Sufficient condition for dominance). {C i } n i=1 dominates C if, ∀i, traces Ai , traces Gi , traces A and trace G are closed under limits and under time-extension and

G 1 ... G n ⊑ A G A G 1 ... G i-1 G i+1 ... G n ⊑ Gi A i , ∀i
The above theorem specifies the proof obligations that have to be satisfied by a system of contracts in order to be able to infer dominance in the second step of the verification methodology presented in §2.

Application to a SysML Model: the ATV Solar Wing Generation System Case Study

The contract-based reasoning method previously described is partially supported by the OMEGA-IFx Toolset [START_REF] Bozga | The IF Toolset[END_REF] for SysML models. The details of the SysML language extended with contracts are left aside for space reasons and can be found in [START_REF] Dragomir | Integrating verifiable Assume/Guarantee contracts in UML/SysML[END_REF]. In the following we present a case study extracted from the industrialgrade system model of the Automated Transfer Vehicle (ATV) and we show how contracts can be used for property verification. This case study consists of the Solar Wing Generation System (SGS) [START_REF] Dragomir | A case study in formal system engineering with SysML[END_REF] responsible for the deployment and management of the solar wings of the vehicle. The SysML model used in the following, provided by Astrium Space Transportation, was obtained by reverse engineering the actual SGS system for the purpose of this study.

The ATV system model illustrated in Fig. 2 summarizes the three main components involved in the case study and the bidirectional communications between them: the mission and vehicle management (MVM ) part that initiates the two functionalities of the SGS (wing deployment and rotation), the SOFTWARE part of the SGS that based on commands received from the MVM executes the corresponding procedures and the HARDWARE part that consists of the four wings. We focus here on the wing deployment mode on which we want to verify the following property ϕ: after 10 minutes from system start-up, all four wings are deployed.

The system explicitly models the redundancy of the hardware equipments which aims to ensure fault tolerance. There are 56 possible failures (14 per wing)

BL_ATV «block,root» MVM 1 SGS 1 HARDWARE 1 WING1 1 WING4 1 WING3 1 WING2 1 SOFTWARE 1 C1 «block,contract» C2 «block,contract» C3 «block,contract» C4 «block,contract» C «block,contract» phi «block,observer»
Fig. 2: Architecture of the SGS system including contracts (simplified view). grouped in 3 classes depending on their target (thermal knives, hold-down and release system and solar array driving group). The following hypothesis is made: throughout any execution of the system, at most one hardware fault may occur (1-fault tolerance). We are interested in verifying ϕ by taking into consideration this hypothesis. But applying model-checking directly on the system leads to combinatorial explosion and the verification does not finish. To give an idea about the complexity of the model at runtime, the system contains 96 objects that communicate through 661 port instances and 504 connectors. In [START_REF] Dragomir | A case study in formal system engineering with SysML[END_REF] we have shown the motivation for using contracts and we have sketched a proof that remained to be formalized and verified. In the following we complete this case study by proving the property ϕ with formalized contract-based reasoning.

Since the property ϕ is expressed with respect to the behavior of the four wings that are contained in the HARDWARE block, with regard to the methodology of Fig. 1, the subsystem S can be identified in our case study with HARD-WARE and the components K i are represented by WINGi, i = 1, 4. The environment of the subsystem is given by the parts with which it communicates: bidirectional communication is directly established between SOFTWARE and HARDWARE, while SOFTWARE depends on the behavior of MVM. So, the environment E of Fig. 1 is represented here by the composition of MVM and SOFTWARE.

The first step of the methodology consists in defining a contract C i = (A i , G i ) for each WINGi, and next proving that WINGi satisfies C i , i = 1, 4. This step checks the validity of the dependency relations between the wings and their corresponding contracts. In order to model a contract, first we need to identify the environment of the component to which the contract is associated and to build an abstraction from the point of view of the component. Thus, for WINGi the environment is given by the environment of the subsystem HARDWARE and all WINGj with j = i. We propose the following abstraction WAj for WINGj : the wing has a not deployed status for at most 400 seconds and a deployed status after 130 seconds, while all other received requests are consumed. The assumption A i is then given by the parallel composition of MVM, SOFTWARE and WAj with j = i. This abstraction of the environment is sufficient to drastically reduce the state space of the verification model, since the exponential explosion in the original model is mainly due to the parallelism of the hardware pieces which are abstracted to the three leaf parts WAj. We want to guarantee that even if WINGi exhibits a failure it ends up being deployed after 400 seconds.

Contract C i = (A i , G i ) where -A i = MVM SOFTWARE ( j =i WAj ).
-G i : the wing answers to requests about its status with not deployed from startup up to 400 seconds or with deployed after 130 seconds and ignores all other requests. Between 130 and 400 seconds it can answer either, nondeterministically.

Since A i is partially given by the concrete environment (MVM SOFTWARE ) and C i has to define a closed system, we have to manually model the behavior of G i for all received requests. This constraint imposes to add as consuming transitions in every state all requests corresponding to wing deployment process. Furthermore, one can remark that this guarantee is stronger than the projection of the property ϕ on WINGi. The abstraction WAj can also be subject to one failure since this case was not excluded from its behavior. Then the fault tolerance property that we verify via contracts is stronger than the initial hypothesis: we guarantee that the system is 4-fault tolerant if faults occur in separate wings. The second step consists in defining a global contract C = (A, G) for HARD-WARE and to prove that the contract is dominated by {C 1 , C 2 , C 3 , C 4 } represented in Fig. 2 by the dependency relation between contracts. We use as assumption A the concrete environment of HARDWARE. The guarantee G is the composition of the four G i . All A i , G i , A and G as defined satisfy the conditions for applying theorem 5.

Contract C = (A, G) where

-A = MVM SOFTWARE -G : for each wing status interrogation it answers as not deployed for at most 400 seconds and as deployed after at least 130 seconds, while all other requests are ignored.

The last step consists in verifying that the composition A G conforms to ϕ, illustrated by the dependency between the contract and the property. Verifying that the environment satisfies the"mirror"contract is trivial since the assumption A is the environment itself.

The proofs of all three steps have been automatically verified within the OMEGA-IFx Toolset which translates SysML models in communicating timed automata [START_REF] Bozga | The IF Toolset[END_REF]. Since trace inclusion is undecidable, we use a stronger simulation relation whose satisfaction implies trace inclusion. So, verifying simulation is sufficient (albeit not necessary) in order to prove the satisfaction of the conformance relation. A variant of this verification algorithm is implemented in the IFx Toolset.

For each step of the verification methodology we have manually modeled the contracts: assumptions as blocks that we had to connect via ports with the other components and guarantees as independent components. The first step gave 4 possible configurations with one concrete wing and 3 abstract ones that were each verified with respect to all 14 possible failures. The average time in seconds needed for the verification of the satisfaction relation for each contract

Related Work

Contract-based specification and reasoning for communicating components has been subject to intensive research recently. As mentioned in the beginning, our contract theory for TIOA is an instance of the meta-theory of [START_REF] Quinton | Design, vérification et implémentation de systèmes à composants[END_REF], which has previously been applied for a number of other components formalisms: Labeled Transition Systems (with priorities) [START_REF] Quinton | Design, vérification et implémentation de systèmes à composants[END_REF], Modal Transition Systems [START_REF] Quinton | Contract-Based Verification of Hierarchical Systems of Components[END_REF], BIP framework [START_REF] Basu | Modeling Heterogeneous Real-time Components in BIP[END_REF][START_REF] Quinton | Design, vérification et implémentation de systèmes à composants[END_REF] and Heterogeneous Rich Components [START_REF] Benvenuti | A contract-based formalism for the specification of heterogeneous systems[END_REF]. To the best of our knowledge, this is the first documented application of this meta-theory to Timed Input/Output Automata. Contract meta-theories have also been built on specification theories. The aim of a specification theory is to provide a complete algebra with powerful operators for logical compositions of specifications and for synthesis of missing components (quotient), the main goal being to provide substitutability results allowing for compositional verification. The meta-theory of [START_REF] Bauer | Moving from Specifications to Contracts in Component-Based Design[END_REF] falls under this category. The main differences with respect to [START_REF] Quinton | Design, vérification et implémentation de systèmes à composants[END_REF] concern (1) the definition of contracts that do not support signature refinement (a partial solution for this problem has been proposed in [START_REF] Bauer | Component Interfaces with Contracts on Ports[END_REF]) and (2) the method for reasoning with contracts which relies on a contract composition operator that is partially defined. However, the meta-theory of [START_REF] Bauer | Component Interfaces with Contracts on Ports[END_REF] does not alleviate this problem. None of these two metatheories supports circular arguments nor defines a methodology for reasoning with contracts. Moreover, the meta-theories do not provide means to formalize requirements and to verify their satisfaction. Other approaches for reasoning with contracts have been developed for interface theories [START_REF] Chilton | Revisiting Timed Specification Theories: A Linear-Time Perspective[END_REF][START_REF] David | Compositional verification of real-time systems using ECDAR[END_REF] and for logical specifications [START_REF] Chilton | Assume-Guarantee Reasoning for Safe Component Behaviours[END_REF]. A complete comparison between (meta-)theories is available in [START_REF] Dragomir | Safety Contracts for Timed Reactive Components in SysML[END_REF].

Only the meta-theory of [START_REF] Bauer | Moving from Specifications to Contracts in Component-Based Design[END_REF] has been instantiated for a variant of TIOA in [START_REF] David | Methodologies for Specification of Real-Time Systems Using Timed I/O Automata[END_REF][START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF][START_REF] David | Compositional verification of real-time systems using ECDAR[END_REF] which is implemented in the ECDAR tool [START_REF] David | ECDAR: An Environment for Compositional Design and Analysis of Real Time Systems[END_REF]. However, several aspects of this specification theory make it unsuitable for representing the semantics of timed components described in SysML or UML. The synchronization between an input of one component and an output of another component becomes an output of the composite, which equates to considering outputs as broadcasts and which is not consistent with the UML/SysML semantics. Moreover, the formalism forbids non-determinism due to the timed game semantics [START_REF] Bourke | New Results on Timed Specifications[END_REF] and does not handle silent transitions, which is problematic for representing the semantics of complex components performing internal computation steps.

In addition, contracts in UML/SysML have until now been explored for the specification of composition compatibility of components via interfaces [START_REF] Weis | A UML Meta-model for Contract Aware Components[END_REF] and for the verification of pre/post conditions of operations as presented by [START_REF] Hoare | An Axiomatic Basis for Computer Programming[END_REF]. Recent work covers the use of pre/post condition contracts for modeling transformation of models [START_REF] Cariou | OCL contracts for the verification of model transformations[END_REF] and for modeling the execution semantics of UML elements [START_REF] Cariou | Contracts for model execution verification[END_REF]. To the best of our knowledge, our work is the first on using assume/guarantee behavioral contracts for the verification of UML/SysML model requirements.

Table 1 :

 1 Average verification time for each contract C i per induced failure group.

		Average verification time (s)
	Type of induced failure	Wing 1 Wing 2 Wing 3 Wing 4
	Thermal knife	13993 6869 18842 11412
	Hold-down and release system 12672 6516 16578 9980
	Solar array driving group	11527 5432 13548 6807
	with respect to each class of failures is presented in

Table 1 .

 1 Even though the system model looks symmetrical, some hardware pieces not represented here do not have a symmetrical behavior and due to their interconnections with the wings the state space of system's abstraction for W IN G1 and W IN G3 is larger than the one of W IN G2 and W IN G4. For the second step, only one model is created on which we verified all 5 proof obligations given by theorem 5: the automatic validation of the global guarantee G and the automatic validation of assumptions A i . Modeling the assumptions A i that play the role of guarantees for dominance verification shows the symmetry of the MVM and SOFTWARE behavior. This means that only one verification is in fact sufficient for proving all 4 relations, verification that was realized in 9 seconds. The verification of the guarantee G needed 1 second. Finally, the same model was used for verifying ϕ that took 1 second.

Conclusions

We have presented a contract framework for Timed Input/Output Automata and results which allow contract-based reasoning for verifying timed safety properties of systems of TIOA components. We have illustrated the method on a case study extracted from an industrial-scale system model and we have showed how contract-based reasoning can alleviate the problem of combinatorial explosion for the verification of large systems.

The present work is a step further towards introducing contracts in SysML and providing a full solution to that problem. In [17] we defined a suitable syntax for contracts in SysML and a set of well-formedness rules that system models must satisfy for reasoning with contracts. For the moment, some steps of the method applied on SysML remain manual like modeling individual systems for each contract satisfaction relation or for each dominance proof obligation. Future work includes: (1) formalizing the semantic mapping between SysML components and contracts and their TIOA counterparts and (2) providing means for automatic verification by automated generation of proof obligations.


Pierre Bisquert
email: bisquert@irit.fr

Claudette Cayrol
email: ccayrol@irit.fr

Florence Dupin De Saint-Cyr

Marie-Christine Lagasquie-Schiex

Goal-driven Changes in Argumentation: A theoretical framework and a tool

Keywords:

This paper defines a new framework for dynamics in argumentation. In this framework, an agent can change an argumentation system (the target system) in order to achieve some desired goal. Changes consist in addition/removal of arguments or attacks between arguments and are constrained by the agent's knowledge encoded by another argumentation system. We present a software that computes the possible change operations for a given agent on a given target argumentation system in order to achieve some given goal.

I. INTRODUCTION An abstract argumentation system (AS)

 [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF]is composed of a set of arguments linked by a binary relation, called attack relation, which represents conflicts between arguments. A "semantics" for such a structure defines the way to select subsets of arguments jointly acceptable. In the last few years, the dynamics of these systems has been garnering increased attention from the researchers in argumentation [START_REF] Boella | Dynamics in argumentation with single extensions: Attack refinement and the grounded extension[END_REF], [START_REF]Dynamics in argumentation with single extensions: Abstraction principles and the grounded extension[END_REF], [START_REF] Cayrol | Change in abstract argumentation frameworks: Adding an argument[END_REF], [START_REF] Baumann | Expanding argumentation frameworks: Enforcing and monotonicity results[END_REF], [START_REF] Moguillansky | Argument theory change through defeater activation[END_REF], [START_REF] Liao | Dynamics of argumentation systems: A division-based method[END_REF]. Change in argumentation raises classical questions: "How to represent a change? What are its consequences?". But also new questions concerning the use of such changes emerge : "Who is concerned by these changes? How to use them in an effective way to achieve a precise goal?". These two questions concerning the audience and optimal change led us to propose a new theoretical framework that is close to classical planning. We want to model the reasoning of an agent who has her own knowledge, a goal and the possibility of acting on a target system. Here, the agent's knowledge is represented by an AS. The target on which she can operate is also an AS. For example, during a debate, the publicly exchanged arguments and their interactions may constitute the target system. An agent can act on the target for adding or removing arguments or attacks. In a public debate, adding an argument simply amounts to expressing it. The removal of an argument [START_REF] Bisquert | Duality between addition and removal[END_REF], [START_REF]Characterizing change in abstract argumentation systems[END_REF] may be due to an objection or may come from the rejection of a given statement not recognized as a proper argument. The addition (resp. removal) of attack may come from the discovery that two already stated arguments are in conflict (resp. compatible). The originality of our proposal lies in the use of two AS: one for the agent and one for the target. This introduces some limitations into the set of possible actions of the agent, (since, for instance, she cannot add arguments or attacks if she does not know them), thus some trivial ways to realize a goal may not be allowed for the agent.

Several software tools have already been designed for helping a user to reason with arguments. They are meant to be cognitive assistants (see for instance [START_REF] Van Gelder | The Rationale for Rationale[END_REF], [START_REF] Tecuci | Computational theory and cognitive assistant for intelligence analysis[END_REF]) or they focus on a particular domain (e.g. [START_REF] Ashley | An AI model of case-based legal argument from a jurisprudential viewpoint[END_REF], [START_REF] Aleven | Using background knowledge in case-based legal reasoning: A computational model and an intelligent learning environment[END_REF] in the domain of case-based legal reasoning). Our proposal is more at a strategical level since it aims at helping the user to persuade an audience, hence to provide means to do it (arguments that could be added, or objections that could be done to existing ones). More precisely, it provides as output the list of actions executable by the agent in order to achieve her goal. This software uses properties characterizing changes that were established in [START_REF] Cayrol | Change in abstract argumentation frameworks: Adding an argument[END_REF], [START_REF] Bisquert | Duality between addition and removal[END_REF]. In this article, we only use a particular semantics (the grounded semantics) but the software can handle others of them (the preferred and stable semantics). In addition, at the current stage, the software handles only some types of change.

In Sect.II, we present an example which will enable us to illustrate our theoretical framework described in Sect.III. In Sect.IV, we present the implemented tool which provides the actions to be carried out by the agent in order to achieve her goal. The experimentation protocols and the results are given in Sect.V.

II. THE COURT HEARING EXAMPLE

This example, already described in [START_REF] Bisquert | Duality between addition and removal[END_REF], is a court hearing which fits well with an argumentation framework. However, while this example illustrates our definitions easily, it does not cover all the possible applications of our work. We present first the protagonists and their goals then we describe the course of the hearing.

A. Protagonists

In this example, four entities are interacting in order to determine if an argument x 0 is acceptable; here, the argument x 0 expresses that the defendant is not guilty. The four entities have quite distinct roles:

• the prosecutor wants to obtain the rejection of the argument x 0 given a set of arguments. • the defense lawyer, with his set of arguments (possibly different from those of his adversary, the prosecutor), tries to obtain the acceptance of the argument x 0 .

• the judge ensures that the process of argumentation takes place under good conditions. When an objection is made by one of the participants, he can accept this objection (thus the corresponding argument is removed), or reject it.

• the jury has the last word. Its role is to listen to the arguments of the prosecutor and lawyer. When the hearing is finished (i.e. when neither the prosecutor, nor the lawyer can, or want to, give new arguments), the jury deliberates and determines whether the argument x 0 is acceptable or not.

In this example, the prosecutor and the lawyer are not interested by convincing each-other. However, they wish to convince the jury who will make the final decision. Thus, both protagonists will act on a target AS representing the state of knowledge of the jury. The target AS, which is empty at the beginning, represents the central place of exchanges between the prosecutor and the lawyer, where each one will place his arguments in turn, trying to make the jury lean in his favor at the end.

B. Protocol

We present a protocol governing the exchange of arguments in the example of the hearing.

1) First of all, the argument x 0 , giving the subject of the hearing, is set up. By convention, the defense lawyer speaks first and states the innocence of his client. The jury AS (the target) is modified. 2) the hearing is a sequence of actions made by the agents (either the prosecutor, or the lawyer) according to their own AS. We consider two types of action:

• an additive action is the addition of arguments and/or attacks directly in the jury AS; • a suppressive action is the removal of one or more arguments and/or attacks from the jury AS. Let us note the particular case of an objection: it consists in asking the judge to rule on the legality of some arguments and/or attacks uttered by the adversary. If the objection is rejected, no modification of the jury AS is carried out. If the objection is accepted, arguments or attacks objected are removed from the jury AS. It is also possible for an agent to do nothing. It is the case, for instance, when the agent does not have any more argument to advance, or when the jury AS is appropriate for her.

3) a side effect of an action is to inform the adversary: if one of the two protagonists was not aware of one argument uttered by the other then he will add it to its own system. In the same vein, if an argument is considered to be illegal after an objection accepted by the judge, the two agents should occult it in order to no more use it.

4) When the agents both decide that they do not have anything to add, the process stops and the jury deliberates thanks to its AS. This protocol highlights two types of change:

• a change operated by an agent on a target system other than her own, • a change operated by an agent on her own system. This last type of change can be studied by using directly the work of [START_REF] Cayrol | Change in abstract argumentation frameworks: Adding an argument[END_REF] and will not be treated here. In this paper, we investigate only the first type of change by defining a theoretical framework in which an agent chooses an action according to a target system, her own system and her goals.

III. CLASSICAL ARGUMENTATION FRAMEWORK AND NEW DEFINITIONS This work is based on various concepts that we will present and illustrate progressively on the example of Sect.II. We will need in particular the notions of argumentation system (AS) and change operation respectively introduced in [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF] and [START_REF] Cayrol | Change in abstract argumentation frameworks: Adding an argument[END_REF]. Beyond the concept of change and the modifications it implies, we are interested in what can cause this change, i.e., why and how a target AS is modified. For this purpose, we will introduce the concept of goal of an agent and we will focus on finding the operations an agent can apply in order to achieve her goal.

A. Abstract Argumentation

Let us consider a set Arg of symbols (denoted by lowercase letters). The set Arg and a relation R ⊆ Arg × Arg enable us to define the set of all possible arguments with their interactions, which we call reference universe. More precisely, Arg represents a potentially infinite set of arguments available in a particular domain (e.g. if the domain is a knowledge base then Arg is the set of all arguments that can be built upon the formulas of the base). It is also possible, following the example below, to suppose that Arg is provided explicitly.

Ex. 1: During an hearing concerning a defendant (Mr. X), several arguments may be examined in order to determine his culpability. The following table presents We slightly modify the AS definition of [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF] in order to take into account a reference universe. Def. 1: An argumentation system (AS) on the universe Arg, R is a partial subgraph of Arg, R , i.e. a pair A, R A , where A ⊆ Arg is a finite nonempty set of arguments and

R A ⊆ R ∩ A × A is called attack relation. Let a, b ∈ A, aR A b means that a attacks b.
A, R A is represented by an argumentation graph G whose vertices and edges correspond respectively to the arguments and the attacks.

x ∈ G is a shortcut for x ∈ A. Given a universe Arg, R , G k = A k , R A k denotes the
AS of the agent k on this universe, and represents the part of the reference universe known by k.

Ex.1 (cont.) The prosecutor does not know all the arguments of the universe (given in Fig. 1). Fig. 2 illustrates the arguments and the attacks that he knows (G pros ). The acceptable sets of arguments ("extensions") are computed using a "semantics" based on the following notions:

Def. 2: Given an AS A, R A , let a ∈ A and S ⊆ A • S attacks a if and only if (iff) ∃x ∈ S such that (s.t.) xR A a. • S is conflict free iff ∄a, b ∈ S s.t. aR A b.
• S defends an argument a iff S attacks any argument attacking a. The set of the arguments defended by S is denoted by

F(S); F is called the characteristic function of A, R A . More generally, S indirectly defends a iff a ∈ i≥1 F i (S).
• S is an admissible set iff it is both conflict free and defends all its elements.

In this article, we focus on one semantics among those proposed by [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF]:

Def. 3 (Grounded semantics): Let E ⊆ A, E is the only grounded extension iff E is the smallest with respect to (wrt) ⊆ fixed point of the characteristic function F.
Ex.1 (cont.) The grounded extension representing the acceptable arguments for the prosecutor is {x 0 , x 3 , x 5 , x 6 }.

In addition, the status of an argument is defined wrt its presence in the extensions of the selected semantics. In our particular case, an argument is "accepted" if it appears in the grounded extension and "rejected" otherwise. Thus, for the prosecutor, x 0 is accepted and x 1 rejected. But, although he does not have the arguments to prove undoubtedly that the defendant is guilty, the prosecutor wishes that x 1 would be accepted by the jury. In the following section, we will see how the prosecutor can act on the jury AS in order to make x 1 accepted.

B. Change in argumentation

According to [START_REF] Cayrol | Change in abstract argumentation frameworks: Adding an argument[END_REF], an elementary change is either the addition/removal of an argument with a set of related attacks, or the addition/removal of one precise attack. In order to be more concise, we only consider the operations concerning the addition or the removal of an argument. Moreover, we refine the concept of elementary operation in the sense of [START_REF] Cayrol | Change in abstract argumentation frameworks: Adding an argument[END_REF] in four steps: first, we define its syntax; then we relate the operation to an agent in order to determine if it is authorized or not for her, i.e. if she knows the elements involved in the operation. We then take into account the target to determine if the operation is executable: the addition (resp. removal) of an argument is only achievable if this argument is absent (resp. present) in the target system. Lastly, we define the impact of an operation on an AS. The restriction to elementary operations is done without loss of generality since any operation can be represented by a sequence of elementary operations, called program in Def.5. In addition, we suppose in this work that all the systems considered are relative to the same universe Arg, R . • an elementary operation op, arg, att is authorized for

k if arg ⊆ A k and att ⊆ R A k 1 .
• an executable operation by k on G is an elementary operation op, arg, att authorized for k s.t.:

-if op = ⊕, then arg ⊂ A and ∀(x, y) ∈ att, (x ∈ A or y ∈ A), -if op = ⊖, then arg ⊆ A. • an operation o = op, arg, att executable by k on G provides a new AS G ′ = O(G) = A ′ , R A ′ s.t.: -if op = ⊕ then G ′ = A ∪ arg, R A ∪ att , -if op = ⊖ then G ′ = A \ arg, R A \ {(x, y) ∈ R A s.t. x ∈ arg or y ∈ arg} .
Ex.1 (cont.) Given the reference universe of Fig. 1, here is a non-exhaustive list of elementary operations:

• ⊕, {x 2 }, {(x 2 , x 1 )} • ⊕, {x 2 }, {(x 2 , x 1 ), (x 3 , x 2 )} • ⊕, {x 6 }, {(x 6 , x 1 )} • ⊕, {x 6 }, ∅ • ⊖, {x 4 }, ∅ • ⊖, {x 2 }
, ∅ Among these elementary operations, the agent (the prosecutor) is not authorized to use those concerning arguments or attacks that she does not know. Thus, she will not be able to use the following operations:

• ⊕, {x 2 }, {(x 2 , x 1 )} , • ⊕, {x 2 }, {(x 2 , x 1 ), (x 3 , x 2 )} , • ⊖, {x 2 }, ∅ .
Let G jury be the jury AS (Fig. 3). Here are some executable operations on G jury by the agent:

• ⊖, {x 4 }, ∅ • ⊕, {x 6 }, {(x 6 , x 1 )} • ⊕, {x 6 }, ∅ • ⊕, {x 5 }, {(x 5 ,
x 4 )} Finally, the impact of the last operation on the jury AS produces:

x5 x4 x1 x0
We consider below the programs, i.e. the sequences of executable operations by an agent on an AS. This enables an agent to carry out several elementary operations in sequence.

Def. 5: Let k be an agent and G any AS. An executable program p by k on G is an ordered finite sequence of m operations

(o 1 , • • • , o m ) s.t.: • m = 1: o 1 is executable by k on G. In this case, p(G) = o 1 (G). • m > 1: (o 1 , • • • , o m-1 ) is an executable program p ′ by k on G s.t. p ′ (G) = G ′ and o m is executable by k on G ′ . In this case, p(G) = o m (G ′ ).
• By extension, an empty sequence is also a program. In this case, p(G) = G.

Let us now define what could be a program achieving a precise goal.

C. Goals and programs

An agent can act on a target AS in order to achieve some goals. A goal is formally represented by a formula in a language that expresses conditions that may hold for some AS (e.g. the target AS).

For representing these goals, we use the symbols appearing in the typology of the change properties defined in [START_REF]Characterizing change in abstract argumentation systems[END_REF]:

• arguments (x, y, z, etc), • extensions (E i , E ′ i ), • the set of extensions (E, E ′ ), their cardinality (|E|, |E ′ |),
• the set of all the extensions containing a particular argument x (E x , E ′ x ) and their cardinality (

|E x |, |E ′ x |),
• classical comparison operators (=, <, >, etc),

• quantifiers ∀ and ∃,

• membership (∈) and inclusion (⊆),

• union (∪) and intersection (∩) of sets,

• classical logical operators (∧, ∨, →, ↔, ¬).

We will note b k the goal of the agent k. Ex.1 (cont.) The goal b pros of the prosecutor can be represented by (x 1 ∈ E ′ ) with E ′ being the grounded extension of the jury AS.

Then, we give the notion of a program achieving a goal. In the next section, we study how to compute the operations that an agent should do in order to achieve her goal.

D. Change characterizations

A "naive" approach is to compute, for each executable operation, the set of extensions of the modified target AS and to check if the goal is achieved. Another more efficient approach uses the change characterizations which were studied in [START_REF] Cayrol | Change in abstract argumentation frameworks: Adding an argument[END_REF] and [START_REF] Bisquert | Duality between addition and removal[END_REF]. A characterization is a property that gives necessary and/or sufficient conditions for achieving a particular goal wrt a kind of operation and a semantics. We give two examples of characterizations:

Charact. 1 ( [START_REF]Characterizing change in abstract argumentation systems[END_REF]): When adding an argument z under grounded semantics, if z is not attacked by G and z indirectly defends x and x ∈ E, then x ∈ E ′ . This characterization concerns the goal of "enforcement" of an argument x. Enforcement, introduced by [START_REF] Baumann | Expanding argumentation frameworks: Enforcing and monotonicity results[END_REF], consists in ensuring that an argument which was rejected would be accepted. This characterization also specifies the operation involved: here the addition of an argument z. Thus, thanks to this characterization, we know (without requiring a new computation of the extensions) that if an operation adds an argument z under the grounded semantics, s.t. z is not attacked and indirectly defends another argument x which was not accepted, then x will become accepted.

Charact. 2 ([9]

): When removing an argument z under grounded semantics, if E = ∅ and z is attacked by G, then E ′ = ∅.

Here the goal concerns the evolution of the non emptiness of the extension. This characterization enables us to know, without any computation, that if an operation removes an argument z s.t. z is attacked by at least one argument of G and knowing that the extension was not empty before the change, then the extension obtained after the change will not be empty. This can be useful when one wants to make sure that the discussion will not be fruitless. This concludes our theoretical framework. The following section presents the tool that has been developed.

IV. PRESENTATION OF THE TOOL

The tool is organized around two modules: an AS handler, and an inference engine (for computing the change operations). The outputs of Module 1 are inputs for Module 2.

A. The argumentation systems manager

We present here the argumentative facet of the program, which may handle the creation of various AS and enable the computation of the extensions. This module is encoded in an object language (Python 2.7) which is convenient for implementing the concepts used. Thus, creating an AS requires a set of arguments and a set of attacks.

This module handles the consistency of the input data by checking that any argument appears only once (with the same name), and that the input attacks relate existing arguments. This module returns information concerning the AS and launches (on request) the computation of the extensions wrt a semantics (which can be provided as a parameter). In accordance with our theoretical framework, the tool makes it possible to create two AS, one for the agent and one for her target. This creation is carried out by providing the list of the arguments and attacks of these two systems. Moreover, the semantics used in the target system is also specified (it will be used to check the achievement of the goals of the agent). The agent AS and the target AS, as well as the extensions of this last, are then transmitted to the second module.

B. Inference Engine

This second module computes the change operations. More precisely, it allows to answer to the question "What are the operations executable by the agent on the target system that achieve her goal?".

The inference engine receives the agent AS and the target AS, as well as the set of extensions of the target for a given semantics. Besides, it is necessary to provide a goal that the agent wants to achieve on the target system and a set of characterizations allowing to check if an operation achieves that goal. Let us note that the user can filter the results by forcing the type of operation, for instance if she is only interested in the additions of arguments.

The heart of this module is a rule which generates all the operations executable by the agent on the target and achieving the goal, and produces, for each operation, the characterization justifying this result. This rule contains two parts, one part builds the operations, and the other checks that the operations fit the desiderata of the agent.

A synthetic vision of the tool, and thus of the articulation between its two modules, is given in Fig. 4.

This second module has been encoded with a logic programming language (Prolog) for two main reasons: the characterizations translate naturally into logical rules, and the mechanism of unification allows us to generate and easily filter the operations wrt the AS and the goal of the agent.

Construction of the operations: The construction of the operations is a direct translation in Prolog of Def.4. Thus, we generate executable operations and their impact on the argumentation graph (it is either the addition or the removal of an argument). This makes it possible to avoid considering operations that are not authorized or not executable and thus to optimize the computing time.

Checking the operations: After its generation by the construction rules, the operation is treated thanks to the characterizations (e.g., Charac.1 or 2). Thus, for a given operation, if there exists a characterization corresponding to the type of operation and the goal requested by the agent and if the conditions of this characterization are satisfied, then this operation will be provided to the user (with the corresponding characterization as an explanation).

Let us note that for the moment the tool only handles programs reduced to one elementary operation.

C. Application to the example

We illustrate the use of the tool on the example of the hearing: the prosecutor wants to have the argument x 1 accepted. He knows the arguments presented in Fig. 2 and has to modify the jury AS, represented in Fig. 3.

First of all, the necessary data must be provided, i.e. the sets of arguments and attacks that the prosecutor knows, the sets of arguments and attacks known by the jury (the target AS) and the semantics used by the jury (we suppose here that it is the grounded semantics).

The tool will deduce from these data the set of the extensions for the jury AS (E = {{x 0 , x 4 }}).

The prosecutor must also specify his goal: "x 1 must belong to the grounded extension".

And finally a set of characterizations must be provided. In order to simplify the explanation, let us suppose that this set is reduced to the single characterization 1.

The tool then generates the operations executable by the prosecutor on the jury AS and their impacts. For example:

({x 0 , x 1 }, {(x 1 , x 0 )}),
• ⊕, {x 5 }, {(x 5 , x 4 )} , which also successfully completes the construction step and whose impact is the system ({x 0 , x 1 , x 4 , x 5 }, {(x 1 , x 0 ), (x 4 , x 1 ), (x 5 , x 4 )}). Let us note that the operations concerning the arguments or attacks unknown by the agent, or which are not executable on the target AS, are not generated by the tool. Thus, the operation ⊖, {x 6 }, ∅ is not generated because the argument x 6 is not present in the jury AS. This ensures the finiteness of the process. Generated operations are examined at the same time through the characterizations. If an operation does not correspond to any characterization, it is rejected; if it matches with one or more characterizations, then the tool returns all the pairs (operation, characterization).

In our example, the operation ⊖, {x 4 }, ∅ is rejected because its type (removal of an argument) does not correspond to that specified in the only characterization available. On the other hand, the type of the operation ⊕, {x 5 }, {(x 5 , x 4 )} corresponds; the tool must thus check that the latter satisfies the constraints specified in the characterization, namely that z, in fact paired with the argument x 5 , is not attacked and that it must defend indirectly x (this last being paired with x 1 ) such as x does not belong to the extension2 . These conditions being satisfied, the operation realizes indeed the goal of the prosecutor.

V. EXPERIMENTS The aim of our tool is to find a "program" (in the sense of Def.5) achieving a goal. Note that, as a first step, we restrict the search to the programs containing only one operation. This search could have been made directly by computing the impact of an operation and then by checking the set of the extensions of the resulting graph. Nevertheless, recomputing extensions can be very expensive (see [START_REF] Liao | Dynamics of argumentation systems: A division-based method[END_REF]), whereas computing the impact of an operation is easy in terms of arguments and attacks (it just amounts to handle elementary operations on sets). Thus, our idea is to generate executable operations and "to check them" thanks to the characterizations, rather than compute the extensions for each resulting system and then check that the goal is satisfied. The benefits in terms of time and of space still remain to be evaluated (this will be the subject of a future study). Before analyzing the results produced by the tool (Sect.V-B), we present, in Sect.V-A, our experimental protocols. In Sect.V-C, we discuss their drawbacks and benefits.

A. Experimental Protocols

We propose two experimental protocols for checking the soundness of the implementation (of course, this use of the tool is not representative of its final use since they are only test protocols). These protocols will also enable us to reveal some lacks in the set of characterizations.

1) Inclusion Hypothesis:

Both protocols suppose that the target AS is a partial subgraph of the agent AS. This assumption seems natural in the court hearing example: the prosecutor and lawyer are aware of everything what is said during the hearing, so they know all the arguments that are present in the jury AS (their target) 3 .

2) Random Generation: This protocol aims at randomly generating two systems (one for the agent and one for the target) respecting the inclusion hypothesis, and at randomly generating a goal to achieve. Thus:

• a set of arguments of size n is created, with n being a random value between 2 and 20, • a set of attacks between these arguments of size nb att is created, with nb att being a random value between n * 0.5 and n * 1.5. This constitutes the first AS. It will be used as a basis to create a partial subgraph representing the target AS:

• two numbers sup arg and sup att are generated randomly, with sup arg being a value between 0 and n-1 and sup att being a value between 0 and nb att -1, • sup arg arguments are removed randomly from the set of arguments, and for each removed argument we subtract from sup att the number of attacks involving this argument, • sup att attacks are removed randomly. This enables us to obtain the second AS. And finally, a goal is randomly selected among

x ∈ E ′ , x / ∈ E ′ , z ∈ E ′ , E = E ′ , E ⊆ E ′ , E ⊂ E ′ , E ′ ⊆ E, E ′ ⊂ E, E ′ = ∅, E ′ = ∅,
where x belongs to the target AS, z belongs to the agent AS and E (resp. E ′ ) is the grounded extension of the target AS before (resp. after) the change.

The generation of operations is executed from these two systems and the goal (see the results obtained in Sect.V-B).

3) Systematic Generation: Although the random generation is efficient, it can leave aside some interesting cases. To solve this problem, we set up another experimental protocol consisting in exhaustively testing a list of pairs of AS.

Thus, for n arguments, we create all the pairs of AS s.t.:

• the first AS has a set of arguments arg agent (indexed from 1 to n) and a set of attacks att agent (the number goes from 0 to n * (n -1)). • the second AS has a set of arguments arg target varying among all the possible subsets of arg agent, and a set of attacks varying among all the possible subsets of att agent restricted to the arguments of arg target. We carry out the generation of operations for a given kind of goals: we have successively considered the enforcement of each of the arguments of the target AS. Our protocol computes the grounded extension of the system resulting from the operation. This enables us to reveal the "covering" problems of the tool, i.e. cases where no operation is found that achieves the goal whereas there is one (see Sect.V-B).

B. Results

For the random generation: For each pair of AS generated (in all five million), the first experimental protocol returns information concerning the generation of the executable operations achieving a goal chosen randomly. Ex.2 proposes a short extract showing a case of successful generation of operations. The tool generates two operations: ⊕, {x 2 }, {(x 2 , x 1 )} and ⊕, {x 2 }, {(x 2 , x 1 ), (x 1 , x 2 )} with the corresponding characterizations (here, it is twice the same -corresponding to Prop.16 of [START_REF]Characterizing change in abstract argumentation systems[END_REF]).

In addition, the protocol also proposes a summary of the results, for each goal, by detailing the number of cases where a solution is found. Tab.I shows an example of such results. For each goal, the second column gives the total number of pairs of AS tested by the tool. The third column (resp. fourth column) gives the number of times where the tool returned a nonempty (resp. empty) set of solutions. Lastly, the fifth column gives the percentage of the cases where the tool returned a nonempty set of solutions compared to the total number of cases tested for a particular goal.

Goal

Whether the tool finds solution or not depends on the goal considered. More precisely, there are two possible explanations when no executable operation is found:

• there does not exist any executable operation achieving the goal; let us note that this case includes the case where it is not possible to achieve this goal with only one operation (cf Ex.3). • a characterization is missing in order to find at least one operation (cf Ex.4).

Ex. 3: Consider the following AS and the goal E ′ = ∅:

Agent AS:

x1 x2 x4 x3
Target AS:

x1 x2 x4 x3
The tool does not generate any operation because there exist no executable operation achieving the goal: on the one hand, there exists no argument attacking at the same time x 2 , x 3 and x 4 and being attacked by at least one of them, and, on the other hand, it is not possible to remove all the arguments in only one operation.

Ex. 4: Consider the following AS and the goal E ′ = ∅:

Agent AS: x1 x2 x4 x3
Target AS: x4

The tool does not generate any operation, and yet, doing nothing would be enough to achieve the goal; thus there is a gap in the set of characterizations (the possibility of doing nothing had not been considered in [START_REF]Characterizing change in abstract argumentation systems[END_REF]).

The set of solutions provided by the tool can thus be empty for very different reasons but which are not distinguished by the protocol. The second experimental protocol has been set up in order to highlight examples revealing lacks in the set of characterizations (results given below).

For the systematic generation: By considering a particular goal, and by treating all the possible cases, this protocol enabled us to concentrate on the cases where the tool does not find a solution and thus to detect the lacks in our set of characterizations. Thus, we have enriched the set of characterizations, so that currently, for the goal corresponding to the enforcement of one argument in the grounded extension, the automatic generation for n = 3 or 4 does not detect any lack of characterization.

C. Discussing the protocols

Our protocol of random generation enables us to test a large number of examples (with various goals). However, the chosen examples are not necessarily representative of all the cases.

Concerning the systematic generation, it is very expensive: for a generation based on n arguments, there are 2 n * (n-1) possible AS for the agent and in the worst case 2 n * (n-1) + (n * 2 (n-1) * (n-2) ) + • • • + (n * 2 0 ) possible cases for the target AS. The total number of possible pairs is about

2 n * (n-1) * (2 n * (n-1) +(n * 2 (n-1) * (n-2) )+• • •+(n * 2 0
)). This is tolerable for a small number of arguments. For example, for n = 3, there are 2 6 * (2 6 + 3 * 2 2 + 3) = 5056 possible pairs. But this becomes prohibitive as soon as they are more than five arguments. This problem is partly due to the useless generation of isomorphic pairs of graphs.

The second disadvantage of this protocol is that it depends on the choice of the goal. It is thus necessary to redefine a protocol with each new goal.

VI. DISCUSSION AND CONCLUSION

We presented a theoretical framework and a tool able to find a change operation which achieves a goal given a target AS and given arguments and attacks from a "source" AS (representing the knowledge of an agent). This tool could be used as a cognitive assistant for human agents. We studied the behavior of this tool by means of two experimental protocols. Nevertheless the experiments are not finished, since our protocols do not allow to evaluate all the possible examples exhaustively.

Future works can be declined along three axes. The first axis relates to the tool itself:

• Since computing the extensions after change is very expensive (in spite of the progress made in [START_REF] Liao | Dynamics of argumentation systems: A division-based method[END_REF]), our objective is to show that our approach is less expensive. That will require to determine the complexity of the inference engine algorithm (written in Prolog), one difficulty being to take into account the check of the applicability of some characterizations4 . • In addition, we could consider programs with more than only one elementary operation (for instance by using standard planners). Considering sequences of operations will make it possible to carry out more complex modifications and thus to find more solutions. • We evoked the use of the tool to locate gaps of characterization; it could be interesting to develop a sharper analyzer which would detect all the executable operations than the tool does not find. The second axis relates to the experiments carried out thanks to the tool and its applications:

• The continuation of experiments, such as those presented in this article, is important in order to create "benchmarks" in the argumentation field. • It could be interesting to consider real cases of argumentation to establish other more concrete "benchmarks". In particular, online debates (on social networks for example) seem well adapted to our problematic. • The previous point constitutes a track of applications of our tool, which could enable a user to be guided in his choice of arguments to utter during an online debate. The third and last axis relates to theoretical points:

• At the time we developed our experimentation protocol, we assumed the inclusion of the target AS in the agent AS. This questions the complete or incomplete knowledge of the system on which the agent wants to act. Moreover the question of how the agent can update her own system deserves a thorough study. • It seems necessary to extend our hearing example in order to allow a real interaction between the prosecutor and the lawyer. In a more general way, this implies that

Figure 1 :

 1 Figure 1: Reference universe of Mr. X case.

Figure 2 :

 2 Figure 2: AS of the prosecutor (Gpros).

Def. 4 :

 4 Let k be an agent, G k = A k , R A k her AS and G = A, R A any AS. • an elementary operation is a triplet o = op, arg, att where op ∈ {⊕, ⊖}, arg ⊆ Arg, att ⊆ R and if op = ⊕ then |arg| = 1 and ∀(x, y) ∈ att, (x = y) and (x ∈ arg or y ∈ arg), if op = ⊖ then |arg| = 1 and att = ∅.

Figure 3 :

 3 Figure 3: AS of the jury (Gjury).

Def. 6 :

 6 Let k be an agent, b k her goal and G any AS. A program p of k on G achieving b k is an executable program by k on G s.t. p(G) = G ′ and b k holds in G ′ (or in (G, G ′ ) if the goal expresses a condition on both systems). Ex.1 (cont.) Considering the goal b pros represented by (x 1 ∈ E ′ ), the programs ( ⊕, {x 5 }, {(x 5 , x 4 )} ) and ( ⊖, {x 4 }, ∅ ) of the prosecutor on G jury achieve b pros .

Figure 4 :

 4 Figure 4: Architecture of the tool.

Ex. 2 :

 2 Consider the following AS and the goal x 1 ∈ E ′ : Agent AS: x1 x2 Target AS: x1

the set Arg. The relation R is represented in the graph of Fig.1.

	x0 Mr. X is not guilty of the murder of Mrs. X
	x1 Mr. X is guilty of the murder of Mrs. X
	x2	Mr. X's business associate has sworn that he met him at the time of the murder.
	x3	Mr. X associate's testimony is suspicious due to their close working business relationship
	x4 Mr. X loves his wife, so he cannot be her killer.
	x5 Mr. X has a reputation for being promiscuous.
	x6	Mr. X had no interest to kill Mrs. X, since he was not the beneficiary of her life insurance

Table I :

 I Summary of results for the protocol of random generation.

			Nb. of cases tested Non empty Set of solutions Empty	%
	x ∈ E ′	499216	443010	56206	88.7
	x / ∈ E ′	500009	397706	102303	79.6
	z ∈ E ′	500196	443931	56265	88.8
	E = E ′	499770	389933	109837	78.0
	E ⊆ E ′	499116	499116	0 100.0
	E ⊂ E ′	500697	489562	11135	97.8
	E ′ ⊆ E	499860	435600	64260	87.1
	E ′ ⊂ E	499546	402207	97339	80.5
	E ′	= ∅	500728	27222	473506	5.4
	E ′	= ∅	500862	279162	221700	55.7
	Total	5000000	3807449	1192551	76.1

In the case of addition of an argument, only a part of the known attacks may be provided; it is thus possible for an agent to carry out a "lie by omission", for example for strategic reasons. On the other hand, the agent is not authorized to provide unknown arguments or attacks; she cannot thus lie actively; this could be the object of future work.

• ⊖, {x 4 }, ∅ , which successfully completes the construction step and whose impact is the system

The notions appearing in the characterizations are implemented in the inference engine (for instance, indirect attack by an argument, direct and indirect defense by an argument, attack and defense of sets, etc).

Removing this assumption would mean to consider that an agent may not agree with the validity of some presented arguments or attacks. This refers to the question of the differentiation between being aware of the existence of an information and believing in its validity. This question would deserve a deeper study which is out of the scope of this paper.

Indeed some characterizations use complex concepts: for example the indirect defense of an argument by a set.