Stéphane Guichard
email: sguichard@cesi.fr

Frédéric Miranville
email: frederic.miranville@univ-reunion.fr

Dimitri Bigot
email: dimitri.bigot@univ-reunion.fr

Bruno Malet-Damour
email: bruno.malet-damour@univ-reunion.fr

Teddy Libelle
email: teddy.libelle@univ-reunion.fr

Harry Boyer
email: harry.boyer@univ-reunion.fr

Empirical validation of a thermal model of a complex roof including phase change materials

Keywords: Phase change materials, Building thermal simulation, Model Optimization, Model validation PACS: J0101

This paper deals with the empirical validation of a building thermal model using a phase change material (PCM) in a complex roof. A mathematical model dedicated to phase change materials based on the heat apparent capacity method was implemented in a multi-zone building simulation code, the aim being to increase understanding of the thermal behavior of the whole building with PCM technologies. To empirically validate the model, the methodology is based both on numerical and experimental studies. A parametric sensitivity analysis was performed and a set of parameters of the thermal model have been identified for optimization. The use of a generic optimization program called GenOpt ® coupled to the building simulation code enabled to determine the set of adequate parameters. We first present the empirical validation methodology and main results of previous work. We then give an overview of GenOpt ® and its coupling with the building simulation code. Finally, once the optimization results are obtained, comparisons of thermal model of PCM with measurements are found to be acceptable and are presented.

Introduction

Buildings are indisputably considered as one of the largest energy consuming sector. According to the International Energy Agency (IEA), the average energy consumed by buildings represents 32% of energy consumption worldwide, with approximately 40% of primary energy used in most countries. In France, the energetic consumption in the building sector is approximately about 43%, representing a quarter of national's carbon dioxide emissions. The use of energy-hungry appliances to improve the thermal comfort is responsible both for the electrical energy consumption and the increase of greenhouse gas emissions [START_REF] Pérez-Lombard | A review on buildings energy consumption information[END_REF].

For this reason, some actions are led to curb energy consumption and to protect environment, for example, the use of renewable energies, passive energy buildings and the use of building codes for new or retrofited buildings. Moreover, several studies and applications have shown that the building thermal inertia is among possible solutions and should be improved, in order to reach high performance and low-energy buildings [START_REF] Zhou | Review on thermal energy storage with phase change materials (PCMs) in building applications[END_REF][START_REF] Zalba | Review on thermal energy storage with phase change: materials, heat transfer analysis and applications[END_REF][START_REF] Farid | A review on phase change energy storage: materials and applications[END_REF]. As a result, the question in the building sector arises as to the increase of the thermal energy capacity storage in the used materials.. With this target in mind, a technology such as the phase change materials may be integrated into building envelopes, both to enhance the thermal energy storage [START_REF] Cabeza | Materials used as PCM in thermal energy storage in buildings: A review[END_REF] and to improve the thermal comfort. Indeed, because of their higher thermal energy storage densities than other heat storage materials, these materials are able to store and release thermal energy as latent heat, when the phase change occurs. It is important to highlight the fact that the latent heat storage is much larger than the sensible heat storage [START_REF] Seong | Energy Saving Potentials of Phase Change Materials Applied to Lightweight Building Envelopes[END_REF]. Usually, organic and inorganic PCMs are often used and solid-liquid phases are chosen [START_REF] Hasan | Energy and cost saving of a photovoltaic-phase change materials (PV-PCM) system through temperature regulation and performance enhancement of photovoltaics[END_REF]. Despite its thermal conductivity that should be improved, paraffin is often used for latent heat thermal energy storage [START_REF] Medina | On the heat transfer rate reduction of structural insulated panels (SIPs) outfitted with phase change materials (PCMs)[END_REF]. Indeed, it has useful thermal properties such as absence of super cooling, chemical stability and low vapor pressure [START_REF] Zalba | Review on thermal energy storage with phase change: materials, heat transfer analysis and applications[END_REF][START_REF] Sarı | Thermal conductivity and latent heat thermal energy storage characteristics of paraffin/expanded graphite composite as phase change material[END_REF].

The use of PCMs in the building envelope may reduce the peak loads and heating, ventilating and air conditioning (HVAC) energy consumptions by increasing the thermal inertia of each walls of the building. Indeed, the peak load may be shifted to the off peak load periods of energy use [START_REF] Khudhair | A review on energy conservation in building applications with thermal storage by latent heat using phase change materials[END_REF]. In addition, the results of PCM-oriented research on buildings have shown that the thermal comfort was improved and energy saving could be made.

Among all the PCM applications to reach high energy efficiency buildings, for example PCM integrated wall, PCM assisted ceiling heating and cooling, photovoltaic system coupled with a PCM-based heat storage [START_REF] Lo Brano | On the efficacy of PCM to shave peak temperature of crystalline photovoltaic panels: an FDM model and field validation[END_REF], and so on, this paper deals with the inclusion of PCMs in the roof system. Generally, the roof is considered as a thermal buffer between the indoor and outdoor environment. This is the part of the building most exposed to solar radiation in hot climates and considered as the weakest part of the building thermal performance [START_REF] Miranville | A combined approach for determining the thermal performance of radiant barriers under field conditions[END_REF][START_REF] Guichard | A thermal model for phase change materials in a building roof for a tropical and humid climate: Model description and elements of validation[END_REF].

A possible solution to reduce heat transfer from outside to inside of the building may be found in the increased use of mass insulation. Nevertheless, this type of thermal insulation allows to reduce heat transfer due to conduction, but does not reduce heat transfer by infrared radiation through the roofing. To overcome, a solution is based on the use of radiant barrier systems, which requires the presence of air layers in order to benefit a reflective radiation [START_REF] Miranville | A combined approach for determining the thermal performance of radiant barriers under field conditions[END_REF]. Based on the same approach, PCM under a flexible sheet form laminated both sides with an aluminum sheet is used in the lower part of the roof between the air layer and the drywall, both to enhance the thermal energy storage and to reduce the solar radiation through the roof system [START_REF] Guichard | Experimental investigation on a complex roof incorporating phase-change material[END_REF].

Furthermore, before integrating PCM into new or retrofit buildings, it will be interested to predict the thermal effects of these materials on the whole building. To contribute to the energy efficiency policy recommendations on buildings energy consumption, a one-dimensional simplified numerical model for phase change material has been developed and implemented in a prototype of building simulation code named ISOLAB. This one is able to take into account the building envelopes, including PCM or not, and the actual impact on energy consumption. Nevertheless, before using PCM model integrated in ISOLAB code and to ensure the reliability of the results, this article focuses on the empirically validation of the latter. We first present the tools used, building simulation code and the generic optimization program GenOpt®. We then briefly describe the studied system as well as main results of previous work. Finally, results of the experimental validation of the thermal model are presented and discussed.

Presentation of tools

A building simulation code: ISOLAB

Developed by MIRANVILLE, ISOLAB is a prototype of building simulation software developed with the Matlab environment [START_REF] Miranville | Contribution à l'étude des parois complexes en physique du bâtiment modélisation, expérimentation et validation expérimentale de complexes de toitures incluant des produits minces réfléchissants en climat tropical humide[END_REF]. Nodal description of buildings and finite difference scheme of the time variable in one-dimensional are used to simulate the dynamic thermal behavior of a monozone or multi-zone building according to its environment (weather data and location). In order to determine temperatures of the whole building, the following matricial formalism (1) is solved by using an implicit finite-difference method [START_REF] Boyer | Thermal building simulation and computer generation of nodal models[END_REF].

C w T ̇w=A w T w +B w , (1)
Where the index w is used for walls and windows. A w is the state matrix including the terms linked to heat conduction and the interior linearized convective exchanges. B w is the vector containing outside or internal solicitations of the system. C w is the capacities matrix. T w is the state vector containing every temperatures of each wall, T ̇w and is the temperature derivative of T w .

ISOLAB code has already been validated with the IEA BESTEST procedure (International Energy Agency, Building Energy Simulation Test), concerned with buildings without PCMs [START_REF] Miranville | Contribution à l'étude des parois complexes en physique du bâtiment modélisation, expérimentation et validation expérimentale de complexes de toitures incluant des produits minces réfléchissants en climat tropical humide[END_REF].

