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


Matteo Casadei, Mirko Viroli

1st International Workshop on Adaptive Service Ecosystems: Natural and Socially Inspired Solutions (ASENSIS 2012), pp. 59-64
10 September 2012
IEEE, SASO 2012, Lyon, France
José Luis Fernandez-Marquez, Sara Montagna, Andrea Omicini, Franco Zambonelli (a cura di)
Pre-proceedings

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.

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

Eventi

  • 1st International Workshop on Adaptive Service Ecosystems: Nature and Socially Inspired Solutions (ASENSIS 2012) — 10/09/2012

Pubblicazione

— autori/autrici

Matteo Casadei, Mirko Viroli

— a cura di

José Luis Fernandez-Marquez, Sara Montagna, Andrea Omicini, Franco Zambonelli

— stato

pubblicato

— tipo

articolo in atti

Sede di pubblicazione

— volume

1st International Workshop on Adaptive Service Ecosystems: Natural and Socially Inspired Solutions (ASENSIS 2012)

— pagine

59-64

— data di pubblicazione

10 September 2012

BibTeX

— BibTeX ID
modelchecking-asensis2012
— BibTeX category
inproceedings

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