APICe » Publications » A Framework to Specify and Verify Computational Fields for Pervasive Systems

A Framework to Specify and Verify Computational Fields for Pervasive Systems

Matteo Casadei, Mirko Viroli
Pervasive context-aware computing networks call for designing algorithms for information propa- gation 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 computa- tional 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 support- ing 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.
ACM Transactions on Autonomous and Adaptive Systems, 2010, ACM, New York, NY, USA
@article{modelchecking-taas10,
	publisher = {ACM},
	journal = {ACM Transactions on Autonomous and Adaptive Systems},
	author = {Casadei, Matteo and Viroli, Mirko},
	title = {A Framework to Specify and Verify Computational Fields for Pervasive Systems},
	year = 2010,
	abstract = {Pervasive context-aware computing networks call for designing algorithms for information propa- gation 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 computa- tional 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 support- ing 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.},
	status = {Submitted},
	venue = {--},
	url = {http://apice.unibo.it/xwiki/bin/view/Publications/ModelcheckingTaas10},
	address = {New York, NY, USA}}