Skip to Main content Skip to Navigation
New interface
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [9 references]  Display  Hide  Download
Contributor : Hai Wan Connect in order to contact the contributor
Submitted on : Tuesday, March 8, 2011 - 7:00:42 AM
Last modification on : Saturday, June 25, 2022 - 10:32:16 AM
Long-term archiving on: : Thursday, June 9, 2011 - 2:20:22 AM


Files produced by the author(s)


  • HAL Id : inria-00516020, version 1



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. ⟨inria-00516020⟩



Record views


Files downloads