Samuel Colin
email: samuel.colin@loria.fr

Arnaud Lanoix
email: arnaud.lanoix@loria.fr

Jeanine Souquières
email: jeanine.souquieres@loria.fr

Trustworthy interface compliancy: data model adaptation using B refinement

Keywords: Component-based approach, correctness, interoperability, formal method, adapter, data model, interface

In component-based software development approaches, components are considered as black boxes, communicating through required and provided interfaces which describe their visible behaviors. Each component interface is equipped with a suitable data model defining all the types occurring in the interface operations. The provided interfaces are checked to be compatible with the corresponding required interfaces, by the way of adapters. We propose a method to develop and verify these adapters when the interface data models are different, using the formal method B. The use of B assembling and refinement mechanisms eases the verification of the interoperability between interfaces and the correctness of the component assembly.

Introduction

Component orientation is a new paradigm for the development of software-based systems. The basic idea is to assemble the software by combining pre-fabricated parts called software COTS (Commercial Off-The-Shelf) components, instead of developing it from scratch [START_REF] Szyperski | Component Software[END_REF]. This procedure is similar to the construction methods applied in other engineering disciplines, such as electrical or mechanical engineering.

Software components are put together by connecting their interfaces. A provided interface of one component can be connected with a required interface of another component if the former offers the services needed to implement the latter. Hence, an appropriate description of the interfaces of a software component is crucial. In earlier papers [START_REF] Chouali | Verifying the compatibility of component interfaces using the B formal method[END_REF][START_REF] Chouali | Proving Component Interoperability with B Refinement[END_REF][START_REF] Hatebur | A Method for Component-Based Software and System Development[END_REF] we have investigated how to formally specify interfaces of software components and how to prove their interoperability, using the formal method B, as presented in Section 2. Each component interface is equipped with a suitable data model defining all the types occurring in the signatures of interface operations.

In this paper, we study how to connect components with different data models by using adapters. We propose a method in three steps, sketched in Section 3, to build a trustworthy adapter following a refinement process: we start with the required interface and refine it until we can include the provided one. Each step expresses a level of interoperability, is supported by the prover and help us to establish the correctness of the adaptation. We support the presentation of this method with an example of an embedded system in Section 4. The paper finishes with the discussion of related work in section 5 and concluding remarks in section 6.

Using B for component-based development

We briefly describe the formal method B and explain how we use it in the context of component-based software. The architecture is modeled by UML diagrams (the components) annotated with B models associated to their interfaces. The B models are then used to verify the interface compliancy.

The B method

B is a formal software development method based on set theory, which supports an incremental development process using refinement [START_REF] Souquières | The B Book[END_REF]. Starting out from a textual description, a development begins with the definition of an abstract model, which can be refined step by step until an implementation is reached. Model refinement is a key feature for incrementally developing more and more detailed models, preserving correctness in each step. Each model consists in variables representing the state, operations representing the possible evolutions of this state and an invariant specifying the safety requirements.

The B method has been successfully applied in the development of several complex real-life applications, such as the METEOR project [START_REF] Behm | METEOR: A Successful Application of B in a Large Project[END_REF]. It is one of the few formal methods which has robust and commercially available support tools for the entire development life-cycle, from specification down to code generation [START_REF] Bert | Adaptable Translator of B Specifications to Embedded C Programs[END_REF]. It provides structuring primitives that allow one to compose models in various ways. Proofs of invariant consistency and refinement are part of each development and POs (Proof Obligations) are generated automatically by support tools such as AtelierB [START_REF]Steria -Technologies de l'information. Obligations de preuve: Manuel de référence[END_REF] or B4free [START_REF] Clearsy | B4free[END_REF]. Checking POs with B support tools is an efficient and practical way to detect errors introduced during development and to validate the B models.

Specifying component architectures

We define component-based systems using UML 2.0 composite structure diagrams [START_REF] Omg | UML Superstructure Specification[END_REF]. They express the overall architecture of the system in terms of components and their required and provided interfaces. UML 2.0 Class diagrams express interface data models with their different attributes and methods.

Component interfaces are then specified as B models, which increases confidence in the developed systems: the correctness of the specifications, as well as the correctness of the refinement process can be checked with support tools. In an integrated development process, the B models can be obtained by applying systematic derivation rules from UML to B [START_REF] Meyer | A systematic approach to transform OMT diagrams to a B specification[END_REF][START_REF] Ledang | Modeling class operations in B: application to UML behavioral diagrams[END_REF].

Proving interoperability of component interfaces

The components must be connected in an appropriate way. To guarantee interoperability of components, we must consider each connection of a provided and a required interface contained in a software architecture and try to show that the interfaces are compatible. Using the B method, we prove that the B model of the provided interface is a correct B refinement of the required one. This result states that the provided interface constitutes a viable implementation of the required interface, and consequently that the two components are compliant as intended [START_REF] Chouali | Proving Component Interoperability with B Refinement[END_REF].

Often, to build a working component architecture, adapters need to be defined, connecting the required interfaces to the provided ones. An adapter is a piece of code that expresses the mapping between a required and a provided interface, usually a mapping between their variables at signature level. In [START_REF] Mouakher | Component Adaptation: Specification and Verification[END_REF], we have studied and proved an adapter specification defined in terms of a B refinement of the required interface that includes the B model of the provided (previously incompatible) interface.

An example of architecture

