Antoine Muller

Coralie Germain

Charles Pontonnier

Georges A Dumont

Simple

A Simple Method to Calibrate Kinematical Invariants: Application to Overhead Throwing

A SIMPLE METHOD TO CALIBRATE KINEMATICAL INVARIANTS:

APPLICATION TO OVERHEAD THROWING Antoine Muller 1,2 , Coralie Germain 1,2 , Charles Pontonnier 1,2,3 and Georges Dumont 1,2

Ecole Normale Supérieure de Rennes, Bruz, France 1 IRISA/INRIA Rennes, Rennes, France 2 Ecoles Militaires de Saint-Cyr Coëtquidan, Guer, France 3 The aim of this paper is to present a simple calibration method aimed at optimizing the kinematical invariants of a whole body motion capture model, meaning limb lengths and some of the marker placements. A case study and preliminary results are presented and give encouraging insights about the generalized use of such a method in motion analysis in sports.

KEY WORDS: Subject-specific model, Inverse kinematics, Optimization, Baseball, INTRODUCTION: Matching lengths and joint centers of a generic biomechanical model with the dimensions of a specific subject is of importance in motion analysis, especially in sports biomechanics. A subject-specific calibrated model has more chances to catch the specificities of a given motion than a generic of badly scaled model. Andersen et al. (Andersen, 2010) proposed a well fashioned method to calibrate kinematical invariant properties of biomechanical models thanks to motion capture. It consists in finding the set of joint angles and kinematical invariants (e.g. limb lengths, or marker placements) minimizing the error between real and reconstructed markers on the whole capture under constraints maintaining joints consistency. The aim of the current paper is to propose a simple two-stage method to calibrate kinematical invariants, aimed at being used as the first step of an inverse dynamics motion analysis pipeline. An application to overhead throwing is proposed and results are discussed.

METHODS:

The calibration method used in this study is structured in 2 steps (Figure 1). The first step initializes the limb lengths, the marker placements and the set of joint angles. In the second step, the calibration itself is performed. The kinematical invariants are optimized. These calibrated parameters can be used to study the kinematical features (e.g. joint angles, joint velocities…) of the current motion or of any motion realized by the same subject. Where 𝑁 is the number of frames and 𝒒 𝑖 is a 𝑛 𝑞 -column vector, where 𝑛 𝑞 is the number of joint coordinates. The inverse kinematics step can be solved with 𝑁 optimization problems: Calibration: The aim of this calibration is to identify the optimal kinematical invariants for each subject. The optimized kinematical invariants are some of the limb lengths 𝒍 ̂ and some of the marker placements 𝒑 ̂𝑚 𝑙𝑜𝑐𝑎𝑙 .The method used in this study is inspired by the methods developed by Andersen et al. ( 2010) and Reinbolt et al. (2005). The set of joint coordinates obtained from the initialization step is defined as 𝒒 𝑖 𝑖𝑛𝑖𝑡 . The calibration consists in an optimization loop, divided into two stages (Figure 1). The first stage aims at finding the optimal parameters (𝒍 ̂, 𝒑 ̂𝑚 𝑙𝑜𝑐𝑎𝑙 ). Equation ( 2) describes the optimization problem applied on a set of frames 𝑁 𝑐 , where 𝑁 𝑐 could be a sub-set of 𝑁 randomly generated by bootstrapping, to reduce the computation time.

