Toward Approximate Stochastic Model Checking of Computational Fields for Pervasive Computing Systems


Mirko Viroli  /  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 analysing 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 modelled 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, exploited for quantitative analysis of systems running on networks composed of hundreds of nodes.


  • 1st International Workshop on Adaptive Service Ecosystems: Nature and Socially Inspired Solutions (ASENSIS 2012) — 10/09/2012



— oratori/oratrici

— autori/autrici

— tipo


— lingua


— contesto


— dove

Lyon, France

— quando


Partita IVA: 01131710376 — Copyright © 2008–2023 APICe@DISI – PRIVACY