In this paper we present an approach for developing adaptable software applications. The problem we are facing is that of a (possibly mobile) user who wants to download and execute an application from a remote server. The user’s hosting device can be of different kinds (laptops, personal digital assistants, cellular phones, communicators, etc.) with specific hardware and software capabilities. The problem is to be able to decide whether the user’s current device characteristics are compatible with the application requirements in order to prevent execution failures. In the negative case we want to identify the reasons that determined the incompatibility and perform an automatic adaptation of the application, so that it can match the user’s device capabilities. We adopt a declarative approach: we provide each device with a declarative description of its characteristics and, possibly, context constraints. Inspired by Proof Carrying Code (PCC), we use first-order logic formulae to model both the behavior of the code, with respect to the properties of interest, and the execution context. The adaptation process is carried out by using theorem proving techniques, in particular, the proof assistant HOL4. The aim is to derive a formal proof which asserts that the behavior of the code can be correctly adapted to the given context. By construction, the proof, if it exists, gives information on how the adaptation has to be done. On the application side, Java2 Micro Edition (J2ME) is the chosen reference application development environment.

A Declarative Framework for Adaptable Applications in Heterogeneous Environments

INVERARDI, PAOLA;NESI, MONICA
2004

Abstract

In this paper we present an approach for developing adaptable software applications. The problem we are facing is that of a (possibly mobile) user who wants to download and execute an application from a remote server. The user’s hosting device can be of different kinds (laptops, personal digital assistants, cellular phones, communicators, etc.) with specific hardware and software capabilities. The problem is to be able to decide whether the user’s current device characteristics are compatible with the application requirements in order to prevent execution failures. In the negative case we want to identify the reasons that determined the incompatibility and perform an automatic adaptation of the application, so that it can match the user’s device capabilities. We adopt a declarative approach: we provide each device with a declarative description of its characteristics and, possibly, context constraints. Inspired by Proof Carrying Code (PCC), we use first-order logic formulae to model both the behavior of the code, with respect to the properties of interest, and the execution context. The adaptation process is carried out by using theorem proving techniques, in particular, the proof assistant HOL4. The aim is to derive a formal proof which asserts that the behavior of the code can be correctly adapted to the given context. By construction, the proof, if it exists, gives information on how the adaptation has to be done. On the application side, Java2 Micro Edition (J2ME) is the chosen reference application development environment.
1-58113-812-1
File in questo prodotto:
File Dimensione Formato  
SAC04-ACM.pdf

non disponibili

Licenza: Creative commons
Dimensione 236.62 kB
Formato Adobe PDF
236.62 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11697/35286
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 13
  • ???jsp.display-item.citation.isi??? ND
social impact