We illustrate our method with the case study of an embedded system where different sensors send alarm events. These alarms can be canceled by a control console and are memorized by a centralized database. The software architecture of this system is shown Figure 1 using the syntax of composite structure diagrams. It uses three COTS components: • Database provides database functionalities described by its provided interface Database O as presented Figure 2 by UML diagrams and its associated B model (with only its signature). The B model of this interface with its data model and one of the operations is given Listing 1: (i) the types, represented as sets in B, used in the interface, (ii) variables as far as necessary to express the effects of the operations, (iii) an invariant on these variables and (iv) an operation specification.

• SensorDriver, the software part of each sensor, requires an interface Sensor U to signal warning and error alarms to the system. These alarms need to be saved in the database. This component is used twice.

• ConsoleDriver, in charge to drive an alarm control console, requires an interface Console U in order to query and cancel the alarms saved in the database. To assemble these three COTS, three adapters have been introduced:

• Alarms DB maps the provided interface Database O to the interface Alarms U that shares the global resources (see Figures 1 and3).

• Console Alarms and Sensor Alarms provide the required interface of each driver component using the interface Alarms U. The adapter must be trustworthy and the proof of the adaptation becomes complex when data models of I U and I O are different. In order to ease this proof, we develop the adapter by incremental refinements guided by the transformation of the variables of I U into the variables of I O.

MODEL Database 0 SETS Indices = {Uid, Value, Attribute } VARIABLES table INVARIANT table ∈ Indices → (N 1 → N) ∧ dom(table(Uid)) = dom(table(Value)) ∧ dom(table(Uid)) = dom(table(Attribute)) ∧ table (Uid) ∈ (N 1 N) INITIALISATION table := { Uid → ∅, Value → ∅, Attribute → ∅ } OPERATIONS add row(uid, value , attr )= PRE uid ∈ N ∧ value ∈ N ∧ attr ∈ N ∧ ∀ ii .(( ii ∈ dom(table(Uid))) ⇒ (uid = table (Uid)( ii ))) THEN ANY indice WHERE indice ∈ N 1 -dom(table(Uid)) THEN table := table -{ Uid → (table(Uid) -{ indice → uid}), Value → (table(Value) -{ indice → value}), Attribute → (table(Attribute ) -{ indice → attr})} END END; remove row uid(uid) = PRE uid ∈ ran( table (Uid)) THEN ANY indice WHERE indice ∈ dom(table(Uid)) ∧ table(Uid)( indice ) = uid THEN table := table -{ Uid → ( (dom(table(Uid)) -{indice}) table (Uid )), Value → ( (dom(table(Value)) -{indice}) table (Value )), Attribute → ( (dom(table(Attribute)) -{indice}) table ( Attribute )) } END END; update attribute (uid , new attr) = PRE uid ∈ ran( table (Uid)) ∧ new attr ∈ N THEN ANY indice WHERE indice ∈ dom(table(Uid)) ∧ table(Uid)( indice ) = uid THEN table := table -{ Attribute → (table(Attribute ) -{ indice → new attr}) } END END END

Process description

The adaptation process is guided by the interface I O and consists of three refinement steps. Each step is proved by using the B refinement mechanism.

(1) Variables adaptation This step prepares a matching between the variables of I U and I O:

• each variable of V U is transformed into a new variable of V U', "corresponding
to" a variable of V O, using the data types D U,

• the body of each operation of OP U is transformed with respect to these new variables into OP U'.

(

2) Data types adaptation

This step provides a matching between the data types of I U and I O:

• each variable of V U' expressed on D U is transformed into a new variable of V U" expressed using the data types D O. To do that, typecasting functions between D U and D O (and reciprocally) have to be defined,

• the body of each operation of OP U' is transformed with respect to the new variables V U" into OP U".

(3) Provided interface inclusion This step, which has been prepared by the two previous ones, consists in:

• associating each variable of V U" to V O variables,
• expressing each operation of OP U" in terms of operations of OP O.

B as a guideline for the adaptation steps

When the required and the provided interfaces are defined on the same data types, the adaptation becomes a problem of transforming variables and calling the right operations.

When the interfaces are similar modulo their data types, the problem is reduced to find whether the elements of D U are subtypes of elements of D O, and then calling the operations with the transformed variables. In the latter case, the role of the adapter is simply the role of a variable wrapper.

With the use of B, the adaptation process and therefore the adapter itself, is validated by the proof of the different refinement steps. A direct consequence is that the adaptation process is less guided by the intuition of the developer and more by mathematical and logical laws. Hence each step of the process might require several refinement steps in practice in order to provably guarantee that the transformation is correct. As a matter of fact, the B refinement mechanism encourages this practice.

Furthermore, in some transformation steps, functions are introduced as constants, which need to be explicit in the implementation step. Hence our method is no silver bullet: great care has to be taken when these functions appear. The developer of the adapter has to ensure that the transformation functions exist. Their existence can be more easily stated if the refinement steps are limited to simple, intuitive and progressive transformations. For instance, instead of transforming enumerated values of a set directly to the set of natural numbers, it is wiser to first transform it to a set of numbers modulo the number of enumerated values and then transform it to the full set of natural numbers. This way the proof of the refinements become easier.

Case study

We now show the application of this method to develop and prove the adapter Alarms DB that must provide the interface Alarms U using the interface Database O, as presented

Variables adaptation

The first step consists in adapting the variables alarms and active alarms of the interface data model of Alarms U to the interface data model of Database O. During this step, we do not introduce new data types. In the database, each entry in the table is characterized by an identifier Uid which has a corresponding Value and an Attribute. Guided by these three variables, we consider mapping the alarms with the Uid field, the type of an alarm with the Value field and its activity status (active alarms) with the Attribute field.