Find 𝒒 𝑖 (
Find 𝒑𝒂𝒓𝒂𝒎 = [𝒍 ̂, 𝒑 ̂𝑚 𝑙𝑜𝑐𝑎𝑙 ] 𝑇 (2) which minimize 𝐺(𝒑𝒂𝒓𝒂𝒎, 𝒒 𝑖 𝑖𝑛𝑡𝑒𝑟 ) = ∑ ∑‖𝒑 𝑚 𝑔𝑙𝑜𝑏𝑎𝑙 (𝒑𝒂𝒓𝒂𝒎, 𝒒 𝑖 𝑖𝑛𝑡𝑒𝑟 ) -𝒑 𝑚,𝑟𝑒𝑎𝑙 (𝑡 𝑖 )‖ 𝑚 𝑖 2
where 𝒒 𝑖 𝑖𝑛𝑡𝑒𝑟 represents the joint coordinates computed in the last inverse kinematics step (e.g. for the first loop, 𝒒 𝑖 𝑖𝑛𝑡𝑒𝑟 = 𝒒 𝑖 𝑖𝑛𝑖𝑡 ). The second stage of the calibration step (Figure 1) aims at actualizing the joint coordinates with the updated (𝒍 ̂, 𝒑 ̂𝑚 𝑙𝑜𝑐𝑎𝑙 ). This inverse kinematics step is solved as shown in equation (1). For each iteration, a reconstruction error is computed. This error corresponds to the average distance between a reconstructed marker and the associated real marker. The optimization loop stops when the variation of the mean error between two iterations is below 5%. Case study: The aim of this case study was to validate the method presented above. For this purpose, this method has been implemented in Matlab® and a visualization tool has been designed thanks to the Simmechanics toolbox. The results of the calibration and the inverse kinematics were compared to the ones obtained with the Andersen at al. ( 2010) method that is already implemented in the Anybody TM modeling software (Anybody Technology). This software is widely used in the biomechanics community. A classical motion capture analysis was used. One pilot trial was performed on a single subject in our lab. The subjecta 60 kg, 170 centimeters, 24 years old manwas not specially trained to baseball throwing. This experiment was composed of 4 overhead throwing. Each of these took about 3 seconds. 40 motion capture markers were placed (Figure 2(a)) on the whole body. The markers were recorded at 100 Hz using a Vicon motion capture system. The addition of asymmetric markers helped to the reconstruction of marker trajectories. Then, these markers trajectories were filtered using a 4-th order Butterworth low pass filter with a cut-off frequency of 5 Hz and no phase shift. For each trial, both calibration methods were applied. Each limb length was optimized. Additionally, placements of the markers for uncertain bony landmarks were optimized. Then, optimized limb lengths and markers placements of a given trial were used to perform inverse kinematics on all the trials to test the inter-trial robustness of the method. For both methods, the optimized limbs lengths were relatively unaffected by the motion capture used as input. Moreover, even if both methods gave slightly different results, they also gave consistent lengths in accordance with the literature. It is therefore interesting to extend this study to different types of motion to test its robustness. Figure 3 compares the mean marker error obtained for each trial after calibration with both methods. Trials were here self-calibrated, meaning that the calibration was realized with the studied trial. The order of magnitude of the error was the same for both methods and was arguably reproducible from one capture to one other. Moreover, the standard deviation seemed to be low compared to the error, meaning that the error remained relatively constant against time. This observation tends to show that the remaining reconstruction error was due to non-calibrated invariants. The results presented above are encouraging since the calibration method showed comparable results to the one of AnyBody TM . However, the small sample size of trials ask for further comparisons to be completely valid. Table 2 shows the reconstruction error for each trial from different calibrations using our calibration method. The standard deviation of these errors was valued at 0.4 mm. Thus, after the inverse kinematics step, the reconstruction error was relatively unaffected by the trial used to calibrate. Furthermore, the use of only one calibration for a set of motion capture seems to be sufficient. For a given throwing trial, the smallest error was expected when the calibration was realized with this trial (diagonal elements). This result was apparent in the first three motion capture contrary to the fourth. The difference observed was very low in comparison with the error. It was probably due to the fact that, in the parameters identification step, only a sub-set of all the motion capture frames was used. For the study, this sub-set was chosen randomly. It is therefore interesting to deepen this work in defining a paradigm enabling a consistent choice for this sub-set.

Figure

  Figure 1: Calibration pipeline Initialization: The whole body skeletal model used in this study is composed of 21 rigid segments linked by 17 joints and exhibits 32 degrees of freedom. The lower limb model is based on Klein Horsman's model (2007). The de Zee's spine model (2007) is integrated to the trunk model. The upper limb model is based on Holzbaur's model (2005). A uniform scaling in all directions (Rasmussen, 2005) is used to initialize kinematical invariants parameters on the basis of the current subject's size. The initialization of the joint angles is an inverse kinematics step. This step aims at computing a set of joint coordinates 𝒒 𝑖 = 𝒒(𝑡 𝑖 ) from a motion capture, for 𝑖 = 1, 2, … , 𝑁.

Figure 2 :

 2 Figure 2: Full body model and marker placements during the throwing the pilot trial. (a) -Experimental setup for Motion capture; (b) -Our model; (c) -AnyBody TM model. RESULTS AND DISCUSSION: Table 1 summarizes the limb lengths 𝒍 ̂ * obtained with our calibration (Figure 2(b)) and the ones obtained in AnyBody TM (Figure 2(c)) for all trials. The lengths of the distal members were not compared due to their dependency to the associated markers location. Markers placement comparison seemed difficult to achieve since their local coordinates were not expressed in the same way for both models.

Figure 3 :

 3 Figure 3: Mean distance between a reconstructed marker and the associated real marker and standard deviation over four throwing motion capture with the two methods

  𝑡 𝑖 ) is the position of the 𝑚-th real marker at the time 𝑡 𝑖 , obtained by the motion capture. 𝒑 𝑚 𝑔𝑙𝑜𝑏𝑎𝑙 (𝑞 𝑖 ) is the global position of the 𝑚-th reconstructed marker at frame 𝑖. At this stage, the local coordinates of the markers 𝒑 𝑚 𝑙𝑜𝑐𝑎𝑙the coordinates relative to the segment coordinates systemare fixed and 𝒑 𝑚 𝑔𝑙𝑜𝑏𝑎𝑙 (𝑞 𝑖 ) are reconstructed thanks to homogeneous transforms.

	which minimize	𝐹(𝒒 𝑖 , 𝒑 𝑚 𝑙𝑜𝑐𝑎𝑙 , 𝒍) = ∑‖𝒑 𝑚 𝑔𝑙𝑜𝑏𝑎𝑙 (𝒒 𝑖 ) -𝒑 𝑚,𝑟𝑒𝑎𝑙 (𝑡 𝑖 )‖	2	1)
	where 𝒑 𝑚,𝑟𝑒𝑎𝑙 (	𝑚

Table 1 : Comparison of the limbs lengths calibration methods using different motion capture. 𝝈

 1

			Anybody TM calibration			Our calibration
	𝒍 ̂ * [cm]	Throw 1	Throw 2	Throw 3	Throw 4	𝜎 𝑛 [%]	Throw 1	Throw 2	Throw 3	Throw 4	𝜎 𝑛 [%]	𝜀 𝑛 [%]
	Pelvis width	15.55 15.55 15.55 15.55 0.02 14.26 14.37 14.21 14.27 0.32 8.19
	Thigh lengths	41.48 41.64 41.47 41.69 0.23 42.49 42.56 42.36 42.49 0.14 2.18
	Shank lengths	39.61 39.44 39.48 39.49 0.13 39.67 39.61 39.61 39.73 0.11 0.38
	Trunk height	55.33 55.67 54.78 54.81 0.64 53.11 53.11 52.94 53.04 0.11 3.80
	Upper arm lengths 28.74 28.48 28.38 27.91 0.83 29.81 29.93 30.03 30.04 0.28 5.56
	Lower arm lengths 27.52 27.47 27.36 27.85 0.54 26.04 25.97 25.84 25.89 0.27 5.87

𝒏 : normalized standard deviation. 𝜺 𝒏 : mean of the relative difference between methods.

Table 2 : Mean markers error depending on the trial used for calibration

 2 The current paper aimed at presenting a simple calibration method for kinematics invariants based on a two-stage optimization scheme. Results obtained on overhead throwing motions showed encouraging results, comparable to the state of the art in terms of accuracy and repeatability. Further investigations are warranted to test the robustness of the method and to add other kinematical invariants (e.g. rotation axes). This work is a first step and further developments to include whole-body inverse dynamics and muscle forces estimation are currently ongoing. This work aims to develop a simple tool ready to use for motion analysis, in particular for sports applications such as training, motion optimization or injury prevention. Journal of biomechanics, 40(6), 1219-1227. Holzbaur, K.R., Murray, W.M. & Delp, S.L. (2005). A Model of the Upper Extremity for Simulating Musculoskeletal Surgery and Analyzing Neuromuscular Control. Annals of Biomedical Engineering, 33(6), 829-840. Horsman, M.K., Koopman, H.F.J.M., Van der Helm, F.C.T., Prosé, L.P. & Veeger, H.E.J. (2007). Morphological muscle and joint parameters for musculoskeletal modelling of the lower extremity. Clinical biomechanics, 22(2), 239-247.

	Mean reconstruction	Calibration
		error [m]	Throw 1 Throw 2 Throw 3 Throw 4
	Motion capture	Throw 1 Throw 2 Throw 3	0.0126 0.0141 0.0138 0.0142 0.0132 0.0130 0.0130 0.0132 0.0131 0.0131 0.0128 0.0132
		Throw 4	0.0133 0.0132 0.0131 0.0132
	CONCLUSION: REFERENCES:
	Andersen, M.S., Damsgaard, M., MacWilliams, B. & Rasmussen, J. (2010). A computationally efficient
	optimisation-based method for parameter identification of kinematically determinate and over-
	determinate biomechanical systems. CMBBE, 13(2), 171-183.
	De Zee, M., Hansen, L., Wong, C., Rasmussen, J. & Simonsen, E.B. (2007). A generic detailed rigid-
	body lumbar spine model.

Rasmussen, J., Zee, M.D., Damsgaard, M., Christensen, S.T.,

Marek, C. & Siebertz, K. (2005)

. A general method for scaling musculo-skeletal models. Int. Symp. on computer simulation in biomechanics. Reinbolt, J.A., Schutte, J.F., Fregly, B.J., Koh, B.I., Haftka, R.T.,

George, A.D., & Mitchell, K.H. (2005)

. Determination of patient-specific multi-joint kinematic models through two-level optimization. Journal of biomechanics, 38(3), 621-626.


Iulia Dragomir
email: iulia.dragomir@irit.fr

Iulian Ober
email: iulian.ober@irit.fr

David Lesens
email: david.lesens@astrium.eads.net

A case study in formal system engineering with SysML

Keywords: system engineering, modelling, SysML, simulation, model-checking, temporal properties, abstraction

In the development of complex critical systems, an important source of errors is the misinterpretation of system requirements allocated to the software, due to inadequate communication between system engineering teams and software teams. In response, organizations that develop such systems are searching for solutions allowing formal system engineering and system to software bridging, based on standard languages like SysML. As part of this effort, we have defined a formal profile for SysML (OMEGA SysML) and we have built a simulation and verification toolbox for this profile (IFx). This paper reports on the experience of modelling and validating an industry-grade system, the Solar Generation System (SGS) of the Automated Transfer Vehicle (ATV) built by Astrium, using IFx-OMEGA. The experience reveals what can currently be expected from such an approach and what are the weak points that should be addressed by future research and development.

I. INTRODUCTION

One of the major risks of errors in the development of real time critical embedded software is the misinterpretation of the system requirements allocated to the software. These misunderstandings between the system team and the software team may have several sources, but are very often due to the following causes:

• Use of ambiguous means to describe the system requirements and the software implementation, leading to different interpretations by the system designers, the software developers and the reviewers.

• Insufficient knowledge by the software team of the formalisms and jargon used by the system team, leading to the development of software that does not satisfy the system requirements.

• Insufficient knowledge by the system team of the formalisms and jargon used by the software team, leading to inefficient reviews of the software specification and code by the system team. The errors potentially introduced during the development are then generally discovered very late by very costly test processes.

This situation is a cause of particular concern in the aerospace domain, where multiple suppliers have to build integrated systems based on common system requirements. It has lead the main actors of the field (agencies and main contractors) to search for solutions allowing formal system engineering and system to software bridging. One such effort was the ASSERT project 1 led by the European Space Agency (ESA), with the objective of defining a complete system/software engineering process for complex and critical space systems. The ASSERT development process is now supported by a set of tools called TASTE [START_REF] Conquet | The TASTE Toolset: turning human designed heterogeneous systems into computer built homogeneous software[END_REF]. The main scope of the ASSERT project was the management of non functional requirements, from the capture of system requirements to the automatic generation of code. The present work is part of a follow-up project, Full MDE 2 [START_REF] Conquet | Formal Model Driven Engineering for Space Onboard Software[END_REF], which aims to complement the ASSERT process on the functional aspects, allowing full functional system modelling based on an adapted use of the SysML standard [START_REF]Systems Modelling Language (SysML) v1.1[END_REF].

SysML is a graphical modelling language well adapted for system engineering and it is increasingly used in industry in the development of real-time embedded systems. For example, Astrium Space Transportation has deployed SysML for capturing the systems requirements of the new version of the Ariane-5 launcher. But its semantics is underspecified in order to preserve the generality of the language. The OMEGA Profile [START_REF] Hooman | Supporting UML-based development of embedded systems by formal techniques[END_REF], previously defined for UML [START_REF]Unified Modelling Language (UML) v2.2[END_REF], has been adapted to SysML in order to suppress any ambiguities and provide a formal operational semantics, rendering SysML models amenable to formal verification. The UML version of the OMEGA profile was conceived to be used in the design and validation of real-time embedded systems, and it has been used in several industry-grade models (e.g., [START_REF] Ober | Modeling and validation of a software architecture for the Ariane-5 launcher[END_REF], [START_REF] Ober | Timing analysis and validation with UML: the case of the embedded MARS bus manager[END_REF]) providing interesting validation results. Like the UML profile, OMEGA SysML is implemented in the IFx toolkit 3 [START_REF] Ober | Validating timed UML models by simulation and verification[END_REF] which provides simulation and timed-automata based model-checking [START_REF] Clarke | Model Checking[END_REF].

In this paper we assess the use of OMEGA SysML and IFx in the design and validation of the system models of a space vehicle control subsystem: the Solar Generation System (SGS), which manages the deployment and positioning of the solar wings of the Automated Transfer Vehicle (ATV) 4 developed by Astrium Space Transportation for the European Space Agency. The case study, led by Astrium, covers the entire system engineering phase of SGS; however, in this paper we concentrate on the aspects that are specific to OMEGA SysML and in which the IFx toolbox plays a role. The OMEGA SysML profile was used in reverse engineering to capture the system architecture, covering software, hardware and external subsystems interacting with the SGS, and to give a high-level functional model for each of these pieces. In terms of SysML, the architecture description takes the form of block diagrams, and the functional description of the blocks takes the form of detailed state diagrams, including timing and lower-level action details. The overall system requirements are also formalized so that their satisfaction can be determined by simulation and model-checking with the IFx toolbox.

The case study shows how a formal system engineering approach helps increasing the confidence in system design models, which are used as starting point in the subsequent development steps. The purpose of this paper is to reveal what can currently be expected from such an approach and what are the weak points that should be addressed by future research and tool development.

Paper structure: In Section II we position the IFx-OMEGA approach in the Full MDE Process, while Section III presents an overview of the OMEGA SysML Profile. Section IV provides a brief description of the architecture and main functionalities of the SGS case study. Section V presents the verification model and the properties this model has to satisfy. The validation methodology and the main results obtained by simulation and model-checking are described in Section VI. In Section VII we position our approach with respect to other toolsets, before concluding.

II. THE FULL MDE PROCESS

The Full MDE project aimed at filling the gaps between system modelling and software modelling, and between the code generated automatically from the software model and manual code corresponding to functional requirements, by using a Model Driven Engineering (MDE) approach.

In the Full MDE process, each step of development of embedded software is formalized by safe and non-ambiguous languages which also provide proof techniques. The Full MDE approach has selected:

• for system design, the OMEGA SysML Profile which is also used in the ASSERT process to capture nonfunctional requirements;

• for software design, SCADE suite [START_REF]SCADE Suite website[END_REF] -a graphical modelling language mixing automata and data flow views -and

• for implementation code, the SPARK Ada language The purpose of a formal approach is to verify as early as possible by simulation and proofs the system and to discover potential errors, an approach that is more reliable and potentially less costly compared to a more traditional one relying only on informal paper documents and on tests.

Figure 1 summarizes the Full MDE process.

The system design is an important task for the development of critical systems and it guides the entire process. The architecture of the system and its properties are expressed in the OMEGA SysML Profile and are subject to formal validation within the IFx toolbox. Once it is verified, the model is transformed and integrated into SCADE modeller which verifies the complementary sets of requirements. SPARK Ada code is then generated automatically from SCADE by a certifiable tool. The combination of SPARK and SCADE allows the verification of correct integration of manual and generated code, the absence of runtime errors and the satisfaction of functional properties. A more detailed description of the process can be found in [START_REF] Conquet | Formal Model Driven Engineering for Space Onboard Software[END_REF].

III. OVERVIEW OF OMEGA SYSML AND IFX

OMEGA SysML defines the semantics of a rich subset of SysML elements, providing the necessary constructs for modelling real-time embedded systems designs. The profile also defines a very few extensions, in the form of stereotypes; their use however is not mandatory and a SysML model can generally be interpreted as an OMEGA SysML model without syntactic changes.

The architecture of a system is defined in terms of blocks; OMEGA supports most of the standard features of SysML blocks, such as properties (attributes and parts), relationships (associations, compositions and generalizations), interconnection elements (connectors, ports, interfaces) and mechanisms for defining structured data types and signals.

As usual in SysML, such elements are described in Block Definition Diagrams (BDDs) and Internal Block Diagrams (IBDs). Being a formal profile, OMEGA defines a set of additional well-formedness rules, in particular for strong static typing. The profile also clarifies the semantics of elements that are not fully described in the SysML standard, such as the default behaviour of ports. The well-formedeness rule set is fully formalized in OCL [START_REF]Object Constraint Language (OCL) v2.2[END_REF] and is enforced by the IFx tools, which encourages rigorous system engineering. Further details on the rules, their rationale and their formalisation can be found in [START_REF]Unambiguous UML Composite Structures: The OMEGA2 Experience[END_REF].

The behaviour of system components is expressed in OMEGA by state machines, possibly involving detailed action descriptions, which can be structured into operations. Actions are expressed in concrete textual semantics, compliant with the UML action metamodel, and cover notions like: variable assignments, signal output, block and connector creation/destruction, operation calls, expression evaluation, value return. As the standard action language of the OMG, ALF [START_REF]Action Language for Foundational UML (ALF)[END_REF], is under work, there are plans to use ALF as action syntax in OMEGA in the future.

OMEGA defines a timed operational semantics, based on the asynchronous composition of the behaviours of different blocks. In order to allow the user to control the concurrency granularity, which can have an important impact on the effectiveness of the verification tools, the semantics partitions the set of blocks into activity groups, based on the concurrency meta-attribute (a standard feature of SysML). Thus each block can be defined as active or passive, and each active block defines an activity group consisting of itself and its dependent passive blocks. Activity groups are executed concurrently and they react to external stimuli (signals) in atomic run-to-completion steps. Details on the execution and communication model can be found in [START_REF] Ober | OMEGA2: A New Version of the Profile and the Tools[END_REF].

The model time base can be either discrete or dense and it is specified by the user when simulation or model-checking is performed. Model time is controlled using the primitives of timed automata with urgency [START_REF] Bornot | An algebraic framework for urgency[END_REF]: clocks, timed guards and transition urgency annotations, which are stereotypes used to control how logical time can progress depending on the transitions that are fireable in a certain state. Time progress can thus be disabled (when at least one urgent transition is fireable), enabled but bounded (when there is no urgent transition but there is at least one delayable transition), or enabled and unbounded.

One of the few syntactic extensions defined in the profile concerns observers, which are used to formalize the system requirements that correspond to timed safety properties. An observer is a special type of block (stereotyped with ≪observer≫) that can monitor the system states and events and give verdicts about the (non-)satisfaction of a requirement. Its behaviour is defined by a state machine, with some states qualified as ≪error≫, respectively ≪success≫, states expressing the (non-)satisfaction of a safety requirement.

The SysML Profile is implemented by the IFx-OMEGA toolbox, which provides static checking, compiling, simulation and model-checking tools. The tools rely on the translation of the relevant parts of a model to the input language of the IFx Toolset5 [START_REF] Bozga | The IF Toolset[END_REF], which is based on asynchronous communicating timed automata.

IV. THE ATV SOLAR GENERATION WING MANAGEMENT SYSTEM

The ATV, developed by Astrium Space Transportation for the European Space Agency, is a space cargo ship launched into orbit by the European heavy launcher Ariane-5 with the aim of resupplying the International Space Station. The case study presented here -the Solar Generation Subsystem (SGS) -manages the solar arrays which provide the vehicle, for up to 6 months, the energy needed to fulfil its mission. SGS is responsible with providing functional chains to realise the solar arrays deployment and controlling the rotation of the solar wings of the ATV.

The SGS consists of a set of hardware and software entities; its software part is a subsystem of the Flight Application Software. The hardware of this subsystem has more than 70 devices, with multiple levels of redundancy for achieving reliability and availability in case of failures. Its main elements are the four wings, each of them being powered by two motors; a set of four motors (one from each wing) is controlled by a solar array driving electronics (SADE). Each wing has four hold-down and release systems (HDRS) which maintain the wing in its initial stowed position during the Ariane-5 flight. To deploy a wing, each HDRS has to be cut by a thermal knife; there are two knives for each HDRS, a nominal one and a redundant one. All these hardware pieces are enabled at the right time by four power units and four thermal control units. The activation of each piece of hardware is given by two command and monitoring units which also supervise the entire system. Each thermal control unit has 2 regulators -solar arrays driving group (SADG) -, which control 4 thermal knives each. Each regulator cannot power more than one thermal knife at a time.

The system has two operating modes:

1) The solar wing deployment mode. During take-off the four wings of the ATV are stowed. Their deployment starts by removing the safety barriers from the thermal control units (TCU). Safety barriers prevent the unwanted release of a wing by forbidding the enabling of the thermal knives by the TCUs. Then the restraint cables are cut by at least 4 of the 8 thermal knives of the wing. In order for the HDRS to be cut, each knife has to be active for 50 seconds. The deployment of the panels starts immediately after the last hold-down system has been cut. The deployment motion is driven by deployment strings at the root hinge and the panel hinges. After the deployment is completed, the panel hinges and root hinge lock positively to provide a stiff, backlash free, deployed configuration and safety barriers are restored.

