Mounira Kezadri Hamiaz

Marc Pantel

Benoit Combemale

Xavier Thirioux

A formal framework to prove the correctness of model driven engineering composition operators

Current trends in system engineering combine modeling, composition and verification technologies in order to harness their ever growing complexity. Each composition operator dedicated to a different modeling concern should be proven to be property preserving at assembly time. These proofs are usually burdensome with repetitive aspects. Our work 3 targets the factorisation of these aspects relying on primitive generic composition operators used to express more sophisticated language specific ones. These operators are defined for languages expressed with OMG MOF metamodeling technologies. The proofs are done with the Coq proof assistant relying on the Coq4MDE framework defined previously. These basic operators, Union and Substitution, are illustrated using the MOF Package Merge as a composition operator and the preservation of model conformance as a verified property.

Introduction and motivation

Safety critical systems are getting more and more complex and software intensive while the safety rules are more and more stringent (e.g. DO-178 in aeronautics [START_REF] Rtca / Eurocae | Software Considerations in Airborne Systems and Equipment Certification[END_REF]). Several technologies are playing a key role to tackle these issues.

First, Model-Based Systems Engineering (MBSE) relying on Model Driven Engineering (MDE) [START_REF] Bézivin | In search of a basic principle for model driven engineering[END_REF] promotes the use of models at the various development phases, composition operators and model transformations to automate parts of the development. Models are abstract specifications of the various system concerns/aspects that are usually purpose oriented and allow early Validation and Verification (V & V) (e.g. the new DO-331 standard [START_REF] Rtca / Eurocae | Model-Based Development and Verification Supplement to DO-178C [ED-12C[END_REF]).

Then, formal methods allow the assessment of the completeness and consistency of specification models, and of the correctness of design models and implementations with respect to specification models. Their mathematical nature provides high level of confidence in their result (e.g. the new DO-333 standard [START_REF] Rtca / Eurocae | Formal Methods Supplement to DO-178C [ED-12C[END_REF]).

In order to benefit from these technologies and avoid doing all the V & V activities on the final system, safety standards require the associated process, methods and tools to be qualified (e.g. the new DO-330 standard: Software Tool Qualification Considerations that adapts the DO-178C to the development and the verification tools [START_REF]Software Tool Qualification Considerations" -clarifying software tools and avionics tool qualification[END_REF]). These qualification activities are very costly and can benefit from the use of formal methods relying on the DO-333 standard [START_REF] Rtca / Eurocae | Formal Methods Supplement to DO-178C [ED-12C[END_REF].

To ease the integration of formal specification and verification technologies, some of the authors proposed in [START_REF] Thirioux | A Framework to Formalise the MDE Foundations[END_REF] a formal embedding of some key aspects of MDE in Set Theory. This embedding was then implemented using the Calculus of Inductive Construction [START_REF] Coquand | The calculus of constructions[END_REF] and the Coq4 proof-assistant. This framework called Coq4MDE5 provides sound mathematical foundations for the study and the validation of MDE technologies. The choice of constructive logic with type theory as formal specification language allows to extract prototype tools from the executable specification that can be used to validate the specification itself with respect to external tools implementing the MDE principles (for example, in the Eclipse 6 Modeling Project).

We proposed in [START_REF] Kezadri | A proof assistant based formalization of components in MDE[END_REF] an extension of Coq4MDE to support the Invasive Software Composition (ISC) [START_REF] Aßmann | Invasive software composition[END_REF] style. We then experimented the design of formalized primitive operators and their use to ease the implementation, and especially the proof of correctness of the ISC operators and other high level ones. This contribution specifies and assesses the properties of the primitive composition operators Union and Substitution that can be used to specify higher level composition operators sharing parts of their implementation and associated properties. The assessed property is the conformance of models to metamodels which is mandatory for all model composition operators. Our proposal is illustrated by the use of these primitive operators to specify and prove the MOF (Meta Object Facility) [START_REF]Meta Object Facility (MOF) 2.4.2 Core Specification[END_REF] Package Merge. Other sophisticated composition operators like ISC (adaptation and glueing) [START_REF] Aßmann | Invasive software composition[END_REF] [20] and aspect weaving [START_REF] Morin | A generic weaver for supporting product lines[END_REF] can also be built from these primitive ones, and their proofs of conformance preservation are also built from the ones of primitive operators. One key point is the use of property specific contracts (pre and post conditions) for the composition operators in order to ensure compositional verification.

This contribution is structured as follows. First, the concepts and an example for a targeted high level operator and the expected properties are given in Section 2. Then, Section 3 presents the formal support for the Coq4MDE framework that is extended to handle the definition of the primitive composition operators associated with the proofs of property preservation. Then, some use cases are provided in Section 4. Related work are given in Section 5. Finally, conclusion and perspectives are provided in Section 6.

Use case : MOF Package Merge

This section introduces our verification proposal applied to the MOF Package Merge operator.

Model Driven Engineering

The core principle of MDE is "everything is a model" [START_REF] Bézivin | In search of a basic principle for model driven engineering[END_REF]. Models are defined using modeling languages. Metamodels are models of modeling languages defined using metamodeling languages. A model M is conforming to a metamodel M M if M M models the language used to define M . Metamodels, like data types, define the structure common to all its conforming models, but can also give semantics properties like dependent types. Derived from [START_REF] Jouault | Km3: A dsl for metamodel specification[END_REF], Coq4MDE separates the model level (value or object) from the metamodel level (type or class), and describes them in Coq with different types.

Meta-Object Facility

The OMG has standardized the MOF, that provides a reflexive metamodeling language (i.e. MOF is defined as a model in the MOF language). MOF is used for the specification of the OMG modeling language standards like MOF itself, UML [START_REF] Omg | Unified modeling language (omg uml)-infrastructure(v2.4.1)[END_REF], OCL [START_REF] Warmer | The object constraint language: getting your models ready for MDA[END_REF], SysML [START_REF] Holt | SysML for systems engineering[END_REF] and many others. The relation between MOF and the metamodels is the same as the one between a metamodel and its conforming models. Based on these principles, the OMG introduced the MDA (Model Driven Architecture) [START_REF] Bernstein | A vision for management of complex models[END_REF] view of software modeling illustrated by the pyramid given in Figure 2. Since the MOF version released in 2006 [START_REF]Meta Object Facility (MOF) 2.0 Core Specification[END_REF], a kernel named EMOF was extracted from the complete version of MOF (CMOF). EMOF provides a minimal set of elements required to model languages. Figure 1 gives the key concepts of EMOF specified as an UML class diagram. The principal concept is Class to define classes (usually called metaclasses) that represent concepts in a modeling language. Classes allow to create objects in models. The type of an object is the class that was used to create it. Classes are composed of an arbitrary number of Property (we will call them reference and attribute in order to avoid ambiguities with the model property we want to assess) and Operation (not detailled here). References allow to create the relations between the objects in the models. Classes can inherit references and attributes from other classes. Inheritance is expressed using the superClass reference from Class. Inheritance introduces a subtyping relation between the types associated to classes. Classes can be abstract (isAbstract): no object can have the type associated to an abstract class as smallest type according to the subtyping relation. Property has a lower and upper attributes that bound the number of objects contained in a given reference. Two references can be opposite to build a bidirectional relation between objects in a model.

In MBSE, many models are used to represent the various system's concerns. They must be composed to build the global system. We present in the following subsection the MOF composition operator that is used in the OMG UML specification [START_REF] Omg | Unified modeling language (omg uml)-infrastructure(v2.4.1)[END_REF] to define and assemble metamodel parts.

MOF Package Merge

Package Merge is a directed relation from a package (merged) to another package (receiving) as mentioned in Figure 3. It can be seen as an operation that takes the content of both packages and produces a new package (resulting) that merges the contents of the initial packages. In the case where some elements in these packages represent the same entity, theirs contents must be combined according to the rules given in [START_REF] Omg | Unified modeling language (omg uml)-infrastructure(v2.4.1)[END_REF]. When there are no conflicts between the two packages, Package Merge is equivalent to an union for all the packages elements (in fact, a special union that preserves the references and attributes for classes).

When conflicts occur, two major kinds are considered: a) when the same class has different attributes and references in the two packages, this conflict is resolved by keeping all the attributes and references from both classes in the merged and receiving models (this is obviously an application of the previous special union operator), b) when two corresponding attributes or references have different values (for example different multiplicity values); the conflicts are resolved by combining the values according to the semantics of the conflicting attribute or reference.

Expected property

The expected property in this use case is the preservation of the metamodel conformance during composition. For a model M and a metamodel M M , this property checks that: 1) every object o in M was created from a class C in M M . 2) every relation between two objects in M is such that there exists, in M M , a reference between the two classes used for creating the two objects. 3) every semantics property defined in M M is satisfied in M . The semantics properties from EMOF (see Figure 1) are: Inheritance (subClass), Abstract classes (isAbstract), Multiplicities (lower, upper), Opposite (isOpposite) and Composite (areComposite) references.

As verifying these properties directly for the MOF Package Merge operator is complex and contains many common aspects with other high level composition operators, we target a divide and conquer approach to capture these commonalities.

Verification strategy

We advocate the use of generic primitive composition operators that are then used to specify and prove more sophisticated ones like MOF Package Merge or ISC. We target pragmatic compositional verification: minimize the residual verification that must be conducted on the result of the composition of correct models. We rely on a simple methodology to design the contract (pre and post conditions) for the composition operators in that purpose. If Φ is the expected property for a model built using composition operators, then Φ must be, on the one hand, the postcondition on the model resulting from the application of each operator; and, on the other hand, the weakest precondition on each parameter of each operator. These preconditions are eventually consolidated with an additional glueing property Ψ depending on the value of all the parameters of the operator. Ψ is the residual property that must be checked at each composition.

Definition 1 (Correct composition operator). For a set of models m 1 , . . . , m n and an n-ary composition operator f over models, we say f is correct (or property preserving) with respect to a property Φ and a glueing condition

Ψ if: 1≤i≤n Φ(m i ) ∧ Ψ (m 1 , . . . , m n ) ⇒ Φ(f (m 1 , . . . , m n ))
The verification that the composition operators are correct will be conducted using the Coq proof assistant, the details are presented in the next Section.

Formalization using Coq4MDE

The concepts of Model and Metamodel are formally defined in Coq4MDE in the following way. Let us consider two sets of labels: Classes, respectively References, represents the set of all possible classes, respectively reference, labels. Then, let us consider instances of such classes, the set Objects of object labels. References includes a specific inh label used to specify the direct inheritance relation.

Definition 2 (Model). Let C ⊆ Classes be a set of class labels. Let R ⊆ { c 1 , r, c 2 | c 1 , c 2 ∈ C , r ∈ References} 7 be a set of references between classes.
A Model over C and R, written M V, M E ∈ M odel(C , R) is a multigraph built over a finite set M V of typed object vertices and a finite set M E 8 of reference edges. such that:

M V ⊆ { o, c | o ∈ Objects, c ∈ C } M E ⊆ o 1 , c 1 , r, o 2 , c 2 o 1 , c 1 , o 2 , c 2 ∈ M V, c 1 , r, c 2 ∈ R
In case of inheritance, the same object label will be used several times in the same model graph. It will be associated to the different classes in the inheritance hierarchy going from a root down to the class used to create the object. This label reuse encodes subtyping. Direct inheritance is represented in the metamodel with a special reference called inh. The following property states that c 2 is a direct subclass of c 1 .

subClass(c 1 , c 2 ∈ Classes, M V, M E ) ∀o ∈ Objects, o, c 2 ∈ M V ⇒ o, c 2 , inh, o, c 1 ∈ M E
Abstract Classes that are specified in a metamodel using the isAbstract attribute are not suitable for instantiation. They are often used to represent abstract concepts that gather common attributes and references.