We introduce three new variables corresponding to Uid, Value and Attribute: alarms ids is directly associated to alarms, whereas AlarmTypes and AlarmStatus are functions expressing the type and the status of an alarm as illustrated Listing 4. The proof of this refinement consists of 18 POs, among which 4 have been proved interactively.

Data types adaptation

Typecasting is a frequent source of bugs, as limit conditions are often overlooked. Consequently, the second step might possibly be the harder one: great care must be taken when casting the variables from one type to another one. The proof process exhibits these limit conditions and oblige to check their validity. In our adaptation process, the typecasting functions are introduced as constants. It means that the validity of the adaptation relies on the existence of these functions, hence it is wiser to choose typecasting functions with well-understood mathematical properties. To ease the proof verification, we break down the data types adaptation step into three refinements:

(2.1) typecasting the non-functional variables (alarms ids), (2.2) typecasting the domain (in the mathematical sense) of each functional variable (alarms type and alarms status),

(2.3) typecasting the codomain of each functional variable (the already transformed alarms type and alarms status).

Typecasting the non-functional variables

The alarms ids variable will be represented at the end of the process by the Uid field of the database. We introduce a constant function id cast in order to typecast from AlarmIds to the natural numbers, i.e. the type of the Uid field. We therefore represent the alarms ids by a new variable nat ids and we add a relationship between both variables in the invariant. The other variables are unchanged, and the result is shown in Listing 5. The invariant expresses the fact that nat ids is the image of the alarms ids by id cast. The proof of this refinement consists of 8 POs, among which 2 have been proved interactively.

Typecasting the domain of each functional variable

The variables alarms status and alarms type depend on alarms ids. As alarms ids has been transformed into nat ids, we must also transform alarms status and alarms type so that they depend rather on nat ids. We thus replace them by the variables nat status and nat type. The result is presented in Listing 6. The invariant helps relating nat status with nat ids, i.e. it states that nat status is the composition of the functions alarm status and id cast. The proof of this refinement consists of 14 POs, among which 5 have been proved interactively. The variables status nn and type nn that we have introduced correspond to nat status and nat type respectively. As the codomains of status nn and type nn are the natural numbers, the codomains of nat status and nat type are transformed by the typecasting functions mentioned above. For notation consistency, we rename nat ids into ids nn. Moreover, we introduce a new variable uid gen for producing a new unique index each time a new alarm is added in the database. All these transformations are shown in Listing 7. The proof of this refinement consists of 20 POs, among which 6 have been proved interactively.

Note that with this last invariant, we obtain that alarm status can be replaced by all the constants and variables we introduced along the refinements. We have: alarm status = status cast -1 • status nn • id cast. The functions status nn • id cast and status cast • alarm status commute. This property is illustrated by Figure 6.

Provided interface inclusion

In the last step, we establish the relationships between the ids nn, status nn and type nn variables and the fields Uid, Attribute and Value of table as illustrated in Listing 8. We also perform the operation calls to Database O to express the operations of Alarms U: the body of the operation new alarm consists mainly of a call to the operation add row of Database O. The proof of this refinement consists of 19 POs, among which 5 have been proved interactively.

The proof of this last step is at the crossroad of the POs of the refinements and the POs of the included (provided) interface, hence the POs here tend to be unreadable because of the size of the terms. Fortunately, the shape of the formulas also tend to resemble the POs of the refinements and the POs of Database O. Hence most of the time similar strategies with the proof strategies of the refinements and the included interface can be used for proving the last step.

