Formal Modeling and Verification of Services Managements for Pervasive Computing Environment

Hai Wan 1 Zoé Drey 2 Zhiyang You 1 Liu Liu 1
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
2 Phoenix - Programming Language Technology For Communication Services
LaBRI - Laboratoire Bordelais de Recherche en Informatique, Inria Bordeaux - Sud-Ouest, EA4136 - Handicap et système nerveux :Action, communication, interaction: rétablissement de la fonction et de la participation [Bordeaux]
Abstract : Various forms of pervasive computing environments are being deployed in an increasing number of areas including hospitals, homes and military settings. Entities in this environment provide rich functionalities (i.e. services). How to organize these heterogeneous and distributed entities to deliver user-defined services is challenging. Pantagruel is an approach to integrate a taxonomical description of a pervasive computing environment into a visual programming language. A taxonomy describes the relevant entities of a given pervasive computing area and serves as a parameter to a sensor-controller-actuator develop- ment paradigm. The orchestration of area-specific entities is supported by high-level constructs, customized with respect to taxonomical information. Pantagruel is also a language that describes and manages services. Further more, Pantagruel can be viewed as a high level service contract between the service designer and the program implementer. This paper presents a for- malization of Pantagruel, both its syntax and semantics. Four kinds of static properties are stated based on the formalization. Predicate abstraction based algorithms are designed to verify the properties.
Type de document :
Communication dans un congrès
The 7th International Conference on Service Systems and Service Management, Jun 2010, Tokyo, Japan. 2010
Liste complète des métadonnées

Littérature citée [9 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00516020
Contributeur : Hai Wan <>
Soumis le : mardi 8 mars 2011 - 07:00:42
Dernière modification le : mercredi 10 octobre 2018 - 14:28:09
Document(s) archivé(s) le : jeudi 9 juin 2011 - 02:20:22

Fichier

ieee-sssm.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00516020, version 1

Citation

Hai Wan, Zoé Drey, Zhiyang You, Liu Liu. Formal Modeling and Verification of Services Managements for Pervasive Computing Environment. The 7th International Conference on Service Systems and Service Management, Jun 2010, Tokyo, Japan. 2010. 〈inria-00516020〉

Partager

Métriques

Consultations de la notice

268

Téléchargements de fichiers

133