isAbstract(c 1 ∈ Classes, M V, M E ) ∀o ∈ Objects, o, c 1 ∈ M V ⇒ ∃c 2 ∈ Classes, o, c 2 , inh, o, c 1 ∈ M E Definition 3 (Metamodel).
A MetaModel is a multigraph representing classes as vertices and references as edges as well as semantics properties over instantiation of classes and references. It is represented as a pair composed of a multigraph (M M V, M M E) built over a finite set M M V of vertices and a finite set M M E of edges, and as a predicate (conf ormsT o) over models representing the semantics properties.

A MetaModel is a pair (M M V, M M E), conf ormsT o such that:

M M V ⊆ Classes M M E ⊆ { c 1 , r, c 2 | c 1 , c 2 ∈ M M V, r ∈ References} conf ormsT o : M odel(M M V, M M E) → Bool
A minimum and maximum number of values that can be associated to an attribute or reference can be defined using the lower and upper attributes. This pair is usually named multiplicity. In order to ease the manipulation of this datatype, we introduce the type Natural = N ∪ { }. Using both attributes, it is used to represent a range of possible numbers of values. Unbounded ranges can be modelled using the value for the upper attribute.

lower(c 1 ∈ MMV, r 1 ∈ MME, n ∈ N atural , MV, ME ) ∀ o ∈ Objects, o, c 1 ∈ MV ⇒ |{m 2 ∈ MV | o, c 1 , r 1 , m 2 ∈ ME}| ≥ n
An analogous formalization is defined for the upper property replacing ≥ by ≤. o1, c1 , r, o2, c2 is denoted in the Coq code as: o1, c1 , o2, c2 , r .

A reference can be associated to an opposite reference. It means that, in a model conforming to its metamodel, for each link instance of this reference between two objects, there must exists a link in the opposite direction between these two objects.

isOpposite(r 1 , r 2 ∈ MME, MV, ME ) ∀ m 1 , m 2 ∈ MV, m 1 , r 1 , m 2 ∈ ME ⇔ m 2 , r 2 , m 1 ∈ ME
A reference can be composite. In this case, instances of the target concept belong to a single instance of source concepts.

areComposite(c 1 ∈ MMV, R ⊆ MME, MV, ME ) ∀ o ∈ Objects ⇒ |{m 1 ∈ MV | m 1 , r, o, c 1 ∈ ME, r ∈ R}| ≤ 1
Figure 4 shows a simple example of metamodel on the left and his Coq4MDE representation on the right. Given one Model M and one MetaModel M M , we can check conformance using the conf ormsT o predicate embedded in M M . This predicate identifies the set of models conforming to a metamodel. Figure 5 shows an example of a model that conforms to the metamodel given in For the implementation, a model in Coq4MDE is a multigraph defined as finite sets of vertices and edges satisfying some properties. Based on this model's definition, every new operator in the Coq4MDE framework needs to be addressed at the three hierarchically related levels (the sets level, the graph level and the MDE level). The following Union and Substitution operators definitions follow this three levels schema.

The Union primitive operator

For the set level, we use the union encoded in the Coq library Uniset9 that we note ∪. The same notation or symbolic abbreviation ∪ is used in our Coq code.

For the graph's level, the result is defined with a proof10 by induction that the union of two graphs is also a graph. The vertices/edges set for the resulting graph is the union of vertices/edges sets of the two initial graphs.

The union of two models vs 1 , es 1 and vs 2 , es 2 is the union of their vertices and edges sets in addition to the proof that the two sets constitute a graph. For simplification, this can be denoted as follows: vs 1 ∪ vs 2 , es 1 ∪ es 2 .

The Substitution primitive operator

As explained in Definition 1, the models are graphs having as nodes typed objects. For example, (o, c) is a model's object whose type is c and whose name is o. The Substitution operator aims to replace the name of an object of a model by another name. This operator is also defined using the three hierarchical levels.

Substituting a model's object whose name is src by a model's object whose name is dst inside the sets of vertices and edges is implemented using a generic map operator encoded in Coq using three basic functions: mapv, mapa and mape that are applied respectively on: the model's objects, the references and the edges. The function mapv is defined as follows: mapv (o, c) = (dst, c) if o = src (o, c) otherwise. The function mape replaces the names of the model's objects in the edges such as:

mape (v 1 , a, v 2 ) = (mapv v 1 , mapa a, mapv v 2 ).
The graph's image11 is then constructed from the initial graph using the images of the vertices and the edges by mapv, mapa and mape.

The sets and the graph obtained from the previous levels and the associated proofs constitute the substituted model.

Proofs of primitive operators

We consider the well typedness (instanceOf ) and the semantics properties discussed in Section 2.4. For every property (Φ), we prove the preservation by the primitive operators. Some properties are fully compositional: no residual verification activity (Ψ ) needs to be conducted at the composition time. Others will require additional verification activities (Ψ ) that can be modeled as preconditions.

For space reason, we only give the example of the hierarchy property (Φ: subClass) for the Union operator. Theorem 1 states12 that the hierarchy property is preserved by Union. So, for any classes c 1 and c 2 , if c 1 is a subClass of c 2 in the models M 1 and M 2 , then c 1 is also a subClass of c 2 in the model resulting from the Union of M 1 and M 2 .

Theorem 1. (subClassUnionPreserved) ∀ M 1 M 2 ∈ M odel, c 1 c 2 ∈ Classes, subClass(c 1 c 2 M 1 ) ∧ subClass(c 1 c 2 M 2 ) ⇒ subClass(c 1 c 2 (U nion M 1 M 2 )).
Table 1 summarizes the pre and postconditions for the verification of the metamodel conformance for the Union and Substitution operators. The proofs for the Union, respectively Substitution, operator are accessible at: http://coq4mde.enseeiht.fr/FormalMDE/Union_Verif.html, respectively http://coq4mde.enseeiht.fr/FormalMDE/Subst_Verif.html.

Φ Mr=Substitution ((o1, c1), (o2, c2), M) Mr=Union (M1, M2) instanceOf Ψ (M )=True Ψ (M i∈{1,2} )=True subClass Ψ (M )=True Ψ (M i∈{1,2} )=True Φ(Mr) = subClass(c1, c2, M ) Φ(Mr) = subClass(c1, c2, Mr) isAbstract Ψ (M )=True Ψ (M i∈{1,2} )=True lower Ψ (M ) = (c1 = c2) ∧ ((o2, c) / ∈ MV) Ψ (M )=lowerCond(c, r, nM1, M2) upper Ψ (M ) = (c1 = c2) ∧ ((o2, c) / ∈ MV) upperCond(c, r, n, M1, M2) isOpposite Ψ (M )=True Ψ (M i∈{1,2} )=True areComposite Ψ (M ) = (c1 = c2) ∧ ((o2, c) / ∈ MV) Ψ (M ) = 1 > |{o2 ∈ MV1 | o, c , r, o2 ∈ ME1}| +|{o2 ∈ MV2 | o, c , r, o2 ∈ ME2}| -|{o2 ∈ (MV1 ∩ MV2) | o, c , r, o2 ∈ (ME1 ∩ ME2)}|
Table 1. pre and postconditions for the Union and Substitution operators

The basic Coq4MDE framework is about 1107 lines, the actual version containing the primitive composition operators and also the proved implementation of the Package Merge described in the next section is about 18000 lines with about 300 Lemmas and Theorems and 200 Definitions. The proofs for the elementary operators are about 3300 lines. The implementation and proofs of the Package Merge using the elementary operators is about 7200, this implementation take advantage from reusing the proofs previously done for the primitive operators. The alternative is the implementation without elementary operators and that would require multiple repetitions of the elementary proofs and would be about 20400 lines. So, our approach enables a reduction with more then 180% in this case.

Validation

The primitive operators have been used for the implementation of higher level composition operators including MOF Package Merge, ISC (considering the adaptation and glueing of components) and aspect weaving. These operators share parts of their implementation and conformance preservation proof that can be captured by the use of the primitive operators. For their implementations, other model operations are required (e.g. extraction of matching between models, verification of some conditions, . . . ) but the only modifications of the models are primitive substitutions and unions. The verifications of the fully compositional properties reuse directly the proofs of the primitive operators without any additional parts. The verification of the properties requiring additional preconditions needs to ensure that the preconditions are satisfied.

We show mainly in this section that our minimal set of primitive operators is sufficient to formalize a high level operator like the MOF Package Merge. A mature formalization for the ISC operators based on the elementary ones is also available, for the details see [START_REF] Kezadri | Assistance à la validation et vérification de systèmes critiques: ontologies et intégration de composants[END_REF].

The Package Merge implementation as summarized hereafter is accessible at: http://coq4mde.enseeiht.fr/PackageMergeCoq/.

To illustrate our methodology, we give an example derived from [START_REF] Zito | UML's Package Extension Mechanism: Taking a Closer Look at Package Merge[END_REF]. The source package (in this case the package BasicEmployee mentioned in Figure 6) is the package receiving. The package EmployeeLocation shown in Figure 7 is the package merged. This package contains the additional elements that must be merged with the package receiving. Two conflicts occur between the models merged and receiving. The first one is related to the attribute upper of worksAs (the maximal bound is equal to 2 in the model BasicEmployee (Figure 6) and is equal to 3 in the model EmployeeLocation (Figure 7)). The second conflict is related to the class Employee that is abstract (name in italic) in the merged package and concrete in the receiving package.

The resolution of this kind of conflicts is done according the the UML specification [START_REF] Omg | Unified modeling language (omg uml)-infrastructure(v2.4.1)[END_REF]. The rule to resolve the conflict for the upper attribute is: upper Resulting = max(upper M erged , upper Receiving ). The rule for the isAbstract attribute is: isAbstract Resulting = isAbstract M erged ∧ isAbstract Receiving . The list of all the possible transformations is available on page 166 of the specification [START_REF] Omg | Unified modeling language (omg uml)-infrastructure(v2.4.1)[END_REF].

Concretely in our abstract syntax, we manipulate the metamodels as models conforming to MOF, so the abstraction property for classes is represented with attributes isAbstract suffixed with the name of the class (this attribute is equal to True in the model BasicEmployee (Figure 6) and equal to False in the model EmployeeLocation (Figure 7)). The same principle is used to represent all the properties linked to MOF such as lower and upper. We show in Figure 8 the representation of the package BasicEmployee as a model conforming to MOF. The EmployeeLocation package is represented using the same principle, we don't show it here for space reason. The first step is to resolve all the conflicts. For this, the Substitution operator is applied twice. The first application replaces 2 by 3 for the upper Job attribute in the merged model. The second application of the Substitution operator replaces T rue by F alse for the isAbstract Employee attribute in the merged model.

Once the conflicts are resolved, the final step is the Union of the obtained models merged and receiving (the constraints of the Union operator are sat- isfied in this case). The result is exactly the merge of the two packages merged and receiving shown in Figure 9.

In the previous example, the Package Merge is expressed using the primitive composition operators Union and Substitution. Defining the Package Merge in this manner ensures that the resulting model is well typed in relation with the packages merged and receiving and also that it satisfies the semantics properties of the metamodel when the preconditions are satisfied.

We have also experimented the use of our primitive operators to define: the aspect weaving [START_REF] Morin | A generic weaver for supporting product lines[END_REF], the merge of statecharts specifications [START_REF] Nejati | Matching and merging of statecharts specifications[END_REF], the weave of State and Sequence Diagrams, the attributes composition [START_REF] Sentilles | Integration of extra-functional properties in component models[END_REF] and also to reimplement the operators of the Invasive Software Composition (ISC) [START_REF] Aßmann | Invasive software composition[END_REF].

Related work

This work targets a formal certified model composition framework. Our notion of model follows the MDE vision and we are interested in the problems of composition and compositional verification. This work is related to several issues highlighted in this Section. First, we take a look at some composition approaches and we rely on a MOF Package Merge formalization to explain our contribution. Then, we discuss some formalizations of the MDE to position our proposal. Finally, we present some work on compositional verification to situate our work.

Composition approaches