The proof process for the development of this example, including the proofs of the consistency of the B models of the interfaces (Listings 1 and 2) and the proofs of the different refinement steps (Listings 4, 5, 6, 7 and 7 ), is composed of 108 POs, among which 30 POs have been proved interactively (see Table 1

Related work

One of the first approaches of module reuse through interface adaptation is the approach of Purtilo and Atlee [START_REF] Purtilo | Module reuse by interface adaptation[END_REF]: they use a dedicated language (called Nimble) for relating a required interface to a provided one, where the adaptation is made by the developer. Our approach is similar modulo the formalism used for representing the interfaces: instead of a dedicated language, we use UML and the B method. We have the benefit of relying on standards. Furthermore we overcome the limited semantics of their approach because we use a formal tool for expressing and verifying the interface adaptation.

Dynamic component adaptation [START_REF] Mätzel | Dynamic component adaptation[END_REF][START_REF] Kniesel | Type-safe delegation for run-time component adaptation[END_REF] goes further than our approach by proposing methods for adapting at run-time components by finding suitable adapter components based on the interfaces of the components to adapt. Unfortunately these methods have strong requirements (knowing inheritance relationships, runtime mapping of interface relationships, . . . ) and rely primarily on types and/or object-oriented peculiarities, hence they are limited to subtype-like adaptations. This is not possible with our approach because trustworthiness would require also proving these strong requirements at run-time.

Our method allows nevertheless a broader range of possible adaptations (not limited to subtypes of a provided interface).

The paper [START_REF] Ehrig | A generic framework for connector architectures based on components and transformation[END_REF] presents a framework for modeling component architectures using formal techniques (Petri Net and CSP): connections between required and provided interfaces (called import and export interfaces) of components are represented by graph transformations (composition, embedding, extension and refinement). Our approach is similar. We use B formal method to express transformations as refinement between the required interface and the provided one.

Zaremski and Wing [START_REF] Zaremski | Specification matching of software components[END_REF] propose an interesting approach to compare two software components. It is determined whether one component can be substituted for another. They use formal specifications to model the behavior of components and the Larch prover to prove the specification matching of components.

Reussner et al. [START_REF] Reussner | Using Parameterised Contracts to Predict Properties of Component Based Software Architectures[END_REF][START_REF] Reussner | Reasoning on software architectures with contractually specified components[END_REF] present adapters in the context of concurrent systems. They consider only a certain class of protocol interoperability problems and generate adapters for bridging component protocol incompatibilities, using interface described by finite parameterized state machines.

The refinement steps of our approach for building an adapter can also be viewed as steps for building morphisms between interfaces. Such methods, for instance the methods presented by Smith [START_REF] Smith | Constructing specification morphisms[END_REF], are based on signature algebras and theory category. Our approach is rather practical because we choose the B method for expressing the interfaces. The B method is indeed easier for software engineers to understand because it is based on set theory. Our results resemble much with interface morphisms, thus these methods could provide means for automating our approach better.

Conclusion

The component-based paradigm has received considerable attention in the software development field in industry and academia like in other engineering domains. In this approach, components are considered as black-boxes described by their visible behavior and their required and provided interfaces. To construct a working system out of existing components, adapters are introduced. An adapter is a piece of glue code that realizes the required interface using the provided interfaces. It expresses the mapping between required and provided variables and how required operations are implemented in terms of the provided ones. We have presented a method in three steps to adapt complex data models, each step expressing a level of interoperability and establishing the correctness of the adaptation.

Using the formal method B and its refinement and assembling mechanisms to model the component interfaces and the adapters, we pay special attention to the question of guaranteeing the interoperability between the different components. The B prover guarantees that the adapter is a correct implementation of the required functionalities in terms of the existing components. With this approach, the verification of the interoperability between the connected components is achieved at the signature, the semantic and the protocol levels.

We are currently working on a method for adding dependability features to componentbased software systems. The method is applicable if the dependability features add new behavior to the system, but do not change its basic functionality [START_REF] Lanoix | Enhancing Dependability of Component-based Systems[END_REF]. The idea is to start with a software architecture whose central component is an application component that implements the behavior of the system in the normal case. The application component is connected to other components, possibly through adapters. It is then possible to enhance the system by adding dependability features in such a way that the central application component remains untouched. Adding dependability features necessitates to evolve the overall system architecture by replacing or newly introducing hardware or software components. The adapters contained in the initial software architecture have to be modified, whereas the other software components need not to be changed. Thus, the dependability of a component-based system can be enhanced in an incremental way.

Figure 1 :

 1 Figure 1: Component architecture

Figure 2 :

 2 Figure 2: The interfaces and their associated B models

Figure 3 :

 3 Figure 3: Adapter Alarms DB

Listing 1 :Listing 3 :

 13 B model of Database O MODEL Alarms U SEES Types VARIABLES alarms, active alarms INVARIANT alarms ⊆ AlarmIds ∧ active alarms ⊆ alarms INITIALISATION alarms := ∅ active alarms := ∅ OPERATIONS nb ←-number of active alarms = BEGIN nb := card( active alarms ) END; active ←-get active alarms = BEGIN active := active alarms END; reset alarm (aid) = PRE aid ∈ active alarms THEN active alarms := active alarms -{ aid } END; aid ←-new alarm(type) = PRE type ∈ AlarmTypes THEN ANY uid WHERE uid ∈ AlarmIdsalarms THEN aid := uid alarms := alarms ∪ {uid} active alarms := active alarms ∪ {uid} END END END Listing 2: B model of the interface Alarms U The types used in the developmentIn the rest of this paper, we focus on the development and the correctness of the adapter Alarms DB which must provide Alarms U using Database O. In terms of B models, we have to prove that Alarms DB is a refinement of Alarms U including Database O in a similar way to[START_REF] Mouakher | Component Adaptation: Specification and Verification[END_REF], as shown Figure3.

3

  Trustworthy method to adapt interface data models Let I U be an interface required by a component A and I O an interface provided by a component B. Our goal is to develop an adapter that implements the data model of I U using the data model of I O. In other words, the adapter must express I U in terms of the variables, data types and operations of I O. I U and I O are defined by B models as presented Figure 4. We denote by V U and V O their sets of variables and by OP U and OP O their sets of operations, respectively. We note D U (resp. D O) the set of data types of the variables V U (resp. V O).

Figure 4 :

 4 Figure 4: Process of the adapter development

Figure 5 .

 5 Figure 5. The specification of the B operations (not shown in this figure) is modified according to the variable transformations realized at each step of the development 1 .

Figure 5 :

 5 Figure 5: Refinement steps of the adapter Alarms DB

REFINEMENT

  Alarms DB ref1 REFINES Alarms U SEES Types VARIABLES alarms ids , alarms status , alarms type INVARIANT alarms ids = alarms ∧ alarms status ∈ alarms ids → AlarmStatus ∧ alarms type ∈ alarms ids → AlarmTypes ∧ alarms status = active alarms×{Active} ∪ ( alarms idsactive alarms )×{Inactive} ASSERTIONS ({Active} * active alarms ∪ { Inactive } * (alarms-active alarms ))[{ Active }] = active alarms INITIALISATION alarms ids := ∅ alarms status := ∅×AlarmStatus alarms type := ∅×AlarmTypes OPERATIONS nb ←-number of active alarms = BEGIN nb := card( alarms status -1 [{Active}]) END; active ←-get active alarms = BEGIN active := alarms status -1 [{Active}] END; reset alarm (aid) = BEGIN alarms status := alarms status -{ aid → Inactive } END; aid ←-new alarm(type) = ANY uid WHERE uid ∈ AlarmIdsalarms ids THEN aid := uid alarms ids := alarms ids ∪ {uid} alarms type := alarms type -{ uid → type } alarms status := alarms status -{ uid → Active } END END Listing 4: Step (1) of the adaptation process

  uid gen := 0 ids nn := ∅ status nn := ∅ type nn := ∅ OPERATIONS nb ←-number of active alarms = BEGIN nb := card( status nn -1 [status cast[{Active }]]) END; active ←-get active alarms = BEGIN active := id cast -1 [ status nn -1 [status cast[{Active}]] ] END; reset alarm (aid) = BEGIN status nn := status nn -{ id cast (aid) → status cast( Inactive ) } END; aid ←-new alarm(type) = BEGIN aid := id cast -1 (uid gen) ids nn := ids nn ∪ {uid gen} type nn := type nn -{ uid gen → type cast(type) } status nn := status nn -{ uid gen → status cast(Active) } uid gen := uid gen + 1 END END Listing 7: Step (2.3) of the adaptation process

Figure 6 :

 6 Figure 6: Commutation diagram

  Typecasting the codomain of each functional variableBefore this step, the codomains of nat status and nat type are not in the data types of Database O. We need to typecast these codomains, namely AlarmStatus and AlarmTypes, to the corresponding data types of the fields of the database, i.e. Attribute and Value respectively. These fields contain natural numbers, hence we introduce two constant functions named status cast and type cast which map AlarmStatus and AlarmTypes to natural numbers.

	REFINEMENT Alarms DB ref3 REFINES Alarms DB ref2 SEES Types VARIABLES nat ids , nat status , nat type INVARIANT nat status ∈ nat ids → AlarmStatus ∧ nat type ∈ nat ids → AlarmTypes ∧ nat status -1 = (alarms status -1 ; id cast) INITIALISATION nat ids := ∅ nat status := ∅ nat type := ∅ OPERATIONS nb ←-number of active alarms = BEGIN nb := card( nat status -1 [{Active}]) END; active ←-get active alarms = BEGIN active := id cast -1 [ nat status -1 [{Active}] ] END; reset alarm (aid) = END END Listing 6: Step (2.2) of the adaptation process REFINES Alarms DB ref3 SEES Types CONSTANTS type cast , status cast PROPERTIES type cast ∈ AlarmTypes → 1..card(AlarmTypes) ∧ status cast ∈ AlarmStatus → 1..card(AlarmStatus) CONCRETE VARIABLES uid gen VARIABLES ids nn , status nn , type nn INVARIANT uid gen ∈ N ∧ ids nn = nat ids ∧ status nn ∈ nat ids → 1.. card(AlarmStatus) ∧ type nn ∈ nat ids → 1.. card(AlarmTypes) ∧ uid gen > max(nat ids) ∧ status nn = (nat status ; status cast ) ∧ type nn = (nat type; type cast ) ASSERTIONS status cast -1 [status cast[{Active }]] = {Active} 4.2.3 REFINEMENT Alarms DB ref4 INITIALISATION

BEGIN nat status := nat status -{ id cast (aid) → Inactive } END; aid ←-new alarm(type) = ANY uid nat WHERE uid nat ∈ N ∧ uid nat /∈ nat ids THEN aid := id cast -1 (uid nat) nat ids := nat ids ∪ {uid nat} nat type := nat type -{ uid nat → type } nat status := nat status -{ uid nat → Active }

Table 1 :

 1 for details).

		Obvious POs	POs	Interactive POs
	Database O	3	24	8
	Alarms U	11	5	0
	Alarms DB ref1	26	18	4
	Alarms DB ref2	21	8	2
	Alarms DB ref3	25	14	5
	Alarms DB ref4	39	20	6
	Alarms DB ref5	23	19	5
	TOTAL	148	108	30

