J.-M Nocquet
email: nocquet@geoazur.unice.fr

C Sue

A Walpersdorf

T Tran

N Lenôtre

P Vernant

M Cushing

F Jouanne

F Masson

S Baize

J Chéry

P A Van Der Beek

Present-day uplift of the western Alps

Collisional mountain belts grow as a consequence of continental plate convergence and eventually disappear under the combined effects of gravitational collapse and erosion. Using a decade of GPS data, we show that the western Alps are currently characterized by zero horizontal velocity boundary conditions, offering the opportunity to investigate orogen evolution at the time of cessation of plate convergence. We find no significant horizontal motion within the belt, but GPS and levelling measurements independently show a regional pattern of uplift reaching ~2.5 mm/yr in the northwestern Alps. Unless a low viscosity crustal root under the northwestern Alps locally enhances the vertical response to surface unloading, the summed effects of isostatic responses to erosion and glaciation explain at most 60% of the observed uplift rates. Rock-uplift rates corrected from transient glacial isostatic adjustment contributions likely exceed erosion rates in the northwestern Alps. In the absence of active convergence, the observed surface uplift must result from deep-seated processes.

The western Alps, the highest topography of Europe, formed during Oligocene-Miocene times, as a consequence of the convergence and indentation of the Adriatic microplate toward Europe 1 . As much as 280 km of shortening was accommodated by underthrusting of the European margin beneath the Adriatic microplate 1-3 . This process resulted in crustal thickening, nappe stacking, and exhumation of crystalline basement, contributing to the building of the present-day topography. During the last million year, the end of active subduction in the Apennines 4 led to a change of the regional plate-kinematics, with the progressive development of extension in the core of the Apennines and counter-clockwise rotation of the Adriatic micro-plate 5 . A decade of continuous GPS measurements show that, with respect to the Alpine foreland, the GPS sites in the western Po plain have an averaged residual motion of 0.1 mm/yr and provide an upper bound of 0.3 mm/yr (95% confidence level) for possible right-lateral strike slip motion across the western Alps (Supplementary Information). Similarly, south of the western Alps, sites in Corsica and Sardinia show less than 0.4 mm/yr of shortening with respect to the southern western Alps 6 . Therefore, the western Alps is presently a mountain range with virtually zero horizontal velocity boundary conditions, offering a unique opportunity to evaluate the contribution of processes unrelated to horizontal tectonics to the evolution of orogens.

In addition to continuous GPS data, we use levelling data spanning a century in order to study the present-day vertical motion in the western Alps and its surroundings. We show in the Supplementary Information that both data sets have an average internal precision of 0.2 mm/yr and are mutually consistent at a level of 0.3 mm/yr over the studied area. GPS sites located west of the Alpine foreland all show zero vertical rates (± 0.2 mm/yr) and therefore define a stable reference frame that we use to express regional vertical rates.

 (1) a 80 × 60 km 2 wide area shows uplift rates exceeding 2 mm/yr in the core of the northwestern Alps (Mont-Blanc and Vanoise massifs), decreasing outward; (2) the southern western Alps (Pelvoux, Queyras and Mercantour massifs) show significantly smaller rates of uplift of the order of 0.5 mm/yr; (3) subsidence reaching 1 mm/yr is observed in the Rhone delta. GPS data further show subsidence rates in the Po plain up to 1.5 mm/yr, increasing eastward 7 .

Unlike horizontal motion that is predominantly controlled by tectonic processes, vertical rates may result from highly diverse mechanisms. At the centennial to millennial time scale, the retreat of Alpine glaciers since the Last Glacial Maximum (LGM) unloads the crust and induces visco-elastic relaxation of the crust-mantle system, still influencing the present-day vertical rates. Modelling results of the Glacial Isostatic Adjustment (GIA) strongly depends on the chosen rheology, the ice cap thickness at LGM and its melting history, all parameters having large uncertainties. In the western Alps, most GIA models predict less than ~0.3 mm/yr of present-day uplift of the Alpine range with respect to its foreland [START_REF] Gardi | Present-day vertical isostatic readjustment of the Western Alps revealed by numerical modelling and geodetic and seismotectonic data[END_REF][START_REF] Stocchi | Isostatic rebound following the Alpine deglaciation: impact on the sea level variations and vertical movements in the Mediterranean region[END_REF] , but values reaching 1.8 mm/yr have recently been proposed for a 2D model with a low viscosity (10 21 Pa.s) crustal root beneath the northwestern Alps [START_REF] Chéry | Ice cap melting and low-viscosity crustal root explain the narrow geodetic uplift of the Western Alps[END_REF] . At the centennial scale, visco-elastic mid-crustal relaxation induced by the shrinkage of glaciers since the Little Ice Age (LIA) induces a small 0.1-0.2 mm/yr regional signal in the western Alps [START_REF] Barletta | Glacier shrinkage and modeled uplift of the Alps[END_REF] . Finally, at the decadal scale, the elastic response to a water-equivalent loss rate of nearly 1 m/yr for glaciers in the French western Alps induces a small regional uplift of 0.2 mm/yr but locally reaching 0.9 mm/yr in the Mont-Blanc area [START_REF] Barletta | Glacier shrinkage and modeled uplift of the Alps[END_REF] . Depending on the model, the summed effects of GIA contributions to the present-day vertical velocities yield a regional signal in the northwestern Alps of ~0.5 mm/yr, possibly reaching ~2 mm/yr in the areas of the largest glaciers (Fig. 2d).

At the million-year timescale, erosion removes rocks from the inner, higher part of mountain ranges, transports the materials by glaciers and rivers, and deposits them in sedimentary basins and major delta fans surrounding the orogen. The response to this mass redistribution implies rock uplift and regional surface height lowering in the erosional areas and rock subsidence and regional surface height increase where sediments load the crust. The amplitude of the response to unloading depends on the density contrast between the crust and the mantle, the characteristic size of the load perturbation and the effective elastic thickness of the lithosphere [START_REF] Braun | Topographic relief driven by variations in surface rock density[END_REF] , but rock uplift reaching 60-80% of the surface unloading are typical values for mountain belts [START_REF] Champagnac | Quaternary erosion-induced isostatic rebound in the western Alps[END_REF] . It has been proposed that the average sediment discharge from the western Alps to their surrounding basins increased by a factor of two since 5 Myr and a factor of three during the last Myr compared to its constant averaged value between 12 Myr and 5 Myr ago [START_REF] Kuhlemann | Post-collisional sediment budget history of the Alps: Tectonic versus climatic control[END_REF] . The related sedimentary discharge for the last Myr has been estimated to be 4.8 × 10 5 km 3 /Myr with an uncertainty of 25% for the western Alps [START_REF] Champagnac | Quaternary erosion-induced isostatic rebound in the western Alps[END_REF][START_REF] Kuhlemann | Post-collisional sediment budget history of the Alps: Tectonic versus climatic control[END_REF] , a value consistent with estimates of excavation of glacial valleys from geophysical relief as well as independent high-resolution thermochronology data [START_REF] Valla | Significant increase in relief of the European Alps during mid-Pleistocene glaciations[END_REF][START_REF] Glotzbach | Episodic exhumation and relief growth in the Mont Blanc massif, Western Alps from numerical modelling of thermochronology data[END_REF] . This sediment flux together with geophysical relief [START_REF] Small | Pleistocene relief production in Laramide mountain ranges, western United States[END_REF] was used to derive the spatial distribution of rock uplift for the western Alps assuming an elastic response to erosional unloading since 1 Myr [START_REF] Champagnac | Quaternary erosion-induced isostatic rebound in the western Alps[END_REF] . Under the assumption that the erosion rate is the same at present as during the last Myr, the model predicts uplift rates of 0.3-0.5 mm/yr within the western Alps (Fig. 2e) with the highest rates being located in the core of the northern part of the belt. Although the pattern of predicted uplift is qualitatively similar to the geodetic results (Fig. 2a-c,e), Myr-scale erosion explains only 50% of the present-day regional uplift and 30% of the present-day high vertical rate in the northwestern Alps.

