APICe » Publications » APMCSasow2012

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

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.
Keywords: Self-organisation patterns, computational fields, formal verification, pervasive service ecosystems
Self-Adaptive and Self-Organizing Systems Workshops (SASOW), pages 199-204, apr 2013.
Jeremy Pitt (eds.), IEEE CS
2012 IEEE Sixth International Conference (SASOW 2012), Lyon, France, 10-14~}#sep#{~2012. Proceedings
@inproceedings{VC-ASENSIS2012,
	Author = {Casadei, Matteo and Viroli, Mirko},
	Booktitle = {Self-Adaptive and Self-Organizing Systems Workshops (SASOW)},
	Doi = {10.1109/SASOW.2012.42},
	Editor = {Pitt, Jeremy},
	Keywords = {Self-organisation patterns, computational fields, formal verification, pervasive service ecosystems},
	Isbn = {978-1-4673-5153-9},
	Month = apr,
	Note = {2012 IEEE Sixth International Conference (SASOW 2012), Lyon, France, 10-14~} # sep # {~2012. Proceedings},
	Pages = {199-204},
	Publisher = {IEEE CS},
	Title = {Toward Approximate Stochastic Model Checking of Computational Fields for Pervasive Computing Systems},
	Year = 2013,
	abstract={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.}
}