2) The solar wing rotation mode. It is realized by two motors that control the position of the wing and connect it with the avionics equipment chain. The position of the wing is measured by reed switches and magnets fixed on the wing's motors. The solar array driving electronics that control the wings are working in cold redundancy: at a given time only one can be on and control the orientation of the 4 wings. The measures captured by the sensors are sent via the active SADE device to a central processing unit which numerically computes the direction in which the wings should be rotating and their speed, results sent back to SADE to be executed. The rotating mode is infinite, by cyclic activation of one SADE device.

V. THE SYSTEM MODEL In the scope of the Full MDE R&T project, the SysML model has been built in reverse engineering by the Astrium engineering team using IBM Rhapsody 6 . In this section we describe the architecture of the model, the structural issues that have been detected by applying the OMEGA well-formedness rules and the changes they induced in the model, and the formalization of the dynamic property that was verified.

A. The original system model

The SysML model captures both the architecture of the system and its timed behaviour. There are three types of blocks:

• 9 hardware block types describe the equipment of the ATV. Their behaviour is generally split in two operating modes: a healthy mode which models the nominal behaviour and a failure mode.

• 3 software block types, each with a specific function (e.g. deployment, rotation, etc). Each block reacts to stimuli coming from the environment (external mission management) and controls the behaviour of the hardware devices by executing automated procedures.