Large fluctuations in erosion and sedimentation rates are expected to occur between glaciations and inter-glacial periods, the highest rates being expected during the deglaciation period [START_REF] Koppes | The relative efficacy of fluvial and glacial erosion over modern to orogenic timescales[END_REF] . As a consequence, it is uncertain whether Myr-scale averaged erosion rates can be used to predict the present-day geodetic rates. At the millennial-scale (~0.5-2.2 kyr), catchment-wide erosion rates derived from in situ produced cosmogenic [START_REF] Chéry | Ice cap melting and low-viscosity crustal root explain the narrow geodetic uplift of the Western Alps[END_REF] Be independently indicate erosion rates in the range 0.27-1.33 mm/yr in the core of the western Alps [START_REF] Glotzbach | Deciphering the driving forces of erosion rates on millennial to millionyear timescales in glacially impacted landscapes: An example from the Western Alps[END_REF][START_REF] Delunel | Frost-cracking control on catchment denudation rates: Insights from in situ produced 10Be concentrations in stream sediments (Ecrins-Pelvoux massif, French Western Alps)[END_REF] . Such estimates lead to an average erosion rate of ~0.5 mm/yr similar or slightly higher than Myr-scale average estimates. Finally, at the decadal scale, erosion rates estimated from river loads and reservoir fills indicate a mean erosion rate of 0.32 mm/yr at the scale of the European Alps, reaching 0.58 mm/yr in the northwestern Alps 30% lower than the estimate derived from cosmogenic [START_REF] Chéry | Ice cap melting and low-viscosity crustal root explain the narrow geodetic uplift of the Western Alps[END_REF] Be estimates for the same area [START_REF] Hinderer | River loads and modern denudation of the Alps -A review[END_REF] . Thus, there is no evidence that present-day erosion rates are significantly higher than their Myr-scale estimates. The discharge rate estimates during the last Myr for the Rhone fan and the Po plain are 1.1 × 10 4 and 1.3 × 10 4 km 3 /Myr respectively [START_REF] Kuhlemann | Post-collisional sediment budget history of the Alps: Tectonic versus climatic control[END_REF] . Taking an area of ~10 5 km 2 for the Rhone fan yields a sedimentation rate of ~1.1 mm/yr and a resulting isostatic subsidence rate of ~0.7-0.9 mm/yr. This estimate is in agreement with the subsidence rates found in and around the Rhone delta observed from both levelling and GPS data, within their respective uncertainties. For the Po plain, taking an area of 5 × 10 4 km 2 , the same calculation leads to a sedimentation rate of ~2.6 mm/yr. This value is an average over the Po basin, but sedimentation rates are about 3 times larger in the eastern Po plain than in the west [START_REF] Kuhlemann | Post-collisional sediment budget history of the Alps: Tectonic versus climatic control[END_REF] . As a consequence, the expected subsidence rate induced by sediment loading is expected to increase from ~1 mm/yr in the western part of the Po plain to ~2 mm/yr in its central part and 3.5-4.0 mm/yr in its easternmost part. These values are again in good agreement with our GPS observations for the western Po plain and also with GPS-derived subsidence rates derived for the eastern Po plain [START_REF] Serpelloni | Vertical GPS ground motion rates in the Euro-Mediterranean region: New evidence of velocity gradients at different spatial scales along the Nubia-Eurasia plate boundary[END_REF] . These simple comparisons suggest that proposed Myr-scale erosion/sedimentation budgets are reasonable first-order estimates of the present-day erosion rates.

Figure 2g,h show the residual GPS and levelling rates once corrected for all surface-process contributions (erosion and GIA) according to previously published models at the scale of the western Alps. While the summed contributions show a similar pattern to the geodetically observed rock-uplift map, the isostatic response to erosion and GIA only explain at most 60% of the highest uplift rates in the central and northern western Alps. The long-term surface uplift rate, defined as the difference between rock uplift rate corrected from GIA transient contributions and erosion rate determines the amount of work against gravity within the orogen [START_REF] England | Surface uplift, uplift of rocks, and exhumation of rocks[END_REF] . Unless erosion rates and/or GIA contributions would have been underestimated by a factor of at least two, our results suggest that surface uplift is positive at least in the northwestern Alps. Since the surface uplift rates are several times larger than horizontal velocities, they must result from upward tractions applied at the base of the Alpine lithosphere. This hypothesis is consistent with the analysis of gravimetric anomalies in the western Alps, which significantly depart from those predicted by the isostatic equilibrium or flexural elastic support of the plate [START_REF] Lyon-Caen | Constraints on the deep structure and dynamic processes beneath the Alps and adjacent regions from an analysis of gravity anomalies[END_REF] . As a consequence, the present-day topography is supported dynamically by more buoyant material underneath the range, also possibly promoting the present-day surface uplift.

Tomographic studies in the Alps support that view, as they image a large low velocity anomaly between depths of 90 and 150 km in the northwestern Alps [START_REF] Lippitsch | Upper mantle structure beneath the Alpine orogen from high-resolution teleseismic tomography[END_REF][START_REF] Fox | Rapid exhumation in the Western Alps driven by slab detachment and glacial erosion[END_REF] . Figure 3 shows that the low velocity anomaly overlies a high velocity anomaly interpreted as a detached remnant of the European oceanic lithosphere [START_REF] Lippitsch | Upper mantle structure beneath the Alpine orogen from high-resolution teleseismic tomography[END_REF] . There is a clear spatial correlation between the observed uplift pattern and the low-velocity zone both across and along the axis of the western Alpine arc. The replacement of dense by more buoyant material is consistent with normal upward traction at the base of the lithosphere that would induce uplift [START_REF] Gardi | Present-day vertical isostatic readjustment of the Western Alps revealed by numerical modelling and geodetic and seismotectonic data[END_REF][START_REF] Baran | The late Miocene to Holocene erosion pattern of the Alpine foreland basin reflects Eurasian slab unloading beneath the western Alps rather than global climate change[END_REF] . Furthermore, the development of a warm mantle anomaly underneath the western Alps is also expected to promote uplift through a progressive reduction of the equivalent elastic thickness (EET) of the lithosphere and low viscosity crustal root, then enhancing the surface response to deep buoyant material and surface related processes [START_REF] Chéry | Ice cap melting and low-viscosity crustal root explain the narrow geodetic uplift of the Western Alps[END_REF][START_REF] Bennett | Increasing long-wavelength relief across the southeastern flank of the Sierra Nevada, California[END_REF] .

Our geodetic results contradict several previously proposed models for the current deformation regime of the western Alps. Within the western Alps, the average horizontal velocities are 0.26 mm/yr (Supplementary Information). Thus, surface uplift rates in the northwestern Alps are one order of magnitude larger than horizontal velocities. The large ratio of uplift to horizontal rates rules out horizontal motions as the primary control on the present-day deformation in the western Alps [START_REF] Calais | Current strain regime in the Western Alps from continuous GPS measurements[END_REF] . It also excludes the hypothesis of crustal-or lithospheric-scale collapse of the mountain range [START_REF] Selverstone | Are the Alps Collapsing?[END_REF] which would imply crustal thinning and surface lowering, rather than the observed surface uplift. The crustal state of stress within the western Alps is characterized by widespread extension radial to the belt as indicated by normal faults, extensional focal mechanisms, local geodetic studies [START_REF] Sue | Extensional neotectonics around the bend of the Western/Central Alps: An overview[END_REF][START_REF] Walpersdorf | Coherence between geodetic and seismic deformation in a context of slow tectonic activity (SW Alps, France)[END_REF] , and extension seen in our GPS solution (Fig. 1b). The areas of extension appear to correlate with the most rapidly uplifting areas (Fig. 2i). Normal faulting would therefore contribute to accommodate the surface uplift-rate gradient driven by the deep dynamics and enhanced by erosion [START_REF] Vernant | Erosion-induced isostatic rebound triggers extension in low convergent mountain ranges[END_REF] , rather than large-scale gravitational collapse.

The western Alps illustrate a case of early post-collisional evolution. Assuming that the present-day boundary conditions have been set in place ca. 1 Myr ago 4 , our geodetic results do not detect any onset of lithospheric collapse. Although centennial-millennial timescale transient contributions of GIA cannot be ruled out as the dominant forcing to the present-day observed uplift, the good spatial correlation between geodetic results and exhumation rates [START_REF] Fox | Rapid exhumation in the Western Alps driven by slab detachment and glacial erosion[END_REF] advocates for processes persistent at the million year time scale. Erosion and asthenosphere-lithosphere interactions are therefore the processes controlling the longer-term orogen evolution in the absence of relative motion at the boundaries of the belt. In the western Alps, erosion, probably enhanced since mid-Pleistocene times [START_REF] Valla | Significant increase in relief of the European Alps during mid-Pleistocene glaciations[END_REF] , carves the valleys and increases the height of topographic peaks, but tends to lower the average surface regionally. Mantle-lithosphere interactions counteract and currently exceed this effect in the northwestern Alps. Our geodetic results suggest that orogens can still be growing in the aftermath of the collision stage.