We previously proposed in [START_REF] Kezadri | A proof assistant based formalization of components in MDE[END_REF] [START_REF] Hamiaz | Correct-byconstruction model composition: Application to the invasive software composition method[END_REF] the formalization and verification of some ReuseWare [START_REF] Henriksson | Extending grammars and metamodels for reuse: the Reuseware approach[END_REF] operators. Several composition methods have focused on the implementation of the merge operators using mappings between models like Rational Software Architect 13 , Bernstein et al. data model [START_REF] Bernstein | A vision for management of complex models[END_REF], Atlas Model Weaver 14 [START_REF] Del Fabro | Towards the efficient development of model transformations using model weaving and matching transformations[END_REF], Epsilon 15 , Theme/UML [START_REF] Clarke | Extending standard UML with model composition semantics[END_REF] and EMF Facet 16 . The ReuseWare operators and the MOF Package Merge operators as presented in the previous frameworks and also in [START_REF] Brunet | A manifesto for model merging[END_REF] and [START_REF] Baya | Composing specific domains for large scale systems[END_REF] are defined as a composition of the primitive operators. The advantages of these implementation relying are the proof of termination of the composition operators (ensured by the Coq proof-assistant), the properties verification for the composition and the support for the extraction of the validated executable code.

Zito in [START_REF] Zito | UML's Package Extension Mechanism: Taking a Closer Look at Package Merge[END_REF] presented an implementation using Alloy 17 [START_REF] Jackson | Software abstractions-logic, language, and analysis[END_REF] of the MOF Package Merge. As Alloy has a poor performance when analysing models with many signatures (e.g. 20 signatures or higher), the analysis is currently limited to an interval between 5 and 10. The UML metamodel contains more than 30 classes which are all modelled with a signature. The authors applies several strategies to reduce the size of the Alloy model: reduce the depth of inheritance, merge similar classes, do not model classes that do not contain any information and do not change by applying the fusion (e.g. PackageImport, PackageMerge, Ele-mentImport, Comment and Constraint), merge multiple inheritance, eliminate recursion, and finally do not model derived attributes and associations.

Elaborating a proved development allows specifying generically the properties and verifying these properties a priori for all the instances. This universal quantification used in the proofs enables to avoid all the constraints and the limitation in relation with the models' size.

Formalization of MDE

A lot of work was conducted aiming to formalize the concepts of MDE.

First, MoMENT (MOdel manageMENT) [START_REF] Boronat | An algebraic semantics for MOF[END_REF] is an algebraic model management framework that provides a set of generic operators to manipulate models. The metamodels are represented as algebraic specifications and the operators are defined independently of the metamodel using the Maude language [START_REF] Clavel | Maude: specification and programming in rewriting logic[END_REF]. Also, A. Vallecillo et al. have designed and implemented a different embedding of metamodels, models ( [START_REF] Romero | Formal and tool support for Model Driven Engineering with Maude[END_REF]) and model transformations ( [START_REF] Troya | Towards a rewriting logic semantics for ATL[END_REF]) using Maude. This embedding is shallow, it relies strongly on the object structure proposed by Maude in order to define model elements as objects, and relies on the object rewriting semantics in order to implement model transformations.

Furthermore, I. Poernomo has proposed an encoding of metamodels and models using type theory ( [START_REF] Poernomo | The meta-object facility typed[END_REF]) in order to allow correct by construction development of model transformation using proof-assistants like Coq ( [START_REF] Poernomo | Proofs-as-model-transformations[END_REF]). Some simple experiments have been conducted using Coq mainly on tree-shaped models ( [START_REF] Poernomo | Correct-by-construction model transformations from partially ordered specifications in Coq[END_REF]) using inductive types. General graph model structure can be encoded using coinductive types. However, as shown in [START_REF] Picard | Coinductive graph representation : the problem of embedded lists[END_REF] by C. Picard and R. Matthes, the encoding is quite complex as Coq enforces structural constraints when combining inductive and co-inductive types that forbid the use of the most natural encodings proposed by Poernomo et al. M. Giorgino et al. rely in [START_REF] Giorgino | Verification of the Schorr-Waite algorithm-from trees to graphs[END_REF] on a spanning tree of the graph combined with additional links to overcome that constraint using the Isabelle proof-assistant. This allows to develop a model transformation relying on slightly adapted inductive proofs and then extract classical imperative implementations. Also, another implementation of the MDE is the HOL-OCL system [START_REF] Brucker | A proposal for a formal ocl semantics in isabelle/hol[END_REF] [10] that constitutes an environment for interactive modelling with UML and OCL and can be used for example to proof class invariants.

These embeddings are all shallow: they rely on sophisticated similar data structure to represent model elements and metamodels (e.g. Coq (co-)inductive data types for model elements and object and (co-)inductive types for metamodel elements). The work described in this paper is a deep embedding, each concept from models and metamodels was encoded in [START_REF] Thirioux | A Framework to Formalise the MDE Foundations[END_REF] using primitive constructs instead of relying on similar elements in Maude, Coq or Isabelle. The purpose of this contribution is not only to implement model transformation using correctby-construction tools but also to give a kind of denotational semantics for the MDE concepts that should provide a deeper understanding and allow the formal validation of the various implemented technologies. Another formalisation in Coq of the MDE concepts by F.Barbier et al is accessible 18 [2], this representation is attached to the proof of the properties shown in [START_REF] Kühne | Matters of (meta-) modeling[END_REF] (instantiation relations and model transformations). Other work aiming to define a semantics for a modelling language by explicitly and denotationally defining the kind of systems the language describes and to focus on the variations and variability in the semantics [12] [28]. Compared to the last work, we are interested in a generic, complete and unique formalisation of the conformity to metamodels and we are focused mainly in the proof of the preservation of this conformity relation by the composition operators.

Compositional verification

The compositional verification, in other words to break up the verification of a system into the verification of its components, is a very old dream. Several work were conduced in this direction using the model checking technique.

For instance, Nguyen, T.H. proposed in [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF] a compositional verification approach to check safety properties of component-based systems described in the BIP (Behavior -Interaction -Priority) language [START_REF] Basu | Modeling heterogeneous real-time components in BIP[END_REF].

Also, another approach allowing to verify systems by composition from verified components was proposed in [START_REF] Xie | Verified systems by composition from verified components[END_REF] where the temporal properties of a software component are specified, verified, and packaged with the component.

In this paper, regarding the previous cited methods, we adopted a generic composition technology that takes into account the EMOF metamodel properties making it usable with any language that can be described with a metamodel.

Conclusions

We have tackled in this paper the problem of model composition formalization and verification. In this purpose, starting from our formal framework for model and metamodel formal specification Coq4MDE, we propose to rely on primitive composition operators that can then be used to build more sophisticated operators. We prove the correctness of the expected properties for these primitive ones introducing mandatory preconditions to reach compositional verification for the targeted properties. The proofs of property preservation for the high level operators combine the proofs of the primitive ones. Our proposal is validated in this contribution with the MOF model conformance property and the MOF package merge operator. All these notions are also currently reflected in the Coq proof-assistant, following the line of thought of our previous work around model and metamodel formalization. This embedding provides correct-by-construction pieces of executable code for the different model operations related to composition. As we target a general purpose MDE-oriented framework, our work applies to any model, modelling language, application and is not restricted to some more-or-less implicit language context. This proposal is a preliminary mandatory step in the formalization of compositional formal verification technologies. We have tackled the formal composition of models independently of the properties satisfied by the model and the expected properties for the composite model. The next step in our work is to improve the notion of model compositional verification relying on several use cases from simple static constraints such as verification of OCL constraints satisfaction, to more dynamic properties such as deadlock freedom as proposed in the BIP framework [START_REF] Basu | Modeling heterogeneous real-time components in BIP[END_REF].

In this last purpose, we need to model the behavioural part of each language. We propose to rely on the generic behaviours applicable to several meta-models sharing some features presented in [START_REF] Lara | From types to type requirements: genericity for modeldriven engineering[END_REF]. This can be applied to families of unrelated meta-models. We plan to experiment the behavioural aspect by considering the merging of Statecharts Specifications [START_REF] Nejati | Matching and merging of statecharts specifications[END_REF]. In the long run, we plan to integrate the work of Garnacho et al. [START_REF] Garnacho | A mechanized semantic framework for real-time systems[END_REF] that provide an embedding in Coq of timed transition systems in order to model the behavioral aspect of languages.

Fig. 1 .Fig. 2 .

 12 Fig. 1. The basic concepts of EMOF

Fig. 3 .

 3 Fig.3. Conceptual view of the Package Merge[START_REF] Omg | Unified modeling language (omg uml)-infrastructure(v2.4.1)[END_REF]

8

 8

2 Fig. 4 .

 24 Fig. 4. A metamodel in the Coq4MDE notation

Figure 4 .Fig. 5 .

 45 Fig. 5. A model in the Coq4MDE notation

  Fig. 6. BasicEmployee

Fig. 8 .Fig. 9 .

 89 Fig. 8. An excerpt from the BasicEmployee model

This work was partly funded by the French ministry of research through the ANR-12-INSE-0011 grant for the GEMOC project.

http://coq.inria.fr

http://coq4mde.enseeiht.fr/FormalMDE/

https://www.eclipse.org/

c1, c2, r in the Coq code is denoted here for simplification as: c1, r, c2 .

http://coq.inria.fr/stdlib/Coq.Sets.Uniset.html

http://coq4mde.enseeiht.fr/FormalMDE/Graph.html#MG.EG

http://coq4mde.enseeiht.fr/FormalMDE/Subst_Verif.html\#elements

http://coq4mde.enseeiht.fr/FormalMDE/Union.html#SCUP


Feng Yan
email: feng.yan@telecom-bretagne.eu

Philippe Martins
email: martins@telecom-paristech.fr

Laurent Decreusefond

Accuracy of Homology based Coverage Hole Detection for Wireless Sensor Networks on Sphere

HAL is

Accuracy of Homology based Coverage Hole Detection for Wireless Sensor Networks on Sphere

Feng Yan, Member, IEEE, Philippe Martins, Senior Member, IEEE, and Laurent Decreusefond Abstract-Homology theory has attracted great attention because it can provide novel and powerful solutions to address coverage problems in wireless sensor networks. They usually use an easily computable algebraic object, Rips complex, to detect coverage holes. But Rips complex may miss some coverage holes in some cases. In this paper, we investigate homology-based coverage hole detection for wireless sensor networks on sphere. The case when Rips complex may miss coverage holes is first identified. Then we choose the proportion of the area of coverage holes missed by Rips complex as a metric to evaluate the accuracy of homology-based coverage hole detection approaches. Closedform expressions for lower and upper bounds of the accuracy are derived. Asymptotic lower and upper bounds are also investigated when the radius of sphere tends to infinity. Simulation results are well consistent with the analytical lower and upper bounds, with maximum differences of 0.5% and 3% respectively. Furthermore, it is shown that the radius of sphere has little impact on the accuracy if it is much larger than communication and sensing radii of each sensor.

Index Terms-Wireless sensor networks, coverage hole, homology.

I. INTRODUCTION

W IRELESS sensor networks (WSNs) have attracted con- siderable research attention due to their large number of potential applications such as battlefield surveillance, environmental monitoring and intrusion detection. Many of these applications require a reliable detection of specified events. Such requirement can be guaranteed only if the target field monitored by a WSN contains no coverage holes, that is to say regions of the domain not monitored by any sensor. But coverage holes can be formed for many reasons, such as random deployment, energy depletion or destruction of sensors. Consequently, it is essential to detect and localize coverage holes in order to ensure the full operability of a WSN.

Most existing works on coverage hole issues mainly focus on two-dimensional (2D) plane or three-dimensional (3D) full space. There is few work on 3D surfaces. But in some real applications, such as volcano monitoring [START_REF] Werner-Allen | Deploying a wireless sensor network on an active volcano[END_REF] and forest monitoring [START_REF] Mo | Canopy closure estimates with greenorbs: sustainable sensing in the forest[END_REF], the target fields are complex surfaces. So it is also important to consider the coverage hole detection problem of WSNs on surfaces. On the other hand, from theoretical point of view, the coverage on 3D surfaces is quite a different problem from its counterpart in 2D plane or 3D full space. As sphere is the simplest case of 3D surfaces, we choose it as the first step for the analysis in this paper, like the authors did in [START_REF] Gupta | The capacity of wireless networks[END_REF] for throughput capacity analysis.