Complete B models are published in[START_REF] Colin | Trustworthy interface compliancy: data model adaptation[END_REF].


Van-Tinh Tran
email: van-tinh.tran@univ-lyon1.fr

Alex Aussem
email: aaussem@univ-lyon1.fr

Correcting a Class of Complete Selection Bias with External Data based on Importance Weight Estimation

Keywords: Selection bias, importance weighting, graphical models

We present a practical bias correction method for classifier and regression models learning under a general class of selection bias. The method hinges on two assumptions: 1) a feature vector, Xs, exists such that S, the variable that controls the inclusion of the samples in the training set, is conditionally independent of (X, Y ) given Xs; 2) one has access to some external samples drawn from the population as a whole in order to approximate the unbiased distribution of Xs. This general framework includes covariate shift and prior probability shift as special cases. We first show how importance weighting can remove this bias. We also discuss the case where our key assumption about Xs is not valid and where XS is only partially observed in the test set. Experimental results on synthetic and real-world data demonstrate that our method works well in practice.

Introduction

Selection bias, which occurs when training and test joint distributions are different, i.e. P tr (x, y) = P te (x, y), is pervasive in almost all empirical studies, including Machine Learning, Statistics, Social Sciences, Economics, Bioinformatics, Biostatistics, Epidemiology, Medicine, etc. It is therefore highly desirable to devise algorithms that remain effective under such distribution shifts. In general, the estimation problem with two different distributions P tr (x, y) and P te (x, y) is unsolvable, as the two terms could be arbitrarily far apart. However, when P tr (x, y) and P te (x, y) differ only in P tr (x) and P te (x) (known as covariate shift) or only in P tr (y) and P te (y) (known as prior probability shift), effective adaptation is possible. In this paper, we present a practical correction method for classifier and regression model learning under a more general class of selection bias. We assume implicitly that there exists a joint probability distribution P (x, y, s) that satisfies: P te (x, y) = P (x, y) = s P (x, y, s) and P tr (x, y) = P (x, y|s = 1), where the variable S controls the selection of examples in the training set (1 means the example is selected, 0 means the example is not selected). While P te (x, y) and P tr (x, y) are derived from the same distribution P (x, y, s), we assume no independence assumption holds between X, Y , and S. This is termed complete selection bias in the literature. In this case, we have to resort to some additional information on the mechanism by which the samples were preferentially selected to the data set to correct the bias.