• A block that "simulates" the mission management. It initiates the two functionalities of the ATV solar generation system (deployment and rotation of wings) respecting the timing constraints imposed by each of these modes. In order to validate the software, the mission management models a finite behaviour -the wing deployment and three wings rotations. Some blocks are further decomposed in sub-blocks, the maximum depth consisting of 4 layers. The model defines a total of 20 block types (7 of which are refined by means of 24 Internal Block Diagrams), 204 ports and 234 connectors. The entire system contains 95 block instances: 12 composite ones refined into 78 hardware devices, 3 software instances, one instance of the mission management and the one representing the entire system; with a total of 517 port instances and 366 connectors.

B. Static coherence and compliance with OMEGA

The first benefit of applying the Full MDE process to this SysML model comes from the application of the static well-formedness rules of the OMEGA profile, which allows detecting a range of inconsistencies, in particular related to typing. Indeed, standard SysML modelling tools like Rhapsody do not impose strong static typing rules, and accept for example the definition of untyped ports. Since ports are not typed, connectors can also be defined between potentially incompatible ports. Such errors can go unnoticed throughout the system engineering phase, and last sometimes until the integration test campaign, when correcting them becomes very costly.

The initial SGS model did not contain any interface definition, and all the 204 ports were untyped. The errors provided by the OMEGA compiler have led to the definition of 18 interfaces which were used to specify port contracts. This allowed us also to detect connection errors in the model, such as duplicated connectors. We found that around 20% of the ports defined throughout the model were not respecting the uniqueness and completeness rules, which means that the destination of an incoming signal was either undefined or ambiguous. This led to another reiteration on the system model either correcting the contract for these ports or splitting their functionality with respect to the target object.

As a counterpart, several syntactic changes were required for static compliance to the OMEGA profile. For example, OMEGA requires unique names within a block or state machine: an attribute and signal reception having the same name or two sub-states within two parallel states of the same statechart with the same identifier are forbidden. The syntax for certain constructs (timers, enumeration literals, access to arrays, etc.) is different from the one used in Rhapsody/C++. However, the effort required for these syntactic changes is minor relative to the size of the project: between 1 and 2 person*days for the SGS model.

C. Preparing the model for formal verification

Once the model is statically coherent and compliant with OMEGA, some effort is still necessary to prepare it for formal verification, in particular for formally defining the properties to be verified. The main objective, for SGS, was to verify that the system is 1-fault tolerant: the mission succeeds even if one component of the system has failed during execution. Injecting failures into the system model. The failure mode was already modelled for each of the 62 hardware devices of the SGS: thermal knives, hold-down and release systems, thermal control units, solar arrays driving groups, power units and command and monitoring units. However, in order to ease the definition of verification configurations, we decided to add a block that commands the failure of one equipment, chosen based on a parameter that can be configured before each verification session without recompiling the whole model. We have added another 144 ports and 138 connectors for inducing errors. The target device fails nondeterministically, at an arbitrary moment during the system execution. Formalizing system properties. Requirements are captured by OMEGA observers, then verified against the model under the 1-fault hypothesis.

The requirement we describe here is defined with respect to temporal properties of the system and is concerned with the behaviour of the system in case of failure: no matter what error for equipment devices is injected in the system, the deployment of the wings shall succeed. This implies that the redundant devices replace nominal ones in case of failure.

Property 1: After 10 minutes since SGS start-up, all four wings are deployed and the mission management is aware of it.

The observer in Figure 2 models this property. In the initial state the system is off. Because we need to observe specific objects from the system and these objects exist only after the initialization of the entire system, the observer waits until the initialized signal is emitted by the ATV. Then it triggers the transition and arms a clock with the value deployment duration, in this case 10 minutes. If after this deadline the four wings have not been deployed, the observer enters the state NOT DEPLOYED and the property is violated. If the wings have been deployed, the observer enters the state DEPLOYED in which it verifies if the mission management is aware of it. After the entire deployment process, the software piece concerned by this task verifies the locked status of the wings, via an intermediary control and monitoring unit (CMU), and forwards the global confirmation to mission management (MVM). The MVM resumes its behaviour and continues its mission until the END state is reached. Then the observer enters the success state MISSION EVENT and the expressed property is satisfied. If it is not the case in the time passed from startup then an error has occurred and the property is violated.

VI. SYSTEM VALIDATION

A. Validation methodology

In IFx-OMEGA, the validation of models consists in performing several steps, supported by different tools, according to the following workflow:

1) The first step is the translation phase from the OMEGA model to an IF model by a sysml2if compiler, which enforces the well-formedness rules defined by the profile and allows detecting some static errors, as already discussed in Section V-B. 2) One can proceed with an interactive random simulation phase, which allows us to quickly detect certain problems, such as deadlocks that occur systematically. 4) The main validation step is the model-checking phase which, in IFx-OMEGA, consists in the exhaustive exploration of the product state space of the relevant part of the model and a set of observers while searching for the absence of error states and stopping at success state. If the model-checking algorithm finds errors then it produces scenarios which can be replayed in the simulator, in order to diagnose the cause. The verification is usually not a one-shot phase, different strategies for reducing the combinatorial explosion of the state space being often applied in an iterative fashion. In IFx-OMEGA, some reduction of the state space can be obtained automatically, for example by applying conservative model transformations based on static analysis techniques (dead code/variable elimination, variable abstractions) or by applying partial order reduction [START_REF] Godefroid | Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem[END_REF]. However, it is often necessary to involve the user for manually defining abstractions, as we will show in the case of SGS.

B. Validation by simulation

Despite the fact that the SysML model had been thoroughly reviewed, the interactive simulation of nominal scenarios and the execution of a series of random simulations allowed several modelling errors to be found.

Most errors discovered in this phase concern unexpected message receptions. When a block receives a message while in a particular state when the message is not expected, it will block and this generally leads to a global deadlock or model failure. In the SGS model, several such problems have been found in the behaviour of thermal knives and of wings. Some unexpected message receptions had to be modelled.

In some cases, like for the SGS mission management block, the unexpected message receptions were due to the existence of parallel composite states reacting to the same message; the designer intended only one parallel state to react to the message during a certain flight phase, but failed to specify correctly the conditions that enabled and disabled the receptions when going from one phase to another. Even if the model is intended to be a high-level system description, such behaviours can be quite intricate and errors are difficult to find without a simulation tool.

We mention that the length of a SGS simulation scenario is around 2400 steps (a step corresponding to the firing of a transition), and needs less than a minute to be executed on a regular desktop computer.

C. Verifying the absence of deadlocks

Even though a large set of deadlocks was detected and corrected during the simulation phase, in unexplored states of the system other deadlocks might appear. These ones concern the hardware devices which can block if the software parts send inadequate (sequences of) requests. The absence of deadlocks ensures only that the system is correctly modelled and does not guarantee that the system correctly behaves. Finding the modelling errors that result in deadlocks is an important task since we can detect unrealistic behaviours of the modelled systems that often go unnoticed due to incorrect interpretations of the model until software integration.

It was the case for solar array driving electronics (SADE), responsible for the wing rotation, which failed due to an incorrect deactivation sequence: the deactivation command preceded the disabling command. The two signals were sent in this order by the software: deactivation via a power unit and disable directly, without any timing constraints being imposed. This error was due to an unrealistic approximation made in the model, namely that the deactivation command is executed in zero time. In the real software, the deactivation command has a 200 ms execution time thus leading to a correct switch-off of the device. The correction consisted in adding a timer for the deactivation command in the power unit.

No other deadlocks were found after this verification step, under the hypothesis of no induced failures.

D. A failed model checking attempt with positive results

The next validation step was to attempt to verify, by model-checking, the property described in Section V-C. This requirement had to be verified against the 62 possible failures of hardware devices. In the current configuration of the system, the verification of this requirement does not finish 7 .

We chose to continue by using a non-exhaustive exploration strategy: the system is executed on only two threads, one thread for the simulation block which induces failures 7 We were using a IA64 computing server with 16GB of memory. The state space generation had to be stopped after 3 hours as the memory was exhausted.

and the second thread for all the other SGS blocks. This execution is partial in the sense that signals sent to different blocks are always handled in the order in which they were sent and different action interleavings are not taken into consideration. But, as long as errors are detected, it is an acceptable search strategy, and it allowed finding the three errors detailed below:

• In case of a power unit failure, the violation of Property 1 led us to discover a major error in the model concerning the connections between the power units and the wings. With the initial connections, in case of power unit failure, a wing could not be deployed, because both the nominal and the redundant connection were established between the same power unit and wing. In order to really be one fault tolerant, each power unit shall power two wings, and each wing shall be powered by two units.

• In the case of a thermal knife failure, in a particular configuration, the state machine of the corresponding hold-down and release system could deadlock because two knife OFF signals were received (one from the nominal, one from the redundant knife) but only one was handled.

