A Framework to Specify and Verify Computational Fields for Pervasive Systems

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, requiring 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 relying on a number of examples, we show that stochastic model checking can be an effective tool for quantitative analysis of pervasive computing networks composed of hundreds of nodes.

journal or series

 ACM Transactions on Autonomous and Adaptive Systems (TAAS)

superseded by

 A Framework to Specify and Verify Computational Fields for Pervasive Computing Systems (paper in proceedings, 2012) — Matteo Casadei, Mirko Viroli