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}}

Journals & Series

Events

Tags:

Publication

— authors

Matteo Casadei, Mirko Viroli

— editors

Flavio De Paoli, Giuseppe Vizzari

— status

published

— sort

paper in proceedings

Venue

— volume

Proceedings of the 13th Workshop on Objects and Agents

— publication date

12 September 2012

URLs & IDs

original PDF

— print ISSN

1613-0073

BibTeX

— BibTeX ID
modelchecking-woa2012
— BibTeX category
inproceedings

Partita IVA: 01131710376 - Copyright © 2008-2021 APICe@DISI Research Group - PRIVACY