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

@talk{pianiniasmcwoa2012,
    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 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.},
    address = {Milano, Italy},
    author = {Casadei, Matteo and Viroli, Mirko},
    date = {2012-09-19},
    externallabel = {WOA 2012 Program},
    howpublished = {13th Workshop on Objects and Agents (WOA 2012)},
    language = {en},
    month = sep,
    slideshare = {http://www.slideshare.net/DanySK/cv-asensis2012},
    sort = {talk},
    speaker = {Pianini, Danilo},
    title = {A Framework to Specify and Verify Computational Fields for Pervasive Computing Systems},
    type = {Talk},
    url = {http://www.lintar.disco.unimib.it/WOA2012/programma.html},
    year = 2012
}