Rima Al Ali
email: alali@d3s.mff.cuni.cz

Ilias Gerostathopoulos
email: iliasg@d3s.mff.cuni.cz

Inti Gonzalez-Herrera

Adrian Juan-Verdejo
email: adrian.juan@cas.de

Michal Kit
email: kit@d3s.mff.cuni.cz

Bholanathsingh Surajbali
email: b.surajbali@cas.de

An Architecture-Based Approach for Compute-Intensive Pervasive Systems in Dynamic Environments

Distributed systems have continued to evolve and we note two important trends: the dramatically increasing level of dynamism in contemporary distributed systems and the convergence of mobile computing with cloud computing. The end result is that it is very difficult to achieve the required level of scalability and dependability in a systematic way when considering pervasive systems that are software-and compute-intensive and whose functionality is typically augmented by static cloud infrastructure resources. This work discusses relevant challenges and requirements for integrating cloud computing with pervasive systems operating in dynamic environments. We present a set of requirements using a holistic case study and describe a reference architecture to address these requirements.

INTRODUCTION

Rapid advancements in mobile devices, wireless sensors and mobile communications have led to the development of cyberphysical systems, pervasive computing and smart environments with important applications in environmental, civilian, military, industry, and government sectors. However, the ability of mobile devices and pervasive systems to perform intense computation is limited due to small battery life and computing power. To alleviate this limitation many research works such as Fog computing [START_REF] Hong | Mobile Fog: A Programming Model for Large-scale Applications on the Internet of Things[END_REF], cloudlets [START_REF] Satyanarayanan | The Case for VM-Based Cloudlets in Mobile Computing[END_REF], or client-edge-server ecosystem [START_REF] Bonomi | Fog Computing and Its Role in the Internet of Things[END_REF] have emerged to bring the computing power of cloud data centers closer to the end devices. The objective is to offload part of the computation, needed to deliver the right quality of experience to the end user, to scalable server infrastructure while ensuring low latency and small delays.

However, these research works do not address problems of dynamic and open-ended environments, such as unreliable communication, intermittent connections and physical mobility, which are typical in modern cyber-physical systems. Such types of systems require a significant level of self-awareness and autonomy so that they can dynamically adapt to changes in their operational environment and recover from potential failures. In this context research initiatives, such as the EU FP-7 projects ASCENS 1 and QUANTICOL 2 , have been leading efforts of featuring the appropriate computation models and development processes to develop large-scale distributed autonomic and adaptive systems. Specifically, ASCENS approach is based on the 1 http://www.ascens-ist.eu 2 http://blog.inf.ed.ac.uk/quanticol/ novel concept of grouped, attributed-based communication between service-components [START_REF] Hölzl | Software Engineering for Ensembles. Software-Intensive Systems and New Computing Paradigms[END_REF].

What is missing is a common reference architecture that will combine the advantages and promises of high-bandwidth, lowlatency cloud-based systems with that of distributed adaptive systems. Using such a reference architecture would allow for building Compute-Intensive Pervasive Systems (CIPS). This paper proposes the following contributions towards reaching this goal:  A CIPS cloud reference architecture. In CIPS resourceconsuming jobs of pervasive devices operating in dynamic environments are delegated to external infrastructure with sufficient computing capabilities, while the system is still able to provide basic services in a best-effort manner when no infrastructure is available or fail gracefully in a controlled manner.  A CIPS model-based validation. We validate our approach using a model-based approach through a holistic case study from the domain of emergency coordination using Kevoree [START_REF] Fouquet | A Dynamic Component Model for Cyber Physical Systems[END_REF] and DEECo [START_REF] Bures | DEECo -an Ensemble-Based Component System[END_REF] component systems.

The paper is structured as follows. First, in Section 2, we describe the main challenges required by CIPS using a fire-fighters usecase scenario. Then, in Section 3 we describe the proposed reference architecture approach, followed by Section 4, where we describe the instantiation of the reference architecture using DEECo and Kevoree. Next, in Section 5 we analyse the applicability of our approach at different scenarios and discuss the implementation aspects of our approach, followed by Section 6 providing an analysis against related work. Finally in Section 7 we present our conclusions and identify areas of future work.

CASE STUDY

Let us consider that an emergency such as a fire or a hurricane breaks out. A firefighting department deploys a team of firefighters and a team leader within the emergency field. The team leader organizes, commands, and sends feedback to teams. Nowadays, firefighting departments can provide their teams with sensing and actuating devices due to the lower cost of technology and the need to improve safety and decision making during an emergency. As a result, firefighting departments and team leaders are able to obtain a lot of data gathered in real-time about firefighters' position, health condition, or surrounding environment. As firefighters can now be better tracked, they can be more effectively commanded by their team leader.

In our case study, team members are provided with batterypowered mobile sensing and computing devices with wireless capabilitiessee Figure 1. Those devices capture information about their environmentfor example humidity, noise, location, air quality, or temperatureand communicate through a mobile ad-hoc network. The devices carried by firefighters' could lose at times wireless connectivity but are always able to independently sense, compute and actuate. However, mobile devices are not necessary able of doing compute-intensive tasks due to battery, or CPU and memory restrictions. Team leaders carry devices with better computation and battery capabilities that aggregate data so that useful global information can be extracted. Additionally, there are data centers in the vicinity of these sensing and/or actuating devices, which are not restricted in terms of battery or computing power. In such setting, mobile devices should be able to offload compute-intensive tasks with real-time requirements to data centers in the vicinity so that the overall system overcomes its inherent risksincreased latencies, slow response times, increased delays, disconnection from the network, or battery drainagethat might hinder the real-time and resourcedemanding scenarios. Additionally, cloud environments accessed through the internet could be employed to execute non real-time tasks such as Big Data analysis, data aggregation that allows coordination with other firefighting departments, or training of prediction models.

We list here some application scenarios where the available technology can greatly benefit the firefighters in their job.

1. Image and video recognition. Thermal images captured by the firefighter's device can be processed to identify potential risks the firefighter is unaware of. Mobile devices carried by the firefighters do not have the necessary resources to carry out this compute-intensive processing [START_REF] Kumar | Cloud computing for mobile users: Can offloading computation save energy?[END_REF].

2. Augmented reality. In an augmented reality scenario, the system sends live video stream to firefighters to notify them of what they cannot see due to smoke, obstacles, or their high levels of stress. This scenario demands low communication latencies and fast response times.

3.

Real-time decision making. Data are sensed via spatially distributed sensors, pre-processed and aggregated in order to extract meaningful information, which is then available to the team leader. This in turn enhances the leader's decision making process due to his or her "virtual sensing" capability.

4.

Timely actuation based on sensed information. Sensed data based on humidity, temperature, or oxygen concentration are aggregated. If these data are timely processed, the output can trigger a response sent to devices carried by firefighters to let them know of a dangerous situation a fellow firefighter might be facingdue to, e.g., high temperatures in his or her surroundings.

APPROACH

In this section the main components of our architectural solution are presented. The solution is inspired by, but not restricted to, the specific challenges outlined in the case study. Indeed, it is envisioned that the proposed architecture can act as a template, in the form of a reference software architecture [1] that will guide the structuring of applications deployed on CIPS.

Nodes and their dependencies

A target application instance comprises a number of entities with distinct roles and dependencies. At the early requirements stage, their dependencies can be depicted using the Strategic Dependency diagram [START_REF] Maiden | Generating requirements from systems models using patterns: a case study[END_REF] as the one depicted in Figure 2.

We differentiate between four types of nodes:

i. Low-power nodes. Typically mobile sensor nodes scattered around in the physical environment. They are responsible for acquiring the sensor data and disseminating them to the other nodes in their vicinity, which are either low-power or resource-poor nodes (described next). For that, they need to possess hardware sensing capabilities. These nodes can also act as actuators, in which case they get to have a direct impact on their physical environment or on the end-user experience.

In the case study, low-power nodes are small wearable devices that can measure a firefighter's acceleration, position, oxygen level and external temperature. In a more sophisticated scenario, the low-power nodes include image/video recording devices and augmented reality glasses, which both sense, by means of capturing the firefighters' vision as a constant video stream, and actuate, by providing visual aid to the firefighters (e.g., pointing to the exit of a building in case of limited visibility because of smoke).

ii. Resource-poor nodes. Mobile nodes with limited computation power and with energy constraints. They are responsible for aggregating the sensor data from the low-power nodes. The aggregated data allow for a number of resource-and computeintensive tasks, such as online image/video analysis. To prevent possible short-term resource starvation, they delegate the task of online data analysis (together with other resourcedemanding tasks) to the more powerful, resource-rich nodes.

