A Framework to Specify and Verify Computational Fields for Pervasive Computing Systems


Danilo Pianini  /  Matteo Casadei, Mirko Viroli

Pervasive context-aware computing networks call for designing algorithms for information propagation and reconfiguration that promote self-adaptation, namely, which can guarantee – at least to a probabilistic extent – certain reliability and robustness properties in spite of unpredicted changes and conditions. The possibility of formally analyzing their properties is obviously an essential engineering requirement, calling for general-purpose models and tools. As proposed in recent works, several such algorithms can be modeled by the notion of computational field: a dynamically evolving spatial data structure mapping every node of the network to a data value. Based on this idea, as a contribution toward formally verifying properties of pervasive computing systems, in this article we propose a specification language to model computational fields, and a framework based on PRISM stochastic model checker explicitly targeted at supporting temporal property verification. By a number of pervasive computing examples, we show that the proposed approach can be effectively used for quantitative analysis of systems running on networks composed of hundreds of nodes.

Events

  • 13º Workshop Nazionale “Dagli Oggetti agli Agenti” (WOA 2012) — 17/09/2012–19/09/2012

Tags:

Talk

— speakers

— authors

— sort

talk

— language

wgb.gif

Context

13th Workshop on Objects and Agents (WOA 2012)

— where

Milano, Italy

— when

19/09/2012

Links

— external

SlideShare
WOA 2012 Program

Partita IVA: 01131710376 - Copyright © 2008-2022 APICe@DISI Research Group - PRIVACY