ACM Transactions on Autonomous and Adaptive 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.