• In the case of a control and monitoring unit failure, Property 1 is rejected. At the end of the deployment mode, wings' status verification does not finish in the given time and the MVM does not receive the confirmation to continue its mission. This type of error is actually incorrect, since, in reality, the CMU is composed by two independent devices which make it 1-fault tolerant, and it has been removed from the set of possible induced failures. A similar case was found for thermal control unit failures, which have also been eliminated. These errors are very similar to those found by interactive simulation, but the particular configurations in which they occur makes them very hard to detect without an automatic search of the state space.

E. Verification using abstractions

After the errors described above were corrected, the state space search with concurrency reduced to two threads produced no further errors. However, since the reduction eliminates potentially problematic executions, this is not sufficient to establish the satisfaction of the required property in the general case. To proceed with verification, we set out to use abstractions.

Figure 3 shows the communication graph of the SGS system, generated automatically from the state space explored as discussed before. Nodes represent block instances and arrows represent the existence of at least one signal communication between the block instances at the ends. In order to make it readable, we structure the graph accordingly to the three categories of the system -mission management, software and hardware -and we group the instances of each As one can see, each of the 4 wings generate a large structure of block instances, corresponding to the hardware equipment of the wing. However, from the point of view of the software blocks (which are the only other blocks with which it communicates), a wing that does not experience any hardware fault exhibits a very simple behaviour: it ends up by being deployed. Therefore, one can set out to verify the property of deployment under 1-fault hypothesis (Property 1) by replacing all the 3 wings in which no fault occurs by an abstract version that models this simple behaviour. This requires to run a separate verification for each one of the 62 faults, using one of four possible versions of the SGS model (one version for every combination of 3 wings that are replaced by an abstract model).

Due to the interconnection of wings and solar array driving groups -members of thermal control units (TCUs), it is actually possible to further group an abstract wing and its corresponding TCU, if the concrete wing is not connected to the same TCU. The corresponding abstraction is represented by a TCU WING block. Thus, after abstraction, each of the 4 versions of the model contains one concrete wing and its TCU, one abstract wing connected to the same TCU, an ABSTRACT TCU block connected to both concrete wing and abstract wing, and two abstract TCU WING blocks. The communication graph of an abstract model is shown in Figure 4. The system is reduced, in average, by 55% with respect to the number of block instances, port instances and connectors.

The behaviour of an abstract wing consumes all received signals and answers not deployed for the first 400 seconds since system start-up (the minimal delay needed for a correct deployment) and as deployed after 350 seconds since startup (the answer between 350 and 400 seconds is nondeterministic). The difference of 50 seconds is related to the end steps of the deployment procedures, in which the wing can be deployed or not. The abstracted TCU WING has a similar behaviour, with the difference that needs at least 280 seconds for deployment and can be not deployed for at most 330 seconds. These intervals were manually computed by adding the time needed for each step and trying to minimize their intersection were the wing has a non deterministic behaviour with respect to its status.

The reduced model was model-checked by injecting failures one at a time. Concerning thermal knives, due to the parallelization, we found an error scenario. Deployment starts by switching on a subset of nominal knives for each wing. The knife will inform the hold-down and release system of its enabling. If, in these 50 seconds needed for the cut, the redundant knife (which is off) fails, it will send the disabling command to the hold-down system, and the HDRS won't be cut. Now, the redundant knife cannot be enabled (due to the failure mode), the cable is not cut and the wing not deployed. The correction is to send the switch off request in case of failure only if the knife is on. For all the other injected failures, the property is satisfied. Table I presents the average time needed for the verification (in seconds) of each class of errors. In the case of the later one, the verification of the induced failure on the power unit responsible for the nominal connection with the concrete wing does not finish, while with the induced failure on the power unit responsible for the redundant connection the requirement is verified in 11394 seconds. This shows the asymmetry of the system model.

F. Towards contract-based reasoning

In order for the verification described in the previous section to be complete, we still need to prove that the abstractions of wings and TCUs that we used are correct. However, this is not possible without making certain assumptions about the environment in which a wing operates, which is composed of the mission management, the software parts, the control and monitoring units and the power units. The assumptions concern the order and the timing in which messages are sent by the environment; in their absence, the concrete model of a wing can deadlock or malfunction, which is not captured by the abstraction.

One then has to verify that the environment actually guarantees these assumptions, which is true only under the assumption that the wings and TCUs operate correctly as specified in the abstraction. This kind of circular argument is used and can be proved to be sound in certain contractbased verification frameworks [START_REF] Quinton | Contract-Based Reasoning for Component Systems with Complex Interactions[END_REF], [START_REF]Contract-Based Verification of Hierarchical Systems of Components[END_REF].

Defining such a contract framework for OMEGA SysML and supporting it in the toolset is part of our future work roadmap. In initial experiments, we have manually represented guarantees as observers and verified each guarantee for the concerned component by manually extracting the relevant model part. When a guarantee needed to be used as assumption for another component, we represented it as a normal SysML block exhibiting all behaviours allowed by the guarantee, again by manually constructing the corresponding state machine. All these steps have been formally verified within our toolbox, thus proving the abstraction correct.

VII. RELATED WORK

In the recent years, several tools have been developed to support model-checking for high-level languages such as UML, SysML or AADL [START_REF] Sae | Architecture Analysis and Design Language (AADL)[END_REF]. Based on well known model checkers, they are either directly integrated into tool modellers or they provide transformation techniques from the input model (usually expressed in an XMI file) to the target language of the model checker used. For example, the toolkit SysML Companion [START_REF]RealTime-at-Work[END_REF] provides as extensions model-checking in UPPAAL [START_REF]UPPAAL v4[END_REF] and Spin [START_REF]Spin Model Checker[END_REF].

IBM Rhapsody includes validation by simulation in its toolbox. [START_REF] Da Silva | Integrando sysml e model checking para v&v de software crítico espacial[END_REF] proposes to use UPPAAL in order to verify Rhapsody state machines, the transformation being based on state name equivalence with intermediary states generated for composed actions. System's properties, even though initially described by requirements diagram, have to be given as Computational Tree Logic (CTL) formulas for the UPPAAL model to be checked. However, the lack of an automatized toolset for these transformations makes the approach error prone -the model described in the two frameworks might not be equivalent, which makes harder to identify if the errors found by model-checking are spurious, introduced at the translation, or true system errors.

ARTiSAN Real-time Studio [START_REF] Artisan | [END_REF] is connected to NuSMV [START_REF] Nusmv | [END_REF] model-checker in [START_REF] Alawneh | A unified approach for verification and validation of systems and software engineering models[END_REF] which translates a large subset of UML/SysML diagrams (e.g., sequence, activity and timing diagrams, state machine diagrams, block definition and internal block diagrams) to the intermediary Configuration Transition Systems (CTS) formal model. The framework proposes to verify system designs both by model-checking and by metrics and program analysis. Structure diagrams are usually subject to metrics analysis, while behavioural diagrams are translated into the intermediate formal model and model-checked with respect to automatically generated properties and manually specified ones as CTL formulas. For example, hierarchical state machines are transformed into CTS where each state represents either its correspondent one in case of top states or a set of states in case of a composite state in the original diagram. For each state of the CTS, reachability and deadlock formulas are automatically generated as CTL formulas and verified on the model. However, the temporal extensions for state machines are not presented and neither their impact on the operational semantics. Moreover, state machines are model-checked separately. Our case study is based on the composition of several individual behaviours, composition that is not taken into consideration within this approach which makes it less suitable to be explored. Furthermore, expressing properties as CTL formulas might be a difficult step since system and software engineers are not experts in formal methods and temporal logic.

The Topcased Environment [START_REF]TOPCASED -The Open-Source Toolkit for Critical Systems[END_REF] provides connections with UPPAAL and CADP toolkit [START_REF] Fernandez | CADP -A Protocol Validation and Verification Toolbox[END_REF] for SysML models. The AGATE project [START_REF] Rochet | AGATE, a transfomation tool for simulation and formal checking for UML/SysML activity (Abstract)[END_REF] uses SysML Activity Diagrams, a different formalism than ours, extended with MARTE Profile [START_REF]Modeling and Analysis of Real-Time and Embedded Systems (MARTE) v1.0[END_REF] stereotypes to model the timed behaviour of a system model and translates them into UPPAAL timed automata in order to analyse the execution of the system on a mono platform processor. A second approach within TOPCASED is the usage the pivot language FIACRE [START_REF] Berthomieu | FIACRE: an Intermediate Language for Model verification in the Topcased Environment[END_REF] to connect AADL and SysML models to CADP. In this case, the latter transformation is not implemented to our knowledge and could not be evaluated.