There are already extensive works on the coverage hole detection problem for WSNs in 2D plane and 3D space. Some of these works used either precise information about sensor locations [START_REF] Fang | Locating and bypassing routing holes in sensor networks[END_REF]- [START_REF] Huang | The coverage problem in three-dimensional wireless sensor networks[END_REF] or accurate relative distances between neighbouring sensors [START_REF] Bejerano | Simple and efficient k-coverage verification without location information[END_REF], [START_REF]Coverage verification without location information[END_REF] to detect coverage holes. The requirement of precise location or distance information substantially limits their applicability since acquiring such information is either expensive or impractical in many settings. Thus connectivity-based approaches are of great interest for us. In this category, homology-based schemes have received special attention because of its powerfulness for coverage hole problems in WSNs.

Homology theory was first adopted by Ghrist and his collaborators in [START_REF] Silva | Blind swarms for coverage in 2-d[END_REF]- [START_REF] Ghrist | Coverage and hole-detection in sensor networks via homology[END_REF] to address the coverage problems in WSNs. They introduced a combinatorial object, Čech complex, which uses sensing ranges of nodes to fully characterize coverage properties of a WSN (existence and locations of holes). Unfortunately, the construction of this object is of very high complexity [START_REF] Chazal | Towards persistence-based reconstruction in euclidean spaces[END_REF] even if the precise location information about sensors is provided. Thus, they introduced another more easily computable complex, Vietoris-Rips complex (we will abbreviate the term to Rips complex in this paper). This complex is constructed with the sole knowledge of the connectivity graph of the network and gives an approximate coverage by simple algebraic calculations. Considering the ease of Rips complex construction, some homology-based algorithms were proposed in [START_REF] Muhammad | Control using higher order laplacians in network topologies[END_REF]- [START_REF] Tahbaz-Salehi | Distributed coverage verification in sensor networks without location information[END_REF] to use Rips complex to detect coverage holes. But all these homology-based approaches do not consider the cases that Rips complex may miss some special coverage holes. If the proportion of the area of coverage holes missed by Rips complex is low enough, then it is acceptable to use these methods for coverage hole detection. If the proportion is too high to be unacceptable, then it may not be proper to use these methods. Therefore, in order to evaluate the accuracy of homology-based coverage hole detection approaches, it is of paramount importance to analyse the coverage holes missed by Rips complex.

The main contributions of our paper are as follows. First, the relationship between Čech complex and Rips complex in terms of coverage hole on sphere is analysed. Furthermore, the case that Rips complex may miss coverage holes is identified and it is found that a hole in a Čech complex missed by a Rips complex must be bounded by a spherical triangle. Based on that, a formal definition of spherical triangular hole is given.

Second, the proportion of the area of spherical triangular holes is chosen as a metric to evaluate the accuracy of homology-based coverage hole detection. Such proportion is analysed under a homogeneous setting and it is related to the communication and sensing radii of each sensor. Closed-form expressions for lower and upper bounds of the proportion are derived. Asymptotic lower and upper bounds are also investigated when the radius of sphere tends to infinity.

Third, extensive simulations are performed to evaluate impacts of communication and sensing radii, radius of sphere on proportion of the area of spherical triangular holes. It is shown that simulation results are well consistent with the analytical lower bound, with a maximum difference of 0.5%, and consistent with the analytical upper bound, with a maximum difference of 3%. Furthermore, simulation results show that the radius of sphere has little impact on the proportion when it is much larger than communication and sensing radii.

The rest of the paper is organised as follows. Section II presents the related work. In Section III, the network model and the formal definition of spherical triangular hole are given. Closed-form lower and upper bounds for proportion of the area of spherical triangular holes are derived in Section IV. Section V compares simulation results and analytical bounds. Finally, Section VI concludes the paper.

II. RELATED WORK

Since this paper aims to evaluate the ratio of the area of coverage holes missed by homology-based approaches, we present the related work in terms of two aspects: coverage hole detection approaches and analytical coverage ratio evaluation.

A. Coverage hole detection approaches

Many approaches have been proposed for coverage hole detection in WSNs. They can be generally classified into three categories: location-based, range-based and connectivitybased.

Location-based approaches are usually based on computational geometry with tools such as Voronoi diagram and Delaunay triangulations, to discover coverage holes [START_REF] Fang | Locating and bypassing routing holes in sensor networks[END_REF]- [START_REF] Zhang | Localized algorithms for coverage boundary detection in wireless sensor networks[END_REF]. Range-based approaches attempt to discover coverage holes by using only relative distances between neighbouring sensors [START_REF] Bejerano | Simple and efficient k-coverage verification without location information[END_REF], [START_REF]Coverage verification without location information[END_REF]. These two types of approaches need either precise location information or accurate distance information, which restricts their applications since such information is not easy to obtain in many settings.

In connectivity-based approaches, homology-based schemes attract particular attention due to its powerfulness for coverage hole detection. De Silva et al. first proposed a centralized algorithm that detects coverage hole via homology in [START_REF] Silva | Coverage in sensor networks via persistent homology[END_REF]. They constructed the Rips complex corresponding to the communication graph of the network and determined the coverage by verifying whether the first homology group of the Rips complex is trivial. Then the above ideas were first implemented in a distributed way in [START_REF] Muhammad | Control using higher order laplacians in network topologies[END_REF]. It is shown that combinatorial Laplacians are the right tools for distributed computation of homology groups and can be used for decentralized coverage verification. In [START_REF] Muhammad | Decentralized computation of homology groups in networks by gossip[END_REF], a gossip-like decentralized algorithm for computation of homology groups was proposed. In [START_REF] Tahbaz-Salehi | Distributed coverage verification in sensor networks without location information[END_REF], a decentralized scheme based on Laplacian flows was proposed to compute a generator of the first homology group. All these homology-based algorithms may be also used to detect coverage holes for WSNs on surfaces, but they do not consider the cases that Rips complex may miss some special coverage holes. One of our objectives in this paper is to identify such cases.

B. Analytical coverage ratio evaluation

Extensive research has been done to analyse coverage ratio of a WSN in 2D plane or on 3D surfaces. In [START_REF] Liu | A study of the coverage of large-scale sensor networks[END_REF], the authors studied the coverage properties of large-scale sensor networks and obtained the fraction of the area covered by sensors. The sensors are assumed to have the same sensing range and are distributed according to a homogeneous Poisson point process (PPP) in plane. In [START_REF] Wan | Coverage by randomly deployed wireless sensor networks[END_REF], the authors studied how the probability of k-coverage changes with the sensing radius or the number of sensors, given that sensors are deployed as either a PPP or a uniform point process. In addition, the distance distribution between two points in random networks was derived in [START_REF] Moltchanov | Distance distributions in random networks[END_REF]. Their results can be used to derive the fraction of areas covered by at least k-sensors. All the above studies only considered homogeneous cases. In [START_REF] Lazos | Stochastic coverage in heterogeneous sensor networks[END_REF], the coverage problem in planar heterogeneous sensor networks are investigated and analytical expressions of coverage are derived. Their formulation is more general in the sense that sensor can be deployed according to an arbitrary stochastic distribution, or can have different sensing capabilities or can have arbitrary sensing shapes. Based on their results, the authors in [START_REF] Zhao | Surface coverage in wireless sensor networks[END_REF] derived the expected coverage ratio of sensors under stochastic deployment on 3D surface. Similarly, the expected coverage ratio under stochastic deployment on 3D rolling terrains was derived in [START_REF] Liu | On coverage of wireless sensor networks for rolling terrains[END_REF]. In [START_REF] Li | Coverage properties of the target area in wireless sensor networks[END_REF], a point in a plane is defined to be tri-covered if it lies inside a triangle formed by three nodes, and the probability of tricoverage was analysed.

All the above research considered only coverage ratio problems, without considering coverage hole detection issues. Their analysis is thus not specific to any coverage hole detection approaches. We provided some initial results about the proportion of the area of triangular holes for WSNs in 2D plane in [START_REF] Yan | Accuracy of homology based approaches for coverage hole detection in wireless sensor networks[END_REF]. In this paper, we aim to analyse the proportion of the area of coverage holes missed by homology-based coverage hole detection approaches for WSNs on sphere and compare it with the case in 2D plane.

III. MODELS AND DEFINITIONS

Consider a collection of stationary sensors (also called nodes) on a sphere S 2 with radius R. The sensors are deployed according to a homogeneous PPP with intensity λ. For any two points p 1 and p 2 on S 2 , the distance between them d(p 1 , p 2 ) is defined to be the great circle distance, which is the shortest distance between them measured along a path on the surface of the sphere. As usual, isotropic radio propagation is assumed. All sensors have the same sensing radius R s and communication radius R c on S 2 . It means for any sensor located at v on S 2 , any point p on S 2 with d(v, p) ≤ R s is inside the sensing range of the sensor; and for any two sensors located at v i , v j on S 2 , they can communicate with each other if d(v i , v j ) ≤ R c . In addition, we assume R s ≪ R, R c ≪ R.

Before defining the two combinatorial objects, known as Čech complex and Rips complex, it is necessary to give a brief introduction to some tools used in the paper. For further readings, see [START_REF] Armstrong | Basic Topology[END_REF]- [START_REF] Hatcher | Algebraic Topology[END_REF]. Given a set of points V , a k-simplex is an unordered set [v 0 , v 1 , ..., v k ] ⊆ V where v i = v j for all i = j, k is the dimension of this simplex. The faces of this k-simplex consist of all (k-1)-simplex of the form [v 0 , ..., v i-1 , v i+1 , ..., v k ] for 0 ≤ i ≤ k. For example, on a sphere S 2 , a 0-simplex [v 0 ] is a vertex , a 1-simplex [v 0 , v 1 ] is the shorter arc of the great circle passing through v 0 and v 1 , a 2-simplex [v 0 , v 1 , v 2 ] is a spherical triangle v 0 v 1 v 2 with its interior included, see Figure 1. An abstract simplicial complex is a collection of simplices which is closed with respect to inclusion of faces. A k-dimensional abstract simplical complex K is an abstract simplicial complex where the largest dimension of any simplex in K is k. Let V denote the set of sensor locations in a WSN on S 2 with radius R and S = {s v , v ∈ V} denote the collection of sensing ranges of these sensors: for a location v, s v = {x ∈ S 2 : d(x, v) ≤ R s }. Then Čech complex and Rips complex can be defined as follows [START_REF] Silva | Blind swarms for coverage in 2-d[END_REF], [START_REF] Silva | Coverage in sensor networks via persistent homology[END_REF].

v 0 v 0 v 1 v 0 v 1 v 2 0-simplex 2-simplex 1-simplex
Definition 1 ( Čech complex). Given a finite collection of sensing ranges {s v , v ∈ V}, the Čech complex of the collection, Č(V), is the abstract simplicial complex whose ksimplices correspond to non-empty intersections of k + 1 distinct elements of {s v , v ∈ V}.

Definition 2 (Rips complex). Given a finite set of points V on S 2 and a fixed radius ǫ, the Rips complex of V, R ǫ (V), is the abstract simplicial complex whose k-simplices correspond to unordered (k +1)-tuples of points in V which are pairwise within distance ǫ of each other.

According to the definitions, the Čech complex and Rips complex of the WSN, respectively denoted by ČRs (V) and R Rc (V), can be constructed as follows: a k-simplex

[v 0 , v 1 , • • • , v k ] belongs to ČRs (V) whenever ∩ k l=0 s v l = ∅ and a k-simplex [v 0 , v 1 , • • • , v k ] belongs to R Rc (V) whenever d(v l , v m ) ≤ R c for all 0 ≤ l < m ≤ k.
In addition, since we consider only coverage holes on the sphere S 2 , it is sufficient to construct 2-dimensional Čech complex and 2-dimensional Rips complex of the WSN, denoted as Č( 2)

Rs (V) and R (2)
Rc (V) respectively.

