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 metadatas

Cited literature [9 references]  Display  Hide  Download

https://hal.inria.fr/inria-00516020
Contributor : Hai Wan <>
Submitted on : Tuesday, March 8, 2011 - 7:00:42 AM
Last modification on : Thursday, April 11, 2019 - 2:34:03 PM
Long-term archiving on : Thursday, June 9, 2011 - 2:20:22 AM

File

ieee-sssm.pdf
Files produced by the author(s)

Identifiers

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

Share

Metrics

Record views

331

Files downloads

236