Publications » ModelcheckingAsensis2012

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.
1st International Workshop on Adaptive Service Ecosystems: Natural and Socially Inspired Solutions (ASENSIS 2012), pages 59-64, 10 September 2012.
José Luis Fernandez-Marquez, Sara Montagna, Andrea Omicini, Franco Zambonelli (eds.), IEEE, SASO 2012, Lyon, France
Pre-proceedings
@inproceedings{modelchecking-asensis2012,
	booktitle = {1st International Workshop on Adaptive Service Ecosystems: Natural and Socially Inspired Solutions (ASENSIS 2012)},
	publisher = {IEEE},
	author = {Casadei, Matteo and Viroli, Mirko},
	title = {Toward Approximate Stochastic Model Checking of Computational Fields for Pervasive Computing Systems},
	year = 2012,
	note = {Pre-proceedings},
	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.},
	pdf-local = {PID2504561.pdf},
	status = {Published},
	pages = {59-64},
	venue = {ASENSIS|SASOW},
	editor = {Fernandez-Marquez, José Luis and Montagna, Sara and Omicini, Andrea and Zambonelli, Franco},
	address = {SASO 2012, Lyon, France},
	month = {10 September},
	venue_e = {Events.Asensis2012}}