Eric Leclercq
email: feric.leclercq@u-bourgogne.fr

Djamal Benslimane
email: djamal.benslimane@u-bourgogne.fr

Kokouy Étongnon
email: kokou.yetongnong@u-bourgogne.fr

AMUN: An Object Oriented Model for Cooperative Spatial Information Systems

The diversity of spatial information systems promote the need to integrate heterogeneous spatial or geographic information systems (GIS) in a cooperative environment. We present an on going research project, called ISIS (Interoperable Spatial Information System), which aims to build an environment to support interoperability of GIS by interconnecting spatial data repositories and spatial processing resources. Our solution combines techniques from traditional interoperable information systems, spatial data modeling and distributed object oriented databases. While object oriented data modeling impact has been studied in spatial databases, research in model for distribution of both data and operations has received little attention. We focus in this paper on modeling problems and describe an hybrid spatial functional OO model that provides tools to model distribution and to resolve heterogeneities.

Introduction

In recent years, a significant amount of research have been directed towards spatial database management systems. They have raised several problems including spatial data modeling, spatial data structure implementations, spatial query languages, query processing and systems architectures [START_REF] Coyle | Experiences with Object Data Models in Geographic Informations Systems[END_REF][START_REF] David | A Unified Approach to Geographic Data Modeling[END_REF][START_REF] Scholl | Object-Oriented Database Systems for Geographic Applications: An Experiment with O2[END_REF][START_REF] Worboys | Objectoriented data modelling for spatial databases[END_REF]. On the other hand, we are witnessing the rapid development of high speed world-wide networks which provides access to a large diversity of informations sources, particularly spatial information systems.

This has created the need to integrate heterogeneous spatial information systems in a cooperative environment. Existing spatial information systems are often designed for specific range of applications, each system may have its own spatial data model and spatial processing capabilities. Users would like to query and manipulate these systems in a uniform way, but the diversity of models and geoprocessing functions specificities render the design of integrated or cooperative GIS a very difficult task to carry out.

Traditionaly, research effort in cooperative information system has been directed at several issues including:

-the definition of concepts and model for allowing uni-form access to multiple heterogeneous data sources. Sheth and Larson in [START_REF] Sheth | Federated database systems[END_REF] present a survey of solution for federating traditional heterogeneous databases systems. Many approaches focus on the definition of techniques for resolving semantic heterogeneity and for constructing integrated schema to support interoperability of autonomous information systems. An alternative to federated systems based on global integrated schema is the multidatabase language approach [START_REF] Pitoura | Object Orientation in multidatabase systems[END_REF]. It avoids the problems inherent to the creation of global integrated schemas by using a multidatabase language to support interoperability; -the definition of concepts and tools for searching, discovering and retrieving informations distributed over a network. New architectures and paradigms are being proposed to enable designers to take advantage of existing networking technology while designing distributed computing systems. They range from client-server architecture to distributed object based processing environment such as CORBA and Web based systems. In client-server architecture, client objects communicate with server objects to request data or processing functions. Distributed object based environment is a generalized client-server paradigm in which a cooperation bus is used to allow computation across different platforms. An intermediate model, typically an OO model, may be used to wrap the components of the different platforms, thus providing them with a uniform interface.

In this paper we address issues relevant to GIS interoperability. We present ISIS (interoperable spatial information system) to allow users to query and manipulate these systems in a uniform way. ISIS is a first step to a cooperative environment. Issues that must be dealt with in order to address GIS interoperability include: 1) distributed access to multiple heterogeneous data sources, 2) data model heterogeneity [START_REF] Worboys | Semantic Heterogeneity in Distributed Geographic Database[END_REF], 3)schema and query translation between components. The key characteristic of the project are: a mediator/wrapper oriented architecture which provides to users a uniform access to distributed spatial databases;

a distributed spatial OO data model (AMUN) which provides a uniform design of spatial data stored in differ-ent GIS and handles localization and distribution of spatial objects;

an implementation build on the top of a distributed object architecture like CORBA which provides a good framework for the definition of a multilayer set of abstract and concrete services that are mapped to mediators and wrapper. This allow systems to share spatial data and geoprocessing functions.

The remainder of the paper is organized as follows. First, we summarize related approaches to GIS interoperability, second we describe how to use mediators and wrappers to provide interoperability between different GIS. Third, we introduce the distributed spatial object model called AMUN. Fourth, we present an overview of the ISIS environment and its operational architecture. Finally, we conclude essentially with a summary of the paper.

Related work

Recently, several researchers have focused on interoperability of GIS [START_REF] Bishr | SEMWEB -A Prototype for Seamless Sharing of Geoinformation on The World Wide Web in a Client/Server Architecture[END_REF][START_REF] Nittel | Mapping A Common Geoscientific Object Model to Heterogeneous Spatial Data Repositories[END_REF][START_REF] Gardels | Open GIS and On-Line Environmental Libraries[END_REF][START_REF] Voisard | A Multilayer Approach to the Open GIS Design Problem[END_REF]. Ken Gardels [START_REF] Gardels | Open GIS and On-Line Environmental Libraries[END_REF] discusses the fundamental requirements of GIS interoperability: 1) a generic model to support a variety of GIS functions and capabilities, 2) a set of known tools or functions necessary for solving problems and 3) heterogeneous methods for exploring and accessing spatial information and resources in a network of systems.

Yaser Bishr et al [START_REF] Bishr | SEMWEB -A Prototype for Seamless Sharing of Geoinformation on The World Wide Web in a Client/Server Architecture[END_REF] describe different levels of GIS interoperability:

Platform level: is devoted to hardware and network protocols interoperability. It provides support for transferring data files between systems. Users need to have prior knowledge of remote file formats and invoke the appropriate converters on the transferred files.

Syntactic level: is concerned with data and systems (GIS) interoperability. It allows physical data exchange between systems. Traditional solutions to GIS interoperability are defined at this level. They are based on format conversion. Software tools are defined for structure conversion between pairs of GIS, by typically using a common exchange format to produce an intermediate structure which is later mapped to the final structure. The identification of remote file formats and the required conversions are transparent to the users. Other solutions at this level, allow users to connect to a remote GIS and to query the remote system using their own local language. This solution is comparable to the multidatabase language approach of traditional databases.

Application level: is relevant to syntactic and application semantics (data model) interoperability. Interoperation at this level is based on a global virtual view of components GIS. Users queries are formulated on this virtual view and mapped on the remote GIS. This solution is similar to federated database approach based on global integrated schema.

Different approaches have been proposed for achieving the above requirements and levels of interoperability. They can be categorized as follows:

the federation approach, which uses a global integrated schema to represent objects contained in component GIS. First, the spatial schema of the participating systems are mapped into a common data model. Next, semantic conflicts among the schema are detected. And finally, correspondence rules are used to integrate the translated schemas to create global federated schemas; the persistent object approach in which each GIS or data repository is seen as a persistent store for spatial objects described by a common data model [START_REF] Nittel | Mapping A Common Geoscientific Object Model to Heterogeneous Spatial Data Repositories[END_REF]. The localization of the spatial objects is transparent to end users. It defines an object environment and related tools to allow reusability of the functionalities of the participating systems; the interface approach extends each GIS with an interface which describes data from remote GIS in the local model. Typically an extended application programmer interface (e.g OO interface extended with query processing capabilities) is used as local model. This allows a user to access spatial objects from other systems as local objects. The interface handles query translation and maps query results into local objects.

Recently, the OpenGIS consortium has defined a generic framework and guidelines for applying classical open system approach to geographic information processing [START_REF]The OpenGIS Abstract Specification: An Object Model for Interoperable Geoprocessing, Revision 1, OpenGIS Consortium[END_REF]. The primary intent of open system model is to allow sharing of data, resources and systems services among applications; to facilitate exchange of information among heterogeneous systems; to enable the reuse of software components; and to permit the design of extensible systems. The OpenGIS specification extends the above properties to geographic information systems 1) to define an operational model in which spatial object or features are not defined by their structural properties, but are rather defined in terms of interfaces and 2) to allow the development of geoprocessing on different data architectures. The OpenGIS guidelines define three interoperation models. The essential model defines geographic formalism such as types, schema and services for representing real world entities [START_REF] Gardels | Open GIS and On-Line Environmental Libraries[END_REF]. The open geodata model can be used to define behavior or methods for geographic elements and to specify a catalog of meta information and spatial references. Finally, the OpenGIS service model define functions for assembling spatial objects and their interface to complex queries and geoprocessing operations.

Several authors have proposed solutions for GIS interoperability based on the OpenGIS specifications. Agnès Voisard et al [START_REF] Voisard | A Multilayer Approach to the Open GIS Design Problem[END_REF] propose a multilayer approach to the OpenGIS design problem. Each layer correspond to a different level of abstraction, from application level to data access level. Their decomposition provide a good framework for facil-itating the design of interoperable GIS. Nittel in [START_REF] Nittel | Mapping A Common Geoscientific Object Model to Heterogeneous Spatial Data Repositories[END_REF] uses OpenGIS specifications in a persistence object approach. Their persistent object manager (geoPOM) provides a homogeneous interface to heterogeneous spatial data repositories. geoPOM's data model is composed of two parts: an object oriented data model based on ODMG93 and a set of predefined spatial object types based on OpenGIS specifications.

