A Framework to Specify and Verify Computational Fields for Pervasive Computing Systems

Matteo Casadei, Mirko Viroli

Flavio De Paoli, Giuseppe Vizzari (eds.)
Proceedings of the 13th Workshop on Objects and Agents
12 September 2012

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

Journals & Series


  • 13º Workshop Nazionale “Dagli Oggetti agli Agenti” (WOA 2012) — 17/09/2012–19/09/2012



Publications / Personal

Publications / Views

tags  |  authors  |  editors  |  journals
per year
2023  |  2022  |  2021  |  2020  |  2019  |  2018  |  2017  |  2016  |  2015  |  2014–1927
per sort
in journal  |  in proc  |  chapters  |  books  |  edited  |  spec issues  |  editorials  |  entries  |  manuals  |  tech reps  |  phd th  |  others
per status
online  |  in press  |  proof  |  camera-ready  |  revised  |  accepted  |  revision  |  submitted  |  draft  |  note
ACM Digital Library  |  DBLP  |  IEEE Xplore  |  IRIS  |  PubMed  |  Google Scholar  |  Scopus  |  Semantic Scholar  |  Web of Science  |  DOI


— authors

— editors

Flavio De Paoli, Giuseppe Vizzari

— status


— sort

paper in proceedings

— publication date

12 September 2012

— volume

Proceedings of the 13th Workshop on Objects and Agents


original PDF


— print ISSN


Partita IVA: 01131710376 — Copyright © 2008–2023 APICe@DISI – PRIVACY