Figure 2 shows a WSN, its Čech complex and two Rips complexes for two different values of R c . Depending on the relation of R c and R s , the Rips complex and the Čech complex may be close or rather different. In this example, for R c = 2R s , the Rips complex sees the hole surrounded by 2, 3, 5, 6 as in the Čech complex whereas it is missed in the Rips complex for R c = 2.5R s . At the same time, the true coverage hole surrounded by 1, 2, 6 is missed in both Rips complexes. In fact, as proved in [START_REF] Bott | Differential Forms in Algebraic Topology[END_REF], any coverage hole can be found in Čech complex. Unfortunately, the construction of Čech complex is of very high complexity even if the precise location information of nodes is provided. So a more easily computable tool, Rips complex, is used. But Rips complex can not always capture all coverage holes. To be more specific, there exist following relations between Č(2) Rs (V) and R

Rc (V). Lemma 1. Let V denote the set of node locations in a WSN on S 2 with radius R, all nodes have the same sensing radius

R s and communication radius R c , R s ≪ R, R c ≪ R, then R (2) Rc (V) ⊂ Č(2) Rs (V) ⊂ R (2) 2Rs (V), whenever R c ≤ R arccos([3 cos 2 (R s /R) -1]/2) (1)
Proof: See the Appendix A. According to [START_REF] Werner-Allen | Deploying a wireless sensor network on an active volcano[END_REF], some relationships between Čech complex and Rips complex in terms of coverage hole can be derived as illustrated in the following corollaries.

Corollary 1. When R c ≤ R arccos([3 cos 2 (R s /R) -1]/2), if there is no hole in R (2) Rc (V), there must be no hole in Č(2) Rs (V). Corollary 2. When R c ≥ 2R s , if there is a hole in R (2)
Rc (V), there must be a hole in

Č(2) Rs (V). Corollary 3. When R arccos([3 cos 2 (R s /R) -1]/2) < R c < 2R s , there is no guarantee relation between Č(2) Rs (V) and R (2) Rc (V).
From Corollary 1, a sufficient condition for coverage verification can be derived. From Corollary 2, we can find a necessary condition for the existence of a hole in Č( 2) Rs (V).

Corollary 3 indicates that when there is no hole in R

(2)

Rc (V), it is possible that there is a hole in Č(2) Rs (V). When there is a hole in R (2) Rc (V), it is also possible that Č(2)
Rs (V) contains no hole. From these corollaries, it can be seen that when

R c > R arccos([3 cos 2 (R s /R) -1]/2), R (2) Rc (V) may miss a hole in Č(2) Rs (V). Furthermore, a hole in a Č(2) Rs (V) not seen in a R (2)
Rc (V) must be bounded by a spherical triangle. Based on this observation, a formal definition of spherical triangular hole is given as follows.

Definition 3 (Spherical triangular hole). For a pair of complexes Č( 2)

Rs (V) and R (2)
Rc (V) of a WSN, a spherical triangular hole is an uncovered region bounded by a spherical triangle formed by three nodes

v 0 , v 1 , v 2 , where v 0 , v 1 , v 2 can form a 2-simplex which appears in R (2) Rc (V) but not in Č(2)
Rs (V). According to Definition 3, it can be seen from Figure 2 that when R c = 2R s , there is one spherical triangular hole bounded by the spherical triangle formed by nodes 1, 2 and 6. And when R c = 2.5R s , there are two additional spherical triangular holes, bounded by spherical triangles formed by nodes 2, 3, 6 and 3, 5, 6 respectively.

A summary of the main notations is given in Table I.

Rs (V) 2-dimensional Čech complex of the WSN denoted by V R (2) Rc (V) 2-dimensional Rips complex of the WSN denoted by V λ the intensity of Poisson point process p(λ)
the probability of any point on sphere being inside a spherical triangular hole

p l (λ) lower bound of p(λ) pu(λ) upper bound of p(λ) p ′ l (λ) asymptotic lower bound of p(λ) when R → ∞ p ′ u (λ) asymptotic upper bound of p(λ) when R → ∞

IV. BOUNDS ON PROPORTION OF SPHERICAL TRIANGULAR

HOLES

In this section, the conditions under which any point on S 2 with radius R is inside a spherical triangular hole are first given. The proportion of the area of spherical triangular holes is chosen as a metric for accuracy evaluation. Closed-form expressions for lower and upper bounds of the proportion are derived. Finally, the asymptotic lower and upper bounds are investigated when the radius of sphere tends to infinity.

A. Preliminary

Rc (V) while σ / ∈ Č(2) Rs (V), so R (2)
Rc (V) ⊂ Č(2) Rs (V). According to (1), we have R c > R arccos([3 cos 2 (R s /R) - 1]/2) ⇒ R s < R arccos [1 + 2 cos(R c /R)]/3. Lemma 4.
Let O be a point inside a spherical triangular hole and l denote the great circle distance between O and its closest neighbour, then

R s < l ≤ R arccos [1 + 2 cos(R c /R)]/3.
The proof is similar as that of Lemma 1. Since nodes are assumed to be distributed on S 2 according to a homogeneous Poisson point process with intensity λ, any point has the same probability to be inside a spherical triangular hole. This probability in a homogeneous setting is also equal to the proportion of the area of spherical triangular holes.

We use spherical coordinates (R, θ, ϕ) to denote points on S 2 with radius R, where θ is polar angle and ϕ is azimuth angle. Without loss of generality, we consider the probability of the point N with spherical coordinates (R, 0, 0) being inside a spherical triangular hole. Since the communication radius of each sensor is at most R c , only the nodes within R c from the point N can contribute to the spherical triangle which bounds a spherical triangular hole containing N . Therefore, we only need to consider the Poisson point process constrained on the spherical cap C(N, R c ) which is also a homogeneous Poisson process with intensity λ, where C(N, R c ) denotes the spherical cap centered at point N and the maximum great circle distance between N and points on the spherical cap is R c . We denote this process as Φ. In addition, T (x, y, z) denotes the property that the point N is inside the spherical triangular hole bounded by the spherical triangle with points x, y, z as vertices. When n 0 , n 1 , n 2 are points of the process Φ, T (n 0 , n 1 , n 2 ) is also used to denote the event that the spherical triangle formed by the nodes n 0 , n 1 , n 2 bounds a spherical triangular hole containing the point N . In addition, we use T ′ (n 0 , n 1 , n 2 ) to denote the event that the nodes n 0 , n 1 , n 2 can not form a spherical triangle which bounds a spherical triangular hole containing the point N .

Let τ 0 = τ 0 (Φ) be the node in the process Φ which is closest to the point N . There are two cases for the point N to be inside a spherical triangular hole. The first case is that the node τ 0 can contribute to a spherical triangle which bounds a spherical triangular hole containing the point N . The second case is that the node τ 0 can not contribute to any spherical triangle which bounds a spherical triangular hole containing the point N but other three nodes can form a spherical triangle which bounds a spherical triangular hole containing the point N . So the probability that the point N is inside a spherical triangular hole can be defined as p(λ) = P{N is inside a spherical triangular hole}

= P{ {n0,n1,n2}⊆Φ T (n 0 , n 1 , n 2 )} = P{ {n1,n2}⊆Φ\{τ0(Φ)} T (τ 0 , n 1 , n 2 )} + p sec (λ) (2)
where

p sec (λ) = P{ {n 0 ,••• ,n 4 } ⊆Φ\{τ 0 (Φ)} T (n 0 , n 1 , n 2 ) | T ′ (τ 0 , n 3 , n 4 )}
denotes the probability of the second case. p sec (λ) is generally very small and is obtained by simulations.

B. Analytical lower and upper bounds

As conjectured from Corollary 1, there exist spherical triangular holes only in the case R c > R arccos([3 cos 2 (R s /R) -1]/2), so we only consider this case. The lower and upper bounds of p(λ) are given as follows.

Theorem 1. When R c > R arccos([3 cos 2 (R s /R) -1]/2), p l (λ) < p(λ) < p u (λ), where p l (λ) = 2πλ 2 R 4 θ0u Rs/R sin θ 0 dθ 0 2ϕm(θ0) 2π-ϕm(θ0) dϕ 1 θ1u(θ0,ϕ1) θ0 sin θ 1 × e -λ|C(N,Rθ0)| e -λ|S + (θ0,ϕ1)| (1 -e -λ|S -(θ0,θ1,ϕ1)| )dθ 1 (3)
and

p u (λ) = 2πλ 2 R 4 θ0u Rs/R sin θ 0 dθ 0 2ϕm(θ0) 2π-ϕm(θ0) dϕ 1 θ1u(θ0,ϕ1) θ0 sin θ 1 × e -λ|C(N,Rθ0)| e -λ|S + (θ0,ϕ1)| (1 -e -λ|S -(θ0,θ0,ϕ1)| )dθ 1 + p sec (λ) (4)
and

θ 0u = arccos [1 + 2 cos(R c /R)]/3 ϕ m (θ 0 ) = π if Rs R < θ 0 ≤ Rc 2R arccos cos Rc R -cos 2 θ0 sin 2 θ0 othewise (5) θ 1u (θ 0 , ϕ 1 ) = min{θ 1u1 (θ 0 , ϕ 1 ), θ 1u2 (θ 0 , ϕ 1 )} (6)
θ 1u1 (θ 0 , ϕ 1 ) = arccos cos(R c /R) 1 -sin 2 θ 0 sin 2 ϕ 1 (7)
+ arctan(cos ϕ 1 tan θ 0 )

θ 1u2 (θ 0 , ϕ 1 ) = arccos cos(R c /R) » 1 -sin 2 θ 0 sin 2 (ϕ 1 -ϕ m (θ 0 )) (8)
+ arctan(cos(ϕ 1 -ϕ m (θ 0 )) tan θ 0 ) |C(N, Rθ 0 )| = 2πR 2 (1 -cos θ 0 ) (9) |S + (θ 0 , ϕ 1 )| = ϕ1 2π-ϕm(θ0) θ1u(θ0,ϕ) θ0 R 2 sin θdθdϕ (10) |S -(θ 0 , θ 1 , ϕ 1 )| = ϕm(θ0) ϕ 2l θ2u θ0 R 2 sin θ 2 dθ 2 dϕ 2 (11)
ϕ 2l = ϕ 1 -arccos cos(R c /R) -cos θ 1 cos θ 0 sin θ 1 sin θ 0 θ 2u = min{θ 1u1 , θ 2u2 } θ 2u2 = arccos cos(R c /R)/ » 1 -sin 2 θ 0 sin 2 (ϕ 2 -ϕ 1 ) + arctan(cos(ϕ 2 -ϕ 1 ) tan θ 1 )
p sec (λ) is obtained by simulations 1 .

Since the proof is tedious, we only give the main steps of the proof. Please refer to Appendix B for detailed computation.

For the lower bound, we only consider the first case that the closest node τ 0 must contribute to a spherical triangle which bounds a spherical triangular hole containing the point N . The main idea is to first fix the closest node τ 0 , and then sequentially decide the regions where the other two nodes may lie in, and finally do a triple integral.

Using spherical coordinates, we assume the closest node τ 0 lies on (R, α 0 , 0). Once the node τ 0 is determined, the other two nodes must lie in the different half spaces: one in H + = R + × (0, π/2) × (π, 2π) and the other in

H -= R + × (0, π/2) × (0, π).
Assume n 1 lies in H + and n 2 lies in H -. Since the great circle distance to τ 0 is at most R c , n 1 and n 2 must also lie in the spherical cap C(τ 0 , R c ). Furthermore, the great circle distance to the point N is at most R c and larger than Rα 0 , they should also lie in the region C(N, R c )\C(N, Rα 0 ). Therefore, n 1 must lie in

H + C(τ 0 , R c ) C(N, R c )\C(N, Rα 0 ) and n 2 must lie in H -C(τ 0 , R c ) C(N, R c )\C(N,
(R s /R) -1]/2) < R c ≤ 2R s or in the case R c > 2R s , R c /(2R) < α 0 ≤ arccos [1 + 2 cos(R c /R)]/3, A + = H + C(τ 0 , R c ) C(N, R c )\C(N, Rα 0 ) C(M 2 , R c ),
shown in Figure 3. M 1 and M 2 are two intersection points between bases of spherical caps C(N, Rα 0 ) and C(τ 0 , R c ). 4, where M is one intersection point between base of spherical caps C(N, Rα 0 ) and the plane xOz.