An overview of ISIS's architecture

This section presents the functional architecture of the ISIS project. The primary goal of the project is to achieve interoperability among GIS by allowing the realization of distributed spatial object system. The main goal of the architecture are: 1) to allow and facilitate access to multiple spatial information sources, 2) to describe, compose and customize information from different sources according to a specific application domain, 3) to allow incremental definition of the system by using dynamic link between mediator and wrapper, and composition of interface repository. Figure 1 shows the functional architecture of ISIS. It consists of a network of software components grouped in three logical levels devoted to mediators, wrappers and local GIS. The mediator level consist of a set of abstract services which are used to provide a uniform and customized view of different heterogeneous data sources. Each view is represented in the AMUN model and is specific to an application domain. This allows the definition of virtual GIS at the user application level. Virtual GIS contains virtual objects which aggregate complex structured objects existing in one or more data sources. Mediator's abstract services handle the decomposition of tasks into subtasks, determine the appropriate data sources and operations required by subtasks and dispatch the subtasks to different local GIS and recombine the results. In summary a mediator comprises an interface repository manager, a distributed object query service, a global transaction manager and an object man-ager. The object interface repository consists of a set of schemas m ; sdb expressed in AMUN common data model. A schema m;sdb corresponds to the description of heterogeneous data (objects classes described by their interface) from one or more sites. The interface repository is associated with an object specification language (ISL). It describes shared spatial object, shared spatial operations and data sources. The distributed object query service is responsible for the decomposition and optimization of global queries. The query decomposition phase must take into account specific geographic operators that are located on different sites. Thus, global decomposition is more complex than in traditional systems. The primary intent is to maximize parallel execution of inter site spatial joins. The global transaction manager is responsible for global concurrency control among tasks. It maintains semantic correctness of global transactions. Global transaction management issues are currently not dealt with in ISIS. The distributed object manager provides tools to create, describe and manage the interface repository.

The wrappers level is a set of concrete services (System GIS Services). The goal of this level is to encapsulate each GIS in a generic spatial object server by a wrapper. A wrapper resolves heterogeneities between a spatial data server and the rest of the system. This is done by defining mappings between local schema (GIS schema) and schema in AMUN. It also deals with invocation of services, execution of operations and data access to and from the underlying spatial data server. A wrapper W i contains a schema w ; sdb i obtained by translating an export schema l;sdb i from the local data model to the common data model AMUN, it also describe spatial operations. Contrary to mediator's schemas which combine information from various sources, a wrapper schema w ; sdb i describes a single data source. Furthermore, there is no direct relation between w ; sdb i .

The local level consist of a set of local GIS. It is devoted to the definition of a set of export schemas l ; sdb i which correspond to partial views of data sources expressed in local data models.

The operational architecture is presented in section 5, AMUN is presented in the following section.

Definition of a common spatial data model

One of the most problem to be dealt with, when interconnecting heterogeneous GIS, is to provide a unique spatial data model and language to access and manipulate the spatial object stored in different repositories. In ISIS environment, we have defined a common spatial data model called AMUN which can used to represent traditional data, spatial data and to manage distributed objects.

As shown in figure 2, AMUN is a three levels model. The first two levels specifies a set of concepts to represent respectively traditional data and spatial data with attached spatial operations. The last level is composed of new concepts to manage distributed and heterogeneous objects. In the following, we detail the AMUN's concepts defined at each level. In this paper we focus on the distribution of spatial data, a description of the concepts for distribution of spatial operation can be found in [START_REF] Leclercq | A Distributed Object Oriented Model for Heterogeneous Spatial Databases[END_REF].

Core concepts

The basic concepts of AMUN are: type, object, class, and the extent of a class. They are described by attributes and operations and their respective signatures. A type interface consists of the properties and operators associated with the type. An interface describes the behavior of the type. Attributes and operations are described by their signatures.

Definitions

The following sets will be used throughout the remainder of this section : O represents the set of real world objects, D is the set of atomic domain values (integer, real, character,. . . ), OIDis the set of object identifiers, C is the set of all classes, A is the set of attribute names, OP is the set of operation names. Definition 1 (type system T) s o 2 S Ois defined by: op(s 1 s 2 : : : s n ) ! t where s i 2 S p i = 1 : : : n is a sequence of attribute signatures and t 2 T is the result of op.

A

Definition 4 (type interface)

Let I be the set of interfaces. A type interface i 2 I, defined on t 2 T, such that t = (i), is a tuple

< Structure Operations > :
Structure is a sequence of attribute signatures.

Operations is a sequence of signatures associated with the set of operations applicable on the type t.

The function : I ! T returns the type associated with the interface.

Definition 5 (subtype, supertype)

Consider two types t 1 and t 2 . Let i 1 i 2 2 I be the interfaces of t 1 and t 2 respectively. t 1 is a subtype of t 2 , noted t 1 t 2 if and only if Structure(t 1 ) S t r u c t u r e (t 2 ) and Operations(t 1 ) operations(t 2 ). t 2 is a supertype of t 1 .

The relation defines a partial order on the set T.

Definition 6 (object)

An object instance or object o 2 O represents a real world entity. An object is defined by a tuple < oid v > where oid 2 OIDis the identifier of o and v 2 V is a value of type t 2 T which represents the state of the object (attributes of o).

Definition 7 (class)

A class c 2 C represents a set of objects with the same type t 2 T (they have the same properties and operations). A class has an interface which is a type and an extent which is denoted by (c). A class is defined by a tuple < i extent >

where i is the interface of t. The extent of a class c 2 C is the set of OID of the objects of c.

Definition 8 (subclass, superclass)

Consider two classes c i =< i i extent i > and c j =< i j extent j > in C. c i is a subclass de c j (noted c i c j ) if and only if (i i ) (i j ) and (c i ) (c j )

An Example using ISL

We have given above a formal description of the core concepts which provide a foundation for the definition of spatial and distributed object types of the AMUN data model.

A complete formal description of the concepts is beyond the scope of this paper. In the remainder of the paper, we will use the interface specification language (ISL) and interface query language (IQL) to present spatial object data types. ISL and IQL are closed to ODL and OQL defined by ODMG-93. We now introduce a simple example of schema that to illustrate the ISL syntax and underly the spatial type definitions given in the remainder of the section. The example represents a schema which models a parcel (plot) of farm land. The information of interest are parcel number, the owner, the type of crop (culture), a list of values representing the harvest and eventually geographic information on the parcel.

Spatial types

The data model AMUN comprises a set of predefined spatial data types and associated operators. The predefined spatial data types are based on a subset of the spatial types of the OpenGIS specifications [START_REF]The OpenGIS Abstract Specification: An Object Model for Interoperable Geoprocessing, Revision 1, OpenGIS Consortium[END_REF]. OpenGIS spatial type are described by well-known structures which represent their semantic. AMUN uses a subset of the OpenGIS hierarchy. Geom is the highest spatial type in the hierarchy. It represents general geometric information. The spatial data type CoordinateGeometry is a subtype of Geom. It models spatial object which have coordinate informations. The low level basic spatial types of the hierarchy are: Point, LineString, Polygon, . . . . The spatial types can be included in a general type to model the geometric aspect of the corresponding object. For example, an attribute Geometry with type TSIMPLEPOLYGON can be added to the type TParcel above to model the geographic properties of the farm land. The new definition for TParcel is shown below.

Distributed Spatial Object Concepts

This section presents concepts for defining virtual global view of classes from heterogeneous spatial data sources. We define types and concepts that can be used to: 1) restructure the value of object, thus allowing multiple representations derived or calculated from the values of an objet; and 2) allow aggregation of information from different sources. To achieve this, we define the concepts of calculated attributes, calculated extents, concrete class and virtual class. We give in the next subsection formal definitions of these concepts.

Calculated attributes and calculated extents

A calculated attribute is an attribute whose value is obtained by the evaluation of an expression on the objects of a class. The signature of a calculated attribute is defined as follows. Definition 9 (calculated attribute signature) Let S c , s c 2 S c denotes the set of calculated attribute signatures and the signature of a calculated attribute respectively. The signature of s c 2 S c is defined by < s e x p r > where s 2 S p is an attribute signature and expr is a well-formed expression over the sets A and OP For example, below is a calculated attribute to represent the best harvest from the type TParcel define above.

calculated attribute integer BestHarvest = Max(Harvests)

A calculated extent is a class extent obtained by evaluating a calculated attribute on the instances of a class. Definition 10 (calculated extent) Let e 2 E e i 2 E i= 1 : : : n be class extents and E be the set of all class extents. Let f be a formula or an expression. A calculated extend is computed from one or more class extents as follows:

f (e) 2 E is a calculated extent from the extent of a single class c of C as follows: It contains the objects of c verifying the formula f. We distinguish two cases:

-if f is a logic formula, then f (e) contains the objects of c verifying the formula f -if f is an expression which compute a new value for each element of c, then f (e) contains the same objects as extent of C.

f (e) 2 E is calculated from two or more extents e i i = 1 : : : n of C, f (e)= S i=1 ::: n (e i ) 2 E is a calculated extent defined by the set union of the concrete/calculated extents e i .

Concrete and Virtual class

A concrete class implements a type interface on a local information system. It is used to describe objects really stored in different data repository. A concrete class is defined as follow:

Definition 11 (concrete class)

A concrete class is defined by < i extent w > where i 2 I is an interface and extent represents the set of objects of the concrete class. Wrapper w contains an implementation for the interface i and is capable of retrieving the corresponding physical objects from a local extent.

Figure 3 shows two concrete classes associated with the type TParcel defined above. The classes are defined in two wrappers w1 and w2 to represent parcel information modeled by two GIS: GIS1 and GIS2. A definition of the concrete classes using the ODL language is given below. A Virtual class which is used to model distributed spatial objects. The definition of virtual class is based on concrete classes, calculated attributes and calculated extents. A virtual class is defined as follows.

Definition 12 (virtual classes)

A virtual class vcis a class which is not implemented on any wrapper. It is defined by < i extent > where i is a type interface and extent is the set of objects of the virtual class.

In our approach, virtual classes are used, at the mediator level, to create global view over distributed information sources. A virtual class enables a user to create virtual objects by restructuring 1) the state or the value of one or more The semantic associated with calculated attributes is applied on the elements of two classes (figure 5(b)). All objects which verify this semantic (whether or not from the same class) are grouped to form the extent of the virtual class. Note that the original objects may have different structural properties. The virtual class interface, which must be compatible with the structural description of the objects, will be used to access and manipulate the resulting virtual objects.

The following example presents the definition of a virtual class CVAllParcel as a union of the two concrete classes EVParcel1 and EVParcel2 (figure 5(b)). The new class represent all parcels modeled by GIS1 and GIS2. The resulting virtual extent is EVAllParcels. of the functional architecture. Our architecture can be used to incorporate different GIS such as GIS Arc/Info, Illustra, GRASS into a multi spatial information system.

An operational architecture based on CORBA

To achieve GIS interoperability, we decompose the architecture in different layers [START_REF] Voisard | A Multilayer Approach to the Open GIS Design Problem[END_REF][START_REF] Bishr | SEMWEB -A Prototype for Seamless Sharing of Geoinformation on The World Wide Web in a Client/Server Architecture[END_REF]. The most important layers are the physical data store layer, the GIS functionalities layer, and the data model layer. Each layer provides a set of schema and services to implement the functionalities of the next higher layer. Platform (hardware and network layers) interoperability is handled by CORBA functions and services. CORBA's Object Request Broker (ORB) supports interconnectivity for high level services. These services deal with high level expressions over OQL and AMUN in an homogeneous environment. Thus, the different services can reside on different machines of a network, and can be implemented in different languages (e.g. ADA, C++, Java, ...).

In our approach, users applications are clients for the mediators. When a query formulated in a global language is submitted to a mediator, the global query processor in the mediator determines the data and the operations requested by the query. The mediator sends multiple sub-queries to the wrappers taking part in the execution of the global user query. Each wrapper receives only sub-query that can be processed locally, that is the required and operations are available on the local site. The wrapper uses transformation rules to translate the query to the local GIS language and provides secure connections to the requested data. It submits the query to the local GIS, converts instances of the result, and send the result to the mediator. Then results from participant sites are combined into a final result in the mediator. The data are mapped to local format and presented to the user.

Figure 1 :

 1 Figure 1: ISIS Mediation Architecture

Figure 2 :

 2 Figure 2: The three different levels of AMUN data model

  create concrete class CParcel1 of TParcel extent EParcel1 on w1 ; create concrete class CParcel2 of TParcel extent EParcel2 on w2 ;

Figure 6 Figure 5 :

 65 Figure 6 shows the operational architecture of ISIS. It is based on OMG distributed object management model and its core component CORBA. The functional architecture of ISIS is implemented on top of CORBA. The common data model (AMUN) and a compliant OQL query language are

  type system T is defined as follows: integer, string, float, boolean T are atomic types if t i 2 T i= 1 : : : n then tuple(t 1 t 2 : : : t n ) 2 T Consider an operation op 2 OP and a type t 2 T. Let S O be the set of operation signatures. An operation signature

	if s i 2 S p i = 1 : : : n then a : tuple(s 1 s 2 : : : s n ) is a
	tuple attribute signature if s i 2 S p i = 1 : : : n then a : S e t (tuple(s 1 s 2 : : : s n ))
	is a structured collection attribute signatures
	Definition 3 (operation signature)
	is a structured type if t 2 T then S e t (t) 2 T is collection types
	Definition 2 (attribute signature) Let a 2 A be an attribute name, t 2 T be an atomic type and S p be the set of attribute signatures. An attribute signature s p 2 S p , called primitive attribute signature, is defined over the set of types T as follows: a : t is an attribute signature in S p a : S e t (t) is collection attribute signatures in S p

  TParcel is given below. The extent of the class CParcel named EParcel is a container for the oid of parcel objects.

	create interface TParcel
	properties
	attribute integer Parcel#;
	attribute string Owner;
	attribute set(float) Harvests;
	attribute string CropType;
	operations
	void write_owner(in string name);
	string read_owner()...
	create class CParcel of TParcel
	extent EParcel

A class description corresponding to

  The spatial type TPOLYGON is used to model simple polygonal surface without hole and island. The chosen representation for polygons is by vertex.

	attribute integer Parcel#;
	attribute string Owner;
	attribute set(float) Harvests;
	attribute string CropType;
	attribute TSIMPLEPOLYGON Geometry;
	operations
	void write_owner(in string name);
	string read_owner()...
	create type interface TPOLYGON
	/* Ring (simple polygon)*/
	properties
	attribute set(Coordinates) Vertex;
	operations
	float surface;
	boolean intersect_poly(Polygon: TPOLYGON);
	boolean intersect_line(Line: TLINE)
	create interface TParcel
	/* A parcel with its geometry */
	properties

  The states of the objects of the virtual class are defined by applying an expression on the state of existing objects. Furthermore, the state of one or more objects can be aggregated to create virtual objects which do not exist in any component GIS. Instead, they are created or calculated on demand from objects in existing systems. For example, to construct a city map, a user may have to aggregate objects from two sources: a GIS which models road traffic information and a second GIS which contains information on buildings.The following example (figure4) presents the definition of a virtual class for the type TParcel defined above. Two calculated attributes MeanHarvest and Surface are used to define new values from the information contained in the type TParcel. The resulting type, which is a subtype of TParcel, is called TParcelHarvest. CVPArvestHarvest is the created virtual class and EV-ParcelCrop is its extent. Each object of the new virtual class CVParcelHarvest is calculated from an element of the concrete extent EVParcel. The semantic associated with the calculated attribute is applied on the elements of a given class (concrete or virtual). In this case, the virtual class corresponds to a selection operation which restricts the extent of the original class (figure5(a)).The following example presents the definition of a virtual class CVParcelWheat1 for the type TParcel defined above. The extent EVParcelWheat of the virtual class is defined by the select query which is used to set the value of attribute CropType to 'wheat'. EVParcelWheat is calculated from the concrete extent EVParcel.

	Virtual Class	Wrapper w1	Wrapper w2
	i'
		concrete class CParcel1	concrete class CParcel2
		Type TParcel	Type TParcel
	Extent
		Imp	Imp
	Concrete Class
	i
	imp	Ex te nt	Ex te nt
	Extent
	Figure 4: Virtual class with calculated attributes	GIS 1	GIS 2
		Figure 3: Concrete Classes
	tion semantics which must be verified by the elements of the
	new virtual class. We distinguish two cases:	objects; or 2) the extent of one or more concrete classes.
		We distinguish two cases for the definition and creation of a
		virtual class.
		Case 1: restructuring attributes to create a virtual class. A
		virtual class is created by restructuring attributes of exist-
	create virtual class CVParcelWheat1 of TParcel extent EVParcelWheat as select p from p in EVParcel1 where p.CropType='wheat' create virtual class CVAllParcel of TParcel extent EVAllParcels as union(EVParcel, EVParcel)	ing objects. create interface TParcelHarvest :: TParcel
		calculated attribute float MeanHarvest
		calculated attribute float Surface
		create virtual class CVParcelHarvest
		of TParcelHarvest
		as select Parcel#: p.Parcel#, Owner: p.Owner,
		CroptType: p.CropType, Harvest: p.Harvest,
		MeanHarvest: Mean(p.Harvest),
		Surface: surface(p.Geometry)
		from p in ESelf
		/* ESelf describes the extension of the class */
		extent EVParcelCrop as EParcel1
		Case 2: restructuring extents to create a virtual class. The
		definition of a calculated attribute can be a logic expression
		which is used to select the objects contained in the extent of
		a virtual class. The logic expression represents an applica-