The academic TTool [START_REF]The TURTLE Toolkit[END_REF] transforms SysML models that comply with the AVATAR Profile [START_REF] Pedroza | AVATAR: A SysML Environment for the Formal Verification of Safety and Security Properties[END_REF] into UPPAAL and CADP for model checking, minimization and bisimulation verification. It takes into account SysML Block Diagrams and state machines extended with temporal operators to express timing constraints (e.g., the delay for which the activity of a block is suspended and computation time for instructions). The communication between blocks is realized via synchronous and asynchronous channels modelled as connectors (between ports). Safety requirement are expressed using TEPE property language [START_REF] Knorreck | TEPE: A SysML Language for timed-constrained property modeling and formal verification[END_REF], while security properties are expressed and checked within ProVerif [START_REF] Proverif | [END_REF]. Because TTool is compatible only with the profiles it supports and our project can't be imported, experiments were carried out on toy models. The main difference between the two approaches relates to the sound typing system that OMEGA-IFx provides with respect to ports and connectors. In AVATAR, ports are typeless (contracts cannot be specified for ports), while connectors statically specify which signals they forward and in which direction. This leads to models of bidirectional ports which are a source of typing inconsistencies when translating a SysML model into an implementation language, as explained in [START_REF]Unambiguous UML Composite Structures: The OMEGA2 Experience[END_REF]. Moreover, a signal can be sent through only one channel and the same channel can transfer requests in both way. This greatly increases the complexity of the verification model, since in our case study the same request is transferred through several connectors; for example, when the four wings communicate their deployment status to the control and monitoring unit, they use the same output port of their owner connected in cascade with the target. Also, the broadcast communication type is not considered in this framework, while OMEGA-IFx implements this option used in industrial system models often implemented in synchronous languages [START_REF] Benveniste | The synchronous languages 12 years later[END_REF]. With respect to the properties model, TEPE uses the parametric diagrams of SysML to express logical and temporal relations between block attributes and signals. The system described by blocks and state machine diagrams is translated into timed automata; parametric diagrams are transformed into observer automata for the UPPAAL model and checked for reachability and liveness. It uses the same principle as our toolbox, with the difference that we express properties as state machines which can be more handy for system engineers than learning a new specification language. One can see than even if AVATAR-TEPE-TTool is an interesting approach, our framework is more industrially-oriented and fits the process of developing safe code for embedded critical systems, also due to the Full MDE Process.

VIII. CONCLUSIONS

The difficulties often met during the development of complex critical systems are well-known: late discovery of errors in the system architecture, incompatible interfaces of interacting components, ambiguities in the descriptions leading to misinterpretations by the development teams. The Model Driven Engineering process proposed by the Full MDE project aims at decreasing the number of misunderstandings during the development process, reducing the cost of verification and validation and improving the quality of the final system.

In this paper we have presented the validation of a reverse engineering model of the Solar Generation System of the ATV by using the IFx-OMEGA approach. We have worked on a subsystem developed with OMEGA SysML Profile for which we expressed requirements by observers that were then verified by simulation and model-checking using the IFx toolset. Due to the complexity of the system model the verifications were performed on an abstraction of the model. This framework has allowed discovering residual errors in the system model at early stages of the development process.

The case study has also allowed to point out the weak points of current tools and the path to future improvements. In particular, all proofs were realized on abstraction that have been manually designed. For industrial models, this might be a difficult and time-consuming task. In order to cope with the complexity of nowadays systems, we propose to develop within our framework automated abstractions generation and proofs by integrating a contract-based approach. [START_REF] Quinton | Contract-Based Reasoning for Component Systems with Complex Interactions[END_REF] has proposed a framework for compositional verification of systems with assume/guarantee contracts for different input formalism, like labelled transition systems, modal transition systems [START_REF]Contract-Based Verification of Hierarchical Systems of Components[END_REF] or input/output automata [START_REF] Quinton | A Framework for Contract-Based Reasoning: Motivation and Application[END_REF]. We are currently working on adopting this methodology and extending it for OMEGA SysML components, which are a version of timed input/output automata.

Figure 1 .

 1 Figure 1. FullMDE: An engineering process based on models, formal methods and model transformation

  6 http://www-01.ibm.com/software/awdtools/rhapsody/

3 )Figure 2 .

 32 Figure 2. Observer modelling that the four wings are deployed 10 minutes after start-up and the mission management is aware

Figure 3 .

 3 Figure 3. System's communication graph displaying the block instances -represented as nodes -and communications between them -represented as arrows

4 Figure 4 .

 44 Figure 4. Abstract system's communication graph -the instances for three of the four wings are replaced with simpler components

http://www-if.imag.fr/

project.net/ 2 Full Model Driven Development for On-Board Software, Contract ESTEC 22618/09/NL/JK 3


Rouaa Wannous
email: rouaa.wannous@univ-lr.fr

Cássia Trojahn
email: cassia.trojahn@irit.fr

Explaining Argumentation over Alignment Agreements

Keywords: argumentation, ontology matching, explanation

Argumentation frameworks have been used as tools for reconciliating ontology alignments, through a series of proposals and counter-proposals, i.e., arguments. However, argumentation outcomes may not be so obvious to human users. Explaining the reasoning behind the argumentation process may help users to understand its outcome, and influence the user's confidence and acceptance on the results. This paper presents a mechanism for providing explanations on the way agreed alignments are established. Our mechanism is based on tracing each step of the argumentation process. These traces are then interpreted using a set of association rules, built from a decision tree that represents all possible statuses of arguments. From these rules, a multi-level explanation, in natural language, is provided to the users.

I. INTRODUCTION

Ontology matching is the process of finding relationships between entities of different ontologies and has been seen as the solution for the ontology heterogeneity problem in different scenarios. In agent communication [START_REF] Laera | Argumentation over Ontology Correspondences in MAS[END_REF], for instance, agents need to reconcile the differences between their vocabularies (ontologies) before starting any kind of cooperation. There are many ways to exploit the features within the ontologies and different matching approaches have been proposed in the literature ( [START_REF] Euzenat | Ontology matching[END_REF], [START_REF] Kalfoglou | Ontology Mapping: The State of the Art[END_REF]). Potentially, matching system may differ in the alignments they generate and argumentation theory has been exploited for conciliating matchers' points of view and iteratively to solve their conflicts ( [START_REF] Laera | Argumentation over Ontology Correspondences in MAS[END_REF], [START_REF] Trojahn | Argumentation for reconciling agent ontologies[END_REF]).

Argumentation is a negotiation model based on building and comparing arguments, for defining the most acceptable of them. In the context of ontology matching [START_REF] Trojahn | Argumentation for reconciling agent ontologies[END_REF], arguments represent correspondences between entities of two ontologies. Agents exchange their arguments in order to identify the most acceptable correspondences. They may have different preferences, which can be taken into account in the process of evaluating and selecting arguments. However, argumentation is a complex process and its outcome may not be intuitively obvious to human users. Thus, users may not agree on the argumentation outcome because they are not able to understand why or how arguments have been accepted. Explanation of argumentation processes has been exploited in few works [START_REF] García | An abstract presentation of dialectical explanations in defeasible argumentation[END_REF]. Explanation consists of exposing something in a way that is understandable for the receiver of the explanation [START_REF] Ye | The impact of explanation facilities on user acceptance of expert systems advice[END_REF]. It makes system's results more acceptable for users by increasing their understanding on the reasons for finding them. This paper presents a mechanism for explaining why and how an alignment agreement, from different matchers that argue on their alignments, has been established. In general, matching systems do not provide explanations on their results and very few approaches have been proposed in the literature [START_REF] Shvaiko | Web explanations for semantic heterogeneity discovery[END_REF], [START_REF] Qian | IMAP: Discovering Complex Semantic Matches between Database Schemas[END_REF]. Providing matching explanations is one of the challenges for ontology matching [START_REF] Shvaiko | Ten challenges for ontology matching[END_REF]. For instance, explanations are useful when matching thousands of entities, where automatic matching of large ontologies may find many plausible correspondences, and hence user input is required for filtering out the alignment [START_REF] Euzenat | Ontology matching[END_REF]. Our explanation mechanism traces each single step of the argumentation process. These traces are then interpreted using a set of association rules, built from a decision tree that represents all possible statuses of arguments. From these rules, a multi-level explanation, in natural language, is provided to the user. It is able to provide explanations on (a) why it was found by an individual matcher, (b) why a correspondence was accepted by an individual matcher, and (c) why it was included in the agreed alignment.

In the following, we introduce ontology matching and argumentation frameworks ( §II) and present our explanation mechanism ( §III) and evaluation experiments ( §IV). Next, we present related work ( §V) and conclude the paper ( §VI).

II. FOUNDATIONS

A. Ontology matching

The matching process takes as input two ontologies o and o ′ and determines as output an alignment A ′ , i.e., a set of correspondences. A correspondence is defined as follows :

Definition 1 (Simple Correspondence [START_REF] Euzenat | Ontology matching[END_REF]) A simple correspondence can be defined as <e,e ′ ,r,n>, such that: e and e ′ are entities (e.g., elements, properties, classes) of o and o ′ , respectively; r is a relation holding between two entities e and e ′ (for instance, equivalence (≡), more general (⊒), disjointness (⊥), overlapping (⊓)); and n is a confidence measure number in the [0;1] range, assigning a degree of trust on the correspondence.

For instance, c = article o , paper o ′ , ≡, 1 states that article in the source ontology is equivalent to paper in the target ontology, with a confidence of 1.0.

Different matching approaches have emerged from the literature [START_REF] Euzenat | Ontology matching[END_REF]. The main distinction between each is due to the type of knowledge encoded within each ontology, and the way it is utilised when identifying correspondences between features or structures within the ontologies. Terminological methods lexically compare strings (tokens or n-grams) used in naming entities (or in their labels and comments), whereas semantic methods utilise model-theoretic semantics to determine whether or not a correspondence exists between two entities. Approaches may consider the internal ontological structure, such as the range of their properties (attributes and relations), their cardinality, transitivity and/or symmetry of their properties, or the external ontological structure, such as the position of the two entities within the ontological hierarchy. The instances (or extensions) of classes could also be compared using extension-based approaches. Matching systems rely not on a single approach.