In the case R c > 2R s , R s /R < α 0 ≤ R c /(2R), A + = H + C(τ 0 , R c ) C(N, R c )\C(N, Rα 0 ) C(M, R c ), as in Figure
Ordering the nodes in A + by increasing azimuth angle so that τ 1 = (R, θ 1 , ϕ 1 ) has the smallest azimuth angle ϕ 1 . And assume the nodes τ 0 , τ 1 and another node τ 2 ∈ H -C(τ 0 , R c ) C(N, R c )\C(N, Rα 0 ) can form a spherical triangle which bounds a spherical triangular hole containing the point N , then τ 2 must lie to the right of the great circle passing through τ 1 and N , denoted by H + (ϕ 1 ) which contains all points with azimuth angle ϕ ∈ (ϕ 1π, ϕ 1 ). In addition, the great circle distance to τ 1 is no larger than R c , so the node τ 2 must lie in the region S -, as illustrated in Figures 4 and5. Assume only τ 0 , τ 1 and nodes in S -(τ 0 , τ 1 ) can contribute to the spherical triangle which bounds a spherical triangular hole containing the point N , we can get a lower bound of the probability that the point N is inside a spherical triangular hole. It is a lower bound because it is possible that τ 1 can not contribute to a spherical triangle which bounds a spherical triangular hole containing point N , but some other nodes with higher azimuth angles in the region A + can contribute to such a spherical triangle. For example, in Figure 6, if there is no node in S -but there are some nodes in S ′-, then τ 1 can not contribute to any spherical triangle which bounds a spherical triangular hole containing point N , but τ ′ 1 can form such a spherical triangle with τ 0 and another node in S ′-.

S -(τ 0 , τ 1 ) = S -(α 0 , θ 1 , ϕ 1 ) = H -C(τ 0 , R c ) C(N, R c )\C(N, Rθ 0 ) H + (ϕ 1 ) C(τ 1 , R c )
Next we will prove the upper bound. As discussed in Section IV-A, there are two cases for the point N being inside a spherical triangular hole. As for the second case that the Fig. 5.

Illustration of regions S + and S -in the case R arccos([3 cos 2 (Rs/R) -1]/2) < Rc ≤ 2Rs closest node τ 0 can not but some other nodes can contribute to a spherical triangle which bounds a spherical triangular hole containing the point N , it is not easy to obtain a closed-form expression for such probability, so we get it by simulations. Simulation results show that this probability is less than 0.16% whenever R c ≤ 3R s with any intensity λ. So we still focus on the probability of the first case.

Still consider the nodes in A + , each node (R, θ, ϕ) corresponds to an area |S -(α 0 , θ, ϕ)|. The higher is the area |S -(α 0 , θ, ϕ)|, the higher is the probability that there is at least one node in S -(α 0 , θ, ϕ), consequently the probability of the first case will be higher. It can be seen from Figures 4 and5 that the closer to α 0 is θ and the closer to ϕ 1 is ϕ, the higher is the area |S -(α 0 , θ, ϕ)|. So the largest area |S -(α 0 , θ, ϕ)| is |S -(α 0 , α 0 , ϕ 1 )|. Based on that, the upper bound can be derived.

As can be seen, the expression for lower bound is closedform, while the expression for upper bound is not exactly closed-form since it includes a non-analytical part p sec (λ). As for lower bound and the closed-form part for upper bound, we use numerical integration to approximate the triple integrals. As for p sec (λ), we get it by simulations since it is very small, it has little impact on the derived bound.

C. Asymptotic lower and upper bounds

Intuitively, when R → ∞, the case on sphere should be the same as that in plane, which is shown in the following theorem.

Theorem 2. When R → ∞ and R c > √ 3R s , lower and upper bounds in (3) and (4) become and

p ′ l (λ) = 2πλ 2 Rc/ √ 3 Rs r 0 dr 0 ϕu(r0) ϕ l (r0) dϕ ′ 1 R1(r0,ϕ ′ 1 ) r0 e -λπr 2 0 × e -λ|S + (r0,ϕ ′ 1 )| (1 -e -λ|S -(r0,r1,ϕ ′ 1 )| )r 1 dr 1 (12)
p ′ u (λ) = 2πλ 2 Rc/ √ 3 Rs r 0 dr 0 ϕu(r0) ϕ l (r0) dϕ ′ 1 R1(r0,ϕ ′ 1 ) r0 e -λπr 2 0 × e -λ|S + (r0,ϕ ′ 1 )| (1 -e -λ|S -(r0,r0,ϕ ′ 1 )| )r 1 dr 1 + p sec (λ) (13)
where

ϕ l (r 0 ) = ® 0 if R s < r 0 ≤ R c /2 2 arccos(R c /(2r 0 )) othewise (14) ϕ u (r 0 ) = ® π if R s < r 0 ≤ R c /2 π -4 arccos Rc 2r0 othewise (15) R 1 (r 0 , ϕ ′ 1 ) = min( » R 2 c -r 2 0 sin 2 ϕ ′ 1 -r 0 cos ϕ ′ 1 , (16)
» R 2 c -r 2 0 sin 2 (ϕ ′ 1 + ϕ l (r 0 )) + r 0 cos(ϕ ′ 1 + ϕ l (r 0 ))) |S + (r 0 , ϕ ′ 1 )| = ϕ ′ 1 ϕ l (r0) R1(r0,ϕ ′ ) r0 rdrdϕ ′ (17) |S -(r 0 , r 1 , ϕ ′ 1 )| = -ϕ l (r0) ϕ ′ 2l R2(r0,r1,ϕ ′ 1 ,ϕ ′ 2 ) r0 r 2 dr 2 dϕ ′ 2 (18) ϕ ′ 2l = ϕ ′ 1 -arccos(r 2 0 + r 2 1 -R 2 c )/(2r 0 r 1 ) R 2 (r 0 , r 1 , ϕ ′ 1 , ϕ ′ 2 ) = min( » R 2 c -r 2 0 sin 2 ϕ ′ 2 -r 0 cos ϕ ′ 2 , » R 2 c -r 2 1 sin 2 (ϕ ′ 2 -ϕ ′ 1 ) + r 1 cos(ϕ -ϕ ′ 1
)) p sec (λ) is obtained by simulations.

Proof: Please refer to Appendix C. Comparing ( 12) and ( 13) to the results in the paper [START_REF] Yan | Accuracy of homology based approaches for coverage hole detection in wireless sensor networks[END_REF], we can find that they are the same, which is quite logical since when R → ∞ the local of each node can be considered to be planar.

V. SIMULATIONS AND PERFORMANCE EVALUATION

In this section, simulation settings are first given. Then simulation results are compared with analytical lower and upper bounds under different settings of R s , R c , R.

A. Simulation settings

A sphere centered at the origin with radius R is considered in the simulations. The probability of the point with spherical coordinate (R, 0, 0) being inside a spherical triangular hole is computed. Sensors are randomly distributed on the sphere according to a homogeneous Poisson point process with intensity λ. The sensing radius R s of each node is set to be 10 meters and communication radius R c is chosen from 20 to 30 meters with interval of 2 meters. Let γ = R c /R s , then γ ranges from 2 to 3 with interval of 0.2. In addition, λ is selected from 0.001 to 0.020 with interval of 0.001. For each pair of (λ, γ), 10 7 simulations are run to check whether the point with spherical coordinate (R, 0, 0) is inside a spherical triangular hole.

B. Impact of R s and R c

As illustrated in Section III, R s ≪ R and R c ≪ R, here we fix R = 10R s , choose R s to be 10 meters and R c to be 20 to 30 meters with interval of 2 meters, to analyse the impact of R s and R c on the probability of any point being inside a spherical triangular hole. Under this configuration, the probability p(λ) obtained by simulations is presented with the lower and upper bounds in Figure 7(a) and 7(b) respectively. Note that the upper bounds contain the simulation results for p sec (λ) which are shown in Figure 7(c).

It can be seen that for any value of γ, p(λ) has a maximum at a threshold value λ c of the intensity. As a matter of fact, for λ ≤ λ c , the number of nodes is small. Consequently the probability of any point being inside a spherical triangular hole is relatively small too. With the increase of λ, the connectivity between nodes becomes stronger. As a result, the probability of any point being inside a spherical triangular hole increases. However, when the intensity reaches the threshold value, the probability is up to its maximum. p(λ) decreases for λ ≥ λ c . The simulations also show that λ c decreases with the increase of γ.

On the other hand, it can be seen from Figure 7(a) and 7(b) that for a fixed intensity λ, p(λ) increases with the increases of γ. That is because when R s is fixed, the larger R c is, the higher is the probability of each spherical triangle containing a coverage hole.

Furthermore, the maximum probability increases quickly with γ ranging from 2.0 to 3.0. These results can also provide some insights for planning of WSNs, which will be discussed in Section V-D.

Finally, it can be found in Figure 7(a) that the probability obtained by simulation is very well consistent with the lower bound. The maximum difference between them is about 0.5%. Figure 7(b) shows that probability obtained by simulation is also consistent with the upper bound. The maximum difference between them is about 3%.

C. Impact of R

Although we assume R s ≪ R and R c ≪ R, to better understand the impact of R on the probability of any point being inside a spherical triangular hole, we choose R to be 5R s , 10R s and 100R s . In these cases, R s is still 10 meters and R c is from 20 to 30 meters with interval of 2 meters. In addition, we also want to know the difference of the probability under spherical and 2D planar cases. Therefore, simulation results, lower and upper bounds of the probability under spheres with radii 5R s , 10R s , 100R s and 2D plane are shown in Figure 8(a), 8(b) and 8(c) respectively. Simulation results for p sec (λ) under spheres with radii 5R s , 10R s , 100R s and 2D plane are shown in Figure 9. From Figure 9, we can find that p sec (λ) is less than 0.16% under any intensity in these cases.

It can be seen from Figure 8 that simulations results, lower and upper bounds under spheres with radii 5R s , 10R s , 100R s and 2D plane are very close with each other. More precisely, the maximum difference of simulations results under spheres with radii 5R s and 10R s is about 0.045%, which is about 0.06% under spheres with radii 5R s and 100R s and is about 0.03% under spheres with radii 10R s and 100R s . In addition, the maximum differences of simulation results between 2D planar case and spherical cases with radii 5R s , 10R s , 100R s are 0.05%, 0.03% and 0.02% respectively. It means the larger the radius of sphere is, the more closer are the simulation results under sphere and 2D plane, it is because the larger the radius of sphere is, the more likely of the local of each node on the sphere to be planar.

With respect to lower and upper bounds, it is found that under any two spheres with radii 5R s , 10R s , 100R s , the maximum difference of lower and upper bounds are 0.06% and 0.12% respectively. Furthermore, under spheres with radii 5R s , 10R s , 100R s and 2D plane, the maximum difference of lower bounds is also 0.06%, and that of upper bounds is also 0.12%. More importantly, under sphere with radius 100R s and 2D plane, the maximum difference of lower bounds is 5 × 10 -6 and that of upper bounds is 2.5 × 10 -5 . It means the probabilities under cases of sphere with radius 100R s and 2D plane are nearly the same, which is quite logical since when the radius of sphere is much more larger than the sensing radius of any node, the local of any node can be considered to be planar.

It can be further found that under above cases, the maximum differences of simulation results, lower and upper bounds are all so small that they can be neglected. Consequently, it also means that the radius of sphere has little impact on the probability of any point on the sphere to be inside a spherical triangular hole.

D. Discussions on applications

