A Framework to Specify and Verify Computational Fields for Pervasive Systems


Matteo Casadei, Mirko Viroli

ACM Transactions on Autonomous and Adaptive Systems,  2010
ACM, New York, NY, USA

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.

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

Pubblicazione

— autori/autrici

Matteo Casadei, Mirko Viroli

— stato

non pubblicato

— tipo

articolo su rivista

Sede di pubblicazione

— rivista

ACM Transactions on Autonomous and Adaptive Systems

— data di pubblicazione

2010

BibTeX

— BibTeX ID
modelchecking-taas10
— BibTeX category
article

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