A generic optimization program: GenOpt ®

The optimization process consists in running several model simulations with different parameters set. The chosen parameters are identified by performing a mathematical tool like parametric sensitivity analysis. Thereafter, each simulation is launched with a different set of parameters (continuous parameters, discrete parameters, or both), and the associated cost function value, with or without constraints, is recorded. Finally, to ensure convergence to the best set of parameters, it is necessary to run many simulations on each parameter for the right different parameter range.

A generic optimization program, called GenOpt ® from the Lawrence Berkeley National Laboratory of University of California, developed with the Java environment by Mickael Wetter is used to optimize the unknown parameters [START_REF] Wetter | GenOpt-A generic optimization program[END_REF]. The choice of GenOpt ® has also been made according to its simulation program interface that allows the coupling with any simulation program, without requiring code modifications. Indeed, the coupling is done by creating some files required by GenOpt ® to run an optimization and also an auto-executable version of the model [START_REF] Bigot | Model optimization and validation with experimental data using the case study of a building equipped with photovoltaic panel on roof: Coupling of the building thermal simulation code ISOLAB with the generic optimization program GenOpt[END_REF]. In addition, GenOpt ® is dedicated for the thermal building simulation. For more details about the generic optimization program, the interested reader may refer to [START_REF] Wetter | GenOpt-A generic optimization program[END_REF].

Before performing the optimization sequences with GenOpt ® , the studied system with the main results of previous work are presented in the following paragraph.

Experimental set up of a complex standard roof including phase change materials

Introduction

The objective of this part is to show the main results of experimental investigations on a complex roof incorporating PCM panels. The use of such a database allows to empirically validate the numerical code developed and implemented in a prototype of building simulation software to determinate the thermal performance of any building envelopes with PCM.

First, a description of the roofing complex and the different associated instrumentation is presented in the following paragraph.

Localization and structure of the test cell

With dimensions of 3m (height) × 3m (width) × 3m (length) and an internal volume about 30 m 3 , the test cell, called LGI, can be considered as a typical room of buildings existing in Reunion Island. It has been designed according to a flexible structure in order to study several configurations and phenomena. Thanks to its modular structure, the movable walls allow to include PCM panels to the standard roof inclined at 20° to the horizontal. The whole building envelopes are constituted of vertical opaque walls, a jalousie, a glass door and a complex roof with PCM panels. The roofing complex is an assembly of homogeneous or inhomogeneous materials, separated by one or several air layers [START_REF] Miranville | A combined approach for determining the thermal performance of radiant barriers under field conditions[END_REF][START_REF] Guichard | Experimental investigation on a complex roof incorporating phase-change material[END_REF][START_REF] Bigot | Model optimization and validation with experimental data using the case study of a building equipped with photovoltaic panel on roof: Coupling of the building thermal simulation code ISOLAB with the generic optimization program GenOpt[END_REF]. The building components of LGI are given in Table 1, and an overall view is depicted in Figure 1a. Located at a low altitude sea level (55 m), the experimental set up was erected on the experimental platform of the University Institute of Technology of Saint-Pierre (Reunion Island). The choice of this location results in a tropical climate with strong solar radiation and humidity. Besides, the test cell is oriented north in order to receive symmetrical solar radiation during the day [START_REF] Guichard | Experimental investigation on a complex roof incorporating phase-change material[END_REF]. With the aim of obtaining extreme solicitations input from the roof, a dark blue color has been chosen for the corrugated iron. During the procedure of experimental validation, the blind windows and the window panes were masked, and the test cell was kept closed, without using mechanical ventilation or air-conditioning system [START_REF] Guichard | A thermal model for phase change materials in a building roof for a tropical and humid climate: Model description and elements of validation[END_REF].

Furthermore, near to the experimental devices, two meteorological stations (a weather station in red circle is depicted in Figure 1b) are installed in order to collect data from the environment, such as solar radiation (global, direct and diffuse, on a horizontal plane), ambient air temperature, exterior relativity humidity, wind speed and direction. As depicted in Figure 2 and because of the important number of days (92 days approximately) of the chosen experimental sequence and, in order not to overload the graphs, only four days of data from August to October 2012 are presented in this paper. The walls (north, south, east and west, inside and outside) are equipped with thermal sensors on surfaces, such as T-type thermocouples and flux meters in order to measure the inside or outside surface temperature of each wall. For air temperature, the thermocouples are inserted into aluminum cylinders. For radiant temperature, the thermocouples are contained in a black globe.

To assess the stratification of the air, the interior volume was measured at three different heights from floor to ceiling (see Figure 3). Many heat sensors have been sealed in the concrete slabs supporting the cell, in order to assess the information on the boundary conditions from the ground. Indeed, the ground model is difficult to develop and to avoid modeling errors concerning this part of the buildings not directly linked to our study, the database from the ground measures will be used during the code validation step.

For more details on sensors location and set-up and the on the associated errors, the interested reader may refer to [START_REF] Guichard | A thermal model for phase change materials in a building roof for a tropical and humid climate: Model description and elements of validation[END_REF].

Instrumentation of the roof

To ensure reliable measurements from the complex roof components, sensors have been located as depicted in Figure 3. To assess the temperatures and the heat flux meters from to the corrugated iron to the ceiling, each component of the complex roof was instrumented. The heat sensors are spread over on both sides of the surfaces of the corrugated iron, on PCM panels and on drywall. Between PCM panels and the corrugated iron, the air layer is not ventilated, and the dry-air and black globe temperatures were also measured.

Before using heat sensors, the thermocouples were calibrated and verified on site according to protocol dictates. Heat flux sensors were calibrated by manufacturer. The accuracy of the thermocouples is estimated to ±0.5°C, and according to manufacturer, the relative error of flux meters is approximately about 5%. In order to avoid air bubbles for both thermocouples and flux meters, a conductive heat paste was applied on the surfaces.

A data logger was installed in the LGI cell in order to collect data from all sensors every 15 min. All data were saved on a computer [START_REF] Guichard | A thermal model for phase change materials in a building roof for a tropical and humid climate: Model description and elements of validation[END_REF].

Previous investigation

Introduction

Since May 2013, both the thermal behavior of building envelopes including PCM and time-varying thermal properties of materials were not taken into account by ISOLAB. For this, a simplified numerical model of the thermal behavior of phase change materials was developed and implemented. However, many constraints on the PCM model have been imposed, such as the respect of the state system formalism and the use of implicit scheme in one-dimension according to the finite difference approach. The apparent heat method capacity has moreover been used.

Description of the roofing complex

The model is intended to predict temperature behavior of each component of the whole building, including the inside air of enclosures. The studied LGI cell is considered as well-isolated and divided into two thermal zones. Indeed, the ceiling is a specific wall separating two zones. It plays the role of ceiling for the first zone and of floor for the second zone. We note that the air gap simulated in zone 2 is considered as a thermal zone in our multi-zone building model (see Figure 3).

The presence of an air layer between the corrugated iron and PCM panels allows to benefit the principle of action of reflective insulation, which is closely linked to the radiative properties of the surfaces of PCM panels. Taking into account the air layer with the combination of homogenous and inhomogeneous materials, the roof system can be qualified as complex with coupled heat transfers involved (conduction, convection and radiative transfers) [START_REF] Guichard | Contribution à l'étude des parois complexes intégrant des matériaux à changements de phase : Modélisation, Expérimentation et évaluation de la performance thermique globale[END_REF]. Therefore, the chosen configuration may complicate the determination of thermal performances due to the multiple configurations of the air layer: opened or closed, naturally ventilated or forced-ventilated [START_REF] Guichard | Experimental investigation on a complex roof incorporating phase-change material[END_REF]. This is the raison explaining that in the proposed approach in this paper, the enclosed air space is considered as a thermal zone.

Description of PCM test

PCM tested is the commercial product from Dupont™ Energain ® . It is a flexible sheet 5 mm thick, made of 60% microencapsulated paraffin wax within a copolymer laminated on both sides with an aluminum sheet [START_REF] Guichard | A thermal model for phase change materials in a building roof for a tropical and humid climate: Model description and elements of validation[END_REF][START_REF] Guichard | Experimental investigation on a complex roof incorporating phase-change material[END_REF]. Its characteristics are summarized in the following Table 2 Values of the heat capacity in each phase and melting point have been determined by DSC (Differential Scanning Calorimetry) measurements. These parameters are exposed in details in refs [START_REF] Kuznik | Experimental investigation of wallboard containing phase change material: Data for validation of numerical modeling[END_REF][START_REF] David | Numerical study of the influence of the convective heat transfer on the dynamical behaviour of a phase change material wall[END_REF].

Mathematical model for phase change material

The solidification and melting process are the most studied in building applications. Usually, numerical modelling of these phenomena is either based on the first law of thermodynamics or second law of thermodynamics. For more details, the interested reader may refer to [START_REF] Dutil | A review on phase-change materials: mathematical modeling and simulations[END_REF].

The thermal model for phase change is based on the apparent heat capacity method from enthalpy method. This method allows to obtain the general form of a heat conduction equation with a nonlinear specific heat, without need to know ahead of time the location of the phase interface. To simplify the mathematical model, some assumptions were made [START_REF] Guichard | A thermal model for phase change materials in a building roof for a tropical and humid climate: Model description and elements of validation[END_REF][START_REF] Guichard | Experimental investigation on a complex roof incorporating phase-change material[END_REF][START_REF] Guichard | A Mathematical Model of Phase Change Materials (PCM) used in Buildings[END_REF]. Through the solid (or liquid) fraction term, called fs, the final expression of transient heat conduction can be written in 1-D along the 𝑥 ⃗ direction as follows [START_REF] Guichard | A thermal model for phase change materials in a building roof for a tropical and humid climate: Model description and elements of validation[END_REF][START_REF] Guichard | A Mathematical Model of Phase Change Materials (PCM) used in Buildings[END_REF]:

C app (T) ∂T(x,t) ∂t =λ PCM (T) ∂ 2 T(x,t) ∂x 2 , (2)
With:

{ C app (T)=ρ s c s +∆(ρc)f s + df s (T) dT (ρ l L m +∆(ρc). (T(x,t)-T m )) ∆(ρc)=ρ l c l -ρ s c s λ PCM (T)= (1-f s (T)) λ s +λ l f s (T) f s (T)= 1 2 - 1 2 tanh (γ T m -T(x,t) 4δT ) df s (T) dT = γ 8∆T[cosh(γ T m -T(x,t) 4δT
)] 2
The governing equation in terms of the heat apparent capacity can be solved using a standard heat transfer code, and a wide range of discretization approach can be used. As a result, one-dimensional finite difference method can be chosen [START_REF] Guichard | Contribution à l'étude des parois complexes intégrant des matériaux à changements de phase : Modélisation, Expérimentation et évaluation de la performance thermique globale[END_REF]. To definitely be in accordance with the formalism of ISOLAB equation, the use of a backward Euler scheme is possible thanks to the solid (or liquid) fraction term. Generally, the expression of solid fraction is given by using an approximation of the Heaviside function. In PCM model, a specific parameter called γ appears in the final expression. The latter is usually equals to 1, for instance in [START_REF] Dauvergne | Réduction et inversion de problèmes de diffusion thermique avec changement de phase[END_REF]. In order to not underestimate or overestimate the latent heat value during the phase change process, a proposed method was given by [START_REF] Guichard | A thermal model for phase change materials in a building roof for a tropical and humid climate: Model description and elements of validation[END_REF]. With this aim, for a given phase change interval δT, and at T=T m , the expression of the apparent heat capacity (𝐶 𝑎𝑝𝑝 ) leads to the first determination of γ, according to the following process [START_REF] Guichard | A thermal model for phase change materials in a building roof for a tropical and humid climate: Model description and elements of validation[END_REF]:

If 𝑻(𝒙, 𝒕) ≥ 𝑻 𝒎 -𝜹𝑻 𝒂𝒏𝒅 𝑻(𝒙, 𝒕) ≤ 𝑻 𝒎 + 𝜹𝑻 𝒕𝒉𝒆𝒏 |𝒎𝒂𝒙(𝜸) = (𝒎𝒂𝒙(𝑪 𝑫𝑺𝑪 ) -( 𝒄 𝒔 + 𝒄 𝒍 𝟐 )) . 𝟖𝜹𝑻 𝑳 𝒎

else

|𝜸 must be determined end

Where max(CDSC) is given by DSC, and δT is chosen very small. In the numerical simulation, δT=0.01°C. In the first approach, γ is evaluated as follows:

γ= L m C ps • (T m -δT) (3)

Main results

The thermal model will be validated only if the validation criteria are reached. These criteria are given by [START_REF] Guichard | A thermal model for phase change materials in a building roof for a tropical and humid climate: Model description and elements of validation[END_REF][START_REF] Bigot | Model optimization and validation with experimental data using the case study of a building equipped with photovoltaic panel on roof: Coupling of the building thermal simulation code ISOLAB with the generic optimization program GenOpt[END_REF]: 1. To reach 10% validation error between numerical solutions and experimental data from actual building; 2. To reach acceptable absolute errors between some numerical solutions and measurements:  ± 2°C for temperatures on each side of each suspended ceiling  ± 1°C for indoor air temperature of real building To definitely validate the numerical thermal model, different steps are required. These steps are illustrated in Figure 4: The two first steps have already been presented in details in [START_REF] Guichard | A thermal model for phase change materials in a building roof for a tropical and humid climate: Model description and elements of validation[END_REF]. The results showed that the numerical thermal model was able to predict the dynamic thermal behavior of PCM. Nevertheless, the validity criteria were not respected. According to the validation methodology, it was necessary to highlight the origins of errors. A parametric sensitivity analysis, according to a method derived from the FAST method (Fast Fourier Amplitude Transform) has been performed and made it possible to put in evidence the parameters with most influence on model outputs [START_REF] Mara | Parametric sensitivity analysis of a test cell thermal model using spectral analysis[END_REF][START_REF] Mara | Empirical validation of the thermal model of a passive solar cell test[END_REF][START_REF] Lauret | A validation methodology aid for improving a thermal building model: case of diffuse radiation accounting in a tropical climate[END_REF]. Following the sensitivity analysis, the main cause of any difference between the model and experimental data can be explained, but also we can focus on the search of the set of unknown parameters of the model in a restricted range. The following important results were showed [START_REF] Guichard | A thermal model for phase change materials in a building roof for a tropical and humid climate: Model description and elements of validation[END_REF]:


The thermal behavior of the complex roof is governed by convective heat transfers, both in the air layer and the faces of the suspended ceiling.



The absorptivity coefficient of corrugated iron was not the same as new sample.



The specific parameter γ can be considered as a non-dimensional velocity of phase change because the phase change is assumed to occur slowly. This parameter can also be used to overcome numerical instabilities in the zone near the interface between the two phases of the PCM. Indeed, during the phase change, a mushy zone between the two phases is created. From a numerical point of view, sharp discontinuities at the phase interface are observed, implying some numerical instabilities very difficult to overtake. Moreover, it influences the derivative gradient of the solid fraction. However, its physical interpretation is still in investigation.

The parameters linked to the convective exchange coefficients are depicted in Figure 5 and all parameters are given by the Table 3. However, the unknown parameters have to be determined. For this, optimization sequences were performed. Outdoor convective exchange coefficient of the corrugated iron 218 (𝛼CI) Solar absorptivity coefficient of the corrugated iron

Empirical validation of PCM model

PCM model optimization using GenOpt ®

The optimization sequence consists in reaching the best set of parameters by maximizing or minimizing a chosen cost function, subject to a set of constraints (or a defined domain), until optimization criteria are reached. Indeed, many simulations are run and when a stopping criterion is reached, like the required error on the studied output for instance, the optimization is stopped.

To optimize the thermal model of PCM implemented in ISOLAB by using GenOpt ® , a methodology for the coupling of the building simulation code with the optimization program is required. The study has already been presented and the interested reader may see [START_REF] Bigot | Model optimization and validation with experimental data using the case study of a building equipped with photovoltaic panel on roof: Coupling of the building thermal simulation code ISOLAB with the generic optimization program GenOpt[END_REF] for details.

Among methods of fixing sets of parameters implemented in GenOpt ® , the GPS (Generalized Pattern Search) Hooke-Jeeves MultiStart Algorithm was used. Indeed, it allows to look over some parameters and to avoid that the result values are obtained from a local minimum value. In addition, this algorithm is compatible with all building thermal insulation code and gives reliable results.

The used cost function is calculated by using a mathematical model tool based on the modified standard deviation:

s= √ 1 n ∑(x i -x ̅) 2 n i=1 (4)
If several model outputs are used to optimize the model, the global cost function is the sum of the absolute values of costs functions for each output. The optimization sequence is stopped, if and only if, same minimum values of the cost functions were reached for 10 different optimization sequences. In our approach, several optimization sequences (1500 optimization sequences were reached approximately) and statistics studies were performed.

Results of the optimization.

Results from the optimization sequence are summarized in Table 4. Each value of an optimized parameter is found in agreement with the physical phenomena. Indeed, convective exchange coefficients are very small and correspond to the non-ventilated upper air layer as the building was kept closed during the experimental sequence. To apply the process for determining γ parameter, this coefficient has been evaluated to 0.01 when 𝑇 ≠ 𝑇 𝑚 . The value of absorptivity coefficient (αCI) is equal to the value that was determined by [START_REF] Bigot | Contribution à l'étude du couplage énergétique enveloppe/système dans le cas de parois complexes photovoltaïques[END_REF]. This value, lower than initially expected, can be justified by the fact that the cell was erected and covered a few years ago, time tending to decrease absorptivity or dark color roof. Indeed, over time, the performances of buildings will be not be the same than when the building was new [START_REF] Miranville | Contribution à l'étude des parois complexes en physique du bâtiment modélisation, expérimentation et validation expérimentale de complexes de toitures incluant des produits minces réfléchissants en climat tropical humide[END_REF].

Comparison between optimized thermal model of PCM with measurements

On the whole period, the dynamic behaviour of the components of the complex roof and the indoor air temperature are well predicted. Through the different curves (see Figure 6), we can ensure that the given melting temperature for this application was correctly chosen because the temperatures on both sides of PCM allow the storage and the release of energy during phase change process.

The surface temperature of suspended ceiling is predicted at ± 1.3°C (see Figure 7). The used conditions show that PCM model is able to properly predict the behavior of the PCM panel. The comparison between numerical simulations and experimental data shows a good agreement. The indoor air temperature of LGI test cell is predicted with an accuracy of ± 0.5°C (see Figure 8). The criteria for the validation of the thermal model are respected.

According to Table 5, the mean errors between numerical solutions and experimental measurements do not exceed 5%. The most important errors result from the prediction of air-gap temperature and the prediction of the metal sheet temperature in zone 2. For the air-gap, the model must be improved and models from literature based on CFD (Computational Fluid Dynamics) models showed that the results are inconclusive due to the influence of boundary conditions. So, an empirical correlation from experimentation will have to be determined. Nevertheless, the values of convective exchange coefficients (hce,CI and hci,PCM) determined by the optimization sequences correspond with the empirical correlation developed by Alamdari and Hammond [START_REF] Alamdari | Improved data correlations for buoyancy-driven convection in rooms[END_REF] (it has been verified later that the obtained results fit the correlation). The proposal of these authors is a combination of two correlations for taking into account both natural convection in laminar regime and turbulent regime:

h= [(1.51 |∆T| 1 4 H ) 6 + (1.33|∆T| 1
3 ) 6 ] 1 6
(5)

Where ∆T is the averaged difference temperature between the surface of the wall and the indoor air of the room. H corresponds to the height of the wall.

With the predicted air temperature in zone 2, the errors between the curves can also be explained by the prediction of the corrugated iron surface temperature. Indeed, the latter has a direct effect on the temperature of each component of the complex roof. To reduce these errors, the radiative model should be improved and the radiosity method should be used [START_REF] Miranville | Contribution à l'étude des parois complexes en physique du bâtiment modélisation, expérimentation et validation expérimentale de complexes de toitures incluant des produits minces réfléchissants en climat tropical humide[END_REF].

To conclude this step, the thermal model was fully-coupled with ISOLAB code and the results of PCM model are very encouraging. Indeed, for different type of walls with PCM or not, the model is able to predict temperatures in actual conditions. However, to definitely validate the PCM model implemented in the building simulation code ISOLAB, it is necessary to compare the numerical solutions with another experimental data sequence as presented in the next part.

The corroboration step

The corroboration step consists in using another experimental period in to verify if all parameters determined can be generalized and are not specific for a given period. Moreover, it also allows evaluating the efficiency of the proposed model. For this step of corroboration, the meteorological data used are from October 2 to 5, 2012. This period was characterized by [START_REF] Guichard | Contribution à l'étude des parois complexes intégrant des matériaux à changements de phase : Modélisation, Expérimentation et évaluation de la performance thermique globale[END_REF]:


an average maximal global radiation of 900 W.m -2  an average wind speed of 3.50 m.s -1  an average outdoor temperature of 26°C  an average rate humidity of 65%

The results from the corroboration step are summarized in Table 6. In this part, the validation criteria are also respected. For instance, comparison between numerical simulations and measurements for the predicted indoor air temperature is depicted in Figure 9. For more details, the interested reader may refer to [START_REF] Guichard | Contribution à l'étude des parois complexes intégrant des matériaux à changements de phase : Modélisation, Expérimentation et évaluation de la performance thermique globale[END_REF]. 6 show that maximum differences between predictions and measurements are a little more important than the results of the first experimental sequence. A possible explanation is a high setting of parameters for specific environmental conditions. Nevertheless, despite these differences the model can be considered as validated because the validation criteria have been reached again. Furthermore, the maximal standard deviation is approximately of 1.6°C and all mean errors are below 5%.

Conclusions and further works

In this paper, a generic thermal model of in building, validated with reliable experimental data, was presented. An actual building equipped with PCM in the complex roof was set up and each component's surfaces in contact with the indoor air temperature were measured. A detailed investigation was carried out to evaluate the efficiency of the thermal behavior of the model, with important steps included in experimental validation.

A mathematical model based on the apparent heat capacity has been presented. Moreover, an approach of nodal description of the complex wall and a finite difference method in one-dimensional were used.

Thanks to parametric sensitivity analysis, the most influential factors on model outputs such as, all convective exchange coefficients, γ parameter and the absorptivity coefficient of corrugated iron, were determined by a generic optimization tool. Then, a new comparison between the optimized thermal model and experimental data was performed. With the corroboration step, the results showed that the validity criteria were respected. Finally, the validation process of model has been reached and the thermal model of PCM has been validated. Despite the empirical validity of PCM's model, further works are necessary to improve the prediction of air-gap temperature and the radiative model used in order to have obtain better agreement between numerical solutions and measurements. Moreover, a mathematical formulation of γ parameter should be presented. Other experimental studies should be led to confirm the use of these materials in tropical climates as Reunion Island. Future works will also focus on the comfort study from the dedicated test cell.

Figure 1 .

 1 Figure 1. (a) LGI cell; (b) Experimental platform.

Figure 2 .

 2 Figure 2. Solar irradiation from 20th September to 24th September 2012 [13].

Figure 3 .

 3 Figure 3. Simplified scheme of LGI cell and instrumentation

Figure 4 :

 4 Figure 4: Methodology used for the empirical validation

Figure 5 . 3 .

 53 Figure 5. Most influential convective exchange coefficients

Figure 6 .Figure 7 .

 67 Figure 6. Comparison of model results with experimental measurements for all components of the complex roof and for inside air temperature (zone 1)

Figure 8 .

 8 Figure 8. Errors between numerical solutions and experimental data for inside air temperature

Figure 9 .

 9 Figure 9. Comparison and errors between model results with experimental measurements for inside air temperature (zone 1) during the corroboration step.

Table 1 .

 1 Arrangement of LGI test cell[START_REF] Guichard | A thermal model for phase change materials in a building roof for a tropical and humid climate: Model description and elements of validation[END_REF]

	Element	Composition	Remark(s)
	Opaque vertical walls	Sandwich board 80mm thick cement-fiber/polyurethane/cement-fiber
	Window	Aluminium frame, 8 mm clear glass	Blind-type 0.8x0.8m
			Glass in upper and
	Glass door	Aluminium frame, 8mm clear glass	lower parts,
			0.7x2.2m
	Roofing complex	Corrugated galvanised steel 1 mm/air layer of 280 mm thick/PCM 5.26 mm thick/ Plasterboard 12.5 mm	PCM is laminated to aluminium protective foils. Roof inclined at 20°
	Floor	Concrete slabs 80mm thick on 60 mm thick polystyrene

Table 2 .

 2 : Characteristics of PCM used[START_REF] Guichard | A thermal model for phase change materials in a building roof for a tropical and humid climate: Model description and elements of validation[END_REF]

	Parameter	Value	Unit
	Thermal properties
	Thermal conductivity: 𝜆 𝑠 /𝜆 𝑙	0.22/0.18	W.m -1 .K -1
	Heat capacity: 𝐶 𝑝𝑠 /𝐶 𝑝𝑙	3134/2833	J.kg -1 .K -1
	Latent Heat: 𝐿 𝑚𝑒𝑙𝑡𝑖𝑛𝑔	71	kJ.kg -1
	Melting temperature	23.4	°C
	Descriptive properties
	Thickness	5.26	mm
	Width	1000	mm
	Length	1198	mm

Table 4 .

 4 Parameters before and after optimization sequences

	Parameters	Before optimization	After optimization
	hci,floor	3.50	5.00
	hci,w	1.00	1.00
	hci,PCM	1.00	1.50
	γ (when 𝑇 ≠ 𝑇 𝑚 )	0.04	0.01
	hci,CI	3.50	1.75
	hce,CI	25	5.7V+11.4 [15]
	αCI	0.85	0.76

Table 5 .

 5 Standard deviations, maximum differences and errors after optimization sequences.

		Standard	Maximum	Maximum	Mean
	Localization	deviation 𝝈	difference	error	error
		[°C]	[°C]	[%]	[%]
	Inside air temperature (zone 1)	0.2	-0.5	-6.2	2.1
	Suspended ceiling inside surface temperature (plasterboard)	0.4	-1.1	-8.9	2.9
	Interface PCM/plasterboard temperature	0.4	-1.3	8.8	3.1
	Suspending ceiling outside surface temperature (PCM)	0.5	-1.7	-9.8	2.3
	Air-gap temperature (zone 2)	1.0	-2.6	-9.4	3.1
	Corrugated iron temperature	1.3	3.5	9.4	3.2

Table 6 .

 6 Standard deviations, maximum differences and errors for the corroboration period.

		Standard	Maximum	Maximum	Mean
	Localization	deviation 𝝈	difference	error	error
		[°C]	[°C]	[%]	[%]
	Inside air temperature (zone 1)	0.2	0.6	5.6	2.1
	Suspended ceiling inside surface temperature (plasterboard)	0.5	1.5	9.2	3.4
	Interface PCM/plasterboard temperature	0.5	1.7	8.9	3.6
	Suspending ceiling outside surface temperature (PCM)	0.5	1.7	9.9	2.8
	Air-gap temperature (zone 2)	1.3	3.4	8.9	3.2
	Corrugated iron temperature	1.6	4.7	9.8	3.3

Table 5 and

 5 Table

Acknowledgments

The authors wish to thank Fonds Social Européen and La Région Réunion for their support and their fundings of the first author's thesis. In addition, this research received fundings from the Ministère de l'Outre-Mer.

Author Contributions

Stéphane GUICHARD designed the experiments and developed PCM model for the experimental and numerical studies. Frédéric MIRANVILLE, Dimitri BIGOT and Harry BOYER helped for the coupling model of PCM with ISOLAB code and performed the validation stages of this one. Bruno MALET-DAMOUR and Teddy LIBELLE helped to monitor the data from the experimentation in order to ensure they were reliable for the empirical validation of the PCM model.

Conflicts of Interest

The authors declare no conflict of interest.


Philip Daian

Yliès Falcone

Patrick Meredith

Traian Florin

S ¸erbȃnut ¸ȃ

Shin'ichi Shiriashi

Akihito Iwai

Grigore Rosu
email: grosu@illinois.edu

RV-Android: E cient Parametric Android Runtime Verification, a Brief Tutorial

RV-Android is a new freely available open source runtime library for monitoring formal safety properties on Android. RV-Android uses the commercial RV-Monitor technology as its core monitoring library generation technology, allowing for the verification of safety properties during execution and operating entirely in userspace with no kernel or operating system modifications required. RV-Android improves on previous Android monitoring work by replacing the JavaMOP framework with RV-Monitor, a more advanced monitoring library generation tool with core algorithmic improvements that greatly improve resource consumption, e ciency, and battery life considerations. We demonstrate the developer usage of RV-Android with the standard Android build process, using instrumentation mechanisms e↵ective on both Android binaries and source code. Our method allows for both property development and advanced application testing through runtime verification. We showcase the user frontend of RV-Monitor, which is available for public demo use and requires no knowledge of RV concepts. We explore the extra expressiveness the MOP paradigm provides over simply writing properties as aspects through two sample security properties, and show an example of a real security violation mitigated by RV-Android on-device. Lastly, we propose RV as an extension to the next-generation Android permissions system debuting in Android M.

Introduction

With the rise in popularity of Android [START_REF]Android Developers[END_REF], a Linux-based consumer smartphone operating system, the need for e↵ective techniques to improve the security and reliability of third-party applications running on end user devices is well established [START_REF] Falcone | Runtime verification and enforcement for Android applications with RV-Droid[END_REF]. One solution explored by previous work in the field is the use of runtime verification and runtime enforcement to detect and recover from violations of formal safety properties during the execution of Android applications [START_REF] Falcone | Runtime verification and enforcement for Android applications with RV-Droid[END_REF] [START_REF] Bauer | Runtime verification meets Android security[END_REF]. Some previous work in this space has relied on using kernel modifications to the Linux base of Android to generate the runtime traces required to verify safety properties [3] [4]. This solution is inflexible for several reasons: it requires root access to the device to install, requires reinstallation on each operating system upgrade, and provides few additional guarantees from a compromised kernel over a userspace monitoring solution.

Other RV-based Android work has used JavaMOP, an experimental monitor oriented programming framework, to generate Android monitoring libraries which are weaved into third-party userspace applications, providing monitoring functionality and guarantees without requiring kernel-level modifications [START_REF] Falcone | Runtime verification and enforcement for Android applications with RV-Droid[END_REF].

This approach has been demonstrated using AspectJ [START_REF]Eclipse: The AspectJ project[END_REF] for weaving, and allows us to weave binary bytecode useful towards instrumenting o↵-the-shelf third party packaged applications (apk's) [START_REF] Falcone | Runtime verification and enforcement for Android applications with RV-Droid[END_REF] [START_REF] Falcone | Weave Droid: aspect-oriented programming on Android devices: fully embedded or in the cloud[END_REF]. Our work focuses on improving these approaches with e cient and versatile runtime verification tools that benefit from the previous research endeavors related to JavaMOP, resulting in a unified and open framework for runtime verification and analysis of Android applications.

Contributions

RV-Monitor is a proprietary library generation technology, allowing for the runtime monitoring, verification, and enforcement of safety properties through the generation of generic monitoring libraries. RV-Monitor is provided free for noncommerical use, and represents the evolution of the prototype JavaMOP tools with improvements in the codebase and core algorithms. Like JavaMOP, RV-Monitor supports logic plugins, allowing for the specifications of properties in multiple formalisms including regular expressions, context-free grammars, automata, and past-time linear temporal logic.

We make the case for the future use of RV-Monitor and its related Android runtime library for use in runtime verification and runtime enforcement of Android applications. We compare monitor-oriented programming techniques to popular aspect-oriented techniques, acknowledging the usefulness of both and supporting both as property inputs to our tools. We analyze a real security violation on the Android platform with the potential to be stopped by monitororiented programming, including the relevant property with our tool's distribution. Lastly, we discuss the future of RV on the Android platform and lay out a roadmap for future industry-lead work in the space.

RV-Android Overview and Build Process

RV-Android consists of two components, a monitoring library generation tool and a runtime environment used in the generation of these libraries for dynamic on-device property monitoring and violation recovery. For the first of these RV-Monitor is used o↵-the-shelf, allowing for the specification of both formal properties over events and the instrumentation points for these events in a single monitor-oriented file. This monitor-oriented programming is achieved through a new version of JavaMOP, a lightweight compiler that generates RV-Monitor (monitoring library) and AspectJ (program instrumentation) output. Unlike versions of JavaMOP used in previous work, which were fully responsible for monitoring applications and did not leverage RV-Monitor, this next-generation JavaMOP stands to benefit from the significant core algorithmic improvements that form the basis of the RV-Monitor IP [START_REF] Luo | RV-Monitor: E cient parametric runtime verification with simultaneous properties[END_REF] while completely separating the generation of e cient monitoring libraries from application instrumentation.

In our work, we will separate the discussion on instrumentation from the discussion on event and property definitions. We do this to leave open the possibility of future instrumentation models. While we focus on instrumentation methods using AspectJ in this work, other instrumentation mechanisms for packaged Android binaries have already been e↵ectively demonstrated and proved [START_REF] Falcone | Runtime verification and enforcement for Android applications with RV-Droid[END_REF][START_REF] Falcone | Weave Droid: aspect-oriented programming on Android devices: fully embedded or in the cloud[END_REF][START_REF] Mulliner | Dynamic binary instrumentation on Android[END_REF][START_REF] Bodden | Instrumenting Android apps with Soot[END_REF]. RV-Monitor is compatible with any Java instrumentation method, and the Java-MOP project can be extended to generate the required input for other instrumentation tools if necessary.

Our website, http://runtimeverification.com/android, provides downloads and full instructions for the use of RV-Android, as well as the examples we discuss in the remainder of the paper and a video demonstrating a few currently available capabilities of the tool.

Build Process

Fig. 1: RV-Android Build Process

The RV-Android process (shown above in Figure 1) forms the basis of all tools based on RV-Android. Taking either a binary packaged Android application or set of source files as input, RV-Android additionally optionally takes any (or all) of aspect files, RV-Monitor properties, and monitor-oriented programming (MOP) files compatible with the JavaMOP tool. This flexibility in input allows RV-Monitor to be used with a wide variety of property formats, including aspectoriented AspectJ properties that do not require formalisms or the additional features provided by RV-Monitor or JavaMOP.

By being able to mix and bundle these diverse formats together into a single set of properties as input to a single tool, property developers and application developers have an easy way to develop, apply, and share dynamic properties of their choice without the need to constrain themselves to a single tool. Futhermore, property developers have the ultimate control over the instrumentation of their properties in the original application: they can choose to use AspectJ directly, use MOP, or use other techniques of manual instrumentation. In doing so, the goal is to create a platform in which all developers of runtime properties for the Android platform feel comfortable using their preferred technologies, encouraging third-party property development.

RV-Monitor also features a flexible plugin architecture that allows for the development of custom or third-party formalisms supported by the tool, allowing virtually unlimited expressiveness in the properties it defines. By combining this with instrumentation in a single monitor-oriented programming files, advanced developers can write complex properties succinctly while defining simple properties not requiring dedicated formalisms in native Java directly through AspectJ.

RV-Android is also an open source project built around the closed source RV-Monitor project, but can be used without RV-Monitor as an aspect oriented programming platform, as well as extended to work with any number of tools supporting Java transformation and analysis. Because it is open source, RV-Android can also be extended by other tool developers who provide runtime analysis and verification of applications to integrate any technique into its workflow. We are already developing prototype extensions for taint analysis and other popular dynamic analysis techniques, extending the capabilities of RV-Android beyond the capabilities of any single tool.

Figure 1 shows the output of RV-Android as a signed, packaged Android application to be distributed to users. By signing all verified and monitored applications with an "RV" key from a source trusted by the user, the user's smartphone can then verify that the application has been correctly monitored and transformed to the specifications provided as input to the tool.

Excluded from the figure is the inclusion of the AspectJ and RV-Monitor runtimes in the monitored and instrumented application. These runtimes are needed for the instrumentation and monitoring of the application on-device, and are simply the binary runtimes as provided by each project.

RV-Android for Developers

In order to provide a full framework for runtime verification and enforcement on the Android platform, we must allow developers to complete their two primary tasks of interest with regards to runtime verification: developing new properties to check on their applications and third-party applications, and checking their own applications against existing property sets. To do this, we provide two versions of RV-Android for developers, targeted at two possible use cases. The first allows developers to integrate RV-Android into projects where they are using the standard Android build process and have access to the source code of the application, instrumenting source code directly. The second version is able to monitor properties of binary Android applications, or apks, and can be used on any application that runs on the Android platform.

Monitoring Source Code To monitor source code, we provide a version of RV-Android called the "developer source" edition. Found in the "developer src" subdirectory of the RV-Android distribution, this edition requires the developer to create two directories, "aspects" and "properties". By placing AspectJ files and RV-Monitor or MOP properties in the relevant directories and following the remainder of the setup instructions for the source edition, developers can integrate monitors and runtime verification in their build and testing process with no modification required to the source of the application itself.

This provides a convenient way for developers interested in obtaining the maximum assurance from their Android applications to leverage runtime verification. Additionally, developers using the default Android build process who wish to ship monitors integrated with their final application to end users (for assurance, security, or enforcement purposes) can use this version to monitor their source directly, requiring no binary transformations.

Monitoring Binary APKs

The second and more flexible distribution of RV-Android for developers focuses on monitoring arbitrary binary Android applications, and is referred to as the "command line" distribution. This distribution can also be used by advanced users who are comfortable using command-line tools. Similarly to the previous application, the tool takes both properties and aspects, and has a simple command-line interface with parameters as follows:

.

/rv_android [apk] [keystore] [keystore password] [signing key alias] [monitors_directory] [aspects_directory]

Because of its simplicity and extensibility, this version of RV-Android can be integrated into any environment or build process. We recommend this version to all new developers interested in RV on Android.

RV-Android for End Users -GUI Frontend

For end-users who are not familiar with command-line applications and property development, but still wish to gain some additional assurance in or control over Fig. 2: RV-Android On-Device Architecture Fig. 3: RV-Android Screenshots, Application and Property Selection their applications, we provided a GUI version of RV-Android. The architecture of this system is shown in Figure 2. RV-Android runs entirely on a remote server in the cloud, which runs the same CLI version of RV-Android with the workflow in Figure 1. The program on the user's device is simply a shell allowing them to manage and select properties, and select an application on their device to instrument. This is similar to previous approaches applied to runtime verification on Android [START_REF] Binns | Domain specific software architectures for guidance, navigation and control[END_REF].

Through this graphical user interface, we allow users that may be completely unfamiliar with RV or its concepts to apply generic "properties" to any of the applications currently on their device. We also allow them to download thirdparty sets of properties and read their descriptions.

Such an application aims to bring RV to the mainstream by providing simple, human-readable descriptions of what each property does or checks for and allowing any property to be used with any userspace application on any Android smartphone, without requiring root access. In the user frontend, there is no distinction made between properties written as aspects, monitors, or other formats, all of which are simply referred to as "properties".

We believe such a platform is an ideal introduction point to runtime verification for users and developers alike. With the increased importance of security on mobile devices, which often carry personal information and other sensitive data [START_REF] Enck | Understanding Android security[END_REF] [START_REF] Shabtai | Google Android: A comprehensive security assessment[END_REF], and the ability to instrument any arbitrary binary Android application by virtue of the Java bytecode format used, we are able to show o↵ the powerful and generic nature of runtime verification technology in an environment becoming increasingly important to end users.

Figure 3 shows two screenshots of the RV-Android frontend for end-users, currently in beta. Users select an application followed by a set of properties to apply to the application, with the remainder of the process being automated. These properties have extended descriptions that can be viewed by the user, and can be extended to include custom or user-defined properties. Applications can also be filtered by those requesting a set of permissions considered by the user to be particularly sensitive.

Towards Practicality -RV-Android Case Studies

Having presented the overall architecture and currently available distributions of the RV-Android tool, the question of whether such techniques are practical and cost e↵ective for use on real applications and devices arises naturally. The practicality of the tools presented hinges on the ability to develop a useful set of properties supported by the tool, which can then be shared, packaged, and distributed to end users for monitoring of arbitrary applications on-device or used by developers to test and evaluate their applications against the given set of API rules, coding best practices, and security properties.

To address the matter of usable properties, we will first consider the ideal language for expressing properties. Because RV-Monitor supports a variety of techniques for writing properties, including raw aspect-oriented properties and monitor-oriented properties that define both formal mathematical properties and their instrumentation, it is important to note the drawbacks and advantages of both techniques.

Two Properties in MOP and AspectJ

Blocking Device Location and Network Accesses The first property is a security property intended to block malicious or questionably-sourced applications from accessing a user's location through the Android location API. The second property is not security oriented as the first one is. Instead, it merely logs and notifies the user when an application attempts to use an Android API call related to networking and connections to the Internet.

The Properties in AspectJ We present how to implement monitors for the two properties in AspectJ. Note, the monitors make use of the following imports: import android.app.Activity; import android.content.Context; import android. content.ContextWrapper; import android.widget.Toast;

The monitor for blocking the device location is shown in full in aspect form in Listing 1.1. It prints a message to the user and log noting the attempted location access, and denies the access by returning null to the aspect around() join point rather than proceeding with the original call. It is clear from examining the property that there is a lot of code that can be automatically generated, including the code required to track the current activity in order to show the notification to the user.

The monitor for keeping track of network accesses is shown in full in aspect form in Listing 1.2. The monitor does not attempt to preserve any security properties (such as an unknown application cannot access user location). Instead, it merely logs and notifies the user when an application attempts to use an Android API call related to networking and connections to the Internet.

The monitors for these properties share a large amount of code, which is expected as both are fundamentally performing the same task (notifying the user of some event occurring on the device). This also suggests that there is a significant potential for automatically generating the monitor, and that both monitors could be expressed more concisely.

The Properties in MOP While aspect-oriented programming is one approach to monitoring and analyzing applications on the Android platform [START_REF] Falcone | Weave Droid: aspect-oriented programming on Android devices: fully embedded or in the cloud[END_REF], a newer paradigm familiar to the runtime verification community involves using the monitoring-oriented programming paradigm. Listing 1.3 shows the same property being enforced as in Listing 1.1 with a monitor defined with significantly less code. Using several keywords provided by RV-Monitor and RV-Android, particularly TOAST and SKIP, which in addition to ACTIVITY form the basic keywords for user interaction currently supported by RV-Monitor, we automatically generate much of the code performing similar functions to the previous monitors in AspectJ. S t r i n g method = t h i s J o i n P o i n t . g e t S i g n a t u r e ( ) . getName ( ) ; 11 S t r i n g c l a s s e = t h i s J o i n P o i n t . g e t S i g n a t u r e ( ) . getDeclaringType ( ) . getName ( ) ; Similarly, Listing 1.4 shows the same monitor as in Listing 1.2 using MOP format. Some clear advantages include shorter property that is easier to write, debug, and validate for developers and even advanced end-users.

a s p e c t BlockG etLocation e x t e n d s A c t i v i t y

Neither of these properties, however, leverage the primary feature of RV-Monitor, which is the ability to define logical properties over the event trace of an application in a variety of formalisms.

One example of using such formalisms is shown in Listing 1.5, which combines the previous two properties by denying all network-related API calls after the user's location is accessed. The access is otherwise permitted by the system.

The property is formally defined by a finite state machine in which the first state is safe, as the application has not accessed any location information. The application accessing any location information brings it to an unsafe state, after which any network access lead to a "denied" state. On entering the denied state, the monitor skips the function call to the network, returning null rather than executing that call. The distinction between the unsafe and deny states is that 1 a s p e c t WebAspect e x t e n d s A c t i v i t y { 2 // Android I n t e r n e t methods Listing 1.2: Aspect-Oriented Property Monitoring Network Accesses the unsafe state does not skip the call, allowing for further location accesses after the first access, but not for further Such a property is useful to users concerned about the leakage of their location data, though it is not in its current form comprehensive for all possible data exfiltration channels on Android devices.

In addition to allowing for the addition of logic to Android programming, RV-Monitor can extremely e ciently monitor parametric properties, or properties of a specific Java object, class, or memory location and allowing for millions of monitors to be created with low runtime overhead [START_REF] Luo | RV-Monitor: E cient parametric runtime verification with simultaneous properties[END_REF]. This expressiveness and low overhead makes RV-Monitor ideal for a wide range of properties, from simple global properties like the above to complex parametric properties.

1 import j a v a . l a n g . ⇤ ;

Preventing Security Violations -A Real Attack

While the above properties may be useful for users wishing to gain fine grained control over the privacy of their data when faced with potentially malicious applications, they are generally ine↵ective in protecting against real attacks. Listing 1.6 shows a MOP monitor in blocking a wide range of attacks. Similarly to the monitors in the previous subsection, this is a simple monitor designed to skip all calls to any exec method in the Runtime class. This method in the Android API allows developers to execute shell code directly through the currently running process, allowing for arbitrary commands interpreted by the Linux kernel underpinning Android [START_REF]Runtime -Android Developers[END_REF].

One potential practical application of this property is the disabling of currently available Tor libraries, which are becoming widely used on Android in a malware context [START_REF]TrendMicro Security Intelligence Blog: Android ransomware uses tor[END_REF]. The Tor network allows malware, including spyware, adware, and ransomeware, to obfuscate its network connections to command and control servers, the location of which can be hidden from law enforcement and the public [START_REF]Cybercriminals are using the Tor network to control their botnets[END_REF]. A 2014 survey of Android security by Google specifically mentions ransomware as an up-and-coming problem needing to be addressed by the Android security team, further suggesting the application of dynamic and static analysis techniques against spyware and other malicious applications which often use Tor to communicate with their operators [START_REF]Google report Android security 2014[END_REF][START_REF]TrendMicro Security Intelligence Blog: Android ransomware uses tor[END_REF].

The above property disbales Tor due to the code in Listing 1.7, which needs to install executable binary blobs of native code. Because there is no native file 1 import j a v a . l a n g . ⇤ ; permission API on Android, the above aspect blocks all attempts to change file permissions and thus install native code from any third-party applications. In doing so, it blocks a wide range of potential attacks and privilege escalation exploits which rely on shell access, rendering it a powerful practical defense against violations of user privacy by malware that leverages the Tor network.

To test this property, it is su cient to instrument the "Orbot" application in the Play store and attempt to run it on-device for the first time. We include detailed instructions and a sample of such monitored applications on https: //runtimeverification.com/android, one of which is a sample of real spyware disabled through the monitoring and enforcement of the above property.

Into the Future -Beyond Android Permissions

The future of the Android platform brings a substantial amount of change, with an ever increasing level of the platform's popularity and a significant number of potentially harmful applications still being deployed to user devices regularly [START_REF]Google report Android security 2014[END_REF].

1 import j a v a . l a n g . ⇤ ;

Android M -A New Permissions Model

One of the most recently announced changes in the fundamental security model of the Android platform is the change in the permissions system being released with Android M. Rather than simply granting an application blanket permission to perform all operations in a given category, application permissions can be revoked at any time by the user [16]. One example of this is the revocation of location permissions from applications which may be leaking user data to third parties. This replaces many of the simpler security properties and aspects previously written targetting Android permissions, including the location property presented in this paper.

Despite this, as shown in Listing 1.5, RV-Android can provide much finer grained control over how permissions are used on device, revoking or granting permissions dynamically based on logical properties of the application state or current trace. In this way, context-sensitive permissions become possible for cases where a high level of control is desirable. One perfect example of this is the revocation of the Internet permission we discussed, which is now granted by default and without user confirmation to all applications being installed in Android M [START_REF]Android Police: Android M will never ask users for permission to use the internet, and that's probably okay[END_REF]. This change potentially removes some control from the user related to which applications have network access. However, because almost all applications rely on network access, context-sensitive permissions in which allowed hosts are whitelisted and certain services (like Tor or known ad networks) are blacklisted, and in which the level of action reacts to other system events may be more appropriate for informing the end user and providing them with ultimate control.

Using runtime verification and monitoring, one can control every category of permission and API access, specifically defining the access patterns and data allowed to the application. By defining such specific and tightly controlled executions, users can notice and prevent malicious or unexpected application behavior. Such control may be useful for employers with employees dealing with sensitive data on Android devices, and in all security-sensitive Android applications. The ability to run third-party applications on such devices introduces security vulnerabilities, a wide range of which can be detected and prevented with runtime verification.

Integrating with Other Approaches

In addition to preventing security violations as they occur, RV-Android can be used as a testing tool on a large number of applications to detect the presence of such violations in third party applications. In doing so, RV-Android can leverage a number of automated unit testing tools already available for Android designed to mimic and mock user behavior on the platform [START_REF] Amalfitano | Using GUI ripping for automated testing of Android applications[END_REF] [19], checking a large number of properties automatically.

In addition to testing, RV-Android could potentially integrate with other dynamic analysis tools, including popular tools designed to ensure data security through taint analysis. Taint analysis is a popular technique that tracks sensitive information as it is handled by applications, preventing it from leaving through any unprivileged API calls or other "sinks" [START_REF] Arzt | Flowdroid: Precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for Android apps[END_REF] [START_REF] Fritz | Highly precise taint analysis for Android applications[END_REF]. By integrating many such techniques, we aim to create the foremost security tool and platform for Android, with an ability to implement any future dynamic analysis techniques desirable to users and developers.

Lastly, runtime verification can integrate with static analysis to improve its e ciency and inform the automatic generation of properties checkable at runtime [START_REF] Bodden | Collaborative runtime verification with Tracematches[END_REF]. While there are no concrete plans to do so in RV-Android currently, this remains a future potential research direction.

Towards a Public Property Database

Undoubtedly the most important work in developing a framework for practical Android runtime verification is the development of properties that thoroughly encompass both known misuses of the Android and Java API's and violations of secure states by previously observed malware. To this end, we are developing a property database which provides annotated copies of both the Android and Java API's with RV-Monitor properties and AspectJ instrumentation built in. The current property database can be viewed and downloaded for free at https://github.com/runtimeverification/property-db/, and can be used by RV-Android with minimal modification. The property database currently contains around 180 safety properties of the Java API, which can be practically simultaneously monitored by our technology. These properties di↵er substantially from the security properties presented in this paper in that they monitor correct use of the API and thus functionality of the application rather than attempting to enforce the security of the device itself. This flexibility of RV-Android in capturing a wide range of potential properties on Android, together with this robust database of existing properties provides a good starting point for the development of a comprehensive dynamic analysis and runtime verification tool.

We further plan on providing additional privacy profiles focused on stronger security guarantees for the security conscious user, such as profiles useful in avoiding data exfiltration when using specific API's. While we will still allow users to define their own properties, the utility of future iterations of RV-Android will stem partially from the robustness of the default properties in our property database.

6 7 9 { 10

 6910 v a t e A c t i v i t y a c t i v i t y ; 5 p r i v a t e Object o b j e c t ; Object around ( ) : c a l l ( ⇤ a n d r o i d . l o c a t i o n . . ⇤ ( . . ) ) 8 && ! w i t h i n ( BlockGetLocation )

3 p

 3 o i n t c u t webCall ( ) : c a l l ( ⇤ a n d r o i d . net . . ⇤ ( . . ) ) | | c a l l ( ⇤ a n d r o i d . webkit . WebView . . ⇤ ( . . ) ) | | c a l l ( ⇤ j a v a . net . HttpURLConnection . .

2 3 5 / 8 SKIP ; 9 } 10 } 2 3 5 / 11 12 }

 258910251112 Android DenyLocation ( ) { 4 / Deny a l l l o c a t i o n package c a l l s 6 e v e n t l o c a t i o n Object around ( ) : c a l l ( ⇤ a n d r o i d . l o c a t i o n . . ⇤ ( . . ) ) { 7 TOAST ( " A p p l i c a t i o n a c c e s s i n g l o c a t i o n i n f o r m a t i o n . " ) ; Listing 1.3: Monitor-Oriented Property Blocking Location Accesses 1 import j a v a . l a n g . ⇤ ; Android MonitorNetwork ( ) { 4 / D i s p l a y a p p l i c a t i o n t o a s t on a l l network API c a l l s 6 e v e n t w e b c a l l a f t e r ( ) : c a l l ( ⇤ a n d r o i d . net . . ⇤ ( . . ) ) 7 | | c a l l ( ⇤ a n d r o i d . webkit . WebView . . ⇤ ( . . ) ) 8 | | c a l l ( ⇤ j a v a . net . HttpURLConnection . . ⇤ ( . . ) ) { 9 TOAST ( " A p p l i c a t i o n a c c e s s i n g th e I n t e r n e t , " ) ; 10 } Listing 1.4: Monitor-Oriented Property Monitoring Network Accesses

2 3 5 e 6 | 7 | 9 } 10 11 e 20 uListing 1 . 5 :

 2567910112015 Android MonitorLocationNetwork ( ) { 4 v e n t w e b c a l l Object around ( ) : c a l l ( ⇤ a n d r o i d . net . . ⇤ ( . . ) ) | c a l l ( ⇤ a n d r o i d . webkit . WebView . . ⇤ ( . . ) ) | c a l l ( ⇤ j a v a . net . HttpURLConnection . . ⇤ ( . . ) ) { 8 TOAST ( " A p p l i c a t i o n a c c e s s i n g th e I n t e r n e t , " ) ; v e n t l o c a t i o n Object around ( ) : c a l l ( ⇤ a n d r o i d . l o c a t i o n . . ⇤ ( . . ) ) { 12 TOAST ( " A p p l i c a t i o n a c c e s s i n g l o c a t i o n i n f o r m a t i o n . " ) ; a t i o n > u n s a f e 18 w e b c a l l > s t a r t 19 ] n s a f e [ 21 w e b c a l l > deny 22 l o c a t i o n > u n s a f e 23 ] c a l l > deny 26 l o c a t i o n > u n s a f e 27 ] Monitor-Oriented FSM Property Preventing Network Accesses after Location

2 3 5 / 7 SKIP ; 8 } 9 } 2 { 3 . . . // Copy f i l e 4 /

 25789234 A n d r o i d B l o c k S h e l l E x e c ( ) { 4 / Skip a l l s h e l l e x e c u t i o n c a l l s 6 e v e n t s h e l l c a l l Object around ( ) : c a l l ( ⇤ Runtime +. e x e c ( . . ) ) { Listing 1.6: Monitor-Oriented Property Blocking Shell Calls 1 p u b l i c s t a t i c v o i d copyRawFile ( Context ctx , i n t r e s i d , F i l e f i l e , S t r i n g mode , b o o l e a n i s Z i p d ) throws IOException , I n t e r r u p t e d E x c e p t i o n / Change t h e p e r m i s s i o n s 5 Runtime . getRuntime ( ) . e x e c ( "chmod "+mode+" "+a b s p a t h ) . w a i t F o r ( ) ; 6 } Listing 1.7: Potentially Malicious Code Installing the Tor Network from Orbot

Acknowledgements

We would like to thank Patrick Meredith for developing the initial prototype of RV-Monitor applied to Android applications and continued feedback, as well as our partners at ITC and Denso for their continued support in the investigation of Android-related work for the automotive domain. We would also like to thank the miSecurity application team, for providing a basis for the graphical user frontend we describe.