Conclusion

We describe ISIS project that is specially design to address issues relevant to the design of distributed interoperable GIS.

We introduce a distributed spatial object model AMUN as an extension of ODMG-93. The main contributions in this paper are the following: concepts to deal with distribution and heterogneties: calculated attributes, extents, concrete and virtual classes; spatial data types to deal with spatial objects; functional extensions to deal with distributed spatial operators. While distribution is addressed with the materialization level, the first two levels (semantic and concrete level) are used to resolve heterogeneities by grouping spatial operation with the same semantic.

We also present the architecture allows sharing of both data and operations. It's major components are: 1) wrappers (one per local GIS) for resolving heterogeneity in the cooperative environment, 2) mediators for coordinating cooperative tasks such as services communications or query dispatching. The main advantage of the architecture is it brings core software components to be used in different contexts and thus it allows flexible and extensible cooperation in different environments such as WEB [START_REF] Bishr | SEMWEB -A Prototype for Seamless Sharing of Geoinformation on The World Wide Web in a Client/Server Architecture[END_REF], federated GIS.

The initial phase of our project is devoted to the definition of the data model. Our future work will focus on spatial query processing to handle the distribution and sharing not only of spatial objects but also of specialized spatial operators.


Mahdi Gueffaz
email: mahdi.gueffaz@u-bourgogne.fr

Sylvain Rampacek
email: sylvain.rampacek@u-bourgogne.fr

Christophe Nicolle
email: christophe.nicolle@u-bourgogne.fr

A new approach based on NµSMV Model to query semantic graph

Keywords: Semantic graph, RDF, Model Checking, Temporal logic, NµSMV, Query checking, SPARQL, temporal logic query

The language most frequently used to represent the semantic graphs is the RDF (W3C standard for meta-modeling). The construction of semantic graphs is a source of numerous errors of interpretation. Processing of large semantic graphs can be a limit to use semantics in modern information systems. The work presented in this paper is part of a new research at the border between two areas: the semantic web and the model checking. For this, we developed a tool, RDF2NµSMV, which converts RDF graphs into NµSMV language. This conversion aims checking the semantic graphs with the model checker NµSMV in order to verify the consistency of the data. The data integration and sharing activities carried on the framework of the Semantic Web lead to large knowledge databases that must be queried, analyzed, and exploited efficiently. Many representation languages of the knowledge of the Semantic Web, starting with RDF, are based on directed, labeled graphs, which can be also manipulated using graph algorithms and tools coming from other domains. In this paper, we propose an analysis approach of RDF graphs by reusing the verification technology developed for concurrent systems. To this purpose, we define a translation from the SPARQL query language into temporal logic query, a general-purpose graph manipulation language implemented in the ScaleSem verification toolbox. This translation makes it possible to extend the expressive power of SPARQL naturally by adding temporal logic formulas characterizing sequences, trees, or general sub-graphs of the RDF graph. Our approach exhibits a performance comparable to dedicated SPARQL query evaluation engines, as illustrated by experiments on large RDF graphs.

Introduction

The increasing development of networks and especially the internet has greatly developed the heterogeneous gap between information systems. In glancing over the studies about interoperability of heterogeneous information systems we discover that all works tend to the resolution of semantic heterogeneity problems. The W3C 1suggest norms to represent the semantic by ontology. Ontology is becoming an inescapable support for information systems interoperability and particularly in the Semantic. Literature now generally agrees on the Gruber's terms to define an ontology: explicit specification of a shared conceptualization of a domain [START_REF] Gruber | Toward principles for the design of ontologies used for knowledge sharing[END_REF]. The physical structure of ontology is a combination of concepts, properties and relationships. This combination is also called a semantic graph.

Several languages have been developed in the context of Semantic Web and most of these languages use XML 2 as syntax [START_REF] Bray | Extensible Markup Language (XML) 1.1[END_REF]. The OWL 3 [START_REF] Bechhofer | OWL Web Ontology Language Reference[END_REF] and RDF 4 [START_REF] Becket | RDF/ XML Syntax Specification (Revised). W3C recommendation[END_REF] are the most important languages of the semantic web, they are based on XML. OWL allows representing the ontology, and it offers large capacity machines performing web content. RDF enhances the ease of automatic processing of Web resources. The RDF (Resource Description Framework) is the first W3C standard for enriching resources on the web with detailed descriptions. The descriptions may be characteristics of resources, such as author or content of a website. These descriptions are metadata. Enriching the Web with metadata allows the development of so-called Semantic Web [START_REF] Berners-Lee | The Semantic Web[END_REF]. The RDF is also used to represent semantic graph corresponding to a specific knowledge modeling. In this paper, we propose a new way using formal verification, which consists in the transformation of semantic graphs into model and verifying them with a Model Checker [START_REF] Clarke | The birth of Model checking[END_REF].

We developed two tools, the first one called "RDF2NµSMV" that transforms semantic graphs into a model represented in NµSMV [START_REF] Cimatti | NuSMV: a new symbolic model checker[END_REF] language. After this transformation, NµSMV verifies the correctness of the model written in NµSMV language with temporal logic in order to verify the consistency of the data described in the model of the huge semantic graphs. The second tool, called "STL RESOLVOR", aims resolving the queries destined to the model of the semantic graph. This query was introduced the first time by William Chan in his innovative work [START_REF] Chan | Temporal-logic queries[END_REF].These requests are not used to verify the model representing the RDF graph, but rather to recognize it.

Our primary goal in this paper is to define a powerful and expressive query language for semantic graphs and to align with SPARQL [START_REF] Chebotko | Semantics preserving SPARQL-to-SQL translation[END_REF], in order to improve the interoperability of applications on the Semantic Web. The other rather competing goal is to keep the query language simple enough that it can be easily built. To satisfy these requirements, we define a new query language that uses the operators of the temporal logic.

The rest of this paper is organized as follows. In Section 2 we present an overview of the semantic graphs, especially the structure of the RDF graphs and the model checking. Then, in section 3, we describe the SPARQL query. The Section 4 presents the temporal logic and the query checking. Section 5 refers to the mapping of the semantic graphs into models, section 6 to the transformation of SPARQL query to temporal logic query. Section 7 defines the functionalities of the STL Resolver tool and we present some benchmarks in section 9. Finally, we end with a conclusion.

An overview of Semantic graphs and Model Checking

Semantic graphs -The RDF is also used to represent semantic graphs corresponding to a specific knowledge modelling. It is a language developed by the W3C to bring a semantic layer to the Web [START_REF] Klyne | Resource Description Framework (rdf): Concepts and abstract syntax[END_REF]. It allows the connection of the Web resources using directed labelled edges. The structure of the RDF documents is a complex directed labelled graph. An RDF document is a set of triples <subject, predicate, object> as shown in the Figure1. In addition, the predicate (also called property) connects the subject (resource) to the object (value). Thus, the subject and the object are nodes of the graph connected by an edge directed from the subject towards the object. The nodes and the edges belong to the "resource" types. A resource is identified by an URI5 [START_REF] Bönström | Storing RDF as a graph[END_REF][START_REF] Berners-Lee | W3C recommendation[END_REF]. The declarations can also be represented as a graph, the nodes as resources and values, and the arcs as properties. The resources are represented in the graph by circles; the properties are represented by directed arcs and the values by a box (a rectangle). Values can be resources if they are described by additional properties. For example, when a value is a resource in another triplet, the value is represented by a circle. The RDF graph in the Figure 2 defines a node "University of Bourgogne" located at "Dijon", having as country "France" and as department "Cote d'Or". RDF documents can be written in various syntaxes, e.g., N3 [START_REF] Berners-Lee | Notation3 (N3): A readable RDF syntax[END_REF], N-Triple [START_REF] Becket | RDF test cases. W3C Working draft[END_REF], and RDF/XML. Below, we present the RDF\XML document corresponding to Figure 2. Model checking -The model checking [START_REF] Katoen | The principal of Model Checking[END_REF] described in Figure 3 is a verification technique that explores all possible system states in a brute-force manner. Similar to a computer chess program that checks all possible moves, a model checker, the software tool that performs the model checking, examines all possible system scenarios in a systematic manner. In this way, it can be shown that a given system model truly satisfies a certain property. Even the subtle errors that remain undiscovered using emulation, testing and simulation can potentially be revealed using model checking.

To make a rigorous verification possible, properties should be described in a precise unambiguous way. It is the temporal logic that is used in order to express these properties. The temporal logic is a form of modal logic that is appropriate to specify relevant properties of the systems. It is basically an extension of traditional propositional logic with operators that refer to the behaviour of systems over time. The following algorithm explains the way that the model checking works. First we put in the stack all the properties expressed in the temporal logic. All of them are verified one by one in the model and if a property does not satisfy the model, it is whether the model or the property that we must refine. In case of a memory overflow, the model must be reduced. Whereas formal verification techniques such as simulation and model checking are based on model description from which all possible system states can be generated, the test, that is a type of verification technique, is even applicable in cases where it is hard or even impossible to obtain a system model.

