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

    

Publication

— authors

Matteo Casadei, Mirko Viroli

— editors

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

— status

published

— sort

paper in proceedings

Venue

— volume

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

— publication date

10 September 2012

— pages

59-64

BibTeX

— BibTeX ID
modelchecking-asensis2012
— BibTeX category
inproceedings

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