The recent paper by Bareinboin et al. [START_REF] Bareinboim | Recovering from selection bias in causal and statistical inference[END_REF] has been very influential in our thinking. Mirroring their work, we show that, if we have a combination of biased data and unbiased data and qualitative probabilistic assumptions that are deemed plausible about our sampling mechanism, our problem becomes solvable. More specifically, we assume we have access to a S-control feature vector, X s , and some additional sample of the form (x s ) that is drawn from the population as a whole, such that S is conditionally independent of (X, Y ) given X s . Despite being limited to specific or idealized situations, this framework includes covariate shift and prior probability shift as special cases. We also consider the case where X s is not fully measured in the target population. This situation typically arises in various clinical studies or epidemiological scenarios, where some variables are too difficult or costly to measure in the target population.

We show that one may account for the difference between P tr (x, y) and P te (x, y) by reweighting the training points using the so-called importance weight, denoted as β(x s ). If the selection process is explicitly known, then β(x s ) is simply given by P (s=1) P (s=1|xs) , otherwise, we resort to an external (bias-free) data set of X s in order to estimate β(x s ) directly [START_REF] Huang | Correcting sample selection bias by unlabeled data[END_REF][START_REF] Kanamori | A least-squares approach to direct importance estimation[END_REF]. Furthermore, as one usually has a partial understanding of the sampling mechanism, we investigate whether covariate shift and prior probability shift corrections may help reduce complete selection bias despite not being valid.

Bias correction

In this section, we investigate the interplay between two types of variables, V B and V P , where V B are variables collected under selection bias, P (V B |S = 1), and V P are variables collected in the population-level, P (V P ) 1 . We assume that Y ∈ V B . In [START_REF] Bareinboim | Recovering from selection bias in causal and statistical inference[END_REF], Bareinbom et al. provide a sufficient condition for P (x, y) to be recoverable when no data is gathered over X and Y in the population level. We extend slightly their result by considering also the case where either Y or some input variables in X are not only collected under selection bias, but also in the population-level, (i.e. {X, Y } ∩ V P ∩ V B = ∅), Theorem 1. The bias-free distribution P (x, y) is recoverable from a S-bias training samples if there exists a set of variables X s ⊆ V B ∩ V P , such that S ⊥ ⊥ (X, Y )|X s and the support of P (x s |s = 1) contains the support of P (x s ). Let β(x s ) = P (s=1) P (s=1|xs) , P (x, y) is then given by the formula,

P (x, y) = xs\{x,y} P (x, y, x s |s = 1)β(x s ) (1)
β(x s ) can be reformulated as β(x s ) = P (xs) P (xs|s=1) . So β(x s ) may be estimated from a combination of biased and unbiased data. Theorem 1 relies on qualitative assumptions (X s controls S over (X, Y )) that may appear difficult to satisfy in practice. However, in certain domains like epidemiology, information about the selection process can sometimes be expressed and modeled in a communicable scientific language (e.g., graphs or structural equations) by the domain experts. The selection bias mechanisms depicted in Figure 1 are common examples2 . in epidemiology [START_REF] Hernán | A structural approach to selection bias[END_REF]. The directed acyclic graphs should be regarded as graphical structures encoding conditional independence between X, Y , and S which may involve other variables as as well variables, like M , that is not observed in the target domain, and thus that is not included as input variable to the model. The S-control vector is shown along each plot. X 1 is some input variable to the model, M denotes a variables that is not observed in the target domain, and thus not used a input variable.

X \ X1 X1 Y S (a) Xs = {X1, Y } X M Y S (b) Xs = {M, Y } X \ X1 X1 Y S (c) Xs = {X1, Y } X M Y S (d) Xs = {M, Y }
Theorem 2. Given that condition of Theorem 1 is satisfied, if P is a distribution such that: P (x, y, x s , s) = P (x, y, x s , s)β(x s ) then P (x, y|s = 1) ≡ P (x, y).

Proof.

P (x, y, x s , s = 1) = P (x, y, x s , s = 1)β(x s ) = P (x, y, x s , s = 1) P (x s ) P (x s |s = 1) = P (s = 1)P (x s |s = 1)P (x, y|x s , s = 1) P (x s ) P (x s |s = 1) = P (s = 1)P (x, y, x s ) Thus, P (x, y, x s , s = 1) = P (x, y, x s )P (s = 1). If we sum this expression over x, y, x s we obtain P (s = 1) = P (s = 1). Therefore, P (x, y, x s |s = 1) = P (x, y, x s , s = 1) P (s = 1) = P (x, y, x s )P (s = 1) P (s = 1) = P (x, y, x s ) Finally, P (x, y|s = 1) = xs\{x,y} P (x, y, x s |s = 1) = P (x, y).

Theorem 2 states that an unbiased training sample can be obtained by weighting each training example by β(x s ) = P (xs) P (xs|s=1) . Note however that the support of P (x s ) should be contained in the support of P (x s |s = 1) for the β(x s ) to be always defined. A similar technique applied to covariate shift was discussed in [START_REF] Zadrozny | Learning and evaluating classifiers under sample selection bias[END_REF]. The unbiased expected loss of the model follows:

Corollary 1. Given that condition of Theorem 1 is satisfied, and P in Theorem 2, for all classifier h, all loss function l = l(h(x), y), E x,y∼P (l) = E x,y∼ P (l|s = 1) E x,y∼P (l) is the loss that we would like to minimize and E x,y∼ P (l|s = 1)) is the loss that may be estimated from the new biased sample drawn from weighted distribution P .

Experiments

In this section, we assess the ability of importance weighting to remove complete selection bias based on Theorem 2. In the toy experiment, we investigate whether covariate shift and prior probability shift corrections may help reduce complete selection bias despite our assumptions between the training and test distributions difference being violated (through an invalid choice for X s ).

When the selection process is explicitly known, β(x s ) is simply given by P (s=1) P (s=1|xs) . Otherwise, we resort to an external (bias-free) data set of X s in order to estimate β(x s ) as P (xs) P (xs|s=1) . In this study, we use the Kernel Mean Matching (KMM) [START_REF] Huang | Correcting sample selection bias by unlabeled data[END_REF][START_REF] Yu | Analysis of kernel mean matching under covariate shift[END_REF] estimator for β(x s ) denoted as KMM(X s ). As one usually has a partial understanding of the sampling mechanism, we investigate whether covariate shift (i.e., β(x) = P (x) P (x|s=1) ) and prior probability shift (i.e., β(y) = P (y) P (y|s=1) ), corrections may help reduce complete selection bias despite not being valid. These strategies are denoted as KMM(X), KMM(Y ). We first apply our method to a simple toy problem and then compare KMM to another estimator called the Unconstrained Least-Square Importance Fitting (uLSIF) [START_REF] Kanamori | A least-squares approach to direct importance estimation[END_REF] on a variety of regression and classification benchmarks from the UCI Archive.

Toy problem

Consider the S-bias mechanism displayed in Fig. 1b, where the feature X has a uniform distribution in [0, 1]: P (X) ∼ U(0, 1). Note that the influence of M on Y is mediated by {X, S}. The observations are generated according to y = 1 -0.5x and are observed in Gaussian noise with standard deviation 0.5 (see Fig. 2c; the black solid line is the noise-free signal). The intermediate variable M , between X and S, is generated according to M = X + N (0, 0.3 2 ). As M is only measured in the training set, it is not used as an input variable in our regression model. Therefore, we investigate a case where X s is partially missing in the test set. The probability of a given example being included in the training set depends on Y and M and is given by Note that the minimum value of P (S = 1|m, y) needs to be greater than 0 so that the support of P (m, y) is contained in the support of P (m, y|s = 1), as required by Theorem 1. The choice of P (m, y) is intended to induce a noticeable discrepancy between P (y|x, s = 1) and P (y|x). We sampled 200 training (red crosses in Fig. 2c) and testing (grey circles) points from P tr and P te respectively. The bias is clearly noticeable from the X-Y contour plots in Fig. 2a andb where P (s = 1|m, y) and P (s = 1) may be obtained from the known selection mechanism shown above or directly estimated by KMM. We attempted to model the observations with a degree 1 polynomial. The black dashed line in Fig. 2c is a best-case scenario given our test points, which is shown for reference purposes: it represents the model fit using ordinary least squared (OLS) on the test set. The brown line is a second reference result, derived only from the training data via OLS, and predicts the test data very poorly. The green dashed line is a third reference result, fit with weighted ordinary least square (WOLS), using the true β(x s ) values calculated from the true data generating mechanism, and predicts the test data quite well. The other three dashed lines are fit with WOLS using the KMM weighting schemes under the three assumptions. Note that the true generating model between X and Y is included in the hypothesis space. We estimated the effect of the number of training points on the estimation of the reweighting factors by examining the average mean square error (MSE) on the test set as a function of the number of training points. As may be observed in Fig. 2d, the error goes down as the sample size increases, until it reaches an asymptotic value. KMM(X s ) performs well even with relatively moderate amounts of data achieving almost optimal error quite quickly, handily outperforming the reweighting method based on KMM(X) and KMM(Y ) by a noticeable margin. More interestingly, KMM(X s ) also outperforms the reweighting method based on the true data generating mechanism, especially when sample size is small. This result may seem counter-intuitive at first sight: the reason is that the exact importance-sampler weights are not always optimal unless we have an infinite sample size. See [START_REF] Shimodaira | Improving predictive inference under covariate shift by weighting the log-likelihood function[END_REF] for a thorough discussion. Remarkably, despite our assumption regarding the difference between the training and test distributions being violated, KMM(Y ) and KMM(X) improve the test performance.

P (S = 1|m, y) ∼      y -m, if 0.1 ≤ (y -m) ≤ 1 0.1, if (y -m) ≤ 0.

Real-world data sets

We now examine whether using importance weighting can reduce selection bias in 10 UCI data sets with 5 classification tasks and 5 regression tasks. We employ three methods to estimate importance weighting: ratio of underlying probability, KMM and uLSIF and compare their performance against the baseline unweighted method. For each data set, X s is chosen to be the label Y and the most correlated input variable to Y (denoted as X 1 for simplicity). The selection bias mechanism is illustrated in Fig. 1c. The selection variable S for each training example is determined according to two scenarios depending on whether it is regression or classification problem. For regression problem, we use P (s = 1|x 1 , y) = exp(ax 1 + by + c)/[1 + exp(ax 1 + by + c)], where a, b, c, are parameters that determine the bias. For binary classification problem, we use:

P (s = 1|x 1 , y) = 0.5 if x 1 > mean(x 1 ) and y = 1 1 if otherwise.
For each data set, we then train 4 predictive models learned under the four weighting schemes discussed above and a model learned from the unbiased data (baseline) using SVM-light [START_REF] Joachims | Making large-scale svm learning practical[END_REF] which allows importance weighting to be fed directly to SVM. All classifiers are trained with the common Radial Basis Function (RBF), with a kernel size σ chosen through a 5-fold cross validation. This procedure is repeated 100 times for each data set. The results are reported in Tab. 1. As may be seen, all importance weighting schemes achieve lower prediction error with respect to the baseline unweighted scheme. The underlying probability weighting scheme performs pretty good. Curiously, on the Boston Housing data set, all three weighting schemes perform worse than the baseline unweighted method. It seems therefore that the effectiveness of bias correction based on importance weighting is data dependent. In order to better assess the overall results obtained for each of the 4 weighting schemes, a non-parametric Friedman test was firstly used to evaluate the rejection of the hypothesis that all the models perform equally well (except the unbiased model of course) at significant level 5%. Statistically significant differences were observed. So we proceeded with the Nemenyi post hoc test. The results along with the average rank diagrams are shown in Fig. 3. The ranks are depicted on the axis, in such a manner that the best ranking algorithms are at the rightmost side of the diagram. The algorithms that do not differ significantly (at p = 0.05) are connected with a line. As may be observed in Fig. 3, contrary to uLSIF, KMM is significantly better than no weighting.

Discussion & Conclusion

The aim of this paper was to elaborate on the idea of exploiting the assumptions that are deemed plausible about the sampling mechanism to correct or reduce Average Rank Fig. 3: post hoc analysis selection bias in machine learning tasks. The method hinges on the existence of a S-control feature vector, X s , and an additional (biased-free) sample that allows us to estimate the distribution of X s . We showed experimentally that direct weighting estimation is able to achieve significant improvements in accuracy over the unweighted method, even in situations where our key assumption is not valid (assuming covariate shift and prior probability shift instead of complete selection bias). However the gain in accuracy is data dependent. In fact, all conclusions are extremely sensitive to which variables we choose for X s . As the choice of X s usually reflects the investigator's subjective and qualitative knowledge of statistical influences in the domain, the data analyst must weight the benefit of reducing selection bias against the risk of introducing new bias carried by unmeasured covariates even where none existed before. Nevertheless, we hope this study will convince others about the importance of selection bias correction methods in practical studies and suggest relevant tools which can be used to achieve that goal.

Fig. 1 :

 1 Fig.1: Examples of complete selection bias mechanisms depicted graphically. The S-control vector is shown along each plot. X 1 is some input variable to the model, M denotes a variables that is not observed in the target domain, and thus not used a input variable.

Fig. 2 :

 2 Fig. 2: Toy regression problem 1. (a) and (b) Contour plots X-Y on training and test sets; (c) Polynomial models of degree 1 fit with OLS and WOLS; (d) Average performances of four WOLS methods and OLS on the test data as a function of the number of training points.

  . The bias-free distribution P (x, y) is recoverable from the S-bias training samples since {M, Y } satisfies Theorem 1. Thus we use Theorem 2, to remove selection bias by weighting each example by the importance ratio: β(x s ) = β(m, y) = P (m, y) P (m, y|s = 1) = P (s = 1|m, y) P (s = 1)

Table 1 :

 1 Mean test error averaged over 100 trials of different weighting schemes on UCI data set. Data sets marked with * are for regression problems

	Data set	No weighting KMM	uLSIF	Underlying P Unbiased model
	India diabetes	0.338 ± 0.049 0.266 ± 0.040 0.332 ± 0.053 0.287 ± 0.055 0.258 ± 0.035
	Ionosphere	0.069 ± 0.039 0.066 ± 0.039 0.067 ± 0.040 0.067 ± 0.039 0.065 ± 0.036
	BreastCancer	0.044 ± 0.016 0.039 ± 0.015 0.043 ± 0.017 0.040 ± 0.016 0.038 ± 0.015
	Haberman	0.264 ± 0.069 0.262 ± 0.071 0.263 ± 0.070 0.262 ± 0.071 0.262 ± 0.071
	GermanCredit	0.300 ± 0.044 0.298 ± 0.046 0.298 ± 0.045 0.298 ± 0.046 0.295 ± 0.046
	Airfoil self noise*	0.534 ± 0.104 0.470 ± 0.122 0.475 ± 0.082 0.445 ± 0.081 0.403 ± 0.059
	Abanlone*	0.526 ± 0.048 0.484 ± 0.054 0.521 ± 0.057 0.466 ± 0.041 0.456 ± 0.036
	Computer Hardware* 0.326 ± 0.308 0.321 ± 0.304 0.321 ± 0.299 0.319 ± 0.307 0.305 ± 0.201
	Auto MGP*	0.268 ± 0.148 0.298 ± 0.192 0.212 ± 0.129 0.203 ± 0.128 0.129 ± 0.063
	Boston Housing*	0.323 ± 0.110 0.327 ± 0.127 0.349 ± 0.133 0.332 ± 0.127 0.298 ± 0.112

Upper-case letters in italics denote random variables (e.g., X, Y ) and lower-case letters in italics denote their values (e.g., x, y). X denotes the input variables and Y the target.

We assume the reader is familiar with the concepts of d-separation[START_REF] Pearl | Probabilistic reasoning in intelligent systems -networks of plausible inference[END_REF]