The SPARQL query

SPARQL [START_REF] Chebotko | Semantics preserving SPARQL-to-SQL translation[END_REF] is a query language for querying metadata and extraction data form an RDF graph or, more precisely a query language for RDF triples.

In SPARQL different query form are available:

 Select: return the value of variables which may be bound by a matching query pattern.

 Ask: return true if a given query matches and false if not.

 Construct: return an RDF graph by substituting the values in given templates.  Describe: return an RDF graph which defines the matching resource.

The Select form is the most used. In this article we showed only the SPARQL query with the select form. A basic SPARQL query has the following form: Select ?variable1, ?variable2,… Where {pattern1.pattern2. …} Where each pattern consists of subject, predicate, object, and each of these is either a variable or a literal. The query model is query-by-example style: the query specifies the known literals and leaves the unknowns as variables. Variables can occur in multiple patterns and thus imply joins. The query processor needs to find all possible variable bindings that satisfy the given patterns and return the bindings from the projection clause to the application. Note that not all variables are necessarily bound (e.g., if a variable only occurs in the projection and not in a pattern), which results in NULL values.

Relational algebra [START_REF] Cyganiak | A relational algebra for SPARQL[END_REF] is introduced to facilitate the mapping of SPARQL query to the applications in temporal logic. We define the operators in RDF relations.

Selection

Selection

, sometimes also called restriction, is an unary operator that selects only those tuples of a relation for which a propositional formula holds. The propositions are assumed to have the expressivity of SPARQL Filter expressions.

Projection