In this paper, we only consider spherical triangular holes, for non-spherical triangular holes, we assume they can be detected and covered by additional nodes. Under this assumption, our analytical results can be used for planning of WSNs. For example, a WSN is used to monitor a mountain and the ratio γ = 2, according to the analytical upper bounds, we can see that the maximum proportion of the area of spherical triangular holes under γ = 2 is about 0.06 %, which can be neglected. It means that as long as the surface of mountain can be spherically triangulated by nodes, we can say the mountain is covered. But if γ = 3 and at least 95% of the surface of the mountain should be covered, then it means that the proportion of the area of spherical triangular holes can be at most 5%. From the analytical upper bounds of γ = 3, it can be seen that when the intensity λ = 0.009, the upper bound is about 5%, so in order to cover at least 95% of the mountain, the intensity of nodes should be larger than 0.009.

VI. CONCLUSIONS

This paper studied the accuracy of homology-based coverage hole detection for wireless sensor networks on sphere. First, the case when Rips complex may miss coverage holes was identified. It was found that a hole missed by Rips complex must be bounded by a spherical triangle and a formal definition of spherical triangular hole was given. Then we chose the proportion of the area of spherical triangular holes as a metric to evaluate the accuracy. Closed-form expressions for lower and upper bounds were derived. Asymptotic lower and upper bounds are also investigated when the radius of sphere tends to infinity. Simulation results are well consistent with the derived lower and upper bounds, with maximum differences of 0.5% and 3% respectively. In addition, simulation results also show that the radius of sphere has little impact on the accuracy as long as it is much larger than communication and sensing radii of each sensor. This means that our results may be potentially applied to more general 3D surfaces although the results are derived on sphere. This problem will be investigated in our future work.

APPENDIX A PROOF OF LEMMA 1

Proof: The second inclusion is trivial because for any

k-simplex [v 0 , v 1 , • • • , v k ] ∈ Č(2)
Rs (V), it means the sensing ranges of these nodes have a common intersection, so the

pairwise distance d(v i , v j ) ≤ 2R s for all 0 ≤ i < j ≤ k, which means [v 0 , v 1 , • • • , v k ] ∈ R (2) 2Rs (V).
As for the first inclusion, it is clear that R [START_REF] Mo | Canopy closure estimates with greenorbs: sustainable sensing in the forest[END_REF] Rc (V) and Č [START_REF] Mo | Canopy closure estimates with greenorbs: sustainable sensing in the forest[END_REF] Rs (V) contain the same 0-simplices. It is also easy to see that all 1-simplices in R

(2) Rc (V) must also be in Č( 2)

Rs (V) since for any 1-simplex [v i , v j ] with distance d(v i , v j ) ≤ R c ≤ R arccos([3 cos 2 (R s /R) -1]/2) < R arccos(2 cos 2 (R s /R) - 1) = 2R s ,
it means that the sensing ranges of the two nodes have a common intersection. So we only need to prove that all 2-simplices in R

(2) Rc (V) must be in Č( 2) Rs (V). It is equivalent to say that for any three nodes with pairwise great circle distance no larger than R c , their sensing ranges must have a common intersection.

Assume a 2-simplex

[v 0 , v 1 , v 2 ] ∈ R (2)
Rc (V), then the three nodes v 0 , v 1 and v 2 must determine a plane α. We consider the spherical cap on S2 cut off by the plane α. Since R c < R, the spherical cap must be on a hemisphere. It is easy to see that the intersection of the plane α and sphere S 2 is a circle c. Let O 1 be the center of circle c, O be the center of S 2 , P be the intersection of line OO 1 and S 2 .

Using spherical coordinates, we assume the point P has a spherical coordinate (R, 0, 0). P may be inside 2 or outside the spherical triangle v 0 v 1 v 2 , which is shown in Figure 10 It can be seen that P has the same great circle distance to v 0 , v 1 and v 2 , denoted by d p . If P is inside the spherical triangle v 0 v 1 v 2 , as shown in Figure 10(a), then we can prove d p ≤ R s . Since P lying inside the spherical triangle v 0 v 1 v 2 means β + γ + δ = 2π, there must be one angle no smaller than 2π/3. Without loss of generality, assume β ≥ 2π/3. According to the spherical law of consines, we have cos

(β) = cos(d01/R)-cos 2 (dp/R) sin 2 (dp/R) ≤ -1/2 ⇒ cos(d 01 /R) ≤ [3 cos 2 (d p /R) -1]/2. In addition, d 01 ≤ R c ≤ R arccos([3 cos 2 (R s /R) -1]/2) ⇒ cos(d 01 /R) ≥ [3 cos 2 (R s /R) -1]/2, and 0 < d 01 /R, d p /R < π/2, so we have [3 cos 2 (R s /R) -1]/2 ≤ [3 cos 2 (d p /R) -1]/2 ⇒ d p ≤ R s , which means the point P is a common intersection of sensing ranges of v 0 , v 1 and v 2 , so [v 0 , v 1 , v 2 ] ∈ Č(2) Rs (V).
If P is outside the spherical triangle v 0 v 1 v 2 , as shown in Figure 10(a), it indicates that the spherical triangle v 0 v 1 v 2 must be contained in half of the spherical cap. Assume v 0 , v 1 and v 2 have spherical coordinates (R, θ, ϕ 0 ), (R, θ, ϕ 1 ) and (R, θ, ϕ 2 ), where θ ∈ (0, π/2), ϕ 0 < ϕ 1 < ϕ 2 , then we have ϕ 1ϕ 0 , ϕ 2ϕ 1 , ϕ 2ϕ 0 ∈ (0, π). Using d 01 , d 12 , d 02 to denote the pairwise great circle distances between v 0 , v 1 , v 2 , then according to the spherical law of consines, we have

cos(d 01 /R) = cos 2 θ + sin 2 θ cos(ϕ 1 -ϕ 0 ) (19) cos(d 12 /R) = cos 2 θ + sin 2 θ cos(ϕ 2 -ϕ 1 ) (20) cos(d 02 /R) = cos 2 θ + sin 2 θ cos(ϕ 2 -ϕ 0 ) (21)
In addition, we use σ to denote the angle between two arcs v0 v 1 and v0 v 2 , M to denote the middle point of the arc v0 v

cos d 1M R = cos d 01 R cos d 0M 2R + sin d 01 R cos d 0M 2R cos σ (23)
From ( 22) and ( 23), we can obtain

cos d 1M R = cos(d 01 /R) + cos(d 12 /R) 2 cos(d 02 /(2R)) (24)
Consequently

cos d 1M R -cos d 0M R = cos d01 R + cos d12 R -cos d02 R -1 2 cos(d 02 /(2R)) (25)
From ( 19), ( 20), ( 21) and ( 25), we get

cos d 1M R -cos d 0M R = sin 2 θ cos ϕ2-ϕ0
Rc (V) must be in Č( 2) Rs (V). Consequently the first inclusion is proved.

APPENDIX B PROOF OF THEOREM 1

Proof: We first prove the lower bound. It can be obtained from (2) that

p(λ) > P{ {n1,n2}⊆Φ\{τ0(Φ)} T (τ 0 , n 1 , n 2 )}
So for the lower bound, we only consider the first case that the closest node τ 0 must contribute to a spherical triangle which bounds a spherical triangular hole containing the point N .

Using spherical coordinates, we assume the closest node τ 0 lies on (R, α 0 , 0) and use |S| to denote the area of the set S, then we can get the distribution of α 0 as

F α0 (θ 0 ) = P (α 0 ≤ θ 0 ) = 1 -e -λ|C(N,Rθ0)| ( 27
)
since the event α 0 > θ 0 means that the spherical cap C(N, Rθ 0 ) does not contain any nodes from the process, which is given by the void probability e -λ|C(N,Rθ0)| . Furthermore, |C(N, Rθ 0 )| can be given as

|C(N, Rθ 0 )| = θ0 0 2π 0 R 2 sin θdϕdθ = 2πR 2 (1 -cos θ 0 ) (28
) From ( 27) and ( 28), we can get the density of τ 0 F α0 (dθ 0 ) = 2πλR 2 sin θ 0 e -λ|C(N,Rθ0)| dθ 0

The integration range for θ 0 can be easily obtained. According to Lemma 4, we have R

s < Rθ 0 ≤ R arccos [1 + 2 cos(R c /R)]/3, so R s /R < θ 0 ≤ θ 0u = arccos [1 + 2 cos(R c /R)]/3.
Therefore the probability of the first case can be given as

P{ {n1,n2}⊆Φ\{τ0(Φ)} T (τ 0 , n 1 , n 2 )} = θ0u Rs/R P{ {n1,n2}⊆Φ ′ θ 0 T ((R, θ 0 , 0), n 1 , n 2 )}F α0 (dθ 0 ) (30)
where Φ ′ θ0 is the restriction of Φ in C(N, R c )\C(N, Rθ 0 ). Once the node τ 0 is determined, a second node τ 1 must lie in the shadow region A + shown in Figures 3 or 4, and a third node τ 2 must lie in the region S -shown in Figures 4 or 5, as illustrated in Section IV-B. The node τ 1 = (R, θ 1 , ϕ 1 ) is assumed to have the smallest azimuth angle in A + , which means that there should be no nodes with a azimuth angle less than ϕ 1 in A + , that is to say no nodes are in the region

S + (τ 0 , τ 1 ) = S + (α 0 , ϕ 1 ) = A + H + (ϕ 1 )
Since the intensity measure of the Poisson point process in spherical coordinates is λR 2 sin θdθdϕ, the density F τ1 of τ 1 can be given as

F τ1 (dθ 1 , dϕ 1 ) = λR 2 sin θ 1 e -λ|S + (α0,ϕ1)| dθ 1 dϕ 1 (31)
Then we derive the integration domain D(α 0 ) with respect to parameters (θ 1 , ϕ 1 ). Consider the case shown in Figure 3, assume the point M 2 has the spherical coordinate (R, α 0 , ϕ m ), ϕ m ∈ (0, π). Since the great circle distance between τ 0 and M 2 is R c , then according to the spherical law of consines, we have cos

(R c /R) = cos 2 α 0 + sin 2 α 0 cos ϕ m ⇒ ϕ m (α 0 ) = arccos[(cos(R c /R) -cos 2 α 0 )/(sin 2 α 0 )].
It can be seen that points M 1 and Q have the spherical coordinates (R, α 0 , 2πϕ m (α 0 )) and (R, α 0 , 2ϕ m (α 0 )) respectively, where Q is one intersection point between bases of spherical caps C(N, Rα 0 ) and C(M 2 , R c ). Thus the integration range for ϕ 1 is [2πϕ m (α 0 ), 2ϕ m (α 0 )]. In addition, assume any point with great circle distance R c to τ 0 has the spherical coordinate (R, θ t , ϕ t ), still using the spherical law of consines, we have cos(R c /R) = cos α 0 cos θ t + sin α 0 sin θ t cos ϕ t ⇒ θ t (α 0 , ϕ t ) = arccos[cos(R c /R)/ 1sin 2 α 0 sin 2 ϕ t ] + arctan(cos ϕ t tan α 0 ). Similarly, assume any point with great circle distance R c to M 2 has the spherical coordinate

(R, θ ′ t , ϕ ′ t ), we can obtain θ ′ t (α 0 , ϕ ′ t ) = arccos[cos(R c /R)/ » 1 -sin 2 α 0 sin 2 (ϕ ′ t -ϕ m (α 0 ))] + arctan(cos(ϕ ′ t -ϕ m (α 0 )) tan α 0 ).
Then the integration range for θ 1 is [α 0 , θ 1u (α 0 , ϕ 1 )], where θ 1u (α 0 , ϕ 1 ) = min{θ 1u1 (α 0 , ϕ 1 ), θ 1u2 (α 0 , ϕ 1 )}, θ 1u1 (α 0 , ϕ 1 ) = θ t (α 0 , ϕ 1 ), θ 1u2 (α 0 , ϕ 1 ) = θ ′ t (α 0 , ϕ 1 ). Consider the case shown in Figure 4, the derivation of the integration domain D(α 0 ) is the same as the case shown in Figure 3. In this case, the point M has the spherical coordinate (R, α 0 , π), and the integration range for ϕ