Figure 1 .

 1 Figure 1. Location map and geodetic results. (a) Location map. Colour indicates the topography averaged using a 25 km-width Gaussian filter. MB: Mont Blanc massif. V: Vanoise massif. P: Pelvoux massif. Q: Queyras massif. M: Mercantour massif. (b) GPS Horizontal GPS velocity field. Error ellipses are at the 95% confidence level. (c) Adjusted levelling rates. Data are decimated every 10 km. (d) GPS vertical velocities. Black lines indicate 1-σ uncertainties. Orange, red and purple bars indicate uplift and blue ones subsidence. Levelling and GPS data are with respect to the Alpine foreland as described in the main text. Figure created with GMT v. 5.1 (http://gmt.soest.hawaii.edu/).

Figure 2 .

 2 Figure 2. Vertical rate maps and models predictions. (a) Vertical rate map from levelling data. (b) Vertical rate map from GPS data. (c) Levelling-GPS combined map of vertical rate. (d) Predicted uplift-rate map from all GIA contributions 9,11 . (e) Uplift-rate map predicted from the response to erosion 11 . (f) Predicted uplift-rate map from the sum of GIA and erosion contributions. (g) Residual geodetic rates once corrected for GIA and erosion contributions. (h) Same as g in map view. (i) Seismotectonic stress tensors 28 superimposed on Fig. 2c. Dashed line in panel h indicates the location of the profile shown in Fig. 3. Figure created with GMT v. 5.1 (http://gmt. soest.hawaii.edu/).

Figure 3 .

 3 Figure 3. Cross-section of vertical rates and deep structure beneath the northwestern Alps. Cross-section location is shown in Fig. 2h. (a) Uplift rates. Green and blue dots are levelling and GPS rates respectively, with error bars (95% confidence level) indicated by the thin black vertical lines. The pink-coloured fill shows the GPS-levelling combined uplift-rate profile from Fig. 2c. The yellow fill shows the summed prediction of GIA and erosion models from Fig. 2f. (b) Topography along the cross section averaged using a 50 km-width Gaussian filter. (c) Upper mantle tomographic model from ref. 24. Figure created using Matplotlib v. 1.4 (http:// matplotlib.org).

Scientific RepoRts | 6:28404 | DOI: 10.1038/srep28404

Acknowledgements

The RENAG GPS Network (http://renag.resif.fr) has been continuously supported by the CNRS-INSU as part of the National Observation Service Geodesy & Gravimetry. The RENAG network also benefited from support from RESIF (http://www.resif.fr). RESIF is a national Research Infrastructure from the French Ministry of higher education and research, involving 18 Research institutions and universities in France. RESIF is additionally supported by a grant from the French national research agency (ANR-11-EQPX-0040) and the French Ministry of ecology, sustainable development and energy. We acknowledge the work of all RENAG members for developing and maintaining the network. We thank the Institut de l′Information Géographique et Forestière (IGN) for providing the levelling data and Continuous GPS data from the RGP (http://rgp.ign.fr/). ORPHEON GNSS data were provided to the authors for scientific use in the framework of the GEODATA-INSU-CNRS convention. INGV, the Piemonte region and contributors to EUREF are acknowledged for the GPS data used in the present study.

Methods

The GPS data used in the study are freely available from http://renag.resif.fr and ftp://renag.unice.fr. The levelling data are subject to prior agreement from the IRSN and BRGM (edward.cushing@irsn.fr, n.lenotre@brgm.fr). GPS and levelling analysis codes are available on request from JMN. The GPS and levelling analysis are fully described in the Supplementary Information.

Author Contributions

J.-M.N. developed the levelling analysis software, did GPS analysis and wrote the paper. A.W., F.J., F.M. and T.T. contributed to the GPS analysis. C.S. commented on the tectonic discussion. M.C., S.B. and N.L. provided the levelling data. N.L. did levelling analysis. J.C. and P.V. commented on the GIA discussion. P.V.D.B. commented on the erosion results. All authors discussed the results, and edited the paper.

Additional Information

Supplementary information accompanies this paper at http://www.nature.com/srep Competing financial interests: The authors declare no competing financial interests.


Sébastien Bardin

Mickaël Delahaye

Nikolai Kosmatov

Michaël Marcozzi

Virgile Prevosto

Generic and Effective Specification of Structural Test Objectives

Keywords: Software and its engineering → Dynamic analysis, Software testing and debugging, Software reliability, Domain specific languages, white-box software testing, code coverage, test requirements, specification language

While a wide range of different, sometimes heterogeneous test coverage criteria have been proposed, there exists no generic formalism to describe them, and available test automation tools usually support only a small subset of them. We introduce a unified specification language, called HTOL, providing a powerful generic mechanism to define test objectives, which permits encoding numerous existing criteria and supporting them in a unified way. HTOL comes with a formal semantics and can express complex requirements over several executions (using a novel notion of hyperlabels), as well as alternative requirements or requirements over a whole program execution. A novel classification of a large class of existing criteria is proposed. Finally, a coverage measurement tool for HTOL objectives has been implemented. Initial experiments suggest that the proposed approach is both efficient and practical.

INTRODUCTION

Context. In current software engineering practice, testing [START_REF] Myers | The Art of Software Testing[END_REF][START_REF] Mathur | Foundations of Software Testing[END_REF][START_REF] Zhu | Software unit test coverage and adequacy[END_REF][START_REF] Ammann | Introduction to Software Testing[END_REF] remains the primary approach to find bugs in a piece of code. We focus here on white-box software testing, in which the tester has access to the source code -as it is the case for example in unit testing. As testing all the possible program inputs is intractable in practice, the software testing community has notably defined code-coverage criteria (a.k.a. adequacy criteria or testing criteria) [START_REF] Zhu | Software unit test coverage and adequacy[END_REF][START_REF] Ammann | Introduction to Software Testing[END_REF], to select test inputs to be used. In regulated domains such as aeronautics, these coverage criteria are strict normative requirements that the tester must satisfy before delivering the software. In other domains, coverage criteria are recognized as a good practice for testing, and a key ingredient of test-driven development.

A coverage criterion fundamentally specifies a set of test requirements or objectives, which should be fulfilled by the selected test inputs. Typical requirements include for example covering all statements (statement coverage criterion) or all branches in the code (decision coverage criterion). These requirements are essential to an automated white-box testing process, as they are used to guide the selection of new test cases, decide when testing should stop and assess the quality of a test suite (i.e., a set of test cases including test inputs). In automated white-box testing, a coverage measurement tool is used to establish which proportion of the requirements are actually covered by a given test suite, while a test generation tool tries to generate automatically a test suite satisfying the requirements of a given criterion. Problem. Dozens of code-coverage criteria have been proposed in the literature [START_REF] Zhu | Software unit test coverage and adequacy[END_REF][START_REF] Ammann | Introduction to Software Testing[END_REF], from basic control-flow or data-flow [START_REF] Laski | A data flow oriented program testing strategy[END_REF] criteria to mutations [START_REF] Demillo | Hints on test data selection: Help for the practicing programmer[END_REF] and MCDC [START_REF] Chilenski | Applicability of modified condition/decision coverage to software testing[END_REF], offering notably different ratios between testing thoroughness and effort. However, from a technical standpoint, these criteria are seen as very dissimilar bases for automation, so that most testing tools (coverage measurement or test generation) are restricted to a very small subset of criteria (cf. Table 1) and that supporting a new criterion is timeconsuming. As a consequence, the wide variety and deep sophistication of code-coverage criteria in the academic literature is barely exploited in practice, and academic criteria have a weak penetration into the industrial world. Goal and challenges. We intend to bridge the gap between the potentialities offered by the huge body of academic work on (code-)coverage criteria on one side, and their limited use in the industry on the other side. In particular, we aim at proposing a well-defined and unifying specification mechanism for these criteria, enabling a clear separation of concerns between the precise declaration of test requirements on one side, and the automation of white-box testing on the other side. This is a fruitful approach that has been successfully applied for example with SQL for databases and with temporal logics for model checking. This is also a challenging task as such a mechanism should be, at the same time: [START_REF] Abdurazik | Evaluation of three specification-based testing criteria[END_REF] well-defined, (2) very expressive (to encode test requirements from most existing criteria), and (3) amenable to automation (coverage measurement and test generation). Proposal. We introduce hyperlabels, a generic specification language for white-box test requirements. Technically, hyperlabels are a major extension of labels proposed by Bardin et al. [START_REF] Bardin | Efficient leveraging of symbolic execution to advanced coverage criteria[END_REF]. While labels can express a large range of criteria [START_REF] Bardin | Efficient leveraging of symbolic execution to advanced coverage criteria[END_REF] (including a large part of weak mutations [START_REF] Howden | Weak mutation testing and completeness of test sets[END_REF] and a weak variant of MCDC [START_REF] Pandita | Guided test generation for coverage criteria[END_REF]), they are still too limited in terms of expressiveness, not being able for example to express strong variants of MCDC [START_REF] Chilenski | Applicability of modified condition/decision coverage to software testing[END_REF] or most dataflow criteria [START_REF] Laski | A data flow oriented program testing strategy[END_REF]. In contrast, hyperlabels are able to encode all criteria from the literature [START_REF] Ammann | Introduction to Software Testing[END_REF] but full mutations [START_REF] Demillo | Hints on test data selection: Help for the practicing programmer[END_REF][START_REF] Howden | Weak mutation testing and completeness of test sets[END_REF].

We also propose a universal coverage measurement tool supporting hyperlabels, and demonstrate that the label-based test generation algorithm from [START_REF] Bardin | Efficient leveraging of symbolic execution to advanced coverage criteria[END_REF] yields acceptable (and automatic) coverage results for hyperlabels.

Contribution. The four main contributions of this paper are the following: 1. We introduce a novel taxonomy of coverage criteria (Section 3), orthogonal to both the standard classification [START_REF] Zhu | Software unit test coverage and adequacy[END_REF] and the one by Ammann and Offutt [START_REF] Ammann | Introduction to Software Testing[END_REF]. Our classification is semantical, based on the nature of the reachability constraints underlying a given coverage criterion. This view is sufficient for classifying all existing criteria but mutations, and yields new insights into coverage criteria, emphasizing the complexity gap between a given criterion and basic reachability. A visual representation of this taxonomy is proposed, the cube of coverage criteria 1 ; 2. We propose HTOL, a formal specification language for test objectives (Section 4) based on hyperlabels. While labels reside in the cube origin, our language adds new constructs in order to combine (atomic) labels, allowing us to encode any criterion from the cube taxonomy. We present the syntax of the language and give a formal semantics in terms of coverage. Finally, we give a few encodings of criteria beyond labels. Notably, HTOL can express subtle differences between the variants of MCDC (Section 4.4.1); 3. As a first application of hyperlabels, and in order to demonstrate their expressiveness, we provide in Section 5 a list of encodings for almost all code coverage criteria defined in the Ammann and Offutt book [START_REF] Ammann | Introduction to Software Testing[END_REF], including many criteria beyond labels (cf. Table 2). The only missing criteria are strong mutations and weak mutations, yet a large subset of weak mutations can be encoded [START_REF] Bardin | Efficient leveraging of symbolic execution to advanced coverage criteria[END_REF]. 4. As a second application of hyperlabels, and in order to demonstrate their practicality, we present the design and implementation of a universal and easily extensible code coverage measurement tool (Section 6) based on HTOL. The tool already supports in a unified way fourteen coverage criteria, including all criteria from Table 1 and six which are beyond labels. We report on several experiments demonstrating that the approach is efficient enough and combines well with label-based automatic test generation.

Potential impact. Hyperlabels provide a lingua franca for defining, extending and comparing criteria in a clearly documented way, as well as a specification language for writing universal, extensible and interoperable testing tools. By making the whole variety and sophistication of academic coverage criteria much more easily accessible in practice, hyperlabels help bridging the gap between the rich variety of academic results in criterion-based testing and their limited use in the industry. We intend to develop a test generation tool dedicated to hyperlabels in a middle term.

BACKGROUND

Basics: Programs, Tests and Coverage

We give here a formal definition of coverage and coverage criteria, following [START_REF] Bardin | Efficient leveraging of symbolic execution to advanced coverage criteria[END_REF].

Given a program P over a vector V of m input variables taking values in a domain D D1 ו • •×Dm, a test datum t for P is a valuation of V , i.e. t ∈ D. A test suite TS ⊆ D is a 1 By analogy to the λ-cube of functional programming. These definitions are generic and leave the exact definition of "covering" to the considered coverage criterion. For example, test objectives derived from the Decision Coverage criterion are of the form c (loc, cond) or c (loc, !cond), where cond is the condition of the branching statement at location loc, and t YP c if t reaches some (loc, S) such that cond evaluates to true (resp. false) in S.

Finally, for a test suite TS and a set C of test objectives, the coverage score of TS w.r.t. C is the ratio of the number of test objectives in C covered by TS to its cardinality |C|. The coverage score of TS w.r.t. a coverage criterion C is then its coverage score w.r.t. the set C = C(P ).

A Quick Tour of Coverage Criteria

A wide variety of criteria have been proposed in the literature [START_REF] Mathur | Foundations of Software Testing[END_REF][START_REF] Ammann | Introduction to Software Testing[END_REF][START_REF] Zhu | Software unit test coverage and adequacy[END_REF]. We briefly review in this section the main criteria used throughout the paper.

Control-flow graph coverage criteria include basic block coverage (BBC, equivalent to statement coverage), branch coverage (BC) and several path-based criteria (where each one specifies a particular set of paths to cover in the graph) such as edge-pair (EPC), prime path (PPC), basis path (BPC), simple/complete round trip (SRTC/CRTC) and complete/specified path (CPC/SPC) coverage.

Call graph coverage criteria include notably function coverage (FC, all the call graph nodes, i.e. each program function should be called at least once) and call coverage (FCC, all the graph edges, i.e. each function should be called at least once from each of its callers). [START_REF] Laski | A data flow oriented program testing strategy[END_REF] concerns checking that each value defined in the tested program is actually used, either by one of its possible uses (all-defs), or by all of them (all-uses), or even along any of its def-use paths (all-du-paths).

Data-flow coverage

Logic coverage criteria focus on exercising various truth value combinations for the logical predicates (i.e. branching conditions) of the tested program. The most basic criteria here are decision coverage (both values for each predicate, DC -equivalent to BC), (atomic) condition coverage (both values for each literal in each predicate, CC) and multiple condition coverage (all literal value combinations for each predicate, MCC). Advanced criteria include MCDC [START_REF] Chilenski | Applicability of modified condition/decision coverage to software testing[END_REF] and its variants [START_REF] Ammann | Coverage criteria for logical expressions[END_REF][START_REF] Ammann | Introduction to Software Testing[END_REF] GACC, CACC (masking MCDC) and RACC (unique-cause MCDC), as well as their inactive clause coverage counterparts GICC and RICC. Other criteria consider the disjunctive normal form of the predicates [START_REF] Ammann | Introduction to Software Testing[END_REF]Chap. 3.6], such as implicant coverage IC, unique true point coverage UTPC and corresponding unique true point and near false point pair coverage CUTPNFP [START_REF] Chen | Test case selection strategies based on boolean specifications[END_REF].

Finally, in mutation coverage [START_REF] Demillo | Hints on test data selection: Help for the practicing programmer[END_REF], test requirements address the ability to detect that each of slight syntactic variants of the tested program (the mutants) behaves differently from the original code. In strong mutation coverage (SMC), the divergence must be detected in the program outputs, whereas in weak mutation coverage (WMC) [START_REF] Howden | Weak mutation testing and completeness of test sets[END_REF] the divergence must be detected just after the mutation. Both SMC and WMC are very powerful coverage criteria [START_REF] Andrews | Is mutation an appropriate tool for testing experiments[END_REF][START_REF] Offutt | An empirical evaluation of weak mutation[END_REF].

Criterion Encoding with Labels

In previous work, Bardin et al. have introduced labels [6], a code annotation language to encode concrete test objectives, and shown that several common coverage criteria can be simulated by label coverage, i.e. given a program P and a criterion C, the concrete test objectives instantiated from C for P can always be encoded using labels. As our main contribution is a major extension of labels into hyperlabels, we recall here basic results about labels.

Labels. Given a program P , a label ℓ ∈ Labs is a pair loc, ϕ where loc is a location of P and ϕ is a predicate over the internal state at loc, that is, such that: (1) ϕ contains only variables and expressions defined at location loc in P , and (2) ϕ contains no side-effect expressions. There can be several labels defined at a single location, which can possibly share the same predicate. We say that a test datum t covers a label ℓ loc, ϕ in P , denoted t L YP ℓ, if there is a state s such that t reaches loc, s (i.e. t YP loc, s ) and s satisfies ϕ. An annotated program is a pair P, L where P is a program and L ⊆ Labs is a set of labels for P . Given an annotated program P, L , we say that a test suite TS satisfies the label coverage criterion (LC) for P, L , denoted TS L Y P,L LC, if TS covers every label of L (i.e. ∀ℓ ∈ L : ∃t ∈ TS : t L YP ℓ). Criterion Encoding. Label coverage simulates a coverage criterion C if any program P can be automatically annotated with a set of labels L in such a way that any test suite T S satisfies LC for P, L if and only if TS covers all the concrete test objectives instantiated from C for P .

It is shown in [START_REF] Bardin | Efficient leveraging of symbolic execution to advanced coverage criteria[END_REF] that label coverage can notably simulate basic-block coverage (BBC), branch coverage (BC) and decision coverage (DC), function coverage (FC), condition coverage (CC), decision condition coverage (DCC), multiple condition coverage (MCC) as well as the side-effect-free fragment of weak mutations. The encoding of GACC can also be deduced from [START_REF] Pandita | Guided test generation for coverage criteria[END_REF]. Figure 1 illustrates the simulation of some criteria with labels on sample code. The main benefit of labels is to unify the treatment of test requirements belonging to different classes of coverage criteria in a transparent way, thanks to the automatic insertion of labels in the program under test. Limits. A label can only express the requirement that an assertion at a single location in the code must be covered by a single test execution. This is not expressive enough to encode the test objectives coming from path-based criteria, data-flow criteria, strong variants of MCDC or full mutations. Our goal. In this work, we aim at extending the expressive power of labels towards all the criteria presented in Section 2.2 (except WMC and SMC). The proposed extension should preserve the automation capabilities of labels.

A NEW TAXONOMY: THE CUBE

We propose a new taxonomy for code coverage criteria, based on the semantics of the associated reachability problem2 . We take standard reachability constraints as a basis, and consider three orthogonal extensions:

Basis location-based reachability, constraining a single program location and a single test execution at a time,

Ext1 reachability constraints relating several executions of the same program (hyperproperties [START_REF] Clarkson | [END_REF]),

Ext2 reachability constraints along a whole execution path (safety [START_REF] Manna | The Temporal Logic of Reactive and Concurrent Systems Specification[END_REF]),

Ext3 reachability constraints involving choices between several objectives.

The basis corresponds to criteria that can be encoded with labels. Extensions 1, 2 and 3 can be seen as three euclidean axes that spawn from the basis and add new capabilities to labels along three orthogonal directions. This gives birth to a visual representation of our taxonomy as a cube, depicted in Figure 2, where each coverage criterion from Section 2.2 (but mutations) is arranged on one of the cube vertices, depending on the expressiveness of its associated reachability constraints. We can also classify test objectives corresponding to the the violation of security properties such as noninterference (cf. Example 4, Section 4.2). This taxonomy is interesting in several respects. First, it is semantic, in the sense that it refers to the reachability problems underlying the test requirements rather than to the artifact which the test requirements are drawn from. In that sense it represents a progress toward abstraction compared to the older taxonomies [START_REF] Ammann | Introduction to Software Testing[END_REF][START_REF] Zhu | Software unit test coverage and adequacy[END_REF], the one of [START_REF] Ammann | Introduction to Software Testing[END_REF] being already more abstract than [START_REF] Zhu | Software unit test coverage and adequacy[END_REF]. Second, it is very concise (only three basic parameters) and yet almost comprehensive, yielding new insights on criteria, through their distance to basic reachability. Interestingly, many standard criteria require two extensions, yet we do not have any example of criterion involving the three extensions.

HYPERLABELS

The previous section shows that our semantic taxonomy is suitable to represent the whole set of coverage criteria we are interested in. Since labels correspond to basic reachability constraints, we seek to extend them in the three directions of axes in order to build a universal test requirement description language. We detail here the principle, syntax and semantics of the proposed language, called HTOL (Hyperlabel Test Objective Language).

Principles

HTOL is based on labels [START_REF] Bardin | Efficient leveraging of symbolic execution to advanced coverage criteria[END_REF] (referred to as atomic now) to which we add five constructions, namely: bindings, sequences, guards, conjunctions and disjunctions. By combining these operators over atomic labels, one builds new objectives to be covered, which we call hyperlabels.

• Bindings ℓ £ {v1 ← e1; . . .} store in meta-variable(s) v1, . . . the value of well-defined expression(s) e1, . . . at the state at which atomic label ℓ is covered;

• Sequence ℓ1 φ -→ ℓ2 requires two atomic labels ℓ1 and ℓ2 to be covered sequentially by a single test run, constraining the whole path section between them by φ;

• Conjunction h1 • h2 requires two hyperlabels h1, h2 to be covered by (possibly distinct) test cases, enabling to express hyperproperties about sets of tests;

• Disjunction h1 + h2 requires to cover at least one of hyperlabels h1, h2. This enables to simulate criteria involving disjunctions of objectives;

• Guard h | ψ expresses a constraint ψ over metavariables observed (at different locations and/or during distinct executions) when covering labels underlying h.

First Examples

We present here a first few examples of criterion encodings using hyperlabels. They are presented in an informal way, a formal semantics of hyperlabels being given in Section 4. The (strong) MCDC criterion requires to demonstrate here that each atomic condition c1

x==y and c2 a<b alone can influence the whole branch decision d c1 ∧ c2. For c1, it comes down to providing two tests where the truth value of c2 at loc1 remains the same, while values of c1 and d change. The requirement for c2 is symmetric. This can be directly encoded with hyperlabels h1 and h2 as follows:

l (loc1, true) £ {c1 ← x==y; c2 ← a<b; d ← x==y&&a<b} l ′ (loc1, true) £ {c ′ 1 ← x==y; c ′ 2 ← a<b; d ′ ← x==y&&a<b} h1 l • l ′ | c1 = c ′ 1 ∧ c2 = c ′ 2 ∧ d = d ′ h2 l • l ′ | c1 = c ′ 1 ∧ c2 = c ′ 2 ∧ d = d ′
h1 requires that the test suite reaches loc 1 twice (through the • operator), with one or two tests. The values taken by the atomic conditions and the decision when loc 1 is reached are bound (through £) to metavariables c1, c2, d for the first execution and to c ′ 1 , c ′ 2 , d ′ for the second one. Moreover, these recorded values must satisfy the guard In order to meet the all-uses dataflow criterion for the definition of variable a at line loc1, a test suite must cover the two def-use paths from loc1 to loc2 and to loc3. These two objectives are represented by hyperlabels h4 (loc1, true) -→ (loc2, true) and h5 (loc1, true) -→ (loc3, true).

c1 = c ′ 1 ∧ c2 = c ′ 2 ∧d = d ′ ,
Example 4 (Non-interference) Last, we present a more demanding example that involves bindings, sequences and guards. Non-interference is a strict security policy model which prescribes that information does not flow between sensitive data (high) towards non-sensitive data (low ). This is a typical example of hypersafety property [START_REF] Clarkson | [END_REF][START_REF] Clarkson | Principles of Security and Trust: Third International Conference[END_REF]. Hyperlabels can express the violation of such a property in a straighforward manner. Consider the code snippet below. int flowcontrol(int high, int low) { // loc 1 {...} // loc 2 return res; } Non-interference is violated here if and only if two executions with the same low input exhibit different output (res) -because it would mean that a difference in the high input is observable. This can be encoded with hyperlabel h6:

l1 (loc1, true) £ {lo ← low} → (loc2, true) £ {r ← res} l2 (loc1, true) £ {lo ′ ← low} → (loc2, true) £ {r ′ ← res} h6 l1 • l2 | lo = lo ′ ∧ r = r ′

Formal definition

We now formally define HTOL's syntax and semantics.

Syntax. The syntax is given in Figure 3, where:

• ℓ loc, ϕ ∈ Labs is an atomic label.

• B ∈ Bindings loc is a partial mapping between arbitrary metavariable names v ∈ HVars and well-defined expressions e at the program location loc;

• l, l1, • • • , li, • • • , ln are atomic labels with bindings;

• φi is a predicate over the metavariable names defined in the bindings of labels l1, . . . , li, over the current program location pc (≈ program counter) and over the variable names defined in all program locations that can be executed in a path going from loci to loci+1.

• h, h1, h2 Hyps are hyperlabels;

• ψ is a predicate over the set nm(h) of h-visible names (i.e. metavariable names guaranteed to be recorded by h's bindings), defined as follows:

nm(ℓ £ B) all the names defined in B nm([l1

φ 1 -→ • • • ln]) nm(l1) ∪ • • • ∪ nm(ln) nm( h | ψ ) nm(h) nm(h1 • h2) nm(h1) ∪ nm(h2) nm(h1 + h2) nm(h1) ∩ nm(h2);
Well-formed hyperlabels. In general, a name can be bound multiple times in a single hyperlabel, which would result in ambiguities when evaluating guards. To prevent this issue, we define a well-formed predicate wf(•) over hyperlabels, whose definition is given in Figure 4.

In particular, on well-formed hyperlabels, nm is compatible with distributivity of • and +. For instance, if we have wf(h) with h h1 • (h2 + h3), then, with h ′ (h1 • h2) + (h1 • h3), we have wf(h ′ ) and nm(h) = nm(h ′ ).

In the remaining part of this paper, we will only consider well-formed hyperlabels.

h ::= l label | [l 1 φ 1 --→ {l i φ i --→ } * ln] sequence of labels | h | ψ guarded hyperlabel | h 1 • h 2 conjunction of hyperlabels | h 1 + h 2 disjunction
wf(h) wf( h | ψ ) ∀i, j, i = j ⇒ nm(li) ∩ nm(lj) = ∅ wf([l1 φ 1 -→ • • • ln]) wf(h1) wf(h2) nm(l1) ∩ nm(l2) = ∅ wf(h1 • h2) wf(h1)
wf(h2) nm(l1) = nm(l2) wf(h1 + h2) Figure 4: Well-formed hyperlabels Semantics. HTOL is given a semantics in terms of coverage. This is an extension of the semantics of atomic labels of Bardin et al. [START_REF] Bardin | Efficient leveraging of symbolic execution to advanced coverage criteria[END_REF].

A primary requirement for covering hyperlabels is to capture execution states into the variables defined in bindings. For that, we introduce the notion of environment. An environment E ∈ Envs is a partial mapping between names and values, that is, Envs HVars Values. Given an execution state s at the program location loc and some bindings B ∈ Bindings loc , the evaluation of B at state s, noted B s is an environment E ∈ Envs such that E (v) = val iff B(v) evaluates to val considering the execution state s.

We can now define hyperlabel coverage. A test suite TS covers a hyperlabel h ∈ Hyps, noted TS H YP h, if there exists some environment E ∈ Envs such that the pair TS , E covers h, noted TS , E H YP h, defined by the inference rules of Figure 5. An annotated program is a pair P, H where P is a program and H ⊆ Hyps is a set of hyperlabels for P . Given an annotated program P, H , we say that a test suite TS satisfies the hyperlabel coverage criterion (HLC) for P, H , noted TS H Y P,H HLC if the test suite TS covers every hyperlabel from H (i.e. ∀h ∈ H : TS H YP h). The notion of criterion simulation introduced for labels [START_REF] Bardin | Efficient leveraging of symbolic execution to advanced coverage criteria[END_REF] can then be generalized to hyperlabels. Hyperlabel coverage simulates a coverage criterion C if any program P can be automatically annotated with a set of hyperlabels H, so that, for any test suite T S, T S satisfies HLC for P, H if TS fulfils all the concrete test objectives instantiated from C for P and conversely. h can be rewritten into a disjunctive normal form (DNF), i.e a coverage-equivalent hyperlabel h dnf arranged as a disjunction

Disjunctive Normal Form. Any well-formed hyperlabel

Label t ∈ TS t Y k P loc, s s ϕ E ⊇ B s t Y k E loc, ϕ £ B TS , E H YP loc, ϕ £ B Guard TS , E H YP h E ψ TS , E H YP h | ψ Conjunction TS , E H YP h1 TS , E H YP h2 TS , E H YP h1 • h2 Disjunction Left TS , E H YP h1 TS , E H YP h1 + h2 Disjunction Right TS , E H YP h2 TS , E H YP h1 + h2 Sequence t ∈ TS ∀i ∈ [1, n] , t Y k i E li ∀i ∈ [1, n -1] , ki < ki+1 ∀i ∈ [1, n -1] , ∀j ∈ ]ki, ki+1[ , (locj , sj) = P (t)j ∧ φi(E , locj , sj ) TS , E H YP [l1 φ 1 -→ {li φ i -→ } * ln]
h dnf c1 + • • • + ci + • • • + cn of guarded conjunctions ci ls i 1 • . . . • ls i p | ψ(B ls i 1 , • • • , B ls i p
) over atomic labels or sequences. The equivalence between h and h dnf is stated as

∀ T S ⊆ D ∀ E ∈ Envs, TS , E H YP h ⇔ TS , E H YP h hnf .
We provide a DNF normalization algorithm in Section 6.1 (Algorithm 6). DNF will prove convenient for defining our coverage measurement algorithm (Section 6.1).

Advanced Examples

We illustrate now a few more advanced encodings.

Playing with MCDC variants

We have given in Example 1 an encoding of the strongest version of MCDC (a.k.a. RACC). Yet, weaker variants exist. Encoding them into hyperlabels helps clarifying the subtle differences between those variants. GACC (General Active Clause Coverage) is the weakest variant of MCDC. It is also the sole variant to be encodable with atomic labels [START_REF] Pandita | Guided test generation for coverage criteria[END_REF]. Let us assume that we have a predicate p composed of n atomic conditions c1, . . . , cn. GACC requires that for each ci, the test suite triggers two distinct executions of the predicate: one where ci is true, one where ci is false, and both such that the truth value of ci impacts the truth value of the whole predicate. Yet, it is not required that switching the value of ci is indeed feasible, and the two executions do not have to be correlated. Going back to the code snippet of Example 1, GACC requirement for c1 can be simulated by the two atomic labels l3 and l4 l3 (loc1, c1 ∧ ((true

∧ c2) = (f alse ∧ c2))) l4 (loc1, ¬c1 ∧ ((true ∧ c2) = (f alse ∧ c2)))
CACC (Correlated Active Clause Coverage), or masking MCDC is stronger than GACC. It includes every requirement from GACC and additionally requires that for each clause ci, the two executions are such that if p is true (resp. false) in the first one, then it is false (resp. true) in the second one. CACC cannot be encoded into atomic labels because of this last requirement that correlates the two executions together. Yet, it can be encoded with hyperlabels.

Using the same code as in Example 1, CACC requirement for c1 can be simulated by the following hyperlabel h7, built on the two atomic labels l3 and l4 defined for GACC:

h7 l3 £ {r ← d} • l4 £ {r ′ ← d} | r = r ′

More DataFlow criteria

The all-defs coverage criterion requires that each definition of a variable must be connected to one of its uses. The criterion adds a disjunction of objectives to the all-uses criterion. Going back to Example 3, the all-defs requirement for the definition of variable a at line loc1 can be simply simulated by hyperlabel h8 h4 + h5, where h4 and h5 are the hyperlabels defined in Example 3.

Finally, we show that data-flow criteria can be refined to consider the definition and use of single array cells, while the standard approach considers arrays as a whole. This is not a trivial refinement as the index of the cell manipulated at one location may not be known statically, making it impossible to relate defs and uses, as well as to define def-free paths without dynamic information. For example, in the following code, the path from loc1 to loc3 is a valid du-path iff i = k = j, which cannot be known statically: int foo(int i,int j,int k){ / * loc_1 * / a[i] = x; / * loc_2 * / a[j] = y; / * loc_3 * / z = a[k] + 1; } Such a test objective can however be perfectly encoded with hyperlabels, by adding bindings to the atomic labels for saving the values of i and j and using the guard operator to force them being equal. The encoding for the previous code is given below, where pc represents the current line of code: l5 (loc1, true) l6 (loc3, true)

h9 l5 £ {v1 ← i} pc=loc 2 ⇒j =v 1 -----→ l6 £ {v2 ← k} | v1 = v2

Path-based Criteria

Most test objectives coming from path-based criteria can be encoded in a straightforward way with the -→ operator. Typically, complete path coverage can be encoded by considering that S is the set of all paths in P . As soon as there is a loop in P , this will produce an infinite set of hyperlabels. This is coherent with the fact that complete coverage is not finitely applicable and thus not feasible in general. A few path-based criteria require also the + operator for expressing choices between several paths, such as simple round trip coverage.

EXTENSIVE CRITERIA ENCODING

As a first application of hyperlabels, we perform an extensive literature review and we try to encode all coverage criteria with hyperlabels. Especially, we have been able to encode all criteria from the Ammann and Offutt book [START_REF] Ammann | Introduction to Software Testing[END_REF], but strong mutations and (full) weak mutations. These results are summarized in Table 2, where we also specify which criteria can be expressed by atomic labels alone, and the required hyperlabel operators otherwise. Interestingly, many criteria fall beyond the scope of atomic labels, and many also require to combine two or three HTOL operators. This is a strong a posteriori evidence that the language of hyperlabel is both necessary and (almost) sufficient to encode state-of-the-art coverage criteria.

All detailed encodings will be made publicly available in a technical report once the paper is accepted for publication.

COVERAGE MEASUREMENT TOOL

As a second application, we describe a universal coverage measurement tool, built on HTOL. This tool is to hyperlabels what LTest [START_REF] Bardin | An all-in-one toolkit for automated white-box testing[END_REF] is to atomic labels. Namely, we first design a coverage measurement procedure for test suites on programs annotated with hyperlabels (instead of atomic labels), then universality is achieved through providing hyperlabeling encodings of standard criteria (cf. Section 5).

This prototype is the first coverage measurement tool able to handle all coverage criteria from [START_REF] Ammann | Introduction to Software Testing[END_REF] (but strongest mutation variants) in a unified way. Fourteen criteria are supported so far. While our coverage measurement algorithm runs in worst-case exponential time, experiments demonstrate that the tool is efficient enough on existing coverage criteria beyond simple labels. Finally, we show that current automatic test generation tools can already be lifted (in a weak but still useful sense) from labels to hyperlabels, by combining them with our coverage measurement tool.

Computing the coverage of a test suite

Given an annotated program P, H and a test suite T S, our coverage measurement algorithm follows three steps: normalization First, each hyperlabel h ∈ H is rewritten into its disjunctive normal form (cf. Section 4.3).

harvesting Second, each test case t from T S is run on P . Every atomic label and label sequence covered during the run is saved on-the-fly, together with the environment (values of metavariables) that instantiate the label's bindings at the coverage points.

consolidation Third, the collected coverage information is propagated within the syntax tree (in DNF) of every h ∈ H, in order to establish if T S covers h or not.

These steps are now described in more details. Normalization. As stated in Section 4.3, any (well-formed) hyperlabel h can be rewritten into an equivalent hyperlabel h dnf in disjunctive normal form. This form of labels is both very convenient for coverage measurement and very common in practice. This is done by applying the rewrite rules of Figure 6 bottom-up from the leaves of the hyperlabel tree. The proof of equivalence between h and h dnf can easily be obtained by induction on h. Environment harvesting. Once hyperlabels in DNF have been obtained, each test t from the suite T S is run on P , and the coverage information for basic labels, sequences and binding values is collected. Note that we need to store all possible binding values encountered along the execution of t, not just the first one. While this is easy for basic labels, the case of sequences must be treated with care, as there are some non deterministic choices there. Due to space limitations, we do not describe this point here, since it is a common issue in runtime monitoring 3 . Consolidating coverage result. Once the coverage information for basic labels, sequences and binding values is fully collected, we can compute the whole hyperlabel-coverage information. This is straightforward on DNF hyperlabels:

l ; l|true s ; s|true h ; i πi|ψi h|ψ ; i πi|ψi ∧ ψ h L ; i π L i |ψ L i h R ; j π R j |ψ R j h L + h R ; i π L i |ψ L i + j π R j |ψ R j h L ; i π L i |ψ L i h R ; j π R j |ψ R j h L • h R ; i j π L i • π R j |ψ L i ∧ ψ R j notation: π l • . . . • s•
• atomic labels and sequences with no guard are covered iff they have been covered in the harvesting step; 3 A detailed description will be available in a separate technical report once the paper is accepted for publication.

• a guarded conjunction c ls1•...•lsp | ψ(B ls 1 , ...B lsp ) is covered iff each label or sequence lsj, j ∈ 1..p is saved as covered in E and there is at least one set of environments Ej ∈ E (one for every lsj with bindings) such that ψ(E1, • • • , Ep) is true;

• a disjunction h hnf c1 + • • • + ci + • • • + cn is covered iff at least one of the ci is covered.
In practice, the tool tries every possible combination of Ej from E for every ci, until it finds one which makes ψ true (in which case T S covers h) or proves that none exists (in which case h is not covered by T S). Optimizations. We first preprocess hyperlabels under consideration in order to remove all unused metavariables appearing in bindings. Then, during harvesting, we ensure that each binding is recorded only once, avoiding duplicated values. Finally, we perform conjunction and disjunction evaluation in a lazy way, in order to avoid unnecessary combinatorial reasoning on guarded conjunctions. About complexity. The algorithm presented so far runs in worst-case exponential time, mainly because of three factors: (1) normalization may yield an exponential-size hyperlabel, (2) consolidation for guarded conjunctions may lead to checking a number of solutions exponential in the size of the conjunction, and (3) monitoring sequences of labels may include harvesting a number of environments exponential in the length of the considered run.

Yet, in practice, our algorithm appears to perform well on existing classes of testing requirements (cf. Section 6.3). Here are a few explanations. First, criteria as encoded in the previous sections are naturally in DNF, hence we do not have any normalization cost. Second, the critical parameters indicated above have very strong limitations on hyperlabels coming from existing criteria: conjunctions are of length 2; sequences are either of length 2, or they do not use bindings -in that case, environment harvesting becomes a simple coverage check, linear with the length of the sequence; the domain of metavariables is often small (boolean).

Implementation

We have implemented a basic hyperlabel support in the open-source testing tool LTest [START_REF] Bardin | An all-in-one toolkit for automated white-box testing[END_REF], an all-in-one testing platform for C programs annotated with labels, developed as a Frama-C [START_REF] Kirchner | Frama-C: A Program Analysis Perspective[END_REF] plugin. LTest is built around standard labels, and provides labeling functions to automatically encode the requirements from common coverage criteria, as well as coverage measurement, automatic coverage-oriented test generation and automatic detection of infeasible test requirements. The tool is written in OCaml, and relies on PathCrawler [START_REF] Williams | On-the-fly generation of k-paths tests for C functions : towards the automation of grey-box testing[END_REF] for test generation and on Frama-C for static analysis.

We have extended the labeling mechanism into an hyperlabeling mechanism, and we have lifted the coverage measurement part from labels to hyperlabels. Moreover, we have implemented hyperlabeling functions for criteria CACC, RACC, all-def, all-use, FCC and BPC in addition to the criteria already available in LTest4 ; support for other criteria is in progress. Finally, we show in Section 6.3 how LTest test generation can be combined with our new hyperlabel-based coverage measurement algorithm.

Our prototype will be available in open-source when the paper is accepted for publication.

Experimentations

Objectives. We assess the practical applicability of our tool and evaluate its integration with label-based test generation from LTest. The addressed research questions are:

[RQ 1 ] Is the proposed unified approach practical and efficient enough? More precisely, how does the tool scale with large test suites on criteria beyond labels?

[RQ 2 ] Does combining our tool with label-directed test generation (LTest) yield an effective full-featured test tool for criteria beyond labels?

Protocol. We consider five standard benchmark C programs from the LTest paper [START_REF] Bardin | Efficient leveraging of symbolic execution to advanced coverage criteria[END_REF], mainly taken from the Siemens test suite [START_REF] Do | Supporting Controlled Experimentation with Testing Techniques: An Infrastructure and Its Potential Impact[END_REF] (tcas), the Verisec benchmark [START_REF] Ku | A Buffer Overflow Benchmark for Software Model Checkers[END_REF] (get_tag and full_bad from Apache source code) and MediaBench [START_REF] Lee | MediaBench: a tool for evaluating and synthesizing multimedia and communications systems[END_REF] (gd from libgd).

For [RQ 1 ], a set of 1000 test cases is randomly generated for each program. Our tool is successively run with 10, 50, 100, 250, 500, 750 and all of these test cases. Each tool run is repeated six times. First, tests are executed without measurement (baseline), and then measuring coverage for the CC and GACC label-encodable criteria (witness). Second, tests are run and measured for the CACC, RACC and all-defs criteria, which involve the five operators from hyperlabels.

For [RQ 2 ], LTest test generation is used on each program to produce test suites tailored for the label-encodable CC, MCC and GACC criteria. Our tool then measures the coverage achieved by these test suites and by random test generation (1000 test cases per program, serving as witness), for criteria CACC and RACC.

All the experiments are performed under Ubuntu Linux 14.04 on an Intel Core i7-4712HQ CPU at 2.30GHz × 8, with 16GB of RAM.

Results and discussion. Part of our results are presented in Table 3, Figure 7 and Figure 8. Detailed test data and results will be available in open-source when the paper is accepted for publication.

[RQ 1 ] Table 3 details, for each program and encoded criterion, the number of defined hyperlabels and labels as well as the coverage measurement time and level for 10 and 1000 test cases. Figure 7 plots, for each criterion and the baseline (no-cov), the mean measurement time for all programs, as a function of the test suite size. In all cases, the measurement time grows linearly with the number of test cases, but the slope is sharper for the criteria involving hyperlabel operators. The time overhead, w.r.t. GACC, is very small for CACC and RACC, which are encoded with labels close to those of GACC, more some bindings, guards and conjunctions. all-defs is encoded using sequences and disjunctions, but its tangible time overhead, compared to the other criteria, is due to the higher number of test objectives that this criterion defines.

Conclusion. These results indicate that upgrading labels with hyperlabels makes it possible to build an (almost) universal coverage measurement tool, without blowing practical applicability off. The measurement time for criteria beyond labels is acceptable and remains linear with the size of the test suite. Moreover, as our tool implementation is not opti- mized, there is still room for a strong reduction of coverage measurement time, when using the approach in a more industrial context.

[RQ 2 ] Figure 8 shows the total percentage, for all the programs, of CACC and RACC objectives that are covered by the generated test suites. Label-directed test generation provides a significantly better coverage than random generation. Coverage is also better with MCC and GACC tests than with CC tests, the two former criteria being much stronger than the latter. The minimal and maximal RACCcoverage obtained on a program with GACC-directed test generation are 61% and 94%, with a mean of 72% (random: minimum 29%, maximum 81%, mean 53%). Note also that these figures may take into account infeasible test objectives, artificially lowering the achieved coverage results.

Conclusion. Combining our tool with LTest test generation provides a full-featured test tool, in the sense that it handles both coverage measurement and (label-based) test generation, for almost all the criteria from the literature. The previous results indicate that this full-featured tool can provide an above-random and often good coverage ratio for beyond-label criteria.

RELATED WORK

The two closest works to ours are labels [START_REF] Bardin | Efficient leveraging of symbolic execution to advanced coverage criteria[END_REF] and FQL. Since the difference with labels has already been presented (Sections 2.3 and 4.1, Table 2), we focus here on FQL. Specification of white-box coverage criteria. The Fshell Query Language (FQL) by Holtzer et al. [START_REF] Holzer | How did you specify your test suite[END_REF] for test suite specification and the associated Fshell [START_REF] Holzer | Proceedings, chapter FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement[END_REF] The scope of criteria that can be encoded in FQL is incomparable with the one offered by HTOL, as FQL handles complex safety-based test requirements but no hyperpropertybased requirement. As an important example, FQL cannot encode MCDC. FQL also offers the interesting ability to encode, in an elegant and standardized way, generic coverage criteria (independently of any concrete program), where HTOL is designed to encode concrete test objectives (i.e. particular instantiations of coverage criteria for a concrete program).

In future work, a promising research direction would be to use HTOL and FQL in a complementary way, by enabling the instantiation of the generic (extended) FQL specification of a criterion into a set of hyperlabels for the program to test.

Note also that FShell focus on test generation, where the tool proposed in this paper focus on coverage measurement. We intend to develop a test generation tool dedicated to hyperlabels in a middle term. Specification of model-based coverage criteria. The work by Blom et al. [START_REF] Blom | Specifying and generating test cases using observer automata[END_REF] proposes to specify test objectives on extended finite state machines (EFSMs) as observer automata with parameters. Test case generation can then be expressed as a reachability problem, which can be solved with the Upaal Cover state-space exploration tool [START_REF] Hessel | Formal methods and testing. chapter Testing Real-time Systems Using UPPAAL[END_REF]. Hong et al. [START_REF] Hong | Tools and Algorithms for the Construction and Analysis of Systems: 8th International Conference[END_REF] also consider EFSM testing, but they encode coverage criteria as sets of formulas in the CTL temporal logic. Both papers provide encoding examples for some classical control-flow and data-flow criteria (on EFSM models). Al-though they are theoretically more expressive than HTOL for safety-related test requirements, HTOL already offers a sufficient subset of features to encode common coverage criteria from the literature. On the other hand, these languages do not support requirements involving multiple related executions (hyperproperties), which do appear in industrial context (MCDC, non-interference).

Formal encodings have been proposed for several coverage criteria in different other formalisms, like set theory [START_REF] Frankl | A formal analysis of the fault-detecting ability of testing methods[END_REF], graph theory [START_REF] Podgurski | A formal model of program dependences and its implications for software testing, debugging, and maintenance[END_REF], predicate logic [START_REF] Tai | Theory of fault-based predicate testing for computer programs[END_REF][START_REF] Abdurazik | Evaluation of three specification-based testing criteria[END_REF], OCL [START_REF] Friske | Composition of model-based test coverage criteria[END_REF] and Z [START_REF] Vilkomir | Formal Methods and Testing: An Outcome of the FORTEST Network[END_REF]. However, for each formalism, the scope of supported criteria is narrow and often limited to simple criteria.

Coverage objectives and hyperproperties. Test requirements from the strongest MCDC variants can be seen as examples of hyperproperties, i.e. software properties over several different traces of the system to verify. Testing hyperproperties is a rising issue, notably in the frame of security [START_REF] Kinder | Hypertesting: The case for automated testing of hyperproperties[END_REF]. However, research in the topic still remains exploratory. Rayadurgam et al. [START_REF] Rayadurgam | Generating mc/dc adequate test sequences through model checking[END_REF] suggests that MCDC can be encoded with temporal logics, by writing the formulas for a self-composition of the tested model with itself. The paper reports that model-checking the obtained formulas rapidly faces scalability issues. Clarkson et al. [START_REF] Clarkson | Principles of Security and Trust: Third International Conference[END_REF] introduces Hy-perLTL and HyperCTL*, which are extensions of temporal logics for hyperproperties, as well as an associated modelchecking algorithm. This work makes no reference to test criterion encoding, but the proposed logics could be used to provide [START_REF] Hong | Tools and Algorithms for the Construction and Analysis of Systems: 8th International Conference[END_REF] with the ability to encode criteria like MCDC. However, the complexity results and first experiments [START_REF] Clarkson | Principles of Security and Trust: Third International Conference[END_REF] indicate that the automation of such an approach still faces strong scalability limits.

In future work, we intend to explore how HTOL formally compares to HyperLTL and HyperCTL*. As an intuition, we think that these languages are theoretically more expressive than HTOL. But while HTOL remains sufficient for encoding common code coverage criteria (including MCDC), it is also a strong starting point for a more general but still lightweight support of hyperproperty testing, like shown in Example 4 with non-interference.

Test description languages. Some languages have been designed to support the implementation of test harnesses at the program (TSTL [START_REF] Groce | Tstl: A language and tool for testing (demo)[END_REF], UDITA [START_REF] Gligoric | Test generation through programming in udita[END_REF]) or model (TTCN-3 [START_REF] Grabowski | An introduction to the testing and test control notation (ttcn-3)[END_REF], UML Testing Profile [START_REF] Schieferdecker | The uml 2.0 testing profile and its relation to ttcn-3[END_REF]) level. A test harness is the helper code that will execute the testing process in practice, which notably includes test definition, documentation, execution and logging. These languages offer general primitives to write and execute easily test suites, but independently of any explicit reference to a coverage criterion.

Coverage measurement tools. Code coverage is used extensively in the industry. As a result, there exists a lot of testing tools that embed some sort of coverage measurement. For instance, in 2007, a survey [START_REF] Yang | A survey of coverage-based testing tools[END_REF] found ten tools for programs written in the C language: Bullseye [START_REF]Bullseye Testing Technology: BullseyeCoverage[END_REF], Code-TEST, Dynamic [START_REF]Dynamic Code Coverage[END_REF], eXVantage, Gcov (part of GCC) [START_REF]GCC's Gcov[END_REF], Intel Code Coverage Tool [START_REF]Intel Code Coverage Tool in Intel C++ compiler[END_REF], Parasoft [START_REF] Parasoft | C++test: Comprehensive dev. testing tool for C/C++[END_REF], Rational Pu-rifyPlus, Semantic Designs [START_REF]Semantic designs: C test coverage tool[END_REF], TCAT [START_REF]TCAT C/C++[END_REF]. To this date (April 2016), there are even more tools, such as COVTOOL, LDRAcover [START_REF]LDRA -LDRACover[END_REF], and Testwell CTC++ [START_REF]Testwell CTC++: Test coverage analyzer for C/C++[END_REF]. Most existing tools only support basic coverage criteria such as statement and branch coverage. For instance, only a few like Testwell CTC++, Parasoft, and LDRAcover support MCDC.

As a rule of thumb, current coverage measurement tools support a limited number of test criteria in a hard-coded, non-generic manner. Table 1 (Section 1) summarizes implemented criteria for some popular tools. Our prototype already supports all these criteria in a generic and extensible way, plus seven other criteria (cf. Section 6.2).

Moreover, the lack of formalization in the reportedly supported coverage criteria prevents users to know with certainty the actually supported criteria. For example, the way shortcut logical operators are supported, or which actual flavor of MCDC is supported, are often left unspecified in the tools' documentation.

However, to be fair, code coverage tools also aim at causing as little overhead as possible. In contrast, as a first step, we only aim at getting a reasonable overhead.

CONCLUSIONS

To sum up, HTOL proposes a unified framework for describing and comparing most existing test coverage criteria. This enables in particular implementing generic tools that can be used for a wide range of criteria. Furthermore, as shown in our first experiments on coverage measurements, the overhead of such tools is sufficiently low to not be a concern in practice. Future work includes the efficient lifting of automatic test generation technologies to hyperlabels, the identification of uncoverable hyperlabels, the extension of HTOL to handle mutation-based criteria, as well as the use (and extension) of HTOL for general hyperproperty testing.

  , BBC: basic blocks, DC: decisions, CC: conditions, DCC: decision condition, MCDC: modified decision condition, BPC: basis paths

Figure 1 :

 1 Figure 1: Encoding of standard test requirements with labels (from [6])

Figure 2 :

 2 Figure 2: The "cube" taxonomy of coverage criteria

  meaning that c1 alone can influence the decision. Similarly, h2 ensures the desired test objective for c2. Example 2 (Call coverage) Let us continue by showing the interest of the disjunction operator. Consider the following code snippet where f and g are two functions. int f() { if (...) { / * loc_1 * / g(); } if (...) { / * loc_2 * / g(); } } The function call coverage criterion (FCC) requires a test case going from f to g, i.e. passing either through loc1 or loc2. This is exactly represented by hyperlabel h3 below: h3 (loc1, true) + (loc2, true) Example 3 (all-uses) We illustrate now the sequence operator • -→. Consider the following code snippet. / * loc_1 * / a := x; if (...) / * loc_2 * / res := x+1; else / * loc_3 * / res := x-1;

{v 1 ← e 1 ;Figure 3 :

 113 Figure 3: Syntax of Hyperlabels

Figure 5 :

 5 Figure 5: Inference rules for hyperlabel semantics

Figure 6 :

 6 Figure 6: Rewriting hyperlabel into DNF

Figure 8 :

 8 Figure 7: Scalability of Coverage Measurement

Table 1 :

 1 Criteria supported in some coverage tools finite set of test data. A (finite) execution of P over some t, denoted P (t), is a (finite) run σ (loc0, s0), . . . , (locn, sn) where the loci denote successive (control-)locations of P (≈ line of code) and the si denote the successive internal states of P (≈ valuation of all global and local variables and of all memory-allocated structures) after the execution of each loci (loc0 refers to the initial program state).A test datum t reaches a location loc at step k with internal state s, denoted t Y k P loc, s , if P (t) has the form σ • loc, s • ρ where σ is a partial run σ of length k. When focusing on reachability, we omit k and write t YP loc, s .Given a test objective c, we write t YP c if test datum t covers c. We extend the notation for a test suite TS and a set of test objectives C, writing TS YP C when for any c ∈ C, there exists t ∈ TS such that t YP c. A (sourcecode based) coverage criterion C is defined as a systematic way of deriving a set of test objectives C = C(P ) for any program under test P . A test suite TS satisfies (or achieves) a coverage criterion C if TS covers C(P ). When there is no ambiguity, we identify the coverage criterion C for a given program P with the derived set of test objectives C = C(P ).

3 .

 3 Example 1 (MCDC) We start with conjunction, bindings and guards. Consider the following code snippet:

	statement_0;
	// loc_1
	if (x==y && a<b) {...};
	statement_2;

Table 2 :

 2 Simulation of criteria from[START_REF] Ammann | Introduction to Software Testing[END_REF]

Table 3 :

 3 Scalability of Cov. Measurement (Details)

More precisely: the reachability problem of the test requirements associated to the coverage criterion.

Namely: FC, BBC, DC, CC, DCC, MCC, GACC, and a subset of WM.