B. Argumentation frameworks

In alignment agreement, arguments are positions that support or reject correspondences [START_REF] Laera | Argumentation over ontology correspondences in MAS[END_REF], [START_REF] Trojahn | Conjunctive queries for ontology based agent communication in mas[END_REF]. Such arguments interact following the notion of attack and are selected according to the notion of acceptability, introduced by Dung [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF]. In Dung's model, an argument should be accepted only if every attack on it is attacked by an accepted argument. Dung defines an argumentation framework as follows :

Definition 2 (Argumentation framework [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF] In Dung's model, all arguments have equal strength and an attack always succeeds (or successfully attacks). Amgoud and Cayrol [START_REF] Amgoud | On the acceptability of arguments in preference-based argumentation[END_REF] have introduced the notion of preference between arguments, where an argument can defend itself against weaker arguments. This model defines a global preference between arguments. In order to relate local preferences to different audiences, Capon [START_REF] Bench-Capon | Persuasion in practical argument using value-based argumentation frameworks[END_REF] proposes to associate arguments to the values which supports them, leading to the notion of successful attacks, i.e., those which defeat the attacked argument, with respect to an ordering on the preferences that are associated with the arguments. However, in ontology matching, an objection can still be raised about the lack of complete mechanisms for handling persuasiveness [START_REF] Isaac | Using quantitative aspects of alignment generation for argumentation on mappings[END_REF]. Matchers output correspondences with a strength that reflects the confidence they have in the fact that the correspondence between the two entities holds, usually derived from similarity assessments made during the matching process. Hence, for associating an argument to a strength Trojahn et al. [START_REF] Trojahn | A cooperative approach for composite ontology mapping[END_REF] introduce the SVAF framework, extending [START_REF] Bench-Capon | Persuasion in practical argument using value-based argumentation frameworks[END_REF]:

Definition 3 (SVAF [16]) A Strength-based argumentation framework (SVAF) is a sextuple A, ⋉, V, v, , s such that A, ⋉ is an AF, V is a nonempty set of values, v : A → V,
is the preference relation over V (v 1 v 2 means that, in this framework, v 1 is preferred over v 2 ), and s : A → [0, 1] represents the strength of the argument.

Each audience α is associated with its own argumentation framework in which only the preference relation α differs. In order to accommodate the notion of strength, the notion of successful attack is extended: Definition 4 (Successful attack [START_REF] Trojahn | A cooperative approach for composite ontology mapping[END_REF]) An argument a ∈ A successfully attacks (or defeats, noted a † α b) an argument b ∈ A for an audience α iff

a ⋉ b ∧ (s(a) > s(b) ∨ (s(a) = s(b) ∧ v(a) α v(b)))
Definition 5 (Acceptable argument [START_REF] Bench-Capon | Persuasion in practical argument using value-based argumentation frameworks[END_REF]) An argument a ∈ A is acceptable to an audience α with respect to a set of arguments S, noted acceptable α (a, S), iff ∀x ∈ A, x † α a ⇒ ∃y ∈ S; y † α x.

A preferred extension represents a consistent position within a framework, which defends itself against all attacks and cannot be extended without raising conflicts [START_REF] Bench-Capon | Persuasion in practical argument using value-based argumentation frameworks[END_REF]. An argument is subjectively acceptable iff it appears in some preferred extension for some specific audience, and an argument is objectively acceptable iff it appears in all preferred extensions for every specific audience.

C. Arguments on correspondences

Representing correspondences as arguments within an AF and attacks between them are as follows:

Definition 6 (Argument [START_REF] Laera | Argumentation over ontology correspondences in MAS[END_REF], [START_REF] Trojahn | Conjunctive queries for ontology based agent communication in mas[END_REF])

An argument a ∈ A is a triple a = c, v, h , such that c is a correspondence,
e, e ′ , r, n ; v ∈ V is the value of the argument and h is one of +,-depending on whether the argument is that c does or does not hold.

Definition 7 (Attack [START_REF] Laera | Argumentation over ontology correspondences in MAS[END_REF], [START_REF] Trojahn | Conjunctive queries for ontology based agent communication in mas[END_REF])

An argument c, v, h ∈ A attacks an argument c ′ , v ′ , h ′ ∈ A iff c = c ′ and h = h ′ .
The way arguments are generated differs in each scenario. The strategy in [START_REF] Trojahn | A cooperative approach for composite ontology mapping[END_REF], negative arguments as failure, relies on the assumption that matchers return complete results. Each possible pair of ontology entities which is not returned by a matcher is considered to be at risk, and a negative argument is generated h = -. An alignment associated with an extension contains only the arguments with h = +.

III. EXPLANATION ON ARGUMENTATION

Our explanation mechanism attempts to fill the gap between users and argumentation outcomes. Basically, it is based on (a) tracing the argumentation process in order to register the statuses of arguments during the argumentation process, and (b) using a rule-based mechanism for interpreting the trace entries. The explanations are given to the user in natural language, with different levels of technical details. These levels allow users to navigate through the explanations from general explanations to more specific contextual ones. More specifically, the following explanations are provided: (a) why a correspondence was found by an individual matcher, (b) why it was accepted by an individual matcher, and (c) why it was included in the agreed alignment. In the following, we detail the justification of correspondences and our explanation on how and why agreements were obtained from argumentation.

A. Justifying correspondences

We assume that matchers can provide one or more justifications about the reasons that support finding their correspondences. In order to consider this information, we extend the definition in §II-A to include the provenance information used for finding a specific correspondence : Definition 8 (Extended correspondence (EC)) An extended correspondence is a tuple <c,J>, such that: c is a correspondence; J is a set of justifications j i for finding c.

From the ontology matching literature, possible justification categories can be established: terminological, such as lexical similarity and synonyms; structural, such as super-class, sub-class, sibling and property; semantic, such as semantics model-based; and extensional, such as instance-based. For instance, in the example provided in §II-A, the extended correspondence (EC) between the article and paper entities is c = article o , paper o ′ , ≡, 1, {terminological} since these terms can be considered synonymous. Hence, an extended argument contains an extended correspondence : Definition 9 (Extended argument (EA)) An extended argument (EA) is a triple a = <EC,v,h> such that EC is an extended correspondence <c,J>; v ∈ V is the value of the argument and h is one of {+,-} depending on whether the argument is that EC does or does not hold.

B. Explanation mechanism

Overall, the explanation process can be summarised as follows : (1) trace the argumentation process and log the outcomes of each single step of it; (2) a query for a correspondence is made by a user; (3) filter the arguments to a list which contains the queried correspondence; (4) apply the rules on the log entries that give the status of the filtered arguments;

(5) provide multi-level explanations in natural language to the user about the queried correspondence.

The explanation mechanism has two main modules: argumentation logger and rule-based interpreter. The argumentation logger module traces each single step of the argumentation process. Each log entry contains the status of each argument, for each matcher. The log entries for each matcher contain the statuses of each single argument A . The argument A may have many statuses during the argumentation process. The output of this module is a set of log entries.

The rule-based interpreter module contains the rules to interpret the log entries and associates to each entry an explanation in natural language. We assume that the argumentation process includes the instantiation of several argumentation frameworks, from several matchers. For defining all possible statuses of arguments within an argumentation process, we have manually draw a decision tree (Figure 1) based on the analysis of the argumentation process and how argumentation frameworks establish their preferred extensions. From this decision tree, we extracted 9 rules to explain all possible statuses for an argument and the inputs of our rules are the outputs from the argumentation logger module (log entries of a given argument and the log entries of its attackers). For instance, rule (1), according to Figure 1, has the log entry attacked for the considered argument A, while the rule (7) has the log entry has successf ul attack for the argument A and for its attacker B. We have also defined two categories of rules: local rule, which considers log entries for one single matcher as an input to a rule; and global rule, which considers log entries for all matchers as an input to a rule. These categories of rules are transparent to user. Below, we present the rules extracted from the decision tree depicted in Figure 1 (the numbers represent the rule number). A is an argument and B is its attacker; s(A) represents the strength of A and ν(A) is the value of A , which represents the preferred value of the matcher generating it; c is the queriedcorrespondence the user asked about. In the explanation, EXP is the output from each rule with multilevel explanations in natural language, representing their technical details (i.e, different levels of explanation): L1 (level 1), where the sentences are presented in an understandable way, without any technical details; L2 (level 2), where sentences are presented with technical details, supporting the explanation provided in level 1. The acceptable conf lict represents a conflict which is not solved. The attackrelation represents the successful attack between the considered arguments, such as A → B that means A successfully attacks B . The argument C represents the argument that attacks B . Hence, for an argument A , that contains the queried correspondence c , and a matcher m , we define the following local rules :

( For the argument A , that contains the queried correspondence c and a set of matchers m 1 , .., m n , the global rules have been defined : (

9) IF

A is not attacked for all matchers EXP L1 all matchers have agreed on aligning c L2 m i has found it because J i A is an acceptable correspondence for all matchers (10) IF A is objectively acceptable EXP L1 A is an acceptable correspondence for all matchers L2 A it is in the preferred extension of all matchers (11) IF A is subjectively acceptable EXP L1 A is accepted from some matchers L2 A is in the same preferred extensions of some matchers

For combining the rules and providing an explanation, we consider the notion of objectively acceptable sets to determine the agreed alignment. So, we always apply the rule [START_REF] Laera | Argumentation over ontology correspondences in MAS[END_REF]. Furthermore, we combine the L2 of the rule [START_REF] Laera | Argumentation over ontology correspondences in MAS[END_REF] at the end of the L2 of the rules (3), ( 6) and ( 9). We did not apply the explanations of L1 of these rules because all of them already have the same L1. For example, in the rule (3), we did not change its L1. However, after combining them, its L2 will be L2: A has no successful attack and it is in the preferred extensions of all matchers.

IV. EXPERIMENTAL EVALUATION

A. Data set and matchers

The OAEI benchmark 1 is a reference data set for evaluating matching systems. The tests in this data set are based on one particular ontology dedicated to the domain of bibliography 1 http://oaei.ontologymatching.org/2011/benchmarks and a number of alternative ontologies of the same domain, for which alignments are provided. For our study case, we have chosen the test 301 of Benchmark. This test is based on aligning the reference ontology to a real one, which is reminiscent to BibTeX. We have choose this test because it is one of the real cases available in Benchmark and it is very known in the ontology matching community. We based our experiments on three basic matchers implemented in the Alignment API2 : (a) string similarity (str): uses an editing (Levenshtein [17]) distance between ontology entity names; (b) synonymous-based similarity (syn): looks for synonymous in the WordNet3 database; (c) property-based similarity (pro): establishes an alignment based on the comparison of the properties that classes have in common.

B. Explanation system

We have used the available implementation of S-VAF as basis for implementing our system. The implementation of this framework is available in Java and we have extended it in order to include our explanation mechanism. We implemented our two modules: the argumentation logger and the rule-based interpreter. In the argumentation logger module, each step of generating the preferred extensions in the argumentation process has been logged. The rule-based interpreter module uses these logs to provide the explanations.

The user can run the system on command line by passing all the required input parameters: (a) name of each matcher used for finding the alignments; (b) RDF files which contain the alignments that matchers have generated; (c) confidence for the negative arguments (h = -); and (d) HTML output file path and name, which will contain the explanations. Once the user has run the system, the agreed alignment is presented. Then he/she can query about a specific correspondence to see the explanations generated for it. In this initial version of our system, the output of the system is an HTML file containing the explanations on the queried correspondence, which are provided by our rules. This file contains both the explanations for the correspondences in the agreed alignment (for all matchers) and the explanations for the correspondences for each individual matcher's point of view. The first level of explanation (L1) is presented by default to the users (Figure 2). If the user is interested in more details, he/she can navigate on the second explanation level (L2) by clicking on 'More explanation'. Figure 2 shows an explanation interface for the queried correspondence "Institution Incollection".

Our system is able to provide the following explanations (for sake of brevity, we provide examples for few cases):

• Why a correspondence was determined between ontology entities: the matchers reasons for finding this correspondence are given in Figure 3 (1). • Why a correspondence is in the agreed alignment: the explanations for accepting a correspondence as an agreement are shown in Figure 3 (2).

Figure 2. Level 1 explanation for "Institution Incollection" query.

Figure 3. Navigation in the explanations for "Institution Incollection" query.

• How a conflict was solved between two correspondences: the explanations show the conflict and the responsible for solving it. • Why a correspondence was acceptable by a particular matcher: the explanations, show the acceptability of a correspondence by a matcher. • Why a correspondence was not in the agreed alignment: the explanations for not accepting a correspondence as an agreement. • When a correspondence was not found between ontology entities (for all matchers): if the user asks about two entities, such as "title Entry", the explanation is "None of these matchers find any correspondence between them".

C. Evaluation and discussion

Evaluating explanation requires human user feedback [18] [19]. Here, we evaluate the explanation in a qualitative way, focusing on criteria such as clearness and usefulness. To that extent, we have prepared a questionnaire (8 questions) that has been used to evaluate each case our system provides an explanation. Each question in the questionnaire had four options to select from: No, Maybe, Yes and Absolutely. Also the user could add any comments they may have. These four options were interpreted as numeric values from 0-3, respectively (no → 0, Maybe → 1, etc.). We have asked two users to fill in the questionnaire, after using our system. Both of them are computer scientists. One is an expert on the ontology matching domain and the other has good notions of ontology matching. Figure 4 shows the evaluation results, for each question in the questionnaire. Regarding to the clearness of the explanations on the agreed alignment, the expert evaluator found the explanations clear while the second evaluator found the explanations not fully clear. With respect to the acceptability of a particular correspondence by a matcher, both of reviewers were not completely convinced with the explanations. It is the same case for the matchers justifications on finding their correspondences. In this point, as we may have no control on the matching process itself, we can not provide more complete or better explanations. Regarding to the clearness of the explanations on solving a conflict, they are also convinced but not fully. With respect to the usefulness of our explanations for understanding the argumentation outcomes, they agree on their usefulness. The evaluators almost fully agree on the clearness of the explanation levels for supporting the understanding. The drawback of our system, however, as stated by the evaluators, is that the way we have provided the explanations (i.e., explanations as long natural language sentences) in HTML file is not clear enough for fully understanding the interactions within the argumentation process. They stated that exploiting more graphical visualisation options could be a solution to this drawback.

V. RELATED WORK Since many years, explanation has been exploited in different areas of artificial intelligence, such as proof [START_REF] Mcguinness | Explaining subsumption in description logics[END_REF], expert systems [START_REF] Swartout | Explanations in knowledge systems: Design for explainable expert systems[END_REF] and belief revision [START_REF] Falappa | Explanations, belief revision and defeasible reasoning[END_REF]. In the proof domain, provers are based on providing reasoning details, usually as reasoning trees, what is easily understandable to experts. In expert systems, different types of explanation, such as trace, justification and strategy, are exploited to provide to human experts the explanations on how the system has taken its decisions. Rule-based and case-based systems exploit differently the knowledge for explaining their decisions. In the specific context of ontology matching, few systems are able to provide explanations on their alignments [7] [8]. S-Match system [START_REF] Shvaiko | Web explanations for semantic heterogeneity discovery[END_REF] uses the Inference Web (IW) infrastructure to provide proofs and explanations to the results from matching process steps. Following a different strategy, IMAP system [START_REF] Qian | IMAP: Discovering Complex Semantic Matches between Database Schemas[END_REF] explains its correspondences by retrieving the justifications from a dependency graph, which represents the steps the system followed to establish its correspondences. Scarlet4 presents how two entities can be related, using information from online available ontologies.

In argumentation frameworks and explanation of its argumentation reasoning process, the closest proposal is from Garcia et al. [START_REF] García | An abstract presentation of dialectical explanations in defeasible argumentation[END_REF]. They proposed a dialectical proof based explanation, based on Dung's framework, for explaining the acceptability of arguments. They provide dialectical trees which represent the interaction between arguments, as an explanation to the user. More recently, these authors formalise dialectical explanation for argumentation in [START_REF] García | Formalizing dialectical explanation support for argument-based reasoning in knowledge-based systems[END_REF]. Similar to provers, this kind of dialectical explanation may be not so intuitive. While the explanations in deductive and dialectical systems are based on reasoning and dialectical trees, respectively, we focus on natural language explanations. In that way, similar to what is done in expert systems, we trace each step of the argumentation process and make a decision tree, which represents the status of each argument within an argumentation framework. The multi-levels of explanations in our system represent different levels of technical details, as in IMAP. Although our focus is on explaining argumentation, if available, we provide justifications from matchers.

VI. CONCLUSION AND FUTURE WORK

This paper has proposed a first attempt to provide multilevel natural language explanations on agreed alignments, using a specific framework (SVAF). Although few users have participated in the evaluation, their feedbacks were useful for evaluating the clearness and the usefulness of our explanations. The overall evaluation is positive, however, there is a room for improvements and our work can be improved in several ways. First, alternative ways for visualising our explanations could be exploited, specially providing more graphics, using coloured graphs of attacks between arguments, and colouring attacks that succeeds, as well as allowing the user to dynamically choose different argumentation settings (agents preferences, strength of attacks, etc). Second, we plan to provide explanations on alternative argumentation frameworks. Third, we can work on extending the justification on finding correspondences that come from matchers. Fourth, we have focused on explanations for users. However, we could think on explanations between matchers, in a similar way of what is done in belief revision. A matcher can explain the way it finds its correspondences for another matchers, in an explanationbased dialogue. Finally, we would like to propose an approach for learning decision trees from the agents interaction.

  (AF)) An AF is a pair A, ⋉ , such that A is a set of arguments and ⋉ (attacks) is a binary relation on A. a ⋉ b means that the argument a attacks the argument b. A set of arguments S attacks an argument b iff b is attacked by an argument in S.

Figure 1 .

 1 Figure 1. Decision tree represents the statuses of an argument, the numbers in the circles refer to the rule number.

Figure 4 .

 4 Figure 4. Evaluating the explanations provided by our system.

http://alignapi.gforge.inria.fr/

http://wordnet.princeton.edu/

http://scarlet.open.ac.uk/