1 is [π, 2π]. If we define ϕ m (α 0 ) = ® π if Rs R < α 0 ≤ Rc 2R arccos cos Rc R -cos 2 α0 sin 2 α0
othewise then the two cases can be regarded as the same in terms of the integration domain D(α 0 ). Furthermore, |S + (α 0 , ϕ 1 )| can be expressed as

|S + (α 0 , ϕ 1 )| = ϕ1 2π-ϕm(α0) θ1u(α0,ϕ) α0 R 2 sin θdθdϕ
As illustrated in Section IV-B, assume only τ 0 , τ 1 and nodes in S -(τ 0 , τ 1 ) can contribute to the spherical triangle which bounds a spherical triangular hole containing the point N , we can get a lower bound of the probability that the point N is inside a spherical triangular hole. Based on the assumption, we have

P{ {n1,n2}⊆Φ ′ θ 0 T ((R, θ 0 , 0), n 1 , n 2 )} > P{ n2⊆Φ ′ θ 0 S -(τ0,τ1) T ((R, θ 0 , 0), τ 1 , n 2 )} = D(θ0) P{ n 2 ⊆Φ ′ θ 0 S -(θ 0 ,θ 1 ,ϕ 1 ) T ((R, θ 0 , 0), (R, θ 1 , ϕ 1 ), n 2 )} F τ1 (dθ 1 , dϕ 1 ) = D(θ0) P{Φ ′ θ0 (S -(θ 0 , θ 1 , ϕ 1 )) > 0}F τ1 (dθ 1 , dϕ 1 ) = D(θ0) (1 -e -λ|S -(θ0,θ1,ϕ1)| )F τ1 (dθ 1 , dϕ 1 ) (32)
where |S -(θ 0 , θ 1 , ϕ 1 )| can be expressed as 12), ( 4) to [START_REF] Ghrist | Coverage and hole-detection in sensor networks via homology[END_REF], we can find that they are very similar. If we can show that each item related with R in (3) and (4) tends to its counterpart in [START_REF] Silva | Coverage in sensor networks via persistent homology[END_REF] and ( 13) when R → ∞, then it is easy to prove Theorem 2. For convenience, let θ 0 = r 0 /R, θ 1 = r 1 /R, ϕ ′ 1 = π + ϕ 1 . Proof: First, we have According to (35), comparing (5) to ( 14) and ( 15), we can get

|S -(θ 0 , θ 1 , ϕ 1 )| = ϕm ϕ 2l θ2u
ϕ l (r 0 ) = π -lim R→∞ ϕ m (θ 0 ) (36) ϕ u (r 0 ) = lim R→∞ 2ϕ m (θ 0 ) -π (37)
Still using l'Hôpital's rule, we can get the following results. The detailed calculation is omitted due to space limitation. where θ 1u1 (θ 0 , ϕ 1 ) and θ 1u2 (θ 0 , ϕ 1 ) are shown in [START_REF] Huang | The coverage problem in a wireless sensor network[END_REF] and [START_REF] Huang | The coverage problem in three-dimensional wireless sensor networks[END_REF]. From (38) and (39), comparing (6) to ( 16), we have

lim R→∞ Rθ 1u (θ 0 , ϕ 1 ) = R 1 (r 0 , ϕ ′ 1 ) (40)
From ( 36), (37) and (40), comparing [START_REF]Coverage verification without location information[END_REF] to [START_REF] Tahbaz-Salehi | Distributed coverage verification in sensor networks without location information[END_REF] and by some simple replacement, we can obtain

Fig. 1 .

 1 Fig. 1. 0-, 1-and 2-simplex

Fig. 2 .

 2 Fig. 2. (a) a WSN, (b) Čech complex, (c) Rips Complex under Rc = 2Rs, (d) Rips Complex under Rc = 2.5Rs

  Rα 0 ). In addition, considering the great circle distance between n 1 and n 2 should be at most R c and the point N should be inside the spherical triangle formed by τ 0 , n 1 and n 2 , n 1 must lie in the shadow region A + shown in Figures3 or 4under different situations. In the case R arccos([3 cos 2

Fig. 3 . 3 Fig. 4 .

 334 Fig. 3. Illustration of region A + in the case R arccos([3 cos 2 (Rs/R) -1]/2) < Rc ≤ 2Rs or in the case Rc > 2Rs, Rc/(2R) < α 0 ≤ arccos [1 + 2 cos(Rc/R)]/3

Fig. 6 .

 6 Fig. 6. Illustrations of regions S ′ + and S ′ -(a) in the case R arccos([3 cos 2 (Rs/R) -1]/2) < Rc ≤ 2Rs or in the case Rc > 2Rs, Rc/(2R) < α 0 ≤ arccos [1 + 2 cos(Rc/R)]/3; (b) in the case Rc > 2Rs, Rs/R < α 0 ≤ Rc/(2R)

Fig. 7 .

 7 Fig. 7. Proportion of the area of spherical triangular holes under R = 10Rs. (a) simulation results and lower bounds; (b) simulation results and upper bounds; (c) simulation results for psec(λ)

Fig. 8 .

 8 Fig. 8. Comparison of the proportion of the area of spherical triangular holes (a) comparison of simulation results; (b) comparison of lower bounds; (c) comparison of upper bounds

Fig. 9 .

 9 Fig. 9. Simulation results for psec(λ)

  (a) and 10(b) respectively.

Fig. 10 .

 10 Fig. 10. Illustrations of P and spherical triangle v 0 v 1 v 2 : (a) P is inside the spherical triangle v 0 v 1 v 2 ; (b) P is outside the spherical triangle v 0 v 1 v 2 .

2

 2 and d 0M , d 1M to denote great circle distances between v 0 , v 1 and M . It can be seen d 0M = d 02 /2. Similarly, we have cos σ = cos(d 12 /R)cos(d 01 /R) cos(d 02 /R) sin(d 01 /R) sin(d 02 /R)(22)

  0 < ϕ 1ϕ 0 , ϕ 2ϕ 1 , ϕ 2ϕ 0 < π and 0 < d 1M /R, d 0M /R, d 02 /R < π/2, it can be obtained from (26) d 1M < d 0M ≤ R c /2 < R s , which means the point M is a common intersection of the sensing ranges of v 0 , v 1 and v 2 , so [v 0 , v 1 , v 2 ] ∈ Č(2) Rs (V).It means all 2-simplices in R

θ0 R 2 sin θ 2 dθ 2 dϕ 2 and ϕ 2l = ϕ 1 » 1 -

 211 arccos cos(R c /R)cos θ 1 cos θ 0 sin θ 1 sin θ 0 θ 2u = min{θ 1u1 , θ 2u2 } θ 2u2 = arccos cos(R c /R)/ sin 2 θ 0 sin 2 (ϕ 2ϕ 1 ) + arctan(cos(ϕ 2ϕ 1 ) tan θ 1 )Therefore, from (29), (30), (31) and (32), the lower bound shown in (3) can be derived.As for the upper bound, replace |S -(θ 0 , θ 1 , ϕ 1 )| by |S -(θ 0 , θ 0 , ϕ 1 )|, we can get the upper bound as illustrated in Section IV-B.APPENDIX C PROOF OF THEOREM 2Comparing (3) to (

= R s lim x→0 3 cos x sin x 1 -

 1 lim R→∞ R arccos([3 cos 2 (R s /R) -1]/2) =R s lim x→0 arccos([3 cos 2 (x) -1]/2) x (let x = R s /R) ([3 cos 2 (x) -1]/2) 2 =R s lim x→0 6 cos x sin x (3 -3 cos 2 x)(1 + 3 cos 2 x) = √ 3R s(33)where (a) follows from l'Hôpital's rule. From (33), we know that when R → ∞, the conditionR c > R arccos([3 cos 2 (R s /R) -1]/2) is equivalent to the condition R c > √ 3R s . Similarly, we can get lim R→∞ cos(R c /R)cos 2 θ 0 )/ sin 2 θ 0 ] = arccos( lim R→∞ cos(R c /R)cos 2 (r 0 /R) sin 2 (r 0 /R) ) 0 /R 2 sin(r 0 /R) cos(r 0 /R) ) = arccos(1 -R 2 c /(2r 2 0 )) (b) = π -2 arccos(R c /(2r 0 ))(35)where (a) uses l'Hôpital's rule and (b) follows from cos(π -2 arccos(R c /(2r 0 ))) = 1 -R 2 c /(2r 2 0 ) and 0 ≤ π -2 arccos(R c /(2r 0 )) ≤ π.

sin 2 ϕ ′ 1 -

 1 r 0 cos ϕ ′ 1 (38) lim R→∞ Rθ 1u2 (θ 0 , ϕ 1 ) = » R 2 cr 2 0 sin 2 (ϕ ′ 1 + ϕ l (r 0 )) (39) + r 0 cos(ϕ ′ 1 + ϕ l (r 0 ))

2 ( 1 -r 1 R×

 211 lim R→∞ |S + (θ 0 , ϕ 1 )| = |S + (r 0 , ϕ ′ 1 )| (41) Similarly, we get lim R→∞ |S -(θ 0 , θ 1 , ϕ 1 )| = |S -(r 0 , r 1 , ϕ ′ 1 )| (42) where |S -(θ 0 , θ 1 , ϕ 1 )| and |S -(r 0 , r 1 , ϕ ′ 1 )| are shown in (11) and[START_REF] Liu | A study of the coverage of large-scale sensor networks[END_REF].In addition, from (9), we havelim R→∞ |C(N, Rθ 0 )| = lim R→∞ 2πR cos(r 0 /R)) = πr 2 0(43) Finally, using (34), (36), (37), (40), (41), (42) and (43), we can obtain from (3× e -λπr 2 0 e -λ|S + (r0,ϕ ′1 )| × (1e -λ|S -(r0,r1,ϕ ′ 1 )| )dr 1 e -λ|S + (r0,ϕ ′ 1 )| (1e -λ|S -(r0,r1,ϕ ′ 1 )| )r 1 dr 1 = p ′ l (λ) Similarly, we can get lim R→∞ p u (λ) = p ′ u (λ).Tech. His main research interests lie in performance evaluation in wireless networks (RRM, scheduling, handover algorithms, radio metrology). His current investigations address mainly three issues: a) the design of distributed sensing algorithms for cognitive radio b) distributed coverage holes detection in wireless sensor networks c) the definition of analytical models for the planning and the dimensioning of cellular systems. He has published several papers on different international journals and conferences. He is also an IEEE senior member and he is co-author of several books on 3G and 4G systems. Laurent Decreusefond is a former student of Ecole Normale Supérieure de Cachan. He obtained his Ph.D. degree in Mathematics in 1994 from Telecom ParisTech and his Habilitation in 2001. He is currently a Professor in the Network and Computer Science Department, at Telecom ParisTech. His main fields of interest are the Malliavin calculus, the stochastic analysis of long range dependent processes, random geometry and topology and their applications. With P. Moyal, he co-authored a book about the stochastic modelling of telecommunication systems.

TABLE I MAIN

 I

NOTATIONS symbols meaning Rs sensing radius of each sensor Rc communication radius of each sensor R the radius of sphere where sensors are deployed V the set of sensor locations sv the sensing range of the sensor located at v S collection of sensing ranges of sensors in V Č(2)

  Lemma 2. For any point on S 2 , it is inside a spherical triangular hole if and only if the following two conditions are satisfied: 1) the great circle distance between the point and its closest node is larger than R s . 2) the point is inside a spherical triangle: the convex hull of three nodes with pairwise great circle distance less than or equal to R c . Lemma 3. If there exists a point O which is inside a spherical triangular hole, then R s < R arccos [1 + 2 cos(R c /R)]/3.

	Proof: According to Definition 3, if there is a point O
	inside a spherical triangular hole, then there exists a 2-simplex
	σ ∈ R (2)

It is a non-trivial task to derive a closed-form expression for psec(λ). Furthermore, we find that it is much less than the closed-form part in upper bound pu(λ) and it has little impact on the derived bound. We thus get it by simulations.

It also includes the case that P is on one arc of the spherical triangle v 0 v 1 v 2 .