Publications » SimulationWOA2012

A Framework to Specify and Verify 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 analyzing 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 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 a number of pervasive computing examples, we show that the proposed approach can be effectively used for quantitative analysis of systems running on networks composed of hundreds of nodes.
Keywords: Pervasive Computing, Formal Methods, Simulation, Service Ecosystems
Proceedings of the 13th Workshop on Objects and Agents, 12 September 2012.
Flavio De Paoli, Giuseppe Vizzari (eds.), CEUR-WS
@inproceedings{modelchecking-woa2012,
	url-pdf = {http://ceur-ws.org/Vol-892/paper2.pdf},
	issn = {1613-0073},
	booktitle = {Proceedings of the 13th Workshop on Objects and Agents},
	publisher = {CEUR-WS},
	author = {Casadei, Matteo and Viroli, Mirko},
	title = {A Framework to Specify and Verify Computational Fields for Pervasive Computing Systems},
	year = 2012,
	status = {Published},
	venue = {WOA},
	editor = {De Paoli, Flavio and Vizzari, Giuseppe},
	month = {12 September}}