The projection operator ) ( restricts a relation to subset of its attributes.

) (

Inner Join and Left Outer Join

The inner join ( ) joins two relations on their shared attributes. A B contains all combinations of a tuple from A and a tuple from B, minus those where the shared attributes are not equal.

The left outer join ( ) additionally contains all those tuples from the first relation that have no matching tuple in the second.

Union

The union of two relations A and B is the set of union of the tuples of A and B. unlike in regular relational algebra, the headings of A and B do not need to be identical.

Temporal logic and the query checking

The concepts of temporal logic used for the first time by Pnueli [START_REF] Pnueli | The temporal logic of programs[END_REF] in the specification of formal properties are fairly easy to use. The operators are very close in terms of natural language. The formalization in temporal logic is simple enough although this apparent simplicity therefore requires significant expertise. Temporal logic allows representing and reasoning about certain properties of the system, so it is well-suited for the systems verification. There are two main temporal logics, that is linear time and branching time. In linear time temporal logic, each execution of the system is independently analyzed. In this case, a system satisfies a formula f, if f holds along every execution. The branching time combines all possible executions of the system into a single tree. Each path in the tree is a possible representation of the system execution [START_REF] Mukund | Model Checking, Automated Verification of Computational Systems[END_REF].

 Linear Temporal Logic or LTL allow representing the behavior of reactive systems using properties that describe the system in which time proceeds linearly. Clearly, we specify the expected behavior of a system, by specifying the only possible future as a sequence of actions that follow, LTL uses for that temporal operators: X (Next), F (Finally), G (Always), U (Until).

 Computation Tree Logic or CTL suggest several possible futures from a system state rather than having a linear view of the system considered. The operators of CTL are obtained by adding A (for any execution) or E (there is an execution) before the operators of linear temporal logic that are: AX φ (all successor states immediately satisfy φ), EX φ (there is an execution whose next state satisfies φ), AF φ (for any execution, there is a state where φ is true), EF φ (there is an execution, leading to a true state φ), AG φ (for any execution, φ is always true), EG (there is an execution, where φ is always true), AφUψ (for any execution φ is true until ψ is true), EφUψ (there is an execution in which φ is true until ψ is true).

) (



The Model-Checking was proposed as a verification technique, it is valuable for understanding the model: The user formulates a hypothesis of the system behavior, expressed as a formula in temporal logic, and tries to use the Model Checker to validate this hypothesis. This use of the model checking has not been sufficiently emphasized in the literature. So in order to help the user understand the system behavior, Chan [START_REF] Chan | Temporal-logic queries[END_REF] introduced the queries in temporal logic and used a technique similar to the Model-Checking to determine the temporal properties as opposed to simply verifying them.

The query checking is an extension of the Model checking who, instead of asking "does the system satisfy a temporal logic formula ", allows us to ask "for what value of X does the system satisfy ?" Here, X is not a system parameter, but a property setting, that we seek to satisfy. These queries do not allow the verification of a specific property of the model but they allow the examination of the model by questioning it. The technique of query-checking can also be used to provide more information to the user in the Model Checking.

The query checking allows the writing of temporal logic formulas easily and can therefore verify any properties on both the data contained in the graph and the structure of the data.   looks for a subject ?x which has the predicate "Name" and an object "Paul" (?x, name, Paul). The equivalent of the previous query in query using the temporal logic operators is:

Finally ( ?x  Next "Paul") (1)
This temporal logic query looks for the same subject ?x, as defined in the SPARQL query above.

The RDF graph transformation

This section speaks about our approach which consists in the transformation of semantic graphs into model in order to verify them with the model-checker. For this, we developed "RDF2NμSMV" tool that transform semantic graph into NµSMV [START_REF] Cimatti | NuSMV: a new symbolic model checker[END_REF] language for the Model-checker NµSMV.

NµSMV is the amelioration of SMV model checker; it works on the sample principles as SMV. NµSMV verify the properties in both linear time logic and computation tree logic.

The RDF graphs considered here are represented as XML verbose files, in which the information is not stored hierarchically (so-called graph point of view). On the one hand, these RDF graphs are not necessarily connected, meaning they may have no root vertex from which all the other vertices are reachable. On the other hand, the NµSMV language manipulated by the verification tools of NµSMV always have a root vertex, which corresponds to the initial state of the system whose behavior is represented by the NµSMV language. The RDF graph transformation into NµSMV language is articulated in three steps: exploring the RDF graph, determining a root vertex and, final step, generating the Model of the RDF graph. This final step is divided into three sub-steps. The first and the second steps consist in generating two tables (triples table and correspondence table). Firstly, the table of all triples is built by exploring the entire graph. The graph traversal algorithms go through the RDF graph and create a table consisting of resources, properties and values. In the source RDF graph, the resource is a vertex, the property represents the edge and the value is the successor vertex corresponding of the edge of the vertex. The table of triples of RDF graph is useful for the next sub-step.

Secondly, a correspondence table is generated. To build the table of correspondence, the algorithm associates an identifier for each resource, property and value.

The last step consists in producing from these tables the model writing in NµSMV language for the Model checker NµSMV. [START_REF] Gueffaz | Evaluation of semantic graph based on Model Checking[END_REF]

SPARQL query to temporal logic query

This section gives an overview of SPARQL query transformation into Temporal Logic query. We focus on the SELECT form. To illustrate this section, we use the RDF example shown in Figure 5. From the graph in Figure 5, we construct SPARQL queries and their query equivalent in temporal logic. The SPARQL query bellow selects the subject with the variable ?x which has Paul as object.

SPARQL

SELECT ?x WHERE { ?x nom "Paul"} LT query

Finally (?x  Next "Paul")

Relational algebra

The SPARQL query bellow selects the subject ?x which has the variable ?y as object, who, at its turn, has "Bob Dylan" as object.

SPARQL

SELECT ?x WHERE { ?x composed_by ?y. ?y name "Bob Dylan"}

LT query

Finally ( ?x  Next Next "Bob Dylan")

The purpose of an optional pattern is to supplement the solution with additional information. If the pattern within an OPTIONAL clause matches, the variables defined within that pattern are bound to one or to many solutions. If the pattern does not match, the solution remains unchanged. The SPARQL query represented bellow selects the subject ?x that has "Paul" and/or "paul@yahoo.fr" as object.

SPARQL SELECT ?x WHERE { ?x name "Paul" OPTIONAL {?x email paul@yahoo.com"}} LT query Finally ( ?x  Next "Paul" Finally ?x  "paul@yahoo.com")

A SPARQL FILTER function can be added to a basic graph pattern in order to restrict the result according to Boolean conditions. The SPARQL query bellow selects the subject ?x which has a word that contains at least the letter P as object.

SPARQL

SELECT ?x WHERE { ?x name ?y FILTER regex (?y, "P") }

LT query

Finally (?x  Next *P*)

Triples Paul object Name predicate x      ? ? ?    Relational algebra
The SPARQL query bellow selects the subjects ?x and ?y that have "John" and respectively "Paul" as objects.

SPARQL

SELECT ?x ?y WHERE { {?x name "John"} UNION { ?y name "Paul"}} LT query

Finally ( ?x  Next "John" ?y  Next "Paul")

The SPARQL query bellow selects the objects ?x where "name" is the predicate.

SPARQL SELECT ?x WHERE { ?y name ?x } LT query

Finally ( ?y  Next ?x) where predicate=name/ ?x

Relational algebra

The SPARQL query bellow selects the object ?y. This query represents a SPARQL's join.

SPARQL

SELECT ?y WHERE { ?x name ?y. ?z performed_by ?x. ?z composed_by ?p. ?p name "Bob Dylan"} LT query Finally ( ?z  Next Next ?y ?z  Next Next "Bob Dylan") where predicate=nom/ ?y The transformation of SPARQL queries into queries using operators of temporal logic was based on the representation of SPARQL queries in the relational algebra seen above.

The advantage of temporal logic queries is their simplicity to write. That means that the temporal logic is closer to the natural language and in addition, one of the great advantages of the temporal logic queries is that they are more expressive than the SPARQL queries using the temporal logic operators. [START_REF] Mateescu | Extending SPARQL with Temporal logic[END_REF] We developed a tool called "SPARQL2LTQ" which aims to transform SPARQL queries into queries using operators of the temporal logic. For the development of this tool, we use LEX & YACC to decompose the SPARQL query in order to facilitate the processing. LEX is used to recognize the lexical entities and replace them with keywords that will be recognized in the grammar of the language defined in YACC; then YACC will recognize and respect the expressions and will verify if they belong to the grammar. LEX & YACC are two very powerful tools, facilitating the lexical and respectively the syntactic analysis, which represent two stages of compilation difficult to program.

In order to demonstrate the usefulness of temporal logic queries we will illustrate an example. Here are two tables in a relational database, table 1 andtable 2 To answer this SPARQL query we must first make a join between the two previous relational database tables. A join is used for joining two multi sets with a constraint. In our example the constraint is the name, see table 3 bellow. The equivalent of the previous SPARQL query in a query using operators of the temporal logic is as follows:

Finally (id  X X ?x)

In this query, in order to retrieve the age of the person identified by id1, one just moves two states (two "next" operators in our query represented by X) in the semantic graph model to find the result, as shown in Figure 7.

For results with temporal logic query one just moves around the graph with the operators of temporal logic. The new interrogation technique will allow us to avoid scanning the graph several times as with SPARQL queries.

The STL Resolver

The ScaleSem toolbox contains a tool used to resolve queries in temporal logic that we have previously seen. This tool is called STL RESOLVOR, it takes as input the temporal logic query and the NμSMV graph representing the semantic graph.

The query checking is an extension of the Model checking. A temporal logic query is a formula with a missing propositional formula, designated by a placeholder ("?"). A solution to a temporal logic query is the set of all propositional formulas that satisfy the query, in our case the formula are the states represented in the NµSMV graph. The table above gives some example of temporal logic queries and their results.

Benchmark

We tested several RDF graphs on our tool "RDF2NµSMV", using a machine that runs on a processor with a capacity of 2.4 GHz and 4 GB of RAM, calculating the time of conversion as shown in Figure 9. Note that the RDF2NµSMV tool is faster in converting semantic graphs. We have almost 22 seconds for a graph of 53 MB size. The transformation tool follows a polynomial curve. In Figure 10, we see the size of the converted semantic graphs from RDF to NµSMV language. We calculate the time of transformation of the SPRAQL query into a query using the operators of the temporal logic with the SPARQL2TLQ tool. The graph of the Figure 11 shows that for 50 000 queries, we have over then 2 minutes and for 100 000 queries, we have 17 minutes. This transformation follows a polynomial curve. In Figure 12, we notice that the size of the queries in temporal logic is smaller than the size of the equivalent SPARQL queries.

Conclusion

This paper presents how to transform a semantic graph into a model for verification by using a powerful formal method, that is the "model checking". Knowing that the model checker does not understand the semantic graphs, we developed a tool called "RDF2NµSMV" to convert them into NµSMV graph in order to be verified with the temporal logics. This transformation is made for the purpose of classifying large semantic graphs in order to verify the consistency of the data from a different ontology. We notice the advantage of NµSMV, whose verification can be made with both linear time logic and computation tree logic formulas.

We also introduce a new tool called "STL RESOLVOR" that is used to find the solution of temporal logic queries to better know the model used by the model checker NµSMV.

We continue our research, understanding the SPARQL queries and trying to convert them into queries using the operators of the temporal logic. The goal of this transformation is to study a new way of expressing a new possibility to explore the semantic graphs.

Figure 1 .

 1 Figure 1. RDF triplet.

Figure 2 .

 2 Figure 2. Example of a partial RDF graph.

  <rdf:Description rdf:about="http://example.org/university of Bourgogne"> <ex:Location> <rdf:Description rdf:about="http://example.org/Dijon"> <ex:Country> France</ex:Country> <ex:Department>Cote d'or</ex:Department> <

Figure 3 .

 3 Figure 3. Model checking approach

Figure 4 .

 4 Figure 4. The query execution time. In the graph of the Figure 4, we can see that there are two RDF triples (B1, name, Paul) and (B1, Phone, 111-111). The following SPARQL query: SELECT ?x WHERE { ?x Name "Paul"} whose representation in relational algebra is: Triples

Figure 5 .

 5 Figure 5. RDF graph for SPARQL query.

Figure 6 .

 6 Figure 6. The architecture of the transformation tool "SPARQL2RLT".

Figure 7 .

 7 Figure 7. The RDF graph model showing the movement to be done to achieve results.

Figure 8 .

 8 Figure 8. An example of NµSMV graph.

Figure 9 .

 9 Figure 9. Time conversion of semantic graphs.

Figure 10 .

 10 Figure 10. Size of the models.

Figure 11 .

 11 Figure 11. Time conversion of SPARQL query.

Figure 12 .

 12 Figure 12. Comparison of size in both SPARQL query and temporal logic query.

Table 1

 1 .

Table 2

 2

	Person Name	Name	Age
	id1	Alice	Alice	33
	id3	Christophe	Bob	42
	id2	Bob	Christophe 15
	SELECT ?x
	WHERE {
	id1 ex :Name ?z
	?z ex :HasAge ?x
	}
	The SPARQL query above seeks the age of the person identified by id1,
	corresponding to "Alice" in our case.

TABLE 3

 3

	Person Name	Age
	1	Alice	33
	2	Bob	42
	3	Christophe	15

TABLE 4

 4

		Query	Result
	1	Finally (?x  X State 3)	?x ={State 1, State 2}
	2	Finally (?x  X X state 3)	?x={State 1}

World Wide Web Consortium

eXtensible Markup Language

Web Ontology Language

Resource Description Framework

Uniform Resource Identifier Ressource Property Value http://example.org/University_of_Bourgogne http://example.org/Dijon http://example.org/Cote_d'or http://example.org/France http://example.org/Location http://example.org/Country http://example.org/Department


Mahdi Gueffaz
email: mahdi.gueffaz@u-bourgogne.fr

Sylvain Rampacek
email: sylvain.rampacek@u-bourgogne.fr

Christophe Nicolle
email: christophe.nicolle@u-bourgogne.fr

RDF2SPIN: Mapping Semantic graphs to SPIN Model Checker

Keywords: Semantic graph, RDF, Model-Checking, Temporal logic, SPIN, IFC, BIM

The most frequently used language to represent the semantic graphs is the RDF (W3C standard for meta-modeling). The construction of semantic graphs is a source of numerous errors of interpretation. The processing of large semantic graphs is a limit to the use of semantics in current information systems. The work presented in this paper is part of a new research at the border between two areas: the semantic web and the model checking. For this, we developed a tool, RDF2SPIN, which converts RDF graphs into SPIN language. This conversion aims checking the semantic graphs with the model checker SPIN in order to verify the consistency of the data. To illustrate our proposal we used RDF graphs derived from IFC files. These files represent digital 3D building model. Our final goal is to check the consistency of the IFC files that are made from a cooperation of heterogeneous information sources.

Introduction

The increasing development of networks and especially the internet has greatly developed the heterogeneous gap between information systems. In glancing over the studies about interoperability of heterogeneous information systems we discover that all works tend to the resolution of semantic heterogeneity problems. Now, the W3C 1 suggest norms to represent the semantic by ontology. Ontology is becoming an inescapable support for information systems interoperability and particularly in the Semantic. Literature now generally agrees on the Gruber's terms to define an ontology: explicit specification of a shared conceptualization of a domain [START_REF] Gruber | Toward principles for the design of ontologies used for knowledge sharing[END_REF]. The physical structure of ontology is a combination of concepts, properties and relationships. This combination is also called a semantic graph.

Several languages have been developed in the context of Semantic Web and most of these languages use XML 2 as syntax [START_REF] Bray | Extensible Markup Language (XML) 1.1[END_REF]. The OWL 3 [START_REF] Bechhofer | OWL Web Ontology Language Reference[END_REF] and RDF 4 [START_REF] Becket | RDF/ XML Syntax Specification (Revised). W3C recommendation[END_REF] are the most 1 World Wide Web Consortium 2 eXtensible Markup Language 3 Web Ontology Language important languages of the semantic web, they are based on XML. OWL allows representing the ontology, and it offers large capacity machines performing web content. RDF enhances the ease of automatic processing of Web resources. The RDF (Resource Description Framework) is the first W3C standard for enriching resources on the web with detailed descriptions. The descriptions may be characteristics of resources, such as author or content of a website. These descriptions are metadata. Enriching the Web with metadata allows the development of so-called Semantic Web [START_REF] Berners-Lee | The Semantic Web[END_REF]. The RDF is also used to represent semantic graph corresponding to a specific knowledge modeling. For example in the AEC 5 projects, some papers used RDF to model knowledge from heterogeneous sources (electricians, plumbers, architects…). In this domain, some models are developed providing a common syntax to represent building objects. The most recent is the IFC 6 [START_REF]Industrial Foundation classes, International Alliance for interoperability[END_REF] model developed by the International Alliance of Interoperability. The IFC model is a new type of BIM 7 and requires tools to check the consistency of the heterogeneous data and the impact of the addition of new objects into the building.

As the IFC graphs have a large size, their checking, handling and inspections are a very delicate task. In [START_REF] Vanland | IFC and Buildings Lifecycle Management[END_REF] we have presented a conversion from IFC to RDF. In this paper, we propose a new way using formal verification, which consists in the transformation of semantic graphs into a model and verifying them with a model checker. We developed a tool called "RDF2SPIN" that transforms semantic graphs into a model represented in SPIN [START_REF] Ben-Ari | Principles of the SPIN Model Checker[END_REF] language. After this transformation, SPIN verifies the correctness of the model written in PROMELA 8 language with temporal logic in order to verify the consistency of the data described in the model of the huge semantic graphs.

The rest of this paper is organized as follows. In Section 2 we present an overview of the semantic graphs, especially the structure of the RDF graphs and the model checking. Then, in section 3, we describe the mapping of the semantic graphs into models and our approach is defined in section 4. Finally, we end with the conclusion.

An overview of Semantic graph and Model Checking

The RDF is also used to represent semantic graphs corresponding to a specific knowledge modeling. It is a language developed by the W3C to bring a semantic layer to the Web [START_REF] Klyne | Resource Description Framework (rdf): Concepts and abstract syntax[END_REF]. It allows the connection of the Web resources using directed labeled edges. The structure of the RDF documents is a complex directed labeled graph. An RDF document is a set of triples <subject, predicate, object> as shown in the Figure 1. In addition, the predicate (also called property) connects the subject (resource) to the object (value). Thus, the subject and the object are nodes of the graph connected by an 4 Resource Description Framework 5 Architecture Engineering Construction 6 Industrial Foundation Classes 7 Building Information Model 8 Process Meta Language edge directed from the subject towards the object. The nodes and the edges belong to the "resource" types. A resource is identified by an URI 9 [START_REF] Bönström | Storing RDF as a graph[END_REF][START_REF] Berners-Lee | W3C recommandation[END_REF]. The declarations can also be represented as a graph, the nodes as resources and values, and the arcs as properties. The resources are represented in the graph by circles; the properties are represented by directed arcs and the values by a box (a rectangle). Values can be resources if they are described by additional properties. For example, when a value is a resource in another triplet, the value is represented by a circle. The RDF graph in the Figure 2 defines a node "University of Bourgogne" located at "Dijon", having as country "France" and as department "Cote d'Or". RDF documents can be written in various syntaxes, e.g., N3 [START_REF] Berners-Lee | Notation3 (N3): A readable RDF syntax[END_REF], N-Triple [START_REF] Becket | RDF test cases. W3C Working draft[END_REF], and RDF/XML. Below, we present the RDF\XML document corresponding to Figure 2. The model checking [START_REF] Katoen | The principal of Model Checking[END_REF] described in Figure 3 is a verification technique that explores all possible system states in a brute-force manner. Similar to a computer chess program that checks all possible moves, a model checker, the software tool that performs the model checking, examines all possible system scenarios in a systematic manner. In this way, it can be shown that a given system model truly satisfies a certain property. Even the subtle errors that remain undiscovered using emulation, testing and simulation can potentially be revealed using model checking.

To make a rigorous verification possible, properties should be described in a precise unambiguous way. It is the temporal logic that is used in order to express these properties. The temporal logic is a form of modal logic that is appropriate to specify relevant properties of the systems. It is basically an extension of traditional propositional logic with operators that refer to the behavior of systems over time. The following algorithm explains the way that the model checking works. First we put in the stack all the properties expressed in the temporal logic. All of them are verified one by one in the model and if a property does not satisfy the model, it is whether the model or the property that we must refine. In case of a memory overflow, the model must be reduced. Whereas formal verification techniques such as simulation and model checking are based on model description from which all possible system states can be generated, the test, that is a type of verification technique, is even applicable in cases where it is hard or even impossible to obtain a system model.

The mapping

This section speaks about our approach which consists in the transformation of semantic graphs into model in order to verify them with the model-checker. For this, we developed "RDF2SPIN" tool that transform semantic graph into PROMELA [START_REF] Ben-Ari | Principles of the SPIN Model Checker[END_REF] language for the Model-checker SPIN.

The RDF graphs considered here are represented as XML verbose files, in which the information is not stored hierarchically (so-called graph point of view). On the one hand, these RDF graphs are not necessarily connected, meaning they may have no root vertex from which all the other vertices are reachable. On the other hand, the NµSMV language manipulated by the verification tools of NµSMV always have a root vertex, which corresponds to the initial state of the system whose behavior is represented by the NµSMV language. The RDF graph transformation into NµSMV language is articulated in three steps: exploring the RDF graph, determining a root vertex and, final step, generating the Model of the RDF graph. The third step is divided into three sub-steps. First and second one consists in generating two tables (triplets table and resources and values table). The last one consists in producing PROMELA language.

Table of triplets -Going through the RDF graph by graph traversal algorithms, we will create a table consisting of resources, properties and values. In our RDF graph, the resource is a vertex, the property represents the edge and the value is the successor vertex corresponding of the edge of the vertex. The table of triples of RDF graph is useful for the next step to create the table of resources and values.

Table of resources and values -Browsing the table triples seen in the previous step, we attribute for each resource and for each value a unique function. These functions are proctype type. We combine all these functions in a table called table of resource and values as you can see in the example in section 3.4.

PROMELA language -In this last step, we will write the PROMELA file corresponding to the RDF graph that we want to check. For this step, we will start by writing the function of the main root of the graph and for each property of the root, we call the function of the corresponding value. We will do the same for all "resource" functions defined in the table resources and values. In the other ones, all the function "value" we'll just display their contents. [START_REF] Gueffaz | Evaluation of Semantic graph based on Model Checking[END_REF]

The verification with the Model Checker

As we saw in section 2, the model checker needs properties in order to check the model of semantic graphs. These properties are expressed in temporal logic. The concepts of temporal logic used for the first time by Pnueli [START_REF] Pnueli | The temporal logic of programs[END_REF] in the specification of formal properties are fairly easy to use. The operators are very close in terms of natural language. The formalization in temporal logic is simple enough although this apparent simplicity therefore requires significant expertise. Temporal logic allows representing and reasoning about certain properties of the system, so it is well-suited for the systems verification. There are two main temporal logics, that is linear time and branching time. In linear time temporal logic, each execution of the system is independently analysed. In this case, a system satisfies a formula f, if f holds along every execution. The branching time combines all possible executions of the system into a single tree. Each path in the tree is a possible representation of the system execution.

This section details our approach which consists in transforming semantic graphs into models in order to be verified by the model-checker. For this, we have developed a tool called "RDF2SPIN" that transforms semantic graphs into SPIN language. The architecture of the Figure 4 is divided into two phases. The first phase concerns the transformation of the semantic graph into a model using our tool "RDF2SPIN", as described in section 3. The second phase concerns the verification of the properties expressed in temporal logic on the model using the model-checker SPIN.

To illustrate our approach, we take an RDF graph represented in the Figure 5 and a temporal logic expressed in the table 1 to verify if the BIM "b1" contains a floor. We tested several RDF graphs on our tool "RDF2SPIN", graphs representing buildings as shown in Figure 6, using a machine that runs on a processor with a capacity of 2.4 GHz and 4 GB of RAM, calculating the time of conversion as shown in Figure 7. Note that the RDF2SPIN tool is faster in converting semantic graphs. We have almost 12 seconds for a graph of 53 MB size. The transformation tool follows a polynomial curve.

Conclusion

This paper presents how to transform a semantic graph into a model for verification by using a powerful formal method, that is the "model checking". Knowing that the model-checker does not understand the semantic graphs, we developed a tool RDF2SPIN to convert them into SPIN language in order to be verified with the temporal logics. This transformation is made for the purpose of classifying large semantic graphs in order to verify the consistency of IFC files representing 3D building.

Figure 1 .

 1 Figure 1. RDF triplet.

Figure 2 .

 2 Figure 2. Example of a partial RDF graph.

  <rdf:Description rdf:about="http://example.org/university of Bourgogne"> <ex:Location> <rdf:Description rdf:about="http://example.org/Dijon"> <ex:Country> France</ex:Country> <ex:Department>Cote d'or</ex:Department> </rdf:Description> </ex:Location> </rdf:Description>

Figure 3 .

 3 Figure 3. Model Checking approach

Figure 4 .

 4 Figure 4. Our architecture.

Figure 5 .

 5 Figure 5. Example of partial RDF graph.

Figure 6 .

 6 Figure 6. The 3D view of an IFC file.

Figure 7 .

 7 Figure 7. Time conversion of semantic graphs.

TABLE 1 .

 1 Temporal logic formula.

	Temporal logic	Meaning	Result
	Eventually (b1 	Is there a floor after two states starting from the state b1	True
	Next Next floor )


Mahdi Gueffaz
email: mahdi.gueffaz@u-bourgogne.fr

Sylvain Rampacek
email: sylvain.rampacek@u-bourgogne.fr

Christophe Nicolle
email: cnicolle@u-bourgogne.fr

SCALESEM : Evaluation of Semantic Graph based on Model Checking

Keywords: Semantic graph, Model-checking, Temporal logic

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

INTRODUCTION

W3C 1 aims to standardize the representation and the exchange of information on the WEB. This objective should help make the information understandable for both automated processes and users. The homogenization of computer exchanges took place due to the introduction of the XML [START_REF] Bray | Extensible Markup Language (XML) 1.1[END_REF] standard. This standard has enabled the program to manipulate information through languages with hierarchical structure mark-up defined by grammars derived from the XML standard. However, this effort has not helped improve the user's understanding of information. Thus, new standards have been developed to enable the semantic representation of information in the form of XML-derived languages. This base is called Semantic Web standards and it is usually represented as a stack of languages ranging from automatic processes oriented languages to languages representing more abstract concepts of formal semantics [START_REF] Berners-Lee | The Semantic Web[END_REF]. These languages are used to represent the semantics associated with information, whatever its form and structure. To allow the construction of semantic graph, many tools have been developed like Annotea [START_REF] Kahan | Annotea: An Open RDF Infrastructure for Shared Web Annotations[END_REF] which is a project of the W3C that specifies 1 World Wide Web Consortium.

the infrastructure for the annotation of Web documents. The main format used in the annotation is RDF and the types of documents can be annotated are HTML documents or XML based. However, none provides the functionality to verify the consistency of semantics, and reduce errors annotations.

This paper proposes a new way to check these semantic graphs by model-checking in order to reduce errors in annotation and make the data more relevant. Model checking is an automatic verification technique, it has been applied to many cases in industry, for example [START_REF] Katoen | The principal of Model Checking[END_REF], in the Netherlands, model-checking has revealed several serious flaws in the design of control system of a barrier protection against flooding which protects the main port of Rotterdam against floods.

Model checking is a powerful tool for system verification because it can reveal errors that were not discovered by other formal methods such as testing or simulation. Model checking uses temporal logic to describe the properties checking the system model.

MODEL-CHECKING AND TEMPORAL LOGIC OVERVIEW

Formal methods [START_REF] Katoen | The principal of Model Checking[END_REF] offer great potential for an early inclusion of verification in the design process, providing technical audit more efficiently and reduce the verification time. Formal methods are highly recommended techniques for the development of software. Two types of formal verification methods can be distinguished: methods based on the proof of the theorem and the methods based on models.

The model checker examines all relevant system states in order to check whether they satisfy the desired property. The model checker gives a counter example that indicates how the model can violate the property. With a help of a simulator, the user can locate the error and adapt the model or the property to prevent the violation of property (Fig. 1). The concepts of temporal logic used for the first time by Pnueli [START_REF] Pnueli | The temporal logic of programs[END_REF] in the specification of formal properties are fairly easy to use. The operators are very close in terms of natural language. The formalization in temporal logic is simple enough although this apparent simplicity therefore requires significant expertise. Temporal logic allows representing and reasoning about certain properties of the system, so it is well-suited for the systems verification.

THE SCALESEM APPROACH

We use SPIN (Ben-Ari, 2008) and NµSMV [START_REF] Cimatti | NuSMV: a new symbolic model checker[END_REF] as model checkers to check the model of semantic graphs. SPIN is a software tool for verifying system models. The system is described in a language model called PROMELA. NµSMV is the amelioration of SMV model checker, working on the same simple principles as SMV. In Fig. 2, we present the architecture of our approach. In this architecture, from a natural language description, we can get the semantic graph (RDF2 ) and its description in temporal logic, as shown in the example found in the section VII. We divide this architecture in two phases. The first phase concerns the transformation of the semantic graph into a model using our tools RDF2SPIN and RDF2NμSMV. There are three steps in this transformation. The first step is to explore the entire RDF graph to obtain the triplets table. The second step is to determine a root for the graph, and the last step is to write the model that represents the semantic graph in the PROMELA or NµSMV languages. The second phase concerns the verification of properties expressed in temporal logic on the model using the model-checker SPIN or NµSMV.

Introducing RDF

RDF is a language developed by the W3C to bring a semantic layer to the Web [START_REF] Becket | RDF/ XML Syntax Specification (Revised). W3C recommandation[END_REF]. It allows the connection of Web resources using directed labelled edges. The structure of RDF documents is a complex labelled directed graph. An RDF document is a set of triples <subject, predicate, object>. These RDF graphs are not necessarily connected, meaning they may have no root vertex from which all the other vertices are reachable.

Exploring RDF Graph

We achieve this by appropriate explorations of the RDF graphs, as explained below. Let us consider that an RDF graph is represented as a couple (V, E), where V is the set of vertices and VxV E  is the set of edges. For a vertex x, we note

Figure 1 :

 1 Figure 1: Model Checking Approach.

Figure 2 :

 2 Figure 2: The Scalesem Architecture.

Resource Description Framework WEBIST 2011 -7th International Conference on Web Information Systems and Technologies

the set of its successor vertices. We use depth-first search algorithm, illustrated below to explore graph, knowing that the breadth-first algorithm also works in this context.

Determining a Root Vertex

If the RDF graph has no vertex root, we must create a root for the graph. The first phase explores the graph until it is fully explored, and inserts in root_list all vertices that have no predecessor. If root_list contains a single vertex, so overall it is the global root of the graph since all the other vertex are accessible from it and it is useless to the second phase has passed. Otherwise, any vertex contained in root_list could also be a root of the graph: the role of the second phase is to determine which of the partial root the root of the global graph is.

The second phase performs a new wave of exploration of the roots contained in partial root_list in reverse order in which they were inserted in the list. If a root in root_list is to be visited by a partial root, it is removed from the list because it is not a partial root. At the end of this phase, all partial roots of the graph are present in root_list. Indeed, each vertex is unreachable from the partial roots which were explored during the second phase. A new root is created (see Fig. 3), having as successor all the partial roots of root_list, which ensures that all vertices of the graph are accessible from the new root. Therefore, such a summit is inaccessible from other nodes of the graph.

Generating the Model

The third step is divided into three sub-steps. The first and the second one consist in generating two tables (triplets table and resources and values table ). The last one consists in producing the model writing in PROMELA language for SPIN and in NµSMV language for NµSMV.

EXAMPLE AND BENCHMARK

To illustrate our approach, we take the natural language description as follows:

Ninety-three is a novel by Victor Hugo published in 1874, whose theme is the French Revolution. Victor Hugo was born in February 26, 1802 in Besançon. From the description above, we can easily extract simple propositions, see Table 1. Table 2 presents the RDF triples derived from the Table 1.

Table 1: Short list of simple propositions.

1

"Ninety-three is a novel" 2 "Ninety-three its author is Victor Hugo" 3 "Ninety-three has been published in 1874" 4 "Ninety-three's theme is the French revolution" 5 "Victor Hugo was born in February 26, 1802" 6 "Victor Hugo was born in Besançon" From the previous description in natural language, we can express it in temporal logic as shown in Table 3. We check that ninety three is a novel 2 Always (Ninety-three  next Victor Hugo)

We check that ninety three is written by Victor Hugo Now, we will be able to transform the RDF graph in Fig. 3 with our tools "RDF2SPIN" and RDF2NμSMV" into a model in order to check each formula of temporal logic described in Table 3 and see if each formula is verified or not in the model.

CONCLUSIONS

This paper presents a new technique for the semantic graphs verification by using a model-checker. Knowing that the model-checker does not understand the semantic graphs, we developed two tools RDF2SPIN and RDF2NµSMV to convert them into PROMELA and NµSMV languages in order to be verified with the temporal logics.

In future work, we would like to convert the SPARQL query language for RDF graphs into queries using the operator of the temporal logic, to have a better verification of RDF graphs representing the building industry.