In the case study, resource-poor nodes are ragged hand-held devices such as PDAs and tablet PCs. They are used by the leaders of the firefighter teams, who require gathering and acting upon data sensed by the firefighters on the field, while being themselves nearby and on the move. Applications running on these nodes are able to perform simple forms of data pre-processing and reasoning (e.g., when a firefighter's breathing apparatus stops working while the firefighter is on the field, then he or she is probably in danger).

iii. Resource-rich nodes. Nodes with ample computational power and memory. They are not energy-constrained. They are responsible for performing some kind of online data analysis, such as image/video analysis (performed e.g., via computer vision algorithms), online trend prediction and immersive graphical visualizations [START_REF] Behzadan | Visualization of construction graphics in outdoor augmented reality[END_REF]. They only temporarily store the data required for these tasks; for long-term data storage and offline analysis they rely on traditional cloud infrastructure nodes.

Figure 1. Firefighter coordination case study.

In the case study, resource-rich nodes are deployed in micro data centers on powerful servers residing in firefighting departments and other organizations that traditionally belong to the public sector (e.g., schools, hospitals, police departments) or to private companies/individuals that voluntarily offer their spare computation power.

iv. Cloud nodes. Dynamically-provisioned nodes deployed on conventional data centers of one or more cloud infrastructure providers. They are responsible for storing historical data and performing offline analysis on them (e.g., Big Data analytics, postmortem documentation). They have the ability to scale out on demand and efficiently process large chunks of data using massively-parallel data processing platforms, such as MapReduce.

In the case study, cloud nodes are pre-configured virtual machines provisioned by an IaaS provider (e.g., Rackspace, Amazon) producing firefighter mission reports and analytics and providing long-term reliable storage of the analyzed data.

Reference architecture

The reference architecture shows the target system as a composition of software components (Figure 3). The components reify the identified nodes and their links reify the nodes' dependencies. A key observation is that different component interactions have different requirements on the underlying end-toend communication links. Notably, the links can be grouped into three types as shown in Figure 3 which highlights the different link types.

(a) low-power ⇔ resource-poor nodes. The main requirement of this type of interaction is that it has to be robust in face of disconnections, meaning that intermittent connections and temporary disconnections should be tolerated. Taking into consideration the physical distribution of sensors in our system, and the fact that they are mobile, the low-power nodes may dynamically join and leave ad-hoc networks created around the resource-poor nodes. To deal with such dynamic behavior, this part of the reference architecture can be instantiated using a component framework tailored for dynamic cyber-physical systems. We provide such an example in Section 4.2.

(b) resource-poor ⇔ resource-rich nodes. Low communication latency is of paramount importance in this type of interaction. Considering that most of the resourcedemanding applications that run on the resource-rich nodes also have soft real-time constraints (e.g., video streaming), network delays can impair user experience and can have safety implications if the network latency is not kept minimal. As a promising technique to implement this link type, we advocate a cloudlet-based approach as described in the next Section (Section 3.3).

(c) resource-rich ⇔ cloud nodes. This type of interaction does not impose any real-time constraints. High bandwidth is more important than low latency here, since typically large amounts of data have to be transmitted upstream. Since the cloud nodes reside in remote data centers accessible through the internet backbone, this type of link type should be realized via traditional IP protocols.

Cloudlet approach to reducing communication latency

In order to achieve low end-to-end latency between the resourcepoor and resource-rich nodes (dashed link in Figure 3) it is necessary to bring the deployed components "close" enough.

Research on offloading mobile multimedia applications to remote data centers has quantified this constraint to the maximal acceptable logical proximity of 1 WiFi [START_REF] Ha | The Impact of Mobile Multimedia Applications on Data Center Consolidation[END_REF]. A promising direction in satisfying such requirement on low latency is to employ the hierarchical architecture of cloudlets [START_REF] Satyanarayanan | The Case for VM-Based Cloudlets in Mobile Computing[END_REF][START_REF] Simanta | A Reference Architecture for Mobile Code Offload in Hostile Environments[END_REF].

A cloudlet is essentially a data center in-a-box, which resides close to the edge of the network with the goal of reducing communication latency. A cloudlet resembles a cluster of multicore computers with gigabit internal connectivity. The main difference from traditional data centers is that a cloudlet has only soft state: virtual machine images and files are cached on local storage from one or more remote data centers. This means that management burden is kept considerably low. The idea is that, once configured, a cloudlet can dynamically self-provision from remote data centers. An approach to cloudlet customization, when following a VM-based approach, is termed dynamic VM synthesis [START_REF] Satyanarayanan | The Case for VM-Based Cloudlets in Mobile Computing[END_REF]: a mobile client delivers a VM overlay (delta between the application-specific and base VM) to the cloudlet infrastructure where the base VM is already installed. This approach not only speeds up customization compared to the alternative of VM migration from remote data centers to cloudlets, but also works when no remote cloud is accessible.

Cloudlets stand as a possible realization of the resource-rich nodes of the reference architecture. In the case study, the utilization of cloudlets is envisioned in the following way. Cloudlet containers reside in micro data centers of organizations (e.g., firefighting and police departments), which are typically scattered around in a city. Once a fire breaks out in a district covered by a specific firefighting department, several teams are dispatched from the nearby departments. The firefighter leaders bring along on their mobile devices the pre-computed VM overlays, which correspond to data analysis tasks relevant to the mission in hand. The overlays are then delivered to the nearest cloudlet-based micro data center, which possesses a number of standard base VMs, and the preconfigured complete VMs are reassembled. This way, the resource-rich components deployed in the cloudlet VMs are able to respond to requests coming from the resource-poor nodes in a timely manner.

INSTANTIATIONS OF REFERENCE ARCHITECTURE

In this section we present two possible instantiations of our reference architecture. Both examples are grounded in standard component-based software engineering techniques and welldefined component models, i.e., collection of rules for component definition, composition and interaction.

To exemplify them, we use as running example a specific scenario from our case study. In the scenario, firefighter (low-power) nodes with thermal image capturing capabilities cooperate with team leader (resource-poor) nodes in order to augment their realtime risk detection capability. Team leaders aggregate image data from their team members but do not directly analyze them; for that they rely on the cloudlets (resource-rich) nodes.

Kevoree model

Kevoree is an example of a dynamic component platform [START_REF] Fouquet | A Dynamic Component Model for Cyber Physical Systems[END_REF] which can be used to realize all the nodes and links of our reference architecture. Kevoree relies on Models@runtime approach [15] to provide model-based dynamic adaptation in form of re-configuration of the running system. It does so by extending the idea of reflection to consider (architectural, but also behavioral) models which can be extracted from the running system (for reasoning, transformation, validation, and simulation purposes) and then automatically resynchronized.

Kevoree provides a number of concepts to structure distributed systems. The Node concept models an infrastructure node, the Component node models a reusable subsystem with well-defined functionality, and the Channel concept models different communication semantics between remote Components. As an example, the Kevoree model of our running example depicted in Figure 4, comprises five instances of Nodes and five instances of Channels. This architecture models the simple case where two firefighter nodes (team members) cooperate with one team leader, whose capability is augmented by one cloudlet and one cloud node. Figure 5 depicts the same configuration in the textual DSL of the Kevoree. Note that bindings between individual components in Kevoree are explicitly modeled (e.g., lines 19-21), which essentially renders it possible to visualize the system in the graphical DSL used in Figure 4.

DEECo model

When structuring the part of the system which is heavily influenced by the dynamicity in the physical world, i.e., lowpower to resource-poor links (dotted links in Figure 3, left part of the architecture in Figure 4), it is beneficial to employ component models that specifically target environments with evolving physical substratum, such as DEECo (Dependable Emergent Ensembles of Components) component model [START_REF] Bures | DEECo -an Ensemble-Based Component System[END_REF][START_REF] Keznikl | Towards Dependable Emergent Ensembles of Components: The DEECo Component Model[END_REF].

In DEECo, a component is an autonomous unit of computation and deployment, which comprises knowledge and processes. An example of a DEECo component modeling the low-power node of our running example is depicted in form of DEECo DSL in Figure 6, lines 7-25. Processes in DEECo operate upon the knowledge of a component and feature cyclic execution based on the concept of feedback loop, similar to processes in real-time systems. DEECo components are not bound to other components neither do they explicitly communicate with each other. Instead, interaction among components is determined by their composition according to their roles (e.g., lines 1-2, 4-5) into groupscalled ensemblescooperating to achieve a particular goal. Ensembles are dynamically formed based on the state of components and external situation (e.g., when a group of firefighters are physically close together, they form an ensemble). Within an ensemble, communication takes the form of knowledge exchange between the selected components, performed by the runtime framework of DEECo. As an example, consider the ImageUpdate ensemble definition (Figure 6, lines 49-57). It captures the fact that, when two components belong to the same team and the firefighter component has a new image to propagate (membership condition, lines 52-54) the image knowledge gets propagated to the knowledge of the team leader (knowledge exchange function, lines 55-56).

Obviously, DEECo is a viable choice in highly dynamic and unpredictable settings where direct bindings à la Kevoree do not scale, as it provides a notion of built-in robustness through periodic execution. It also copes well with the dynamicity of opportunistic networks [START_REF] Huang | A Survey of Opportunistic Networks[END_REF], which typically underlies type (a) link type (red links) of our reference architecture by relying on stateless interaction templates for component linking. However, DEECo is not the best choice for realizing the non-dynamic parts of the reference architecture (in particular, data replication used to achieve robustness in DEECo can harm performance); for them, more "traditional" component models, such as Kevoree, are the preferred choice.

DISCUSSION

In this section, we first discuss the implications of our approach by performing a what-if analysis of the situations that can arise in the target system (Section 5.1). Then, in Section 5.2 we elaborate on the implementation aspects of our approach by focusing on both parts of the target system: the mobile ad hoc system part (MANET) and the Ethernet backbone part.

What-if analysis

With the aim of showing how our approach optimizes resources and data provisioning and availability, we explain five levels of system availability. Each level reflects on the potential connectivity issues of the use case presented in Section 2.

Level-4all components can communicate with each other. All the optimization and resource harvesting features are enabled. As a result, type 2 and 3 devices (see Section 3) benefit from the offloading of computation-intensive tasks. The offloading enables us to support the decision making with resource-greedy techniques. Additionally, if cloud platforms provide big data capabilities the nodes profit from additional data processing possibilities. From the firefighters' perspective, they have access to all the information that could possibly support their actions in the field. These data include latency-free results of highly intensive computation performed by the cloudlet such as image processing or voice recognition. Due to the use of resourceunconstrained computational poweri.e., cloudlet and cloud platformsteam leaders get instant access to analyses that could increase the correctness of a strategy selection when managing team members.

Level-3the cloudlet constitutes a communication edge and the system is not able to leverage the cloud back end. This could possibly degrade the offline analysis support to team leaders' decision-making. In this case, we assume that the information provided by the cloud infrastructure is not critical for the currently ongoing operation in the field but it is useful for analysis performed afterwards.

Level-2we assume here no cloudlet connectivity, which results in degradation of system performance and data availability. Team leaders and firefighterswho benefit directly from the cloudlet latency-free resourcesneed to adapt to the situation by reducing their resource utilization. In turn, less information is available which constraints the decision support.

Level-1team leaders are disconnected from the rest of the team. Hence, team members can no longer rely on their leader's support and they depend on each other to optimize the access to information. We assume that each firefighter is able to communicate with at least one other team member, so that minimal data exchange exists.

Level-0no communication is available. Team members execute in isolation and depend only on their own sensor data. Nevertheless, the system remains available and provides minimally required informationsuch as oxygen level, temperature, or exit directionto a firefighter. Therefore, the information available satisfies the aforementioned requirement regarding system availability.

Our hybrid DEECo-Kevoree approach (described in Section 4.2) aims to address all of these levels. In particular, the system's operability is sustained by employing DEECo at Level-2, Level-1, and Level-0. DEECo components are autonomous and able to execute in isolation. Hence, knowledge about the remote components is not required all the times. Moreover, their processes implement adaptation techniques that provide reaction mechanisms depending on the level of data and resources availability. Those characteristics of the DEECo component model imply higher system resilience, which subsequently prolongs the system's operability and availability. These properties are of course critical for the end users in our case study.

Figure 7 summarizes this section by depicting our 5-level model of system availability.

Implementation Aspects

In this section we discuss the technical aspects of the target system, elaborating on the MANET and Ethernet subsystems separately.

MANET jDEECo

As a part of the discussed system realization, we envision to employ the jDEECo framework 3 . It is a Java realization of the DEECo component model that provides the necessary programming abstractions and runtime environment for building and running DEECo-based applications. The reference architecture can be mapped directly to components and ensembles in jDEECo, constituting the basic building blocks of the framework. Considering our case study scenario, we presume that 3 https://github.com/d3scomp/JDEECo jDEECo will be deployed on the low-power and resource-poor nodes. In principle ensembles in DEECo are ubiquitous, and as such they are supposed to be evaluated globally, which requires access to all component data. In order to achieve this and, at the same time, sustain both distribution and scalability, ensembles are evaluated locally by each of the jDEECo (runtime and component host) node. For that each jDEECo node periodically distributes (broadcasts to a radio channel) its local component data, which is then received by firefighter nodes in the communication range. Apart from publishing its own local data, jDEECo nodes rebroadcast other nodes' data (called replicas), taking the role of relays. In order to minimize the network traffic overhead produced by periodic broadcasts, a concept of communication boundary is used, which considerably reduces the amount of data generated by jDEECo runtimes. An important characteristic in case of data dissemination in jDEECo is the absence of the network layer (from the OSI model), as no routing is required. This approach fits the semantics of ensemble, which, as previously mentioned, needs to be ubiquitous.

In terms of jDEECo targeted communication standards (i.e. IEEE 802.15.4) the data being sent in a single packet is limited to approx. 100 bytes.

Ethernet Backbone

On the other hand, the case study scenario and the proposed architecture assume reliable communication links between resource-poor and resource-rich nodes. In such settings jDEECo would introduce unnecessary overhead that comes mainly from data replication techniques employed internally by the framework implementation. As such, for this part of the architecture we aim to build on existing VM-based approaches suggested by Satyanarayanan et al. [START_REF] Satyanarayanan | The Case for VM-Based Cloudlets in Mobile Computing[END_REF] and Ha et al. [START_REF] Ha | The Impact of Mobile Multimedia Applications on Data Center Consolidation[END_REF]. By that, we leverage on both flexibility with respect to software stack used inside the VM being offloaded to the cloudlet, and generic mechanisms (dealing only with the VM images and overlays) employed in the cloudlet management. Those characteristics enable further sharing of latency-free infrastructure with other (emergency) service providers, using proprietary software solutions.

Nevertheless, we can simplify the offloading process with the execution of Kevoree framework 4 in the cloudlet server. Since, 4 http://kevoree.org Kevoree supports the concept of continuous deployment based on models@run.time and it also allows the definition of new semantic for its fundamental concepts (Node, Channel, Group, Component), we can envision an architecture with a master node in charge of deploying applications on demand. Indeed, such an idea has been partially implemented by the Kevoree team to support the deployment of components in LXC containers 5 Using Kevoree decreases the network traffic. This is because, using a Kevoree model only the components in the application need to be specified and for each component the associated dependencies are then downloaded from the network. Thus, the time to offload an application to the cloudlet or the cloud is only the time to execute the new VM plus the time of downloading the components. This approach has two advantages: first, on using a VM-overlay this requires more bandwidth as it requires the deployment of all the associated components; and second, the intensive communication is no longer between low-power devices and the cloudlet, but between the cloudlet and Internet. On the other hand, this requires the pre-installation of Kevoree on each cloudlet instance. Nonetheless, assuming the pre-installation of Java and a standardized model@runtime (based for instance on OSGi) is a plausible solution at mid-term.

RELATED WORK

Our approach tries to bridge the gap between models of composition and execution tailored to the domain of cyberphysical systems, and computation offload from mobile devices to the cloud. The goal is to augment the capabilities of constrained devices while keeping power consumption low. Related areas of research are Mobile Cyber-Physical systems [START_REF] Kim | Cyber-Physical Systems: A Perspective at the Centennial[END_REF] and Edge/Fog computing [START_REF] Bonomi | Fog Computing and Its Role in the Internet of Things[END_REF].

Satyanarayanan et al. [START_REF] Satyanarayanan | The Case for VM-Based Cloudlets in Mobile Computing[END_REF] were the first to introduce the term "cloudlet" as an approach to bring the cloud closer to the edges of the network and to support the non-disruptive execution of both interactive and resource-demanding applications in mobile devices. In [START_REF] Ha | The Impact of Mobile Multimedia Applications on Data Center Consolidation[END_REF] the authors evaluate the approach of delegating intensive tasks to the cloud infrastructure. The results show the need of a resource-rich-layer physically closer to end-user devices since it is impossible to satisfy all non-functional requirements with the cloud due to high latency. Likewise, the authors of [START_REF] Ravi | Energy Efficient Seamless Service Provisioning in Mobile Cloud Computing[END_REF] propose the combination of cloud and cloudlet infrastructures as targets for resource-intensive jobs. Mobile nodes execute a heuristic, based on the trade-off between minimal delay and higher throughputs, to decide where to offload a job, either to the cloud or the cloudlet. The work also presents a mechanism to route answers to the source mobile when the nearest cloudlet changes. Preliminary results suggest under which conditions the cloudlet approach outperforms the cloud approach. However, such approaches cannot provide service when neither connection to the cloud nor to the cloudlet is available. In our framework, it is essential to maintain system operation even when no resource-rich infrastructure is available. Moreover, such approaches consider that both the cloudlet and the cloud execute the same jobs. Instead, we propose to separate at design time the tasks with realtime response needs that are executed in the cloudlet from those that are executed offline in the cloud.

Simanta et al. [START_REF] Simanta | A Reference Architecture for Mobile Code Offload in Hostile Environments[END_REF] propose approaches to decrease start-up time of offloaded applications in cloudlets. To avoid the offload of a full VM-Image, they propose the construction of a VM-Overlay, which is the difference between a VM-Image with specific applications and a VM-Base-Image within the cloudlet infrastructure. Mobile devices send such an overlay to a cloudlet server, which in turn synthesizes the image and instantiates the fully-customized VM. The usability in highly mobile environments where the overlay must be sent to different cloudlet servers over and over is limited because the size of overlays is not negligible. On the other hand, Unikernel [START_REF] Madhavapeddy | Unikernels: Library Operating Systems for the Cloud[END_REF] proposes a solution based on the observation that in many cases a traditional software stack is not required on a hosted virtual machine because few features of the underlying system are used. Hence, the authors advocate the construction of a specialized operating system with small software stack that comprises only essential functionality for each application. The resulting VM-Image is on the order of kilobytes in many cases, which eases the rapid deployment to remote locations. Nevertheless, we intend to use the former approach in our framework implementation because it allows access to legacy code, which is not possible when following the Unikernel approach.

In [START_REF] Ravi | Energy Efficient Seamless Service Provisioning in Mobile Cloud Computing[END_REF], the authors also face the problem of task delegation and data sharing for mobile devices in a dynamic network environment. They present a framework to use the energy of mobile devices in a more efficient way, by combining execution of tasks both on traditional cloud infrastructure and on ad-hoc mobile cloud. The framework uses a service discovery mechanism and offload decision algorithms to find the lowest offloading cost. Nodes rely on the ad-hoc mobile cloud if the cloud infrastructure is not available. A device accesses a service either through peers of connected nodes in the ad-hoc mobile cloud or directly via the cloud. The decision of choosing the offload target depends on two factors: the historical cost of the computation and the cost of communication with the nodes providing the service. However, the authors only consider two classes of infrastructure for doing computation and neither distinguish between mobile devices nor consider resource-rich infrastructures other than the cloud.

The authors of [START_REF] Bonomi | Fog Computing and Its Role in the Internet of Things[END_REF] and [START_REF] Hong | Mobile Fog: A Programming Model for Large-scale Applications on the Internet of Things[END_REF] try to solve the problem of performing resource-intensive jobs by delegating the execution to as many devices as possible and not only to a dedicated infrastructure as the cloud or the cloudlet. Their thesis is that, nowadays, many installed devices are capable of executing offloaded jobs; but there is a lack of proper software frameworks and protocols to achieve this goal. Their idea is to define a framework with different logical layers, which reifies a hierarchical relationship within the network (e.g., sensor/actuator nodes, mobile nodes, routing devices in the network and cloud infrastructure). Each node executes processes as part of the application and communicates with any reachable node in the network since the aim is to provide a framework for distributed computing. Nonetheless, the framework encourages communication that follows the hierarchy due to performance advantages. Within this scheme, mobile devices offload tasks to a resource-rich node responsible for its region and they change the target-region node while on the move. Simulation-based evaluations show lowlatency in large-scale systems with wide geospatial distribution.

While their work focuses on finding an efficient programming model for the so-called "Mobile Fog" paradigm, we adopt an architecture-based approach, which is platform and language agnostic.

CONCLUSIONS AND FUTURE WORK

In this paper we have presented a reference architecture that can act as a template for the structuring of applications deployed on Compute-Intensive Pervasive Systems. Our reference architecture approach is designed to handle high dynamicity and low latency requirements of CIPS. Furthermore, we have used a model-driven approach to validate the proposed reference architecture using two component-based frameworks, DEECo and Kevoree. We strongly believe our approach improves on availability of CIPS and using a cloudlet approach reduces the latency, thereby enhancing the operability of CIPS.

As future work we plan to fulfill the design view and validate it by real experiments. A couple of points we are considering as next steps:

1. Different experimentations. We plan to do different experiments using different reference architecture instantiation (i.e. Kevoree, DEECo) of our reference architecture to evaluate their performance and latencies. 2. Focus on the physical attributes. We will focus on extending the reference architecture to correlate with attributes of the physical world, and consider them in data propagation part. For example, we plan to instantiate our reference architecture with models and techniques that build on opportunities offered by cyber-physical systems (e.g., geospatial routing in data propagation, gossip-based communication between components in MANETs, etc.).

Figure 2 .

 2 Figure 2. Nodes and their dependencies in an application deployed on CIPS.

Figure 3 .

 3 Figure 3. Proposed components and their links in the reference architecture.

Figure 4 .

 4 Figure 4. Modeling of the running example in Kevoree.

Figure 5 .

 5 Figure 5. Kevoree DSL example.

Figure 6 .

 6 Figure 6. Modeling the MANET part of the running example inDEECo.

Figure 7 .

 7 Figure 7. The five levels of system availability.

  . A Kevoree component running within a LXC Node type is waiting for messages that trigger the execution of a new Java-based Kevoree Runtime within a new LXC container. Such a runtime can deploy a set of components under additional request. We envision that both the process of executing a new Container and the process of deploying the new model in Kevoree can be atomic.The application of this method to other Operating-System virtualization solutions as Jail is straightforward. It is also applicable with other virtualization providers as Amazon since those services provide a public interface to deploy VMs. The implementation of a Node Type must use such an interface to deploy a new instance of a VM-image with Kevoree pre-installed.

http://linuxcontainers.org/

ACKNOWLEDGMENTS

This work has been supported by the European Union Seventh Framework Programme FP7-PEOPLE-2010-ITN under grant agreement n°264840. The authors would like to thank Petr Hnetynka and Jaroslav Keznikl for the constructive feedback and discussions.


Mary Southern
email: marys@cs.umn.edu

Kaustuv Chaudhuri
email: kaustuv.chaudhuri@inria.fr

A Two-Level Logic Approach to Reasoning about Typed Specification Languages

The two-level logic approach (2LL) to reasoning about computational specifications, as implemented by the Abella theorem prover, represents derivations of a specification language as an inductive definition in a reasoning logic. This approach has traditionally been formulated with the specification and reasoning logics having the same type system, and only the formulas being translated. However, requiring identical type systems limits the approach in two important ways: (1) every change in the specification language's type system requires a corresponding change in that of the reasoning logic, and (2) the same reasoning logic cannot be used with two specification languages at once if they have incompatible type systems. We propose a technique based on adequate encodings of the types and judgements of a typed specification language in terms of a simply typed higher-order logic program, which is then used for reasoning about the specification language in the usual 2LL. Moreover, a single specification logic implementation can be used as a basis for a number of other specification languages just by varying the encoding. We illustrate our technique with an implementation of the LF dependent type theory as a new specification language for Abella, co-existing with its current simply typed higher-order hereditary Harrop specification logic, without modifying the type system of its reasoning logic.

Introduction

Higher-order abstract syntax (HOAS) [START_REF] Pfenning | Higher-order abstract syntax[END_REF], also known as λ-tree syntax (λTS) [START_REF] Miller | A computational logic approach to syntax and semantics[END_REF], has become a standard representational style for data structures with variable binding. Such data are pervasive in the syntax of programming languages, proof systems, process calculi, formalized mathematics, etc. Variable binding issues are a particularly tricky aspect of the meta-theory of computational systems given in the form of structural operational semantics (SOS). Such specifications are nearly always formulated as relations presented in the form of an inference system; for instance, the typing judgement for the simply typed λ-calculus is a relation between λ-terms and their types, usually defined in terms of a natural deduction proof system. Such relations on higher-order data can then be systematically formalized as higher-order logic programs in languages such as λProlog [START_REF] Miller | Programming with Higher-Order Logic[END_REF] or Twelf [START_REF] Pfenning | System description: Twelf -A meta-logical framework for deductive systems[END_REF], which lets us directly animate the specifications by means of logic programming interpreters and compilers such as Teyjus [START_REF] Nadathur | System description: Teyjus -A compiler and abstract machine based implementation of λProlog[END_REF].

In this paper, we are concerned with proving properties about such higher-order relational specifications. For example, if the specification is of the typing relation for simply typed λ-terms, then we may want to prove that a given λ-term has exactly one type (type-uniqueness), or that the type of a λ-term remains stable during evaluation (type-preservation). This kind of reasoning proceeds by induction on the derivations of the specified relations, so we need a formalism that supports both inductive definitions and reasoning by induction. The two-level logic approach (2LL) is a general scheme for such reasoning systems, where the specification language derivations are viewed as an inductively defined object in a reasoning logic. In this reasoning logic, the specification language derivations are given a closed world reading, which is to say that that derivability in the specification language is completely specified: it can not only establish that certain specification formulas or judgements are derivable, but also that others are not derivable, or that two specification derivations are (bi)similar. We focus on the Abella implementation of the 2LL, which is an interactive tactics-based theorem prover designed to reason about a subset of higher-order λProlog programs seen as the logic of higher-order hereditary Harrop (HOHH) formulas [START_REF]The Abella web-site[END_REF][START_REF] Wang | Reasoning about higher-order relational specifications[END_REF].

We consider an extension of the 2LL that can use a single reasoning logic to reason about a number of different specification languages in the same development. The HOHH language has only simple types, which makes both the specifications and the reasoning somewhat verbose because structural invariants must be separately specified and explicitly invoked in theorems. Richer type systems can often encode such invariants intrinsically in the types; to illustrate, dependent types can be used to define a type of (representations of) well-typed λ-terms, which is not possible with just simple types. Moreover, with such richer type systems one can often use the inductive structure of the terms themselves to drive the inductive argument rather than using auxiliary relations.

Unfortunately, the 2LL as currently defined [START_REF] Gacek | A two-level logic approach to reasoning about computations[END_REF] does not sufficiently address these desiderata. In particular, the specification and reasoning languages are required to have the same type system because the specificationlevel constants and their types are directly lifted to reasoning-level constants with the same type. Thus, if we required a version of Abella based on a dependent type theory as a specification language, we would need to also change its reasoning logic G to be dependently typed. This goes against the 2LL philosophy where the reasoning logic is seen as common, static, and eternal. More importantly, it both breaks portability of developments and causes duplication of effort.

Our position is that we should extend the 2LL in such a way that the reasoning-level and specification-level type systems are separated. Indeed, the specification types and judgements must themselves be encoded as terms and formulas of the reasoning logic. This encoding must be coherent with that of specification-level terms and formulas, both of which are encoded as reasoning-level atomic formulas. This is achieved by guaranteeing that our encoding of the type systems is adequate; that is, the encoding of the specification-level type system must be able to represent all specification-level typing derivations, and that reasoning about the specification-level type system should be reducible to reasoning, by induction, on the encoding. An essential ingredient of adequacy is a right-inverse of the encoding that extracts a specification-level typing judgement from a reasoning-level formula when the formula is in the image of the encoding.

To be concrete, we illustrate the extended 2LL in this paper by giving an encoding of the LF dependent type theory, which is then implemented as a translation layer in Abella. The reasoning logic of Abella is left untouched, as is the existing HOHH specification language for reasoning about λProlog programs. Our encoding of LF is based on that of [START_REF] Snow | A meta-programming approach to realizing dependently typed logic programming[END_REF][START_REF] Southern | A λProlog based animation of Twelf specifications[END_REF], suitably modified to the context of interactive theorem proving rather than logic programming. Since both LF and HOHH are based on intuitionistic logic, our extension of Abella uses a core implementation of an intuitionistic specification language that is shared by both the HOHH and the LF languages. Interestingly, the details of the encoding into this core language can almost entirely be obscured for the user; in particular, to use the system the user does not need to know how the specification language is encoded, since the system uses the right inverse mentioned above to present the types, terms, and judgements of the specification language in their native forms.

The rest of the paper is organized as follows. Section 2 presents the two-level logic approach (2LL) and its implementation in the Abella theorem prover. Section 3 presents LF and its adequate translation into a simply typed higher-order logic programming language. This is then used in section 4 to explain our extension of the 2LL by means of adequate translations. Related work is surveyed in section 5.

Background

This section sketches the two-level logic approach (2LL) as implemented in the Abella theorem prover [START_REF]The Abella web-site[END_REF]. More details, including the full proof systems and their meta-theory, can be found in the following sequence of papers: [START_REF] Wang | Reasoning about higher-order relational specifications[END_REF][START_REF] Gacek | A two-level logic approach to reasoning about computations[END_REF].

The Reasoning Logic G

The reasoning logic of Abella, G, is a predicative and intuitionistic version of Church's Simple Theory of Types. Types are built freely from primitive types, which includes the type prop of formulas, using the function type constructor →. Intuitionistic logic is introduced into this type system by means of the constants true, false : prop, binary connectives ∧, ∨, ⊃: prop → prop → prop, and an infinite family of quantifiers ∀ τ , ∃ τ : (τ → prop) → prop for types τ that do not contain prop. For every type τ not containing prop, we also add an atomic predicate symbol = τ : τ → τ → prop to reason about intensional (i.e., up to αβη-conversion) equality. Following usual conventions, we write ∧,∨, ⊃, and = τ infix, and write ∀x : τ . A for ∀ τ (λx. A) (and similarly for ∃). We also omit the type subscripts and type-ascription on variables when unambiguous.

To provide the ability to reason on open λ-terms, which is necessary when reasoning about HOAS representations, G also supports generic reasoning. This is achieved by adding, for each type τ not containing prop, an infinite set of nominal constants and a generic quantifier ∇ τ : (τ → prop) → prop. We also add a weaker form of intensional equality called equivariance that equates two terms whose free nominal constants may be systematically permuted to each other. Note that equivariance is only used to match conclusions to hypotheses in the G proof system; = continues to have the standard λ-conversion semantics. The support of a term t, written supp(t), is the multiset of nominal constants that occur in it; whenever we introduce a new eigenvariable, such as using the ∀-right or ∃-left rules, we raise the eigenvariables over the support of the formula. This raising is needed to express permitted dependencies on these nominal constants.

To accommodate fixed-point definitions, G is parameterized by sets of definitional clauses. Each such clause has the form ∀ x. (∇ z. A) B where A (the head) is an atomic formula whose free variables belong to x or z, while B (the body) is any arbitrary formula that can only mention the variables in x, and can additionally have recursive occurrences of the predicate symbol in the head. Each clause partially defines a relation named by the predicate in the head. We additionally require that supp(∇ z. A) and supp(B) be both empty, and that recursive predicate occurrences satisfy a stratification condition [START_REF] Gacek | Nominal abstraction[END_REF]. 1 Finally, some of these definitions in G can be marked as inductive or co-inductive, in which case the set of definitional clauses for that relation are given least or greatest fixed-point semantics. This is approximated in Abella by means of size annotations, which are formally defined and proved correct in [START_REF] Gacek | A Framework for Specifying, Prototyping, and Reasoning about Computational Systems[END_REF].

seq L (G1 & G2) seq L G1 ∧ seq L G2 seq L (F ⇒ G) seq (F :: L) G seq L (pi F ) ∇x. seq L (F x) seq L A mem F L ∧ bch L F A seq L A prog F ∧ bch L F A bch L (F1 & F2) A bch L F1 A ∨ bch L F2 A bch L (G ⇒ F ) A seq L G ∧ bch L F A bch L (pi F ) A ∃t. bch L (F t) A bch L A A true

The Specification Language: HOHH

The essence of the 2LL is to encode the deductive formalism of the specification language in terms of an inductive definition. However, before this can be done, the terms and formulas-and types!-of the specification language must be represented in the reasoning logic. This is trivial if the specification and reasoning logics have the same term and type language, which is the case for the HOHH language. To encode HOHH formulas, we use a new basic type o, and formula constructors ⇒, & : o → o → o (written infix), and an infinite family of specification-level quantifiers pi τ : (τ → o) → o (standing for universal quantification, written prenex) for types τ that do not contain o. To prevent circularity, we disallow the type prop and the reasoning level formula constructors from occurring inside specification level types and terms.

The proof system for HOHH is a standard focused sequent calculus for this fragment of the logic, assuming that all atoms have negative polarity; this is equivalent to saying that the proof system implements backchaining [START_REF] Wang | Reasoning about higher-order relational specifications[END_REF]. This proof system is implemented in G using two predicates, seq : olist → o → prop and bch : olist → o → o → prop, standing for goal reduction and backward chaining respectively, with the definitional clauses shown in figure 1. Here, specification contexts have the type olist, the type of lists of o, with constructors nil : olist and (::) : o → olist → olist (written infix), and a membership relation mem : o → olist → prop that has the obvious inductive definition. In Abella, these two relations are displayed using the more evocative notation {L ⊢ G} and {L, [F ] ⊢ G} for seq L G and bch L F G. The final clause for seq uses a separate predicate prog : o → prop that is true exactly for the clauses in the specification program. It is easy to see that with this syntax, the definitional clauses of figure 1 are precisely the inductive definition of a backchaining proof system.

Example: Type Uniqueness

The need for the two kinds of specification sequents and the mechanism for proving properties about the specification logic are best described with an example. Consider the simply typed λ-calculus, itself specified as an object logic in HOHH. The simple type system is represented using a new basic type ty with two constructors, i : ty (a basic sort), and arr : ty → ty → ty for constructing arrow types. The λ-terms are typed using a different basic type tm with two constructors: app : tm → tm → tm and abs : ty → (tm → tm) → tm. The λ-term λx:i. λf :i → i. f x would be represented as abs i (λx. abs (arr i i) (λf. app f x)). The relation between terms (of type tm) and types (of type ty) is usually expressed in the form of an inference system such as:

Γ, x:A ⊢ M : B Γ ⊢ (λx:A. M ) : A → B → I Γ ⊢ M : A → B Γ ⊢ N : A Γ ⊢ M N : B → E Γ, x:A ⊢ x : A var
This relation is succinctly expressed as a pair of HOHH program clauses for the predicate of : tm → ty → o, which is used both for assumptions of the form x:A and for conclusions of the form M : A in the inference system above. Note that there is no clause for var; rather, it is folded into an assumption in the body of the abs case, which delimits its scope. It is generally easier to read such clauses when they are written using the standard λProlog syntactic convention of using capital letters for universally closed variables, writing implications in the reverse direction with the head first, and separating assumptions by commas rather than repeated implications. Thus, the above clauses correspond to:

of ( app M N ) B ⇐ of M ( arr A B ) , of N A . of ( abs A R ) ( arr A B ) ⇐ pi x \ of ( R x ) B ⇐ of x A .
The formula pi (λx. F ) is rendered as pi x\ F in the concrete syntax, and the scope of x extends as far to the right as possible. Note that all the types are inferred.

In the reasoning mode of Abella, the above λProlog specification is imported by reflecting all specification constants and types in the reasoning signature, and by generating a definition for prog that is true only for the two clauses for of. The typing judgement x:A, y:B ⊢ M : C in the inference system (2.3), for instance, would be represented by seq (of y B :: of x A :: nil) (of M C). As an example of reasoning on this specification, we can prove that of is deterministic in its second argument:

forall M A B , { ⊢ of M A } → { ⊢ of M B } → A = B .
This theorem is proved by induction on the derivation of one of the seq assumptions, such as the first one. This induction would repeatedly match the form seq nil M A against the left hand sides of the definitional clauses in figure 1; for every successful match, the corresponding right hand side of the clause would give us new assumptions, which may then be used in the inductive hypothesis.

Initially, the only clause that matches is the final one for seq corresponding to backchaining on a program clause. In the case where the clause for abs is selected, the corresponding bch clause for it would in turn call seq with a different list of assumptions. Thus, the inductive argument cannot proceed with empty dynamic specification contexts (the first argument to seq and bch) alone: we must also allow for reasoning under an abstraction. This is achieved in the reasoning logic by inductively characterizing all such dynamic context extensions with a new atom, say ctx : olist → prop, with the following inductive definitional clauses:

ctx nil true. ∀A. ∀G. (∇x. ctx (of x A :: G)) ctx G.
We can then prove a stronger lemma:

forall G M A B , ctx G → { G ⊢ of M A } → { G ⊢ of M B } → A = B .
Now, when the dynamic context does grow when backchaining on the clause for abs, it will grow exactly by the form in the head of the second clause of ctx, i.e., with a formula of the form of n A where n is a nominal constant that does not occur in A nor in the original context G. Thus, when we in turn backchain on the dynamic clauses (using the penultimate clause for ctx in figure 1), we will know the precise form of the selected clause.

An Adequate Translation of LF to HOHH

The Edinburgh Logical Framework (LF) is a dependently typed λ-calculus which is used for specifying formal systems. Terms of this language belong to one of the following three syntactic categories:

Kinds K ::= type | Πx:A. K Types A, B ::= a M 1 . . . M n | Πx:A. B Objects M, N ::= c | x | λx:A. M | M N Types,
sometimes called families, classify objects and kinds classify types. Here a represents a type-level constant, c an object level constant, and x an object level variable. Following standard convention, we will write A → B as a shorthand for Πx:A. B when x does not appear free in B. We will use U to denote both types and objects and P for both kinds and types, so U : P will stand either for a typing or a kinding judgement. We will write U [M 1 /x 1 , . . . , M n /x n ] to denote the capture avoiding substitution of M 1 , . . . , M n for free occurrences of x 1 , . . . , x n respectively.

An LF specification is a list of object or type constants together with their types or kinds, called a signature. Let us revisit the example of the simply typed λ-calculus and its associated typing relation used in section 2.3. The λ-terms are encoded using the following signature: For the typing relation of, in LF we declare it as a dependent type rather than as a predicate as in HOHH. The clauses of the of type are then viewed as constructors for the dependent type, and are therefore also given names. Here, the concrete syntax {x:A} B denotes Πx:A. B. The LF type system is formally defined in [START_REF] Harper | A framework for defining logics[END_REF] and will not be repeated here. Instead, we will directly give an adequate encoding of the LF type system in terms of HOHH, based on the variant of the encoding in [START_REF] Felty | Encoding a dependent-type λ-calculus in a logic programming language[END_REF] defined in [START_REF] Snow | A meta-programming approach to realizing dependently typed logic programming[END_REF], with the inverse mapping defined in [START_REF] Southern | A λProlog based animation of Twelf specifications[END_REF].

The encoding proceeds in two steps. First, we transform our dependently typed terms into simply typed HOHH terms. The encoding of types and kinds is defined as a mapping, written φ (-). These types indicate that the term is an encoding of an LF type and an LF object, respectively. For each constant c : P in the LF signature, we generate a simply typed term c of type φ (P ). Using this mapping, the dependently typed λ-terms are converted into simply typed λ-terms using the mapping -. Figure 2 contains the rules for both -and φ (-). Note that φ (-) erases not just the type dependencies but also the identities of the types. For an atomic type

A = a M 1 • • • M n , we further write A to stand for a M 1 • • • M n .
The second pass uses two new predicates, hastype : lfobj → lftype → o and istype : lftype → o, to encode the type and kind judgements of LF. Whenever M : A is derivable in LF under a given signature, it must be the case that {{A}} M is derivable in HOHH from the clauses for hastype and istype produced from encoding the signature. Likewise, when A : K is derivable, it should be the case that {{K}} A is derivable. The rules for this encoding are shown in figure 3.

Theorem 1 (Adequacy, [START_REF] Snow | A meta-programming approach to realizing dependently typed logic programming[END_REF]). The LF hypothetical judgement x 1 : P 1 , . . . , x n : P n ⊢ M : A is derivable in the LF type theory [START_REF] Harper | A framework for defining logics[END_REF] from an LF signature Σ if and only if the HOHH formula {{P 1 }}x 1 ⇒ • • • ⇒ {{P n }}x n ⇒ {{A}} M is derivable from the HOHH encoding of Σ according to the rules in figures 2 and 3.

Because this encoding is adequate, it is possible to define a right-inverse that maps a HOHH formula in the image of the translation in figure 3 back to an LF judgement. This inverse will be very useful in the next section where we will use the encoding of LF to extend the 2LL via translations. The user of the system will not need to be aware of the details of the encoding as the HOHH formulas will be inverted into their corresponding LF judgements.

Defining such an inverse requires a small amount of care. We obviously cannot invert every HOHH formula, just those that correspond to a given signature. However, even for formulas constructed using the encodings of an LF signature, we may not necessarily be able to invert them; for instance, the formula may be the translation of a malformed or ill-typed LF judgement. This inverse will also not necessarily recover exactly the LF judgement used to construct the HOHH formula in the first place; rather, the inversion will only produce a unique inverse (if one exists) up to βη-conversion.

The inversion operation is defined in terms of the following four sequent forms:

Γ ⊢ hastype m a -→ M : A inverting typing; M , A output Γ ⊢ istype a -→ A : type inverting kinding; A output Γ ⊢ m : A M inverting canonical terms; M output Γ ⊢ m M : A inverting atomic terms; M , A output
The rules are shown in figure 4. In each case, Γ contains the type and kind information for the signature constants and the typing assumptions for the bound variables in the input terms. A and B range over LF types, M and N over LF terms, F and G over HOHH formulas and a, m and n over simply typed λ-terms produced by -. The rules for inverting typing and kinding are novel, but those for inverting terms are standard from bidirectional type-checking, and have already been developed in [START_REF] Southern | A λProlog based animation of Twelf specifications[END_REF] (in a slightly more general form).

Theorem 2 (Right inverse). If {{P }} U = F under the translation of Γ and Γ ⊢ F -→ U ′ : P , then Γ ⊢ U = βη U ′ : P in LF.

(a:Πx Proof. By structural induction on the inversion derivation. Note the requirement for η-contraction of the term to a variable in the second premise of inv-nest is necessary, for otherwise the rule would produce an unsound abstraction. If the formula F was generated from the translation of figures 2 and 3, then this η-contraction check will always succeed.

1 :A 1 . • • • Πx k :A k . B) ∈ Γ Γ ⊢ m 1 : A 1 M 1 • • • Γ, x 1 :A 1 , . . . , x k-1 :A k-1 ⊢ m k : A k M k Γ ⊢ m : a M 1 • • • M k M Γ ⊢ hastype m (a m 1 • • • m k ) -→ M : a M 1 • • • M k inv-has (a:Πx 1 :A 1 . • • • Πx k :A k . type) ∈ Γ Γ ⊢ m 1 : A 1 M 1 • • • Γ, x 1 :A 1 , . . . , x k-1 :A k-1 ⊢ m k : A k M k Γ ⊢ istype (a m 1 • • • m k ) -→ a M 1 • • • M k : type inv-is Γ ⊢ F -→ R : A R =η x Γ, x:A ⊢ G -→ M : B Γ ⊢ pi x:a. F ⇒ G -→ (λx:A.
Γ ⊢ m M : Πx:A. B Γ ⊢ n : A N Γ ⊢ m n M N : B[N/x] inv-app Γ ⊢ m M : A Γ ⊢ m : A M inv-switch (x:A) ∈ G Γ ⊢ x x : A inv-hyp (c:A) ∈ G Γ ⊢ c c : A inv-const

Translational Two-level Logic Approach

We will now use both the translation of LF signatures to HOHH formulas and its inverse to extend the 2LL in such a way that we can reason about LF signatures just as we were able to reason on λProlog specifications as shown in the example of section 2.3.

Importing the LF Specification

As the type system of LF and G are different, we cannot directly reflect the constants and types of the LF specification logic like we did with HOHH in section 2. Instead, for every LF constant c of LF type or kind P in the LF signature, we do the following: (1) add a constant c : φ (P ) to the G signature; and (2) add the clause {{P }}c to the prog definition. Note that because the clauses are always of the form {{P }}c for a constant c, there will never be any redexes in the clauses, i.e., the generated clauses are β-normal. They are also η-long, because the definition of {{-}} traverses the type or kind until it is atomic.

Example 3. Consider again the LF signature in section 3. When it is imported into G, the following constants are added to the G signature by step [START_REF] Savary | Automatically deriving schematic theorems for dynamic contexts[END_REF]:

ty : lftype . tm : lftype . i : lfobj . app : lfobj → lfobj → lfobj . arr : lfobj → lfobj . abs : lfobj → ( lfobj → lfobj ) → lfobj . of : lfobj → lfobj → lftype . ofApp : lfobj → lfobj → lfobj → lfobj → lfobj → lfobj → lfobj . ofAbs : lfobj → lfobj → ( lfobj → lfobj ) → ( lfobj → lfobj → lfobj ) → lfobj .
The following clauses are then added to prog by step [START_REF] Cave | Programming with binders and indexed data-types[END_REF]

lfisty ( of Z1 Z2 ) ⇐ lfhas Z1 tm , lfhas Z2 ty . lfhas ( ofApp A B M N Z1 Z2 ) ( of ( app M N ) B ) ⇐ lfhas A ty , lfhas B ty , lfhas M tm , lfhas N tm , lfhas Z1 ( of M ( arr A B )) , lfhas Z2 ( of N A ) . lfhas ( ofAbs A B R Z1 ) ( of ( abs A ( x \ R x )) ( arr A B) ) ⇐

lfhas A ty , lfhas B ty , ( pi x \ lfhas x tm ⇒ lfhas ( R x ) tm ) ,

( pi x \ lfhas x tm ⇒ pi z \ lfhas z ( of x A) ⇒ lfhas ( Z1 x z ) ( of (R x ) B )) .
The variables named Z i are generated by the translator for those variables that are omitted from the input signature by the use of → instead of Π. We write clauses using standard λProlog syntax for clarity; it is simple to take the output of translation into this form. It is instructive to compare these clauses to those for the pure HOHH version in section 2.3. Although, on the surface, these two look quite different, there are similarities in the kinds of subgoals that are produced for the three constructors of of. For example, consider the case of ofApp. Two of the formulas, hastype Z 1 (of M (arr A B)) and hastype Z 2 (of N A) are already present in nearly this form in the HOHH specification. The additional assumptions are just repetitions of the typing assumptions for the arguments to ofApp; indeed, many of them are redundant since the ofApp term is already assumed to be type-correct. This kind of redundancy analysis can be used to further improve the translation, making it nearly identical to the simply typed specification [START_REF] Snow | A meta-programming approach to realizing dependently typed logic programming[END_REF][START_REF] Southern | A λProlog based animation of Twelf specifications[END_REF].

Representing LF Hypothetical Judgements

We use the concrete syntax M : A or A : K to depict {{A}}M or {{K}}A, respectively. In fact, since the LF type system is given in terms of hypothetical derivations, we generalize this syntax to the form: x 1 : P 1 , ..., x n : P n ⊢ U : P as an abbreviation for: seq ( x 1 : P 1 :: • • • :: x n : P n ) ( U : P ). As an example,2 the uniqueness theorem for the of relation is (eliding types):

∀G, M, A, B, P 1 , P 2 , ctx G ⊃ G ⊢ P 1 : of M A ⊃ G ⊢ P 2 : of M B ⊃ A = B.
(1)

Here, P 1 and P 2 are (encodings of) the LF proof-terms for the judgements of M A and of M B respectively; these proof terms are built out of the constructors for the of relation, viz. ofApp and ofAbs.

Of course, in order to prove this theorem we would require a suitable ctx definition. Unlike in the simply typed case, the recursive case for λ-abstractions not only introduces a new variable but also a proof that it has a given LF type at the same time. This gives us the following definitional clauses. It is interesting to note that, because variables are introduced (bound) in a different place than their typing assumptions, it would be just as valid to use the following clause instead for the second clause above: This reordering of the context that is not strictly allowed in the LF type system poses no problems for us. Indeed, when we reason about the elements of the context, we can always recover these two assumptions that are always simultaneously added to the context. forall G , nabla p x , ctx ( G x p ) → mem x : tm ( G x p ) → exists A , mem p : of x A ( G x p ) ∧ fresh p A ∧ fresh x A .

The dependency of G on x and p is indicated explicitly using application. For A, this dependency is implicit, because the exists occurs in the scope of the corresponding nablas, so we use the predicate fresh : lfobj → lfobj → prop to further assert that its first arguments are nominal constants that do not occur in its second arguments. This is definable with the single clause: ∀A. (∇x. fresh x A) true.

The proof of (1) proceeds by induction on the second assumption, G ⊢ P 1 : of M A , using the clauses added to prog when importing the specification. There are exactly three backchaining possibilities for prog clauses, corresponding to the ofApp and ofAbs cases, respectively. Finally, when backchaining on the dynamic clauses in G, we use the ctx definition to characterize the shape of the selected clause: if the selected clause is x : tm , then the branch immediately succeeds since x : tm will not unify with P 1 : of M A . Thus, the only backchaining case worth considering is when the selected dynamic clause is of the form p : of x A ′ . In this case, we continue by case-analysis of the second derivation, P 2 : of M B , in which case again the only possibility that is not immediately ruled out by unification is the case of p ′ : of x B ′ being selected from G. In this case, we appeal to a uniqueness lemma [START_REF] Savary | Automatically deriving schematic theorems for dynamic contexts[END_REF] of the following form:

∀G, X, A, B, P1, P2, ctx G ⊃ mem P : of X A G ⊃ mem P2 : of X B G ⊃ A = B.
The rest of the proof is fairly systematic, and largely identical in structure to that of the HOHH case. It is also worth remarking that once we have shown that the types A and B are identical in (1), we can then also show that the proof terms P 1 and P 2 must also be equal (up to αβη, of course).

forall G M A B P1 P2 , ctx G → G ⊢ P1 : of M A → G ⊢ P2 : of M B → P1 = P2 .
This is expected from the LF type theory, but would be difficult to state in LF itself because of the lack of equality as a built-in relation.

The Implementation

The implementation of the translational 2LL can be found in the lf branch of the Abella repository. 3 This implementation also comes with a few examples of reasoning on LF specifications that can be browsed online without needing to run Abella. We have made the following observations about these developments:

• The user of the system never needs to look at the encoding of LF in HOHH directly. The system always translates LF judgements, written using -, transparently to HOHH, and also inverts any HOHH formulas in the image of the translation back into an LF (hypothetical) judgement. Hence, the only domain knowledge the user needs to use the system is the tactics-based proof language of Abella itself.

• Our implementation currently does not perform type-checking on the LF judgements written by the user, either in the specification itself or as part of reasoning. This is not as such a problem, since we can never prove anything false about well-typed judgements. However, without type checking we have no way to verify that the theorem which has been proved is really meaningful since we are allowed to reason about ill-formed LF judgements. It would also be useful for users to have a type-checker as a sanity check. For the time being, we run the input specification through the Twelf system [START_REF] Pfenning | System description: Twelf -A meta-logical framework for deductive systems[END_REF], both to type-check it and to get an explicit form of the specification.

Related Work and Conclusion

We have proposed here a translational extension to the two-level logic approach for reasoning about specifications. By adding a translation layer to the Abella theorem prover we have been able to reason over dependently typed LF specifications without needing to change the reasoning logic, and allowing LF to co-exist with the HOHH specification logic. We are already in the process of extending this implementation to arbitrary pure type systems instead of just LF; in particular, extending the type system with polymorphism, which is the most common feature request for Abella, should be encodable via our translation that realizes specification types as reasoning terms.

The translation of LF to HOHH used in this work is a minor variant of the simple translation from [START_REF] Snow | A meta-programming approach to realizing dependently typed logic programming[END_REF], which is itself based on earlier work [START_REF] Felty | Encoding a dependent-type λ-calculus in a logic programming language[END_REF], while the inversion on terms is similar to the definition in [START_REF] Southern | A λProlog based animation of Twelf specifications[END_REF], omitting metavariables. Various optimized versions of this translation have been used to use λProlog as an engine for logic programming with LF specifications; in particular, the Parinati system [START_REF] Snow | A meta-programming approach to realizing dependently typed logic programming[END_REF] and its extension to meta-variables in [START_REF] Southern | A λProlog based animation of Twelf specifications[END_REF]. The meta-theory of the optimized translation is not as immediate as for the simple translation, but it would be interesting to investigate its use for the Abella/LF variant in the future. The combination of Parinati and Abella/LF gives us both an efficient execution model for dependently typed logic programs and a mechanism to reason about the meta-theory of such specifications in the extended 2LL. In effect, LF becomes as much a first class citizen of the Abella ecosystem as HOHH and λProlog have traditionally been.

There are many other systems designed to reason with and about LF specifications. The most mature implementation is Twelf [START_REF] Pfenning | System description: Twelf -A meta-logical framework for deductive systems[END_REF], which has a very efficient type-checker incorporating sophisticated term and type reconstruction. As mentioned in section 4.3, we use Twelf to type-check and elaborate the LF specifications we import in Abella. In addition to the type-checker, Twelf has a suite of meta-theoretic tools that can verify certain properties of LF specifications, such as that a declared relation determines a total function. Twelf is, however, not powerful enough to reason inductively on arbitrary LF derivations. For example, although Twelf can check coverage, it cannot express the logical formula that corresponds to the coverage property. Some of these expressive deficiencies of Twelf have been addressed in the Delphin [START_REF] Poswolsky | System description: Delphin -A functional programming language for deductive systems[END_REF] and Beluga [START_REF] Pientka | Beluga: A framework for programming and reasoning with deductive systems (system description)[END_REF] systems that add a functional programming language that can manipulate and reason inductively on LF syntax. The Beluga system, in particular, extends the LF type theory with contextual modal types [START_REF] Nanevski | Contextual model type theory[END_REF] that give a typetheoretic treatment for meta-variables and explicit substitutions; in addition, Beluga also allows abstraction over contexts and substitutions [START_REF] Cave | Programming with binders and indexed data-types[END_REF]. The type-checker of Beluga is therefore very sophisticated and performs many kinds of reasoning on contexts automatically that must be done manually in Abella. On the flip-side, Abella has a small trusted core based on the logic G with a well-understood and-importantly!-stable proof system [START_REF] Miller | A theory for generic judgments[END_REF][START_REF] Gacek | Nominal abstraction[END_REF]. It would be interesting to formally compare the representational abilities of Abella/LF and Beluga. Moreover, Abella has recently acquired a Plugin architecture that allows arbitrary (but soundness-preserving) user-written extensions to its automation capabilities [START_REF] Savary | Automatically deriving schematic theorems for dynamic contexts[END_REF], which might help us add more automation in the future.

Figure 1 :

 1 Figure 1: Encoding HOHH using definitional clauses in G. F and G range over arbitrary specification formulas, while A ranges over atomic specification formulas. All clauses are implicitly universally closed over their capitalized variables.

  pi a:ty. pi b:ty. pi m:tm. pi n:tm. of m (arr a b) ⇒ of n a ⇒ of (app m n) b. pi a:ty. pi b:ty. pi r:tm → tm. (pix:tm.of x tm ⇒ of (r x) tm) ⇒ of (abs a r) (arr a b).

φFigure 2 :Figure 3 :

 23 Figure 2: Encoding of LF types and kinds as simple types and LF objects as simply typed λ-terms. {{Πx:A. P }} := λm:φ (Πx:A. P ). pi x:φ (A). {{A}}x ⇒ {{P }}(m x) {{a M1 • • • Mn}} := λm:lfobj. hastype m (a M1 • • • Mn ) {{type}} := λm:lftype. istype mFigure 3: Encoding of LF types and kinds using the hastype and istype predicates.

  M ) : Πx:A. B inv-nest . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Γ, x:A ⊢ m : B M Γ ⊢ (λx:T . m) : (Πx:A. B) λx:A. M inv-lam

Figure 4 :

 4 Figure 4: Inverting the LF encoding of judgements (-→) and terms ( ).

  ctx nil true. ∇x:lfobj. ∇p:lfobj. ctx ( x : tm :: p : of x A :: G) ctx G.

  ∇x:lfobj. ∇p:lfobj. ctx ( p : of x A :: x : tm :: G) ctx G.

  described above:

	lfisty ty .
	lfhas i ty .
	lfhas ( arr Z1 Z2 ) ty ⇐ lfhas Z1 ty , lfhas Z2 ty .
	lfisty tm .
	lfhas ( app Z1 Z2 ) tm ⇐ lfhas Z1 tm , lfhas Z2 tm .

lfhas ( abs Z1 Z2 ) tm ⇐ lfhas Z1 ty , ( pi x \ lfhas x tm ⇒ lfhas ( Z2 x) tm ).

Roughly, stratification prevents definitions such as p ¬p, which would lead to inconsistency.

The full Abella/LF development may be interactively browsed online at http://abella-prover.org/lf.

Details for downloading and building this branch can be found in http